Skip to content

Commit

Permalink
refactor: rename theorems about Char.utf8Size (#901)
Browse files Browse the repository at this point in the history
  • Loading branch information
@chabulhwi
chabulhwi authored Aug 1, 2024
1 parent 0f3e143 commit 41bc768
Showing 1 changed file with 27 additions and 27 deletions.
54 changes: 27 additions & 27 deletions Batteries/Data/String/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,14 @@ instance : Batteries.BEqOrd String := .compareOfLessAndEq String.lt_irrefl

attribute [simp] toList -- prefer `String.data` over `String.toList` in lemmas

private theorem add_csize_pos : 0 < i + Char.utf8Size c :=
private theorem add_utf8Size_pos : 0 < i + Char.utf8Size c :=
Nat.add_pos_right _ (Char.utf8Size_pos c)

private theorem ne_add_csize_add_self : i ≠ n + Char.utf8Size c + i :=
Nat.ne_of_lt (Nat.lt_add_of_pos_left add_csize_pos)
private theorem ne_add_utf8Size_add_self : i ≠ n + Char.utf8Size c + i :=
Nat.ne_of_lt (Nat.lt_add_of_pos_left add_utf8Size_pos)

private theorem ne_self_add_add_csize : i ≠ i + (n + Char.utf8Size c) :=
Nat.ne_of_lt (Nat.lt_add_of_pos_right add_csize_pos)
private theorem ne_self_add_add_utf8Size : i ≠ i + (n + Char.utf8Size c) :=
Nat.ne_of_lt (Nat.lt_add_of_pos_right add_utf8Size_pos)

/-- The UTF-8 byte length of a list of characters. (This is intended for specification purposes.) -/
@[inline] def utf8Len : List Char → Nat := utf8ByteSize.go
Expand All @@ -64,7 +64,7 @@ private theorem ne_self_add_add_csize : i ≠ i + (n + Char.utf8Size c) :=
@[simp] theorem utf8Len_reverse (cs) : utf8Len cs.reverse = utf8Len cs := utf8Len_reverseAux ..

@[simp] theorem utf8Len_eq_zero : utf8Len l = 0 ↔ l = [] := by
cases l <;> simp [Nat.ne_of_gt add_csize_pos]
cases l <;> simp [Nat.ne_of_gt add_utf8Size_pos]

section
open List
Expand Down Expand Up @@ -92,7 +92,7 @@ attribute [ext] ext
theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (Char.utf8Size_pos _)

private theorem zero_ne_addChar {i : Pos} {c : Char} : 0 ≠ i + c :=
ne_of_lt add_csize_pos
ne_of_lt add_utf8Size_pos

/-- A string position is valid if it is equal to the UTF-8 length of an initial substring of `s`. -/
def Valid (s : String) (p : Pos) : Prop :=
Expand Down Expand Up @@ -154,7 +154,7 @@ theorem utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len c
| c::cs, cs' =>
simp only [utf8GetAux, List.append_eq, Char.reduceDefault, ↓Char.isValue]
rw [if_neg]
case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_csize
case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_utf8Size
refine utf8GetAux_of_valid cs cs' ?_
simpa [Nat.add_assoc, Nat.add_comm] using hp

Expand All @@ -173,7 +173,7 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len
| c::cs, cs' =>
simp only [utf8GetAux?, List.append_eq]
rw [if_neg]
case hnc => simp [← hp, Pos.ext_iff]; exact ne_self_add_add_csize
case hnc => simp [← hp, Pos.ext_iff]; exact ne_self_add_add_utf8Size
refine utf8GetAux?_of_valid cs cs' ?_
simpa [Nat.add_assoc, Nat.add_comm] using hp

Expand All @@ -188,7 +188,7 @@ theorem utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i
| c::cs, cs' =>
simp only [utf8SetAux, List.append_eq, List.cons_append]
rw [if_neg]
case hnc => simp [← hp, Pos.ext_iff]; exact ne_self_add_add_csize
case hnc => simp [← hp, Pos.ext_iff]; exact ne_self_add_add_utf8Size
refine congrArg (c::·) (utf8SetAux_of_valid c' cs cs' ?_)
simpa [Nat.add_assoc, Nat.add_comm] using hp

Expand Down Expand Up @@ -228,14 +228,14 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat}
case hnc =>
simp only [Pos.ext_iff]
rw [Nat.add_right_comm, Nat.add_left_comm]
apply ne_add_csize_add_self
apply ne_add_utf8Size_add_self
refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_
simp [Nat.add_assoc, Nat.add_comm]

theorem prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
prev ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs + c.utf8Size⟩ = ⟨utf8Len cs⟩ := by
simp only [prev]
refine (if_neg (Pos.ne_of_gt add_csize_pos)).trans ?_
refine (if_neg (Pos.ne_of_gt add_utf8Size_pos)).trans ?_
rw [utf8PrevAux_of_valid] <;> simp

theorem prev_of_valid' (cs cs' : List Char) :
Expand All @@ -255,7 +255,7 @@ theorem back_eq (s : String) : back s = s.1.getLastD default := by
theorem atEnd_of_valid (cs : List Char) (cs' : List Char) :
atEnd ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ ↔ cs' = [] := by
rw [atEnd_iff]
cases cs' <;> simp [Nat.lt_add_of_pos_right add_csize_pos]
cases cs' <;> simp [Nat.lt_add_of_pos_right add_utf8Size_pos]

unseal posOfAux findAux in
theorem posOfAux_eq (s c) : posOfAux s c = findAux s (· == c) := rfl
Expand All @@ -276,7 +276,7 @@ theorem findAux_of_valid (p) : ∀ l m r,
| l, [], r => by unfold findAux List.takeWhile; simp
| l, c::m, r => by
unfold findAux List.takeWhile
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
have h1 := get_of_valid l (c::m++r); have h2 := next_of_valid l c (m++r)
simp only [List.cons_append, Char.reduceDefault, List.headD_cons] at h1 h2
simp only [List.append_assoc, List.cons_append, h1, utf8Len_cons, h2]
Expand All @@ -298,7 +298,7 @@ theorem revFindAux_of_valid (p) : ∀ l r,
| [], r => by unfold revFindAux List.dropWhile; simp
| c::l, r => by
unfold revFindAux List.dropWhile
rw [dif_neg (by exact Pos.ne_of_gt add_csize_pos)]
rw [dif_neg (by exact Pos.ne_of_gt add_utf8Size_pos)]
have h1 := get_of_valid l.reverse (c::r); have h2 := prev_of_valid l.reverse c r
simp only [utf8Len_reverse, Char.reduceDefault, List.headD_cons] at h1 h2
simp only [List.reverse_cons, List.append_assoc, List.singleton_append, utf8Len_cons, h2, h1]
Expand All @@ -320,7 +320,7 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p)
rw [
dif_pos <| by
rw [hstop, ← hl₁, ← hl₂]
refine Nat.lt_min.2 ⟨?_, ?_⟩ <;> exact Nat.lt_add_of_pos_right add_csize_pos,
refine Nat.lt_min.2 ⟨?_, ?_⟩ <;> exact Nat.lt_add_of_pos_right add_utf8Size_pos,
show get ⟨l₁ ++ a :: r₁⟩ ⟨p⟩ = a by simp [hl₁, get_of_valid],
show get ⟨l₂ ++ b :: r₂⟩ ⟨p⟩ = b by simp [hl₂, get_of_valid]]
simp only [bne_iff_ne, ne_eq, ite_not, decide_eq_true_eq]
Expand Down Expand Up @@ -360,7 +360,7 @@ theorem extract.go₂_append_left : ∀ (s t : List Char) (i e : Nat),
e = utf8Len s + i → go₂ (s ++ t) ⟨i⟩ ⟨e⟩ = s
| [], t, i, _, rfl => by cases t <;> simp [go₂]
| c :: cs, t, i, _, rfl => by
simp only [go₂, utf8Len_cons, Pos.ext_iff, ne_add_csize_add_self, ↓reduceIte, List.append_eq,
simp only [go₂, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq,
Pos.addChar_eq, List.cons.injEq, true_and]
apply go₂_append_left; rw [Nat.add_right_comm, Nat.add_assoc]

Expand All @@ -379,15 +379,15 @@ theorem extract.go₁_add_right_cancel (s : List Char) (i b e n : Nat) :

theorem extract.go₁_cons_addChar (c : Char) (cs : List Char) (b e : Pos) :
go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e := by
simp only [go₁, Pos.ext_iff, Pos.byteIdx_zero, pos_add_char, Nat.ne_of_lt add_csize_pos,
simp only [go₁, Pos.ext_iff, Pos.byteIdx_zero, pos_add_char, Nat.ne_of_lt add_utf8Size_pos,
↓reduceIte]
apply go₁_add_right_cancel

theorem extract.go₁_append_right : ∀ (s t : List Char) (i b : Nat) (e : Pos),
b = utf8Len s + i → go₁ (s ++ t) ⟨i⟩ ⟨b⟩ e = go₂ t ⟨b⟩ e
| [], t, i, _, e, rfl => by cases t <;> simp [go₁, go₂]
| c :: cs, t, i, _, e, rfl => by
simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_csize_add_self, ↓reduceIte, List.append_eq,
simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq,
Pos.addChar_eq]
apply go₁_append_right; rw [Nat.add_right_comm, Nat.add_assoc]

Expand All @@ -404,7 +404,7 @@ theorem extract_zero_endPos : ∀ (s : String), s.extract 0 (endPos s) = s
| ⟨[]⟩ => rfl
| ⟨c :: cs⟩ => by
simp only [extract, Pos.byteIdx_zero, endPos_eq, utf8Len_cons, ge_iff_le, Nat.le_zero_eq,
Nat.ne_of_gt add_csize_pos, ↓reduceIte]
Nat.ne_of_gt add_utf8Size_pos, ↓reduceIte]
congr
apply extract.go₁_zero_utf8Len

Expand Down Expand Up @@ -645,7 +645,7 @@ theorem offsetOfPosAux_of_valid : ∀ l m r n,
| l, [], r, n => by unfold offsetOfPosAux; simp
| l, c::m, r, n => by
unfold offsetOfPosAux
rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_csize_pos))]
rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos))]
simp only [List.append_assoc, atEnd_of_valid l (c::m++r)]
simp only [List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r)]
simpa [← Nat.add_assoc, Nat.add_right_comm] using
Expand All @@ -660,7 +660,7 @@ theorem foldlAux_of_valid (f : α → Char → α) : ∀ l m r a,
| l, [], r, a => by unfold foldlAux; simp
| l, c::m, r, a => by
unfold foldlAux
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
simp only [List.append_assoc, List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r),
get_of_valid l (c :: (m ++ r)), Char.reduceDefault, List.headD_cons, List.foldl_cons]
simpa [← Nat.add_assoc, Nat.add_right_comm] using foldlAux_of_valid f (l++[c]) m r (f a c)
Expand All @@ -674,7 +674,7 @@ theorem foldrAux_of_valid (f : Char → α → α) (l m r a) :
rw [← m.reverse_reverse]
induction m.reverse generalizing r a with (unfold foldrAux; simp)
| cons c m IH =>
rw [if_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
rw [if_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r]
simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)]
simpa using IH (c::r) (f c a)
Expand All @@ -688,7 +688,7 @@ theorem anyAux_of_valid (p : Char → Bool) : ∀ l m r,
| l, [], r => by unfold anyAux; simp
| l, c::m, r => by
unfold anyAux
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r),
Bool.if_true_left, Bool.decide_eq_true, List.any_cons]
Expand Down Expand Up @@ -732,7 +732,7 @@ theorem takeWhileAux_of_valid (p : Char → Bool) : ∀ l m r,
| l, [], r => by unfold Substring.takeWhileAux List.takeWhile; simp
| l, c::m, r => by
unfold Substring.takeWhileAux List.takeWhile
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r)]
cases p c <;> simp
Expand Down Expand Up @@ -809,7 +809,7 @@ theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
rw [if_neg (mt Pos.ext_iff.1 ?a)]
case a =>
simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
@ne_add_csize_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c
@ne_add_utf8Size_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c
have := next_of_valid (l ++ m₁) c (m₂ ++ r)
simp only [List.append_assoc, utf8Len_append, Pos.add_eq] at this ⊢; rw [this]
simp [Nat.add_assoc, Nat.add_sub_cancel_left]
Expand All @@ -822,7 +822,7 @@ theorem prev : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
| _, ⟨⟩ => by
simp only [Substring.prev, List.append_assoc, List.cons_append]
rw [if_neg (mt Pos.ext_iff.1 <| Ne.symm ?a)]
case a => simpa [Nat.add_comm] using @ne_add_csize_add_self (utf8Len l) (utf8Len m₁) c
case a => simpa [Nat.add_comm] using @ne_add_utf8Size_add_self (utf8Len l) (utf8Len m₁) c
have := prev_of_valid (l ++ m₁) c (m₂ ++ r)
simp only [List.append_assoc, utf8Len_append, Nat.add_assoc, Pos.add_eq] at this ⊢; rw [this]
simp [Nat.add_sub_cancel_left]
Expand Down

0 comments on commit 41bc768

Please sign in to comment.