pigeon.mlw 1.88 KB
 Jean-Christophe Filliatre committed May 16, 2012 1 `````` `````` Jean-Christophe Filliatre committed Jun 01, 2018 2 ``````(** {1 Pigeon hole principle} *) `````` Jean-Christophe Filliatre committed May 16, 2012 3 `````` `````` Andrei Paskevich committed Dec 22, 2017 4 ``````module Pigeonhole `````` Jean-Christophe Filliatre committed May 16, 2012 5 `````` `````` Andrei Paskevich committed Jun 15, 2018 6 7 `````` use int.Int use map.Map `````` Jean-Christophe Filliatre committed Jun 01, 2018 8 `````` `````` Jean-Christophe Filliatre committed Jun 01, 2018 9 `````` let rec lemma pigeonhole (n m: int) (f: int -> int) `````` Jean-Christophe Filliatre committed Jun 01, 2018 10 11 12 `````` 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 } `````` Jean-Christophe Filliatre committed Jun 01, 2018 13 14 15 16 17 18 19 20 `````` variant { m } = for i = 0 to n - 1 do invariant { forall k. 0 <= k < i -> f k < m - 1 } if f i = m - 1 then begin for j = i + 1 to n - 1 do invariant { forall k. i < k < j -> f k < m - 1 } if f j = m - 1 then return done; `````` Jean-Christophe Filliatre committed Jun 01, 2018 21 `````` let function g k = if k < i then f k else f (k + 1) in `````` Jean-Christophe Filliatre committed Jun 01, 2018 22 23 24 25 `````` pigeonhole (n - 1) (m - 1) g; return end done; pigeonhole n (m - 1) f `````` Jean-Christophe Filliatre committed Jun 01, 2018 26 27 28 29 30 31 32 33 34 `````` end (* An instance where a list is included into a set with fewer elements. Contributed by Yuto Takei (University of Tokyo) *) module ListAndSet `````` Andrei Paskevich committed Jun 15, 2018 35 36 37 38 `````` use int.Int use list.List use list.Length use list.Append `````` Andrei Paskevich committed Jun 15, 2018 39 `````` use list.Mem as Mem `````` Andrei Paskevich committed Jun 15, 2018 40 `````` use set.Fset `````` Jean-Christophe Filliatre committed May 16, 2012 41 42 43 44 45 46 47 48 49 50 `````` type t predicate pigeon_set (s: set t) = forall l: list t. (forall e: t. Mem.mem e l -> mem e s) -> (length l > cardinal s) -> exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3))) `````` Andrei Paskevich committed Jun 15, 2018 51 52 `````` clone set.FsetInduction as FSI with type t = t, predicate p = pigeon_set `````` Jean-Christophe Filliatre committed May 16, 2012 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 `````` lemma corner: forall s: set t, l: list t. (length l = cardinal s) -> (forall e: t. Mem.mem e l -> mem e s) -> (exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3)))) \/ (forall e: t. mem e s -> Mem.mem e l) lemma pigeon_0: pigeon_set empty lemma pigeon_1: forall s: set t. pigeon_set s -> forall t: t. pigeon_set (add t s) lemma pigeon_2: forall s: set t. pigeon_set s lemma pigeonhole: forall s: set t, l: list t. (forall e: t. Mem.mem e l -> mem e s) -> (length l > cardinal s) -> exists e: t, l1 l2 l3: list t. l = l1 ++ (Cons e (l2 ++ (Cons e l3))) end``````