feat: assorted lemmas (#12980)

This PR adds theorems about `Char`, `Nat` and `List`.

src/Init/Data/BEq.lean

@@ -36,6 +36,8 @@ theorem BEq.symm [BEq α] [Std.Symm (α := α) (· == ·)] {a b : α} : a == b
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
+theorem bne_eq [BEq α] {a b : α} : (a != b) = !(a == b) := rfl
+
 theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
   rw [bne, BEq.comm, bne]
 

src/Init/Data/Char/Lemmas.lean

@@ -86,4 +86,16 @@ theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
 @[simp]
 theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
 
+@[simp]
+theorem toNat_val {c : Char} : c.val.toNat = c.toNat := rfl
+
+theorem val_inj {c d : Char} : c.val = d.val ↔ c = d :=
+  Char.ext_iff.symm
+
+theorem toNat_inj {c d : Char} : c.toNat = d.toNat ↔ c = d := by
+  simp [← toNat_val, ← val_inj, ← UInt32.toNat_inj]
+
+theorem isDigit_iff_toNat {c : Char} : c.isDigit ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat := by
+  simp [isDigit, UInt32.le_iff_toNat_le]
+
 end Char

src/Init/Data/Char/Ordinal.lean

@@ -217,7 +217,7 @@ theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal
           Nat.reduceLeDiff, UInt32.left_eq_add]
         grind [UInt32.lt_iff_toNat_lt]
       · grind
-    · simp [coe_ordinal]
+    · simp [coe_ordinal, -toNat_val]
       grind [UInt32.lt_iff_toNat_lt]
   | case2 =>
     rw [Fin.addNat?_eq_some]

src/Init/Data/List/Lemmas.lean

@@ -877,6 +877,11 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
 theorem getLast?_cons {a : α} : (a::l).getLast? = some (l.getLast?.getD a) := by
   cases l <;> simp [getLast?, getLast]
 
+theorem getLast?_cons_of_ne_nil {x : α} {xs : List α} (h : xs ≠ []) : (x::xs).getLast? = xs.getLast? := by
+  cases xs with
+  | nil => contradiction
+  | cons => simp [getLast?_cons]
+
 @[simp] theorem getLast?_cons_cons : (a :: b :: l).getLast? = (b :: l).getLast? := by
   simp [getLast?_cons]
 
@@ -1283,6 +1288,13 @@ theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
     cases h : p a <;> simp [*]
     intro h; exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)
 
+theorem filter_bne_eq_self_of_not_mem [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∉ l) :
+    l.filter (· != a) = l := by
+  rw [List.filter_eq_self]
+  intro c hc
+  simp only [bne_iff_ne, ne_eq]
+  exact fun heq => absurd (heq ▸ hc) h
+
 @[simp]
 theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a := by
   induction l with
@@ -1336,6 +1348,16 @@ theorem foldl_filter {p : α → Bool} {f : β → α → β} {l : List α} {ini
     simp only [filter_cons, foldl_cons]
     split <;> simp [ih]
 
+theorem foldl_ite_left {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} :
+    (l.foldl (init := init) fun sofar a => if P a then f sofar a else sofar) = (l.filter P).foldl (init := init) f := by
+  simp [List.foldl_filter]
+
+theorem foldl_ite_right {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} :
+    (l.foldl (init := init) fun sofar a => if P a then sofar else f sofar a) =
+      (l.filter (fun a => ¬ P a)).foldl (init := init) f := by
+  simp +singlePass only [← ite_not]
+  rw [foldl_ite_left]
+
 theorem foldr_filter {p : α → Bool} {f : α → β → β} {l : List α} {init : β} :
     (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
   induction l generalizing init with

src/Init/Data/List/Sublist.lean

@@ -706,6 +706,11 @@ theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
 
 grind_pattern suffix_cons => _ <:+ a :: l
 
+@[simp]
+theorem suffix_cons_append {a : α} {l₁ l₂ : List α} : l₂ <:+ a :: (l₁ ++ l₂) := by
+  rw [← List.cons_append]
+  exact List.suffix_append (a :: l₁) l₂
+
 theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨l₁', l₂', h⟩ => ⟨a :: l₁', l₂', h ▸ rfl⟩
 
 theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨l₁', l₂', h⟩ =>
@@ -1299,6 +1304,121 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
   ⟨fun h => append_cancel_right <| (prefix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
     fun e => e.symm ▸ take_prefix _ _⟩
 
+theorem prefix_iff_exists_append_eq {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ l₃, l₁ ++ l₃ = l₂ :=
+  Iff.rfl
+
+theorem prefix_iff_exists_eq_append {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ l₃, l₂ = l₁ ++ l₃ := by
+  simp [prefix_iff_exists_append_eq, eq_comm]
+
 -- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`.
 
+theorem suffix_iff_exists_append_eq {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ l₃, l₃ ++ l₁ = l₂ :=
+  Iff.rfl
+
+theorem suffix_iff_exists_eq_append {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ l₃, l₂ = l₃ ++ l₁ := by
+  simp [suffix_iff_exists_append_eq, eq_comm]
+
+theorem suffix_append_self_iff {l₁ l₂ l₃ : List α} : l₁ ++ l₃ <:+ l₂ ++ l₃ ↔ l₁ <:+ l₂ := by
+  constructor
+  · rintro ⟨t, h⟩
+    exact ⟨t, List.append_cancel_right (by rwa [← List.append_assoc] at h)⟩
+  · rintro ⟨t, h⟩
+    exact ⟨t, by rw [← List.append_assoc, h]⟩
+
+theorem prefix_self_append_iff {l₁ l₂ l₃ : List α} : l₃ ++ l₁ <+: l₃ ++ l₂ ↔ l₁ <+: l₂ := by
+  constructor
+  · rintro ⟨t, h⟩
+    exact ⟨t, List.append_cancel_left (by rwa [List.append_assoc] at h)⟩
+  · rintro ⟨t, h⟩
+    exact ⟨t, by rw [List.append_assoc, h]⟩
+
+theorem suffix_append_inj_of_length_eq {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) :
+    l₁ ++ s₁ <:+ l₂ ++ s₂ ↔ l₁ <:+ l₂ ∧ s₁ = s₂ := by
+  simp only [suffix_iff_exists_eq_append]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨l₃, h⟩
+    rw [← List.append_assoc] at h
+    obtain ⟨rfl, rfl⟩ := List.append_inj' h hs.symm
+    refine ⟨⟨l₃, by simp⟩, by simp⟩
+  · rintro ⟨⟨l₃, rfl⟩, rfl⟩
+    refine ⟨l₃, by simp⟩
+
+theorem prefix_append_inj_of_length_eq {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) :
+    s₁ ++ l₁ <+: s₂ ++ l₂ ↔ s₁ = s₂ ∧ l₁ <+: l₂ := by
+  constructor
+  · rintro ⟨t, h⟩
+    rw [List.append_assoc] at h
+    obtain ⟨rfl, rfl⟩ := List.append_inj h.symm hs.symm
+    exact ⟨rfl, ⟨t, rfl⟩⟩
+  · rintro ⟨rfl, t, rfl⟩
+    exact ⟨t, by simp⟩
+
+theorem singleton_suffix_iff_getLast?_eq_some {a : α} {l : List α} : [a] <:+ l ↔ l.getLast? = some a := by
+  rw [suffix_iff_exists_eq_append, getLast?_eq_some_iff]
+
+theorem singleton_prefix_iff_head?_eq_some {a : α} {l : List α} : [a] <+: l ↔ l.head? = some a := by
+  simp [prefix_iff_exists_eq_append, head?_eq_some_iff]
+
+theorem singleton_prefix_cons_iff {a b : α} {l : List α} : [a] <+: b :: l ↔ a = b := by
+  simp
+
+@[simp]
+theorem singleton_suffix_append_singleton_iff {a b : α} {l : List α} :
+    [a] <:+ l ++ [b] ↔ a = b := by
+  refine ⟨fun h => Eq.symm ?_, by rintro rfl; simp⟩
+  simpa [List.suffix_iff_exists_eq_append] using h
+
+@[simp]
+theorem singleton_suffix_cons_append_singleton_iff {a b c : α} {l : List α} :
+    [a] <:+ b :: (l ++ [c]) ↔ a = c := by
+  rw [← List.cons_append]
+  exact singleton_suffix_append_singleton_iff
+
+theorem infix_append_iff {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔
+    l <:+: xs ∨ l <:+: ys ∨ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys) := by
+  constructor
+  · rintro ⟨s, t, ht⟩
+    rcases List.append_eq_append_iff.mp ht with ⟨as, hxs, _⟩ | ⟨bs, hsl, hys⟩
+    · exact Or.inl ⟨s, as, hxs.symm⟩
+    · rcases List.append_eq_append_iff.mp hsl with ⟨cs, hxs', hl⟩ | ⟨ds, _, hbs⟩
+      · exact Or.inr (Or.inr ⟨cs, bs, hl,
+          List.suffix_iff_exists_eq_append.mpr ⟨s, hxs'⟩,
+          List.prefix_iff_exists_eq_append.mpr ⟨t, hys⟩⟩)
+      · exact Or.inr (Or.inl ⟨ds, t, by rw [hys, ← hbs]⟩)
+  · rintro (⟨s, t, ht⟩ | ⟨s, t, ht⟩ | ⟨l₁, l₂, rfl, hl₁, hl₂⟩)
+    · exact ⟨s, t ++ ys, by rw [← List.append_assoc, ht]⟩
+    · exact ⟨xs ++ s, t, by
+        rw [List.append_assoc] at ht
+        rw [List.append_assoc (xs ++ s), List.append_assoc xs, ht]⟩
+    · rw [List.suffix_iff_exists_eq_append] at hl₁
+      rw [List.prefix_iff_exists_eq_append] at hl₂
+      obtain ⟨s, hxs⟩ := hl₁
+      obtain ⟨t, hys⟩ := hl₂
+      exact ⟨s, t, by rw [← List.append_assoc s l₁, List.append_assoc (s ++ l₁), hxs, hys]⟩
+
+theorem infix_append_iff_ne_nil {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔
+    l <:+: xs ∨ l <:+: ys ∨ (∃ l₁ l₂, l₁ ≠ [] ∧ l₂ ≠ [] ∧ l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys) := by
+  rw [List.infix_append_iff]
+  constructor
+  · rintro (h | h | ⟨l₁, l₂, hl, hl₁, hl₂⟩)
+    · exact Or.inl h
+    · exact Or.inr (Or.inl h)
+    · cases l₁ with
+      | nil =>
+        simp only [List.nil_append] at hl
+        subst hl
+        exact Or.inr (Or.inl hl₂.isInfix)
+      | cons hd tl =>
+        cases l₂ with
+        | nil =>
+          simp only [List.append_nil] at hl
+          subst hl
+          exact Or.inl hl₁.isInfix
+        | cons hd' tl' =>
+          exact Or.inr (Or.inr ⟨_, _, List.cons_ne_nil _ _, List.cons_ne_nil _ _, hl, hl₁, hl₂⟩)
+  · rintro (h | h | ⟨l₁, l₂, -, -, hl, hl₁, hl₂⟩)
+    · exact Or.inl h
+    · exact Or.inr (Or.inl h)
+    · exact Or.inr (Or.inr ⟨l₁, l₂, hl, hl₁, hl₂⟩)
+
 end List

src/Init/Data/List/TakeDrop.lean

@@ -297,6 +297,14 @@ theorem dropWhile_cons :
     (a :: l).dropWhile p = a :: l := by
   simp [dropWhile_cons, h]
 
+theorem dropWhile_beq_eq_self_of_head?_ne [BEq α] [LawfulBEq α] {a : α} {l : List α}
+    (h : l.head? ≠ some a) : l.dropWhile (· == a) = l := by
+  cases l with
+  | nil => simp
+  | cons hd tl =>
+    rw [List.dropWhile_cons_of_neg]
+    simpa [beq_iff_eq] using h
+
 theorem head?_takeWhile {p : α → Bool} {l : List α} : (l.takeWhile p).head? = l.head?.filter p := by
   cases l with
   | nil => rfl

src/Init/Data/Nat/Div/Lemmas.lean

@@ -253,4 +253,16 @@ theorem ext_div_mod {n a b : Nat} (h0 : a / n = b / n) (h1 : a % n = b % n) : a
 theorem ext_div_mod_iff (n a b : Nat) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
   ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_div_mod h0 h1⟩
 
+/-- An induction principle mirroring the base-`b` representation of the number. -/
+theorem base_induction {P : Nat → Prop} {n : Nat} (b : Nat) (hb : 1 < b) (single : ∀ m, m < b → P m)
+    (digit : ∀ m k, k < b → 0 < m → P m → P (b * m + k)) : P n := by
+  induction n using Nat.strongRecOn with | ind n ih
+  rcases Nat.lt_or_ge n b with hn | hn
+  · exact single _ hn
+  · have := div_add_mod n b
+    rw [← this]
+    apply digit _ _ (mod_lt _ (by omega)) _ (ih _ _)
+    · exact Nat.div_pos_iff.mpr ⟨by omega, hn⟩
+    · exact div_lt_self (by omega) (by omega)
+
 end Nat

src/Init/Data/Nat/ToString.lean

@@ -94,6 +94,14 @@ protected theorem digitChar_ne {n : Nat} (c : Char)
   match n with
   | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | _ + 16 => simp [digitChar] at h
 
+theorem toNat_digitChar_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat = 48 + n :=
+  match n with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => by simp [digitChar]
+  | _ + 10 => by omega
+
+theorem toNat_digitChar_sub_48_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat - 48 = n := by
+  simp [toNat_digitChar_of_lt_ten hn]
+
 private theorem isDigit_of_mem_toDigitsCore
     (hc : c ∈ cs → c.isDigit) (hb₁ : 0 < b) (hb₂ : b ≤ 10) (h : c ∈ toDigitsCore b fuel n cs) :
     c.isDigit := by

src/Init/Data/String/Decode.lean

@@ -64,7 +64,7 @@ public theorem Char.utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2
   match c.utf8Size, c.utf8Size_pos, c.utf8Size_le_four with
   | 1, _, _ | 2, _, _ | 3, _, _ | 4, _, _ => simp
 
-theorem Char.toNat_val_le {c : Char} : c.val.toNat ≤ 0x10ffff := by
+theorem Char.toNat_le {c : Char} : c.toNat ≤ 0x10ffff := by
   have := c.valid
   simp [UInt32.isValidChar, Nat.isValidChar] at this
   omega
@@ -193,10 +193,10 @@ theorem helper₄ (s : Nat) (c : BitVec w₀) (v : BitVec w') (w : Nat) :
 -- TODO: possibly it makes sense to factor out this proof
 theorem String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_one {c : Char} (h : c.utf8Size = 1) :
     ((String.utf8EncodeChar c)[0]'(by simp [h])).toBitVec = 0#1 ++ c.val.toBitVec.extractLsb' 0 7 := by
-  have h₀ : c.val.toNat < 128 := by
-    suffices c.val.toNat ≤ 127 by omega
+  have h₀ : c.toNat < 128 := by
+    suffices c.toNat ≤ 127 by omega
     simpa [Char.utf8Size_eq_one_iff, UInt32.le_iff_toNat_le] using h
-  have h₁ : c.val.toNat < 256 := by omega
+  have h₁ : c.toNat < 256 := by omega
   rw [← BitVec.toNat_inj, BitVec.toNat_append]
   simp [-Char.toUInt8_val, utf8EncodeChar_eq_singleton h, Nat.mod_eq_of_lt h₀, Nat.mod_eq_of_lt h₁]
 
@@ -977,9 +977,9 @@ theorem assemble₄_eq_some_iff_utf8EncodeChar_eq {w x y z : UInt8} {c : Char} :
         BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' (by simp),
         BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' (by simp),
         ← BitVec.setWidth_eq_extractLsb' (by simp), BitVec.setWidth_setWidth_eq_self]
-      have := c.toNat_val_le
+      have := c.toNat_le
       simp only [Nat.reduceAdd, BitVec.lt_def, UInt32.toNat_toBitVec, BitVec.toNat_twoPow,
-        Nat.reducePow, Nat.reduceMod, gt_iff_lt]
+        Nat.reducePow, Nat.reduceMod, gt_iff_lt, Char.toNat_val]
       omega
 
 theorem verify₄_eq_isSome_assemble₄ {w x y z : UInt8} :