1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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
|
(** {1 Pigeon hole principle} *)
module Pigeonhole
use int.Int
use map.Map
let rec 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 }
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;
let function g k = if k < i then f k else f (k + 1) in
pigeonhole (n - 1) (m - 1) g;
return end
done;
pigeonhole n (m - 1) f
end
(** An instance where a list is included into a set with fewer elements.
Contributed by Yuto Takei (University of Tokyo) *)
module ListAndSet
use int.Int
use list.List
use list.Length
use list.Append
use list.Mem as Mem
use set.Fset
type t
predicate pigeon_set (s: fset 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)))
clone set.FsetInduction as FSI with
type t = t, predicate p = pigeon_set
lemma corner:
forall s: fset 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: fset t. pigeon_set s ->
forall t: t. pigeon_set (add t s)
lemma pigeon_2:
forall s: fset t. pigeon_set s
lemma pigeonhole:
forall s: fset 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
|
