From dd2efcbf57dd85e6a07f454ab1f29b93babc32c0 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Fri, 1 Jun 2018 09:05:31 +0200
Subject: [PATCH] a more general pigeon hole principle

---
 examples/bellman_ford.mlw             |  2 +-
 examples/bellman_ford/why3session.xml |  8 ++++----
 stdlib/pigeon.mlw                     | 20 +++++++++++++++++---
 3 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/examples/bellman_ford.mlw b/examples/bellman_ford.mlw
index a9c57602f..5aa1ce988 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 e564f9bef..9bdd9ce6f 100644
--- a/examples/bellman_ford/why3session.xml
+++ b/examples/bellman_ford/why3session.xml
@@ -174,7 +174,7 @@
    <proof prover="1"><result status="valid" time="0.04" steps="69"/></proof>
    </goal>
    <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>
    <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>
    <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>
   </transf>
   </goal>
   <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>
   <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>
   <goal name="VC bellman_ford.9" expl="assertion" proved="true">
   <proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
diff --git a/stdlib/pigeon.mlw b/stdlib/pigeon.mlw
index e59502cef..1fde34cf7 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
-- 
GitLab