diff --git a/examples/bellman_ford.mlw b/examples/bellman_ford.mlw index a9c57602f41887abeb199d15a3fa10d2ccbe33cd..5aa1ce9888a4761a9e61ac447c2611b439593739 100644 --- a/examples/bellman_ford.mlw +++ b/examples/bellman_ford.mlw @@ -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) = diff --git a/examples/bellman_ford/why3session.xml b/examples/bellman_ford/why3session.xml index e564f9bef26963bc84e2bccc515b4d929d62ecef..9bdd9ce6fde29fb756676a3749a5f94e3f6479c1 100644 --- a/examples/bellman_ford/why3session.xml +++ b/examples/bellman_ford/why3session.xml @@ -174,7 +174,7 @@ - + @@ -335,15 +335,15 @@ - + - + - + diff --git a/stdlib/pigeon.mlw b/stdlib/pigeon.mlw index e59502cefc7cab56f8f91fc06da179ea28f06a0e..1fde34cf7dec510859c00a8b58fd607cc0e05a56 100644 --- a/stdlib/pigeon.mlw +++ b/stdlib/pigeon.mlw @@ -1,10 +1,24 @@ -(** {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 } + +end + +(* 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