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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
import Std.Data.HashSet
/--
Type Class to mark a type as having a finite number of elements.
Done by providing a bijective mapping to Fin.
-/
class Finite (α : Type u) where
cardinality : Nat
enumerate : α → Fin cardinality
nth : Fin cardinality → α
nth_inverse_enumerate : nth ∘ enumerate = id
enumerate_inverse_nth : enumerate ∘ nth = id
theorem Finite.surjective {α : Type u} [Finite α] {a b : Fin (Finite.cardinality α)} : nth a = nth b → a = b := λh₃ ↦
have h₁ := Finite.enumerate_inverse_nth (α := α)
have h₄ := congrArg enumerate h₃
have h₂ : ∀(x : Fin (Finite.cardinality α)), (enumerate ∘ nth) x = x := λ_↦h₁.substr rfl
have h₅ := Function.comp_apply.subst (h₂ a).symm
have h₆ := Function.comp_apply.subst (h₂ b).symm
h₅.substr $ h₆.substr h₄
theorem Finite.injective {α : Type u} [Finite α] {a b : α} : enumerate a = enumerate b → a = b := λh₁↦
have h₂ := Finite.nth_inverse_enumerate (α := α)
have h₃ := congrArg nth h₁
have h₄ : ∀(x : α), (nth ∘ enumerate) x = x := λ_↦h₂.substr rfl
have h₅ := Function.comp_apply.subst (h₄ a).symm
have h₆ := Function.comp_apply.subst (h₄ b).symm
h₅.substr $ h₆.substr h₃
def Finite.tuple_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] (x : α × β) : Fin ((Finite.cardinality α) * (Finite.cardinality β)) :=
let (a, b) := x
let idxa := (Finite.enumerate a)
let idxb := (Finite.enumerate b)
let idx := idxa.val + (Finite.cardinality α) * idxb.val
have h : idx < (Finite.cardinality α) * (Finite.cardinality β) :=
two_d_coordinate_to_index_lt_size idxa.isLt idxb.isLt
⟨idx,h⟩
where two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ : y < h) : x + w*y < w*h :=
Nat.le_pred_of_lt h₂
|> Nat.mul_le_mul_left w
|> Nat.add_le_add_iff_right.mpr
|> (Nat.mul_pred w h).subst (motive :=λx↦w * y + w ≤ x + w)
|> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right w (Nat.zero_lt_of_lt h₂))).subst
|> (Nat.add_comm _ _).subst (motive := λx↦x ≤ w*h)
|> Nat.le_sub_of_add_le
|> Nat.lt_of_lt_of_le h₁
|> λx↦(Nat.add_lt_add_right) x (w * y)
|> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt h₁)).mpr h₂))).subst
def Finite.tuple_nth {α : Type u} [Finite α] {β : Type v} [Finite β] (idx : Fin ((Finite.cardinality α) * (Finite.cardinality β))) :=
let idxav := idx % (Finite.cardinality α)
let idxbv := idx / (Finite.cardinality α)
have h₁ : Finite.cardinality α > 0 :=
if h : 0 = Finite.cardinality α then
have : cardinality α * cardinality β = 0 := h.subst (motive := λx↦x*cardinality β = 0) $ Nat.zero_mul (cardinality β)
(Fin.cast this idx).elim0
else
Nat.pos_of_ne_zero (Ne.symm h)
let idxa : Fin (Finite.cardinality α) := ⟨idxav, Nat.mod_lt _ h₁⟩
let idxb : Fin (Finite.cardinality β):= ⟨idxbv, Nat.div_lt_of_lt_mul idx.isLt⟩
(Finite.nth idxa, Finite.nth idxb)
theorem Finite.tuple_nth_inverse_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_nth (α := α) (β := β) ∘ Finite.tuple_enumerate (α := α) (β := β) = id := by
unfold Finite.tuple_enumerate Finite.tuple_nth
funext
simp
congr
case h.e_fst x =>
simp[Nat.mod_eq_of_lt]
rw[←Function.comp_apply (f := Finite.nth) (x := x.fst), Finite.nth_inverse_enumerate]
rfl
case h.e_snd x =>
have h₁ : (↑(Finite.enumerate x.fst) + (Finite.cardinality α) * ↑(Finite.enumerate x.snd)) / Finite.cardinality α = ↑(Finite.enumerate x.snd) := by
rw[Nat.add_mul_div_left]
simp[Nat.div_eq_of_lt]
exact Nat.zero_lt_of_lt (Finite.enumerate x.fst).isLt
simp[h₁]
rw[←Function.comp_apply (f := Finite.nth) (x := x.snd), Finite.nth_inverse_enumerate]
rfl
theorem Finite.tuple_enumerate_inerse_nth {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_enumerate (α := α) (β := β) ∘ Finite.tuple_nth (α := α) (β := β) = id := by
funext
unfold Finite.tuple_enumerate Finite.tuple_nth
simp
rename_i x
rw[Fin.eq_mk_iff_val_eq]
simp
rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
simp[Nat.mod_add_div]
instance {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite (Prod α β) where
cardinality := (Finite.cardinality α) * (Finite.cardinality β)
enumerate := Finite.tuple_enumerate
nth := Finite.tuple_nth
enumerate_inverse_nth := Finite.tuple_enumerate_inerse_nth
nth_inverse_enumerate := Finite.tuple_nth_inverse_enumerate
theorem Finite.forall_nth {α : Type u} [Finite α] (p : α → Prop) (h₁ : ∀(o : Fin (Finite.cardinality α)), p (Finite.nth o)) : ∀(a : α), p a := λa↦
have : p ((nth ∘ enumerate) a) := Function.comp_apply.substr $ h₁ (Finite.enumerate a)
Finite.nth_inverse_enumerate.subst (motive := λx ↦ p (x a)) this
def Finite.set (α : Type u) [Finite α] [BEq α] [Hashable α] : Std.HashSet α :=
match h: (Finite.cardinality α) with
| 0 => Std.HashSet.emptyWithCapacity
| l+1 => set_worker Std.HashSet.emptyWithCapacity ⟨l,h.substr (p := λx ↦ l < x) $ Nat.lt.base l⟩
where set_worker (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) : Std.HashSet α :=
let e := Finite.nth n
let set := set.insert e
match n with
| ⟨0,_⟩ => set
| ⟨m+1,h₁⟩ => set_worker set ⟨m, Nat.lt_of_succ_lt h₁⟩
protected theorem Finite.set_worker_contains_self' (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] (a : α) (oldSet : Std.HashSet α) (h₁ : oldSet.contains a) (n : Fin (Finite.cardinality α)) : (Finite.set.set_worker α oldSet n).contains a := by
cases n
case mk n h₂ =>
induction n generalizing oldSet
case zero => unfold set.set_worker; simp[h₁]
case succ m hm =>
unfold set.set_worker
exact hm (oldSet.insert (nth ⟨m + 1, h₂⟩)) (by simp[h₁]) (Nat.lt_of_succ_lt h₂)
protected theorem Finite.set_worker_contains_self (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α), (Finite.set.set_worker α set (Finite.enumerate a)).contains a := by
intros a oldSet
unfold set.set_worker
rw[←Function.comp_apply (f := nth), Finite.nth_inverse_enumerate, id_def]
split
case h_1 => apply Std.HashSet.contains_insert_self
case h_2 =>
apply Finite.set_worker_contains_self'
exact Std.HashSet.contains_insert_self
protected theorem Finite.set_worker_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α) (o : Nat) (h₁ : Finite.enumerate a + o < Finite.cardinality α), (Finite.set.set_worker α set ⟨Finite.enumerate a + o, h₁⟩).contains a := by
intros a oldSet offset h₁
induction offset generalizing oldSet
case zero =>
exact Finite.set_worker_contains_self _ _ _
case succ p hi =>
unfold set.set_worker
simp
have : ↑(enumerate a) + p < cardinality α := Nat.lt_of_succ_lt $ (Nat.add_assoc (enumerate a) p 1).substr h₁
exact hi (oldSet.insert (nth ⟨↑(enumerate a) + (p + 1), h₁⟩)) this
theorem Finite.set_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α), (Finite.set α).contains a := λa ↦ by
unfold set
split
case h_1 h => exact (Fin.cast h $ Finite.enumerate a).elim0
case h_2 l h =>
let o := l - enumerate a
have h₁ : (Finite.enumerate a).val + o = l := by omega
have h₂ := Finite.set_worker_contains _ a Std.HashSet.emptyWithCapacity o (by omega)
simp[h₁] at h₂
assumption
protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α]
: ∀(set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_ : ∀(x : Fin (Finite.cardinality α)) (_ : x ≤ n),
¬set.contains (Finite.nth x)), (Finite.set.set_worker α set n).size = set.size + n + 1
:= by
intros set n h₂
simp at h₂
unfold Finite.set.set_worker
cases n
case mk n h₁ =>
split
case h_1 m isLt he =>
simp at he
simp[Std.HashSet.size_insert, h₂, he]
case h_2 m isLt he =>
simp
have h₄ : m < n := have : n = m.succ := Fin.val_eq_of_eq he; this.substr (Nat.lt_succ_self m)
have h₅ : ∀ (x : Fin (cardinality α)), x ≤ ⟨m, Nat.lt_of_succ_lt isLt⟩ → ¬(set.insert (nth ⟨n, h₁⟩)).contains (nth x) = true := by
simp
intros x hx
constructor
case right => exact h₂ x (Nat.le_trans hx (Nat.le_of_lt h₄))
case left =>
have h₅ : x ≠ ⟨n, h₁⟩ := Fin.ne_of_val_ne $ Nat.ne_of_lt $ Nat.lt_of_le_of_lt hx h₄
have h₆ := Finite.surjective (α := α) (a := x) (b := ⟨n,h₁⟩)
exact Ne.symm (h₅ ∘ h₆)
have h₃ := Finite.set_worker_size α (set.insert (nth ⟨n, h₁⟩)) ⟨m, Nat.lt_of_succ_lt isLt⟩ (h₅)
rw[h₃]
simp at he
simp[he, Std.HashSet.size_insert]
split
case isFalse => rw[Nat.add_assoc, Nat.add_comm 1 m]
case isTrue hx =>
subst n
have h₂ := h₂ ⟨m+1,h₁⟩ (Fin.le_refl _)
have hx := Std.HashSet.mem_iff_contains.mp hx
exact absurd hx h₂
termination_by _ n => n.val
theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : (Finite.set α).size = Finite.cardinality α := by
unfold set
split
case h_1 h => exact Std.HashSet.size_empty.substr h.symm
case h_2 l h =>
rewrite(occs := .pos [3])[h]
have := Finite.set_worker_size α Std.HashSet.emptyWithCapacity ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λx _↦Bool.eq_false_iff.mp (Std.HashSet.contains_empty (a:=Finite.nth x)))
simp only [this, Std.HashSet.size_emptyWithCapacity, Nat.zero_add, Nat.succ_eq_add_one]
|
