From fcfead8cde816c28f29a3ce6fe4eaf4c015c13a7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 7 Sep 2024 08:14:56 +1000 Subject: [PATCH] feat: lemmas about List.attach (#5273) #5272 should be merged first; this contains some material from that PR. --- src/Init/Data/List/Attach.lean | 161 +++++++++++++++++++++++++-------- src/Init/Data/List/Lemmas.lean | 14 +++ 2 files changed, 137 insertions(+), 38 deletions(-) diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 0182934e8e..ab5ee32097 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -55,11 +55,14 @@ theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) : · rfl · simp only [*, pmap, map] -theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂} +theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂} (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by induction l with | nil => rfl - | cons x l ih => rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)] + | cons x l ih => + rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)] + +@[deprecated pmap_congr_left (since := "2024-09-06")] abbrev pmap_congr := @pmap_congr_left theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) : map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by @@ -74,15 +77,16 @@ theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) · simp only [*, pmap, map] @[simp] theorem attach_cons (x : α) (xs : List α) : - (x :: xs).attach = ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by + (x :: xs).attach = + ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and] - apply pmap_congr + apply pmap_congr_left intros a _ m' _ rfl theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) : pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by - rw [attach, attachWith, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl + rw [attach, attachWith, map_pmap]; exact pmap_congr_left l fun _ _ _ _ => rfl theorem attach_map_coe (l : List α) (f : α → β) : (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by @@ -95,11 +99,13 @@ theorem attach_map_val (l : List α) (f : α → β) : (l.attach.map fun i => f theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l := (attach_map_coe _ _).trans (List.map_id _) -theorem countP_attach (l : List α) (p : α → Bool) : l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by +theorem countP_attach (l : List α) (p : α → Bool) : + l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val] @[simp] -theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a := +theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : + l.attach.count a = l.count ↑a := Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ @[simp] @@ -114,6 +120,11 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} : b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm] +theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) : + f a (H a h) ∈ pmap f l H := by + rw [mem_pmap] + exact ⟨a, h, rfl⟩ + @[simp] theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pmap f l H) = length l := by induction l @@ -125,17 +136,26 @@ theorem length_attach (L : List α) : L.attach.length = L.length := length_pmap @[simp] -theorem pmap_eq_nil {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by +theorem pmap_eq_nil_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by rw [← length_eq_zero, length_pmap, length_eq_zero] -theorem pmap_ne_nil {P : α → Prop} (f : (a : α) → P a → β) {xs : List α} +theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : List α} (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by simp @[simp] -theorem attach_eq_nil {l : List α} : l.attach = [] ↔ l = [] := - pmap_eq_nil +theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] := + pmap_eq_nil_iff +theorem attach_ne_nil_iff {l : List α} : l.attach ≠ [] ↔ l ≠ [] := + pmap_ne_nil_iff _ _ + +@[deprecated pmap_eq_nil_iff (since := "2024-09-06")] abbrev pmap_eq_nil := @pmap_eq_nil_iff +@[deprecated pmap_ne_nil_iff (since := "2024-09-06")] abbrev pmap_ne_nil := @pmap_ne_nil_iff +@[deprecated attach_eq_nil_iff (since := "2024-09-06")] abbrev attach_eq_nil := @attach_eq_nil_iff +@[deprecated attach_ne_nil_iff (since := "2024-09-06")] abbrev attach_ne_nil := @attach_ne_nil_iff + +@[simp] theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) : (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by induction l generalizing n with @@ -157,6 +177,7 @@ theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : simp only [get?_eq_getElem?] simp [getElem?_pmap, h] +@[simp] theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat} (hn : n < (pmap f l h).length) : (pmap f l h)[n] = @@ -179,8 +200,38 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : simp only [get_eq_getElem] simp [getElem_pmap] +@[simp] +theorem getElem?_attach {xs : List α} {i : Nat} : + xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) := by + induction xs generalizing i with + | nil => simp + | cons x xs ih => + rcases i with ⟨i⟩ + · simp only [attach_cons, Option.pmap] + split <;> simp_all + · simp only [attach_cons, getElem?_cons_succ, getElem?_map, ih] + simp only [Option.pmap] + split <;> split <;> simp_all + +@[simp] +theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) : + xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem xs i (by simpa using h)⟩ := by + apply Option.some.inj + rw [← getElem?_eq_getElem] + rw [getElem?_attach] + simp only [Option.pmap] + split <;> rename_i h' _ + · simp at h + simp at h' + exfalso + exact Nat.lt_irrefl _ (Nat.lt_of_le_of_lt h' h) + · simp only [Option.some.injEq, Subtype.mk.injEq] + apply Option.some.inj + rw [← getElem?_eq_getElem, h'] + @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) - (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m) := by + (H : ∀ (a : α), a ∈ xs → P a) : + (xs.pmap f H).head? = xs.attach.head?.map fun ⟨a, m⟩ => f a (H a m) := by induction xs with | nil => simp | cons x xs ih => @@ -194,6 +245,42 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : | nil => simp at h | cons x xs ih => simp [head_pmap, ih] +@[simp] theorem head?_attach (xs : List α) : + xs.attach.head? = xs.head?.pbind (fun a h => some ⟨a, mem_of_mem_head? h⟩) := by + cases xs <;> simp_all + +theorem head_attach {xs : List α} (h) : + xs.attach.head h = ⟨xs.head (by simpa using h), head_mem (by simpa using h)⟩ := by + cases xs with + | nil => simp at h + | cons x xs => simp [head_attach, h] + +theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) : + pmap f (pmap g l H₁) H₂ = + pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach + (fun a _ => H₁ a a.2) := by + induction l with + | nil => rfl + | cons x xs ih => + simp only [pmap, ih, cons.injEq, true_and] + ext1 i + simp only [getElem?_pmap, Option.pmap] + split <;> rename_i h _ <;> split <;> rename_i h' _ + · rfl + · simp only [getElem?_attach, Option.pmap_eq_none, getElem?_eq_none_iff] at h + simp [getElem?_eq_none h] at h' + · simp only [getElem?_pmap, Option.pmap_eq_none, getElem?_eq_none_iff] at h' + rw [getElem?_eq_none] at h + simp only [reduceCtorEq] at h + simpa using h' + · simp only [getElem?_attach, Option.pmap_eq_some, exists_and_left] at h + simp only [getElem?_pmap, Option.pmap_eq_some, mem_cons, exists_and_left] at h' + obtain ⟨a, h, x, rfl⟩ := h + obtain ⟨a, h', x', rfl⟩ := h' + simp only [h, Option.some.injEq] at h' + subst h' + rfl + @[simp] theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι) (h : ∀ a ∈ l₁ ++ l₂, p a) : (l₁ ++ l₂).pmap f h = @@ -212,11 +299,13 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : pmap_append f l₁ l₂ _ @[simp] theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) - (H : ∀ (a : α), a ∈ xs.reverse → P a) : xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by + (H : ∀ (a : α), a ∈ xs.reverse → P a) : + xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by induction xs <;> simp_all theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) - (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by + (H : ∀ (a : α), a ∈ xs → P a) : + (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by rw [pmap_reverse] @[simp] theorem attach_append (xs ys : List α) : @@ -224,33 +313,36 @@ theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_of_mem_right xs h⟩ := by simp only [attach, attachWith, pmap, map_pmap, pmap_append] congr 1 <;> - exact pmap_congr _ fun _ _ _ _ => rfl + exact pmap_congr_left _ fun _ _ _ _ => rfl -@[simp] theorem attach_reverse (xs : List α) : xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by +@[simp] theorem attach_reverse (xs : List α) : + xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by simp only [attach, attachWith, reverse_pmap, map_pmap] - apply pmap_congr + apply pmap_congr_left intros rfl -theorem reverse_attach (xs : List α) : xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by +theorem reverse_attach (xs : List α) : + xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by simp only [attach, attachWith, reverse_pmap, map_pmap] - apply pmap_congr + apply pmap_congr_left intros rfl - +@[simp] theorem getLast?_attach {xs : List α} : - xs.attach.getLast? = match h : xs.getLast? with | none => none | some a => some ⟨a, mem_of_getLast?_eq_some h⟩ := by - rw [getLast?_eq_head?_reverse, reverse_attach, head?_map] - split <;> rename_i h - · simp only [getLast?_eq_none_iff] at h - subst h - simp - · obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.mp h - simp + xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast?_eq_some h⟩ := by + rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach] + simp + +@[simp] +theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) : + xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by + simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach] @[simp] theorem getLast?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) - (H : ∀ (a : α), a ∈ xs → P a) : (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m) := by + (H : ∀ (a : α), a ∈ xs → P a) : + (xs.pmap f H).getLast? = xs.attach.getLast?.map fun ⟨a, m⟩ => f a (H a m) := by simp only [getLast?_eq_head?_reverse] rw [reverse_pmap, reverse_attach, head?_map, pmap_eq_map_attach, head?_map] simp only [Option.map_map] @@ -259,14 +351,7 @@ theorem getLast?_attach {xs : List α} : @[simp] theorem getLast_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) (h : xs.pmap f H ≠ []) : (xs.pmap f H).getLast h = f (xs.getLast (by simpa using h)) (H _ (getLast_mem _)) := by - simp only [getLast_eq_iff_getLast_eq_some, getLast?_pmap, Option.map_eq_some', Subtype.exists] - refine ⟨xs.getLast (by simpa using h), by simp, ?_⟩ - simp only [getLast?_attach, and_true] - split <;> rename_i h' - · simp only [getLast?_eq_none_iff] at h' - subst h' - simp at h - · symm - simpa [getLast_eq_iff_getLast_eq_some] + simp only [getLast_eq_head_reverse] + simp only [reverse_pmap, head_pmap, head_reverse] end List diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index ef102bb8fe..713def2ac2 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -993,6 +993,15 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys | [], h => absurd rfl h | _::_, _ => .head .. +theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l := by + intro l a h + cases l with + | nil => simp at h + | cons b l => + simp at h + cases h + exact mem_cons_self a l + theorem head?_concat {a : α} : (l ++ [a]).head? = l.head?.getD a := by cases l <;> simp @@ -2374,6 +2383,11 @@ theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head theorem head?_eq_getLast?_reverse {xs : List α} : xs.head? = xs.reverse.getLast? := by simp +theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a ∈ l := by + rw [getLast?_eq_head?_reverse] at h + rw [← mem_reverse] + exact mem_of_mem_head? h + @[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by induction l <;> simp [*]