Commit dd2efcbf authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

a more general pigeon hole principle

parent 4af9081d
......@@ -61,7 +61,7 @@ theory Graph
Two cases depending on l3=[] (and thus u=v) conclude the proof. Qed.
clone pigeon.Pigeonhole with type t = vertex
clone pigeon.ListAndSet with type t = vertex
predicate cyc_decomp (v: vertex) (l: list vertex)
(vi: vertex) (l1 l2 l3: list vertex) =
......@@ -174,7 +174,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="69"/></proof>
<goal name="VC relax.0.2" expl="VC for relax" proved="true">
<proof prover="11"><result status="valid" time="1.12"/></proof>
<proof prover="11"><result status="valid" time="0.54"/></proof>
<goal name="VC relax.0.3" expl="VC for relax" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="117"/></proof>
......@@ -335,15 +335,15 @@
<proof prover="1"><result status="valid" time="0.02" steps="57"/></proof>
<goal name="VC bellman_ford.6.1" expl="VC for bellman_ford" proved="true">
<proof prover="1"><result status="valid" time="1.52" steps="1717"/></proof>
<proof prover="1"><result status="valid" time="0.81" steps="1717"/></proof>
<goal name="VC bellman_ford.7" expl="assertion" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="1.07" steps="1190"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.55" steps="1190"/></proof>
<goal name="VC bellman_ford.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.60" steps="1109"/></proof>
<proof prover="1"><result status="valid" time="0.34" steps="1109"/></proof>
<goal name="VC bellman_ford.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
(** {1 Pigeon hole principle}
Contributed by Yuto Takei (University of Tokyo) *)
(** {1 Pigeon hole principle} *)
module Pigeonhole
use import int.Int
use import map.Map
val lemma pigeonhole (n m: int) (f: int -> int)
requires { 0 <= m < n }
requires { forall i. 0 <= i < n -> 0 <= f i < m }
ensures { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
(* An instance where a list is included into a set with fewer elements.
Contributed by Yuto Takei (University of Tokyo) *)
module ListAndSet
use import int.Int
use import list.List
use import list.Length
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment