pigeonhole.mlw 987 Bytes
 Jean-Christophe Filliatre committed May 04, 2015 1 `````` `````` Jean-Christophe Filliatre committed May 05, 2015 2 3 4 ``````(** Pigeonhole principle (also know as Dirichlet's drawer principle) Proved using a lemma function. *) `````` Jean-Christophe Filliatre committed May 04, 2015 5 `````` `````` Jean-Christophe Filliatre committed May 20, 2015 6 ``````module Pigeonhole `````` Jean-Christophe Filliatre committed May 04, 2015 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 `````` use import HighOrd use import int.Int use import set.Fset use import ref.Ref exception Exit let rec below (n: int) : set int requires { 0 <= n } ensures { forall i. mem i result <-> 0 <= i < n } ensures { cardinal result = n } variant { n } = if n = 0 then empty else add (n-1) (below (n-1)) `````` Jean-Christophe Filliatre committed May 20, 2015 22 `````` let lemma pigeonhole (n m: int) (f: int -> int) `````` Jean-Christophe Filliatre committed May 04, 2015 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 `````` 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 } = let s = ref empty in try for i = 0 to n-1 do invariant { cardinal !s = i } invariant { forall x. mem x !s <-> (exists j. 0 <= j < i /\ x = f j) } if mem (f i) !s then raise Exit; s := add (f i) !s done; let b = below m in assert { subset !s b }; absurd with Exit -> () end end``````