diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean index 7345b9900f..6f0d377241 100644 --- a/src/Init/Data/BEq.lean +++ b/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] diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index 5246a1107b..1f4b6af86c 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/Char/Ordinal.lean b/src/Init/Data/Char/Ordinal.lean index acb5fc9645..eac0a21189 100644 --- a/src/Init/Data/Char/Ordinal.lean +++ b/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] diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 328689ead8..6db7245314 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 13bfd54403..0ed0f6f1bb 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/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 diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 6deba2cc57..7694777b40 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/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 diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean index b74db44843..269cc7b250 100644 --- a/src/Init/Data/Nat/Div/Lemmas.lean +++ b/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 diff --git a/src/Init/Data/Nat/ToString.lean b/src/Init/Data/Nat/ToString.lean index bd37ea9893..4390acc5b4 100644 --- a/src/Init/Data/Nat/ToString.lean +++ b/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 diff --git a/src/Init/Data/String/Decode.lean b/src/Init/Data/String/Decode.lean index 2b61e19b59..83c2ca854d 100644 --- a/src/Init/Data/String/Decode.lean +++ b/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} :