pigeonhole.mlw 881 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 `````` `````` Mário Pereira committed Jul 11, 2018 8 `````` use int.Int, set.Fset, ref.Ref `````` Jean-Christophe Filliatre committed May 04, 2015 9 10 11 12 13 14 15 16 `````` 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 17 `````` let lemma pigeonhole (n m: int) (f: int -> int) `````` Jean-Christophe Filliatre committed May 04, 2015 18 19 20 21 22 23 24 25 `````` 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 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) } `````` Andrei Paskevich committed Jun 06, 2017 26 `````` if mem (f i) !s then return; `````` Jean-Christophe Filliatre committed May 04, 2015 27 28 29 30 31 32 `````` s := add (f i) !s done; let b = below m in assert { subset !s b }; absurd end``````