Skip to content

Commit 35c26cc

Browse files
yuuki14202028yuuki14202028
committed
Complete CaseFold equivalence proofs
1 parent bd5ff89 commit 35c26cc

2 files changed

Lines changed: 159 additions & 88 deletions

File tree

‎correctness/RegexCorrectness/Unicode/CaseFoldBinarySearch.lean‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,42 @@ theorem getCaseFoldChar_eq_of_mem (src tgt : UInt32) :
190190
exact this
191191
simp only [beq_iff_eq, h_idx_src, not_true_eq_false] at h
192192

193+
/-- If getCaseFoldChar_spec c = tgt and c ≠ tgt, then (c.val, tgt.val) is in caseFoldTable. -/
194+
theorem getCaseFoldChar_spec_ne_implies_in_table (c tgt : Char)
195+
(h_folds : Internal.getCaseFoldChar_spec c = tgt)
196+
(h_ne : c ≠ tgt) :
197+
(c.val, tgt.val) ∈ caseFoldTable.toList := by
198+
unfold Internal.getCaseFoldChar_spec at h_folds
199+
set idx := binarySearch c.val caseFoldTable (·.1) 0 caseFoldTable.size with h_idx_def
200+
have h_idx_lt : idx < caseFoldTable.size :=
201+
binarySearch_lt_size c.val caseFoldTable 0 caseFoldTable.size
202+
caseFoldTable_nonempty (Nat.le_refl _)
203+
have h_get_internal : caseFoldTable.get!Internal idx = caseFoldTable[idx]! := rfl
204+
simp only [← h_idx_def, h_get_internal] at h_folds
205+
split at h_folds
206+
case isTrue h_src_eq =>
207+
-- Binary search found c.val at idx, so (c.val, tgt.val) is in the table
208+
have h_src : (caseFoldTable[idx]!).1 = c.val := by
209+
simp only [beq_iff_eq] at h_src_eq
210+
exact h_src_eq
211+
have h_tgt_char : Char.ofNat (caseFoldTable[idx]!).2.toNat = tgt := h_folds
212+
have h_tgt : (caseFoldTable[idx]!).2 = tgt.val := by
213+
have h_valid := caseFoldTable_tgt_valid idx h_idx_lt
214+
have h_eq := congrArg Char.val h_tgt_char
215+
simp only [Char.ofNat, h_valid, dite_true] at h_eq
216+
exact h_eq
217+
have h_getElem!_eq : caseFoldTable[idx]! = caseFoldTable[idx] := getElem!_pos caseFoldTable idx h_idx_lt
218+
have h_entry : caseFoldTable[idx] = (c.val, tgt.val) := by
219+
rw [← h_getElem!_eq]
220+
exact Prod.ext h_src h_tgt
221+
rw [Array.mem_toList_iff, Array.mem_iff_getElem]
222+
exact ⟨idx, h_idx_lt, h_entry⟩
223+
case isFalse h_src_ne =>
224+
-- Binary search did not find c.val, so c is returned unchanged
225+
exfalso
226+
have h_c_eq_tgt : c = tgt := h_folds
227+
exact h_ne h_c_eq_tgt
228+
193229
theorem getCaseFoldChar_fixed_of_is_target (tgt : UInt32) :
194230
(∃ src, (src, tgt) ∈ caseFoldTable.toList) →
195231
Internal.getCaseFoldChar_spec (Char.ofNat tgt.toNat) = Char.ofNat tgt.toNat := by

‎correctness/RegexCorrectness/Unicode/CaseFoldEquiv.lean‎

Lines changed: 123 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,6 @@ def CaseFoldEquiv (c₁ c₂ : Char) : Prop :=
1818
def CaseFoldEquiv' (c₁ c₂ : Char) : Prop :=
1919
Internal.getCaseFoldChar_spec c₁ = Internal.getCaseFoldChar_spec c₂
2020

21-
theorem char_mem_caseFoldEquivTable (c : Char) : c.val ∈ caseFoldEquivTable[(Internal.getCaseFoldChar_spec c).val]! := by
22-
unfold caseFoldEquivTable caseFoldEquivTableThunk
23-
dsimp [Thunk.get, Thunk.mk]
24-
have h_mem_table := getCaseFoldChar_pair_mem_table c
25-
obtain ⟨arr, h_some, h_mem⟩ := buildCaseFoldEquivTable_complete c.val (Internal.getCaseFoldChar_spec c).val h_mem_table
26-
simp only [Std.HashMap.getElem!_eq_get!_getElem?, h_some, Option.get!_some]
27-
exact h_mem
28-
2921
theorem buildCaseFoldEquivTable_soundness (u tgt : UInt32) :
3022
(∃ arr, buildCaseFoldEquivTable[tgt]? = some arr ∧ u ∈ arr) →
3123
((u, tgt) ∈ caseFoldTable.toList ∨ u = tgt) := by
@@ -34,96 +26,139 @@ theorem buildCaseFoldEquivTable_soundness (u tgt : UInt32) :
3426
intro k
3527
exact Std.HashMap.getElem?_empty
3628

37-
theorem caseFoldEquivTable_mem_cases (u : UInt32) (tgt : Char)
38-
(h_mem : u ∈ caseFoldEquivTable[tgt.val]!) :
39-
(u, tgt.val) ∈ caseFoldTable.toList ∨ u = tgt.val := by
40-
simp only [caseFoldEquivTable, caseFoldEquivTableThunk, Thunk.get,
41-
Std.HashMap.getElem!_eq_get!_getElem?] at h_mem
42-
cases h_lookup : buildCaseFoldEquivTable[tgt.val]? with
43-
| none =>
44-
simp only [h_lookup, Option.get!_none] at h_mem
45-
exact (Array.not_mem_empty u h_mem).elim
46-
| some arr =>
47-
simp only [h_lookup, Option.get!_some] at h_mem
48-
exact buildCaseFoldEquivTable_soundness u tgt.val ⟨arr, h_lookup, h_mem⟩
49-
50-
theorem caseFoldTable_sound (u : UInt32) (tgt : Char) :
51-
u ∈ caseFoldEquivTable[tgt.val]! → Internal.getCaseFoldChar_spec (Char.ofNat u.toNat) = tgt := by
52-
intro h_mem
53-
have h_tgt_eq : Char.ofNat tgt.val.toNat = tgt := Char.ofNat_toNat tgt
54-
cases caseFoldEquivTable_mem_cases u tgt h_mem with
55-
| inl h_in_table =>
56-
rw [getCaseFoldChar_eq_of_mem u tgt.val h_in_table, h_tgt_eq]
57-
| inr h_u_eq_tgt =>
58-
subst h_u_eq_tgt
59-
have h_exists_src : ∃ src, (src, tgt.val) ∈ caseFoldTable.toList := by
60-
simp only [caseFoldEquivTable, caseFoldEquivTableThunk, Thunk.get,
61-
Std.HashMap.getElem!_eq_get!_getElem?] at h_mem
62-
cases h_lookup : buildCaseFoldEquivTable[tgt.val]? with
63-
| none =>
64-
simp only [h_lookup, Option.get!_none] at h_mem
65-
exact (Array.not_mem_empty tgt.val h_mem).elim
66-
| some _ =>
67-
exact buildCaseFoldEquivTable_key_exists tgt.val (by simp [h_lookup])
68-
rw [getCaseFoldChar_fixed_of_is_target tgt.val h_exists_src, h_tgt_eq]
69-
70-
theorem caseFoldEquivTable_valid (u : UInt32) (tgt : Char) :
71-
u ∈ caseFoldEquivTable[tgt.val]! → UInt32.isValidChar u := by
72-
intro h_mem
73-
cases caseFoldEquivTable_mem_cases u tgt h_mem with
74-
| inl h_in_table =>
75-
have h_in_array : (u, tgt.val) ∈ caseFoldTable := Array.mem_toList_iff.mp h_in_table
76-
obtain ⟨i, hi, h_entry⟩ := Array.mem_iff_getElem.mp h_in_array
77-
have h_i_bang : caseFoldTable[i]! = caseFoldTable[i] := getElem!_pos caseFoldTable i hi
78-
have h_src_eq : (caseFoldTable[i]!).1 = u := by rw [h_i_bang, h_entry]
79-
rw [← h_src_eq]
80-
exact caseFoldTable_src_valid i hi
81-
| inr h_u_eq_tgt =>
82-
rw [h_u_eq_tgt]
83-
exact tgt.valid
29+
theorem getCaseFoldChar_spec_idempotent (c : Char) :
30+
Internal.getCaseFoldChar_spec (Internal.getCaseFoldChar_spec c) = Internal.getCaseFoldChar_spec c := by
31+
let c' := Internal.getCaseFoldChar_spec c
32+
if h : c' = c then
33+
have h_eq : Internal.getCaseFoldChar_spec c = c := h
34+
rw [h_eq]
35+
exact Char.ext (congrArg Char.val h)
36+
else
37+
have h_in := getCaseFoldChar_spec_ne_implies_in_table c c' rfl (Ne.symm h)
38+
have h_exists : ∃ src, (src, c'.val) ∈ caseFoldTable.toList :=
39+
⟨c.val, h_in⟩
40+
have h_res := getCaseFoldChar_fixed_of_is_target c'.val h_exists
41+
have h_char_eq : Char.ofNat c'.val.toNat = c' := by
42+
simp [Char.ofNat]
43+
simp [c'.valid]
44+
exact Char.ext rfl
45+
rw [h_char_eq] at h_res
46+
exact h_res
47+
48+
theorem caseFoldEquivTable_mem_self
49+
(k : UInt32) (arr : Array UInt32) :
50+
caseFoldEquivTable[k]? = some arr → k ∈ arr := by
51+
rw [caseFoldEquivTable, caseFoldEquivTableThunk, Thunk.get, buildCaseFoldEquivTable]
52+
generalize caseFoldTable.toList = l
53+
suffices ∀ (m : Std.HashMap UInt32 (Array UInt32)),
54+
(∀ (k' : UInt32) (arr' : Array UInt32), m[k']? = some arr' → k' ∈ arr') →
55+
let res := l.foldl insertCaseFoldEquiv m
56+
res[k]? = some arr → k ∈ arr by
57+
apply this {} (fun _ _ h => by simp at h)
58+
intro m h_inv
59+
induction l generalizing m with
60+
| nil =>
61+
exact h_inv k arr
62+
| cons pair tail ih =>
63+
simp only [List.foldl_cons]
64+
apply ih
65+
intro k' arr' h_get
66+
rcases pair with ⟨src, tgt⟩
67+
dsimp [insertCaseFoldEquiv] at h_get
68+
split at h_get <;> rename_i existing_arr h_found
69+
· by_cases h_kt : k' = tgt
70+
· subst h_kt
71+
rw [Std.HashMap.getElem?_insert_self] at h_get
72+
injection h_get with h_eq
73+
subst h_eq
74+
rw [Array.mem_push]
75+
left
76+
grind
77+
· rw [Std.HashMap.getElem?_insert] at h_get
78+
simp [Ne.symm h_kt] at h_get
79+
exact h_inv k' arr' h_get
80+
· by_cases h_kt : k' = tgt
81+
· subst h_kt
82+
rw [Std.HashMap.getElem?_insert_self] at h_get
83+
injection h_get with h_eq
84+
subst h_eq
85+
simp
86+
· rw [Std.HashMap.getElem?_insert] at h_get
87+
simp [Ne.symm h_kt] at h_get
88+
exact h_inv k' arr' h_get
89+
90+
theorem caseFoldEquivTable_none_imp_eq_fold
91+
(c : Char) (u : Char)
92+
(h_spec : Internal.getCaseFoldChar_spec c = u) :
93+
caseFoldEquivTable[u.val]? = none → c = u := by
94+
intro h_none
95+
by_contra h_ne
96+
have h_in := getCaseFoldChar_spec_ne_implies_in_table c u h_spec h_ne
97+
have ⟨arr, h_found, h_mem⟩ := buildCaseFoldEquivTable_complete c.val u.val h_in
98+
rw [caseFoldEquivTable, caseFoldEquivTableThunk, Thunk.get] at h_none
99+
rw [h_found] at h_none
100+
contradiction
84101

85102
theorem mem_getCaseFoldEquivChars_iff {c₁ c₂ : Char} :
86-
c₂ ∈ Internal.getCaseFoldEquivChars_spec c₁ ↔ c₂.val ∈ caseFoldEquivTable[(Internal.getCaseFoldChar_spec c₁).val]! := by
87-
simp only [Internal.getCaseFoldEquivChars_spec]
88-
set folded := Internal.getCaseFoldChar_spec c₁ with h_folded
89-
have h_c₁_mem : c₁.val ∈ caseFoldEquivTable[folded.val]! := char_mem_caseFoldEquivTable c₁
90-
simp only [Std.HashMap.getElem!_eq_get!_getElem?] at h_c₁_mem ⊢
91-
cases h_lookup : caseFoldEquivTable[folded.val]? with
92-
| none =>
93-
simp only [h_lookup, Option.get!_none] at h_c₁_mem
94-
exact (Array.not_mem_empty c₁.val h_c₁_mem).elim
103+
c₂ ∈ Internal.getCaseFoldEquivChars_spec c₁ ↔
104+
Internal.getCaseFoldChar_spec c₂ = Internal.getCaseFoldChar_spec c₁ := by
105+
dsimp [Internal.getCaseFoldEquivChars_spec]
106+
let u₁ := Internal.getCaseFoldChar_spec c₁
107+
let u₂ := Internal.getCaseFoldChar_spec c₂
108+
match h_map : caseFoldEquivTable[u₁.val]? with
95109
| some arr =>
96-
simp only [Option.get!_some]
97110
constructor
98111
· intro h_mem
99-
simp only [Array.mem_map] at h_mem
100-
obtain ⟨u, h_u_in_arr, h_u_eq⟩ := h_mem
101-
have h_valid : UInt32.isValidChar u := caseFoldEquivTable_valid u folded (by
102-
simp only [Std.HashMap.getElem!_eq_get!_getElem?, h_lookup, Option.get!_some]
103-
exact h_u_in_arr)
104-
have h_c₂_eq : c₂.val = u := by
112+
rw [Array.mem_map] at h_mem
113+
obtain ⟨u, h_u_in, h_u_eq⟩ := h_mem
114+
have h_sound := buildCaseFoldEquivTable_soundness u u₁.val ⟨arr, h_map, h_u_in⟩
115+
rcases h_sound with h_in_table | h_eq_val
116+
· have h_fold := getCaseFoldChar_eq_of_mem u u₁.val h_in_table
117+
rw [h_u_eq] at h_fold
118+
change _ = Char.ofNat u₁.toNat at h_fold
119+
rw [Char.ofNat_toNat] at h_fold
120+
exact h_fold
121+
· rw [h_eq_val] at h_u_eq
122+
change Char.ofNat u₁.toNat = c₂ at h_u_eq
123+
rw [Char.ofNat_toNat] at h_u_eq
105124
rw [← h_u_eq]
106-
simp only [Char.ofNat, h_valid, dif_pos, Char.ofNatAux]
107-
cases u; simp [UInt32.toNat]
108-
rw [h_c₂_eq]
109-
exact h_u_in_arr
125+
exact getCaseFoldChar_spec_idempotent c₁
126+
· intro h_eq
127+
rw [Array.mem_map]
128+
exists c₂.val
129+
constructor
130+
· by_cases h_ne : c₂ ≠ u₁
131+
· have h_spec : Internal.getCaseFoldChar_spec c₂ = u₁ := h_eq
132+
have h_in_table := getCaseFoldChar_spec_ne_implies_in_table c₂ u₁ h_spec h_ne
133+
obtain ⟨arr', h_found, h_mem_arr⟩ := buildCaseFoldEquivTable_complete c₂.val u₁.val h_in_table
134+
rw [caseFoldEquivTable, caseFoldEquivTableThunk, Thunk.get] at h_map
135+
rw [h_found] at h_map
136+
injection h_map with h_arr_eq
137+
subst h_arr_eq
138+
exact h_mem_arr
139+
· simp only [not_not] at h_ne
140+
subst h_ne
141+
exact caseFoldEquivTable_mem_self u₁.val arr h_map
142+
· change Char.ofNat c₂.toNat = c₂
143+
exact Char.ofNat_toNat c₂
144+
| none =>
145+
have h_c1_eq_u1 : c₁ = u₁ := caseFoldEquivTable_none_imp_eq_fold c₁ u₁ rfl h_map
146+
constructor
110147
· intro h_mem
111-
simp only [Array.mem_map]
112-
refine ⟨c₂.val, h_mem, ?_⟩
113-
exact Char.ofNat_toNat c₂
148+
simp only [Array.mem_singleton] at h_mem
149+
rw [h_mem, h_c1_eq_u1]
150+
· intro h_eq
151+
rw [h_c1_eq_u1] at h_eq
152+
have h_none_u2 : caseFoldEquivTable[u₂.val]? = none := by
153+
grind
154+
have h_c2_eq_u2 : c₂ = u₂ := caseFoldEquivTable_none_imp_eq_fold c₂ u₂ rfl h_none_u2
155+
rw [h_c2_eq_u2]
156+
grind
114157

115158
theorem CaseFoldEquiv_iff_CaseFoldEquiv' {c₁ c₂ : Char} : CaseFoldEquiv c₁ c₂ ↔ CaseFoldEquiv' c₁ c₂ := by
116159
simp only [CaseFoldEquiv, CaseFoldEquiv']
117-
have h_c₂_id : Char.ofNat c₂.val.toNat = c₂ := Char.ofNat_toNat c₂
118-
constructor
119-
· intro h
120-
rw [mem_getCaseFoldEquivChars_iff] at h
121-
have h_sound := caseFoldTable_sound c₂.val (Internal.getCaseFoldChar_spec c₁) h
122-
rw [h_c₂_id] at h_sound
123-
exact h_sound.symm
124-
· intro h
125-
rw [mem_getCaseFoldEquivChars_iff, h]
126-
exact char_mem_caseFoldEquivTable c₂
160+
rw [mem_getCaseFoldEquivChars_iff]
161+
tauto
127162

128163
scoped infix:50 " ≃ " => CaseFoldEquiv
129164

0 commit comments

Comments
 (0)