From 0aac83fe40ea162bbb2a170656d5342a24a15c3b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 16 Sep 2024 12:24:14 +1000 Subject: [PATCH] feat: List.attachWith lemmas (#5352) --- src/Init/Data/List/Attach.lean | 183 ++++++++++++++++++++++++++------- 1 file changed, 146 insertions(+), 37 deletions(-) diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index e2229454af..76c16eefdc 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -48,6 +48,8 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep @[simp] theorem attach_nil : ([] : List α).attach = [] := rfl +@[simp] theorem attachWith_nil : ([] : List α).attachWith P H = [] := rfl + @[simp] theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : List α) (H) : @pmap _ _ p (fun a _ => f a) l H = map f l := by @@ -81,7 +83,12 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) : subst h simp -@[simp] theorem attach_cons (x : α) (xs : List α) : +theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} : + l₁.attachWith P H = l₂.attachWith P fun x h => H _ (w ▸ h) := by + subst w + simp + +@[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 simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and] @@ -89,6 +96,12 @@ theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) : intros a _ m' _ rfl +@[simp] +theorem attachWith_cons {x : α} {xs : List α} {p : α → Prop} (h : ∀ a ∈ x :: xs, p a) : + (x :: xs).attachWith p h = ⟨x, h x (mem_cons_self x xs)⟩ :: + xs.attachWith p (fun a ha ↦ h a (mem_cons_of_mem x ha)) := + 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_left l fun _ _ _ _ => rfl @@ -104,15 +117,37 @@ 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 attachWith_map_coe {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) : + ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by + rw [attachWith, map_pmap]; exact pmap_eq_map _ _ _ _ + +theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H : ∀ a ∈ l, p a) : + ((l.attachWith p H).map fun i => f i.val) = l.map f := + attachWith_map_coe _ _ _ + +@[simp] +theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) : + (l.attachWith p H).map Subtype.val = l := + (attachWith_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 simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val] +theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) : + (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by + simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val] + @[simp] 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] +theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) : + (l.attachWith p H).count a = l.count ↑a := + Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _ + @[simp] theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach | ⟨a, h⟩ => by @@ -137,7 +172,11 @@ theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : length (pm · simp only [*, pmap, length] @[simp] -theorem length_attach (L : List α) : L.attach.length = L.length := +theorem length_attach {L : List α} : L.attach.length = L.length := + length_pmap + +@[simp] +theorem length_attachWith {p : α → Prop} {l H} : length (l.attachWith p H) = length l := length_pmap @[simp] @@ -155,6 +194,15 @@ theorem attach_eq_nil_iff {l : List α} : l.attach = [] ↔ l = [] := theorem attach_ne_nil_iff {l : List α} : l.attach ≠ [] ↔ l ≠ [] := pmap_ne_nil_iff _ _ +@[simp] +theorem attachWith_eq_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} : + l.attachWith P H = [] ↔ l = [] := + pmap_eq_nil_iff + +theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} : + l.attachWith P H ≠ [] ↔ 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 @@ -205,34 +253,26 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : simp only [get_eq_getElem] simp [getElem_pmap] +@[simp] +theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} : + (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (getElem?_mem a)) := + 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 + xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) := + getElem?_attachWith + +@[simp] +theorem getElem_attachWith {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a} + {i : Nat} (h : i < (xs.attachWith P H).length) : + (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem xs i (by simpa using h))⟩ := + getElem_pmap .. @[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'] + xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem xs i (by simpa using h)⟩ := + getElem_attachWith h @[simp] theorem head?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) (H : ∀ (a : α), a ∈ xs → P a) : @@ -250,11 +290,23 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) : | nil => simp at h | cons x xs ih => simp [head_pmap, ih] +@[simp] theorem head?_attachWith {P : α → Prop} {xs : List α} + (H : ∀ (a : α), a ∈ xs → P a) : + (xs.attachWith P H).head? = xs.head?.pbind (fun a h => some ⟨a, H _ (mem_of_mem_head? h)⟩) := by + cases xs <;> simp_all + +@[simp] theorem head_attachWith {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) : + (xs.attachWith P H).head h = ⟨xs.head (by simpa using h), H _ (head_mem _)⟩ := by + cases xs with + | nil => simp at h + | cons x xs => simp [head_attachWith, h] + @[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) : +@[simp] 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 @@ -264,6 +316,32 @@ theorem attach_map {l : List α} (f : α → β) : (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by induction l <;> simp [*] +theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} : + (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map + fun ⟨x, h⟩ => ⟨f x, h⟩ := by + induction l <;> simp [*] + +theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a} + (f : { x // P x } → β) : + (l.attachWith P H).map f = + l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩) := by + induction l with + | nil => rfl + | cons x xs ih => + simp only [attachWith_cons, map_cons, ih, pmap, cons.injEq, true_and] + apply pmap_congr_left + simp + +/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/ +theorem map_attach {l : List α} (f : { x // x ∈ l } → β) : + l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id) := by + induction l with + | nil => rfl + | cons x xs ih => + simp only [attach_cons, map_cons, map_map, Function.comp_apply, pmap, cons.injEq, true_and, ih] + apply pmap_congr_left + simp + theorem attach_filterMap {l : List α} {f : α → Option β} : (l.filterMap f).attach = l.attach.filterMap fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by @@ -304,6 +382,9 @@ theorem attach_filter {l : List α} (p : α → Bool) : ext1 split <;> simp +-- We are still missing here `attachWith_filterMap` and `attachWith_filter`. +-- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`. + 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 @@ -334,6 +415,12 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ : congr 1 <;> exact pmap_congr_left _ fun _ _ _ _ => rfl +@[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α} + {H : ∀ (a : α), a ∈ xs ++ ys → P a} : + (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_of_mem_left ys h)) ++ + ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by + simp only [attachWith, attach_append, map_pmap, pmap_append] + @[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 @@ -344,6 +431,17 @@ theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by rw [pmap_reverse] +@[simp] theorem attachWith_reverse {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs.reverse → P a} : + xs.reverse.attachWith P H = + (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := + pmap_reverse .. + +theorem reverse_attachWith {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs → P a} : + (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := + reverse_pmap .. + @[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] @@ -358,17 +456,6 @@ theorem reverse_attach (xs : List α) : intros rfl -@[simp] -theorem getLast?_attach {xs : List α} : - 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 @@ -383,4 +470,26 @@ theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) : simp only [getLast_eq_head_reverse] simp only [reverse_pmap, head_pmap, head_reverse] +@[simp] theorem getLast?_attachWith {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs → P a} : + (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast?_eq_some h)⟩) := by + rw [getLast?_eq_head?_reverse, reverse_attachWith, head?_attachWith] + simp + +@[simp] theorem getLast_attachWith {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) : + (xs.attachWith P H).getLast h = ⟨xs.getLast (by simpa using h), H _ (getLast_mem _)⟩ := by + simp only [getLast_eq_head_reverse, reverse_attachWith, head_attachWith, head_map] + +@[simp] +theorem getLast?_attach {xs : List α} : + 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] + end List