From 61ba0bdc67d306df814181c837df5e4d09e36406 Mon Sep 17 00:00:00 2001 From: tjf801 <47402907+tjf801@users.noreply.github.com> Date: Sun, 28 Apr 2024 18:23:02 -0400 Subject: [PATCH 1/2] Add `String.length_join` and `List.length_join` --- Std/Data/List/Lemmas.lean | 3 +++ Std/Data/String/Lemmas.lean | 5 +++++ 2 files changed, 8 insertions(+) diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean index 514ed09dbc..00404fa38c 100644 --- a/Std/Data/List/Lemmas.lean +++ b/Std/Data/List/Lemmas.lean @@ -365,6 +365,9 @@ theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_ theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩ +theorem length_join (l : List (List α)) : (join l).length = Nat.sum (l.map length) := by + induction l <;> simp [*] + /-! ### bind -/ theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean index e87013574d..3bede5e5c9 100644 --- a/Std/Data/String/Lemmas.lean +++ b/Std/Data/String/Lemmas.lean @@ -499,6 +499,11 @@ theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss @[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).join := by rw [join_eq] +@[simp] theorem comp_length_data : List.length ∘ String.data = String.length := rfl + +theorem length_join (l : List String) : (String.join l).length = Nat.sum (l.map String.length) := by + simp [length, List.length_join, List.map_map] + theorem singleton_eq (c : Char) : singleton c = ⟨[c]⟩ := rfl @[simp] theorem data_singleton (c : Char) : (singleton c).data = [c] := rfl From 445b714d20e70dee0c01027c33f2becf83b93331 Mon Sep 17 00:00:00 2001 From: tjf801 <47402907+tjf801@users.noreply.github.com> Date: Tue, 30 Apr 2024 21:54:37 -0400 Subject: [PATCH 2/2] Update Std/Data/List/Lemmas.lean Update Std/Data/String/Lemmas.lean Co-Authored-By: Kim Morrison --- Std/Data/String/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean index 3bede5e5c9..4e996d14e0 100644 --- a/Std/Data/String/Lemmas.lean +++ b/Std/Data/String/Lemmas.lean @@ -499,10 +499,10 @@ theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss @[simp] theorem data_join (ss : List String) : (join ss).data = (ss.map data).join := by rw [join_eq] -@[simp] theorem comp_length_data : List.length ∘ String.data = String.length := rfl +@[simp] theorem length_data (s : String) : s.data.length = s.length := rfl -theorem length_join (l : List String) : (String.join l).length = Nat.sum (l.map String.length) := by - simp [length, List.length_join, List.map_map] +theorem length_join (l : List String) : (join l).length = Nat.sum (l.map length) := by + simp [length, List.length_join, List.map_map, (funext length_data : List.length ∘ data = length)] theorem singleton_eq (c : Char) : singleton c = ⟨[c]⟩ := rfl