max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: List.attachWith lemmas (#5352)

Browse source
This commit is contained in:
Kim Morrison 2024-09-16 12:24:14 +10:00 • committed by GitHub
parent 8c6ac845b1
commit 0aac83fe40
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 146 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

183
src/Init/Data/List/Attach.lean
View file

@ -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