diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 51ea705406e5..5b5a1583fa1a 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -572,6 +572,14 @@ theorem reverseAux_reverseAux {as bs cs : List α} : | nil => rfl | cons a as ih => simp [reverseAux, ih (bs := a::bs), ih (bs := [a])] +theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by + induction as generalizing bs with + | nil => rfl + | cons a as ih => simp [reverseAux, ih] + +@[simp] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by + simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl + /-! ### append -/ /-- @@ -654,6 +662,24 @@ theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux a simp [reverse, reverseAux] rw [← reverseAux_eq_append] +@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by + induction as <;> simp_all + +grind_pattern reverse_append => (as ++ bs).reverse where + as =/= [] + bs =/= [] +grind_pattern reverse_append => bs.reverse ++ as.reverse where + as =/= [] + bs =/= [] + +theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by + rw [reverse_append]; rfl + +grind_pattern reverse_concat => (l ++ [a]).reverse where + l =/= [] +grind_pattern reverse_concat => a :: l.reverse where + l =/= [] + /-! ### flatten -/ diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 247a2374948f..b363d9fc7ec6 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -124,6 +124,20 @@ def filterAuxM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : let b ← f h filterAuxM f t (cond b (h :: acc) acc) +theorem filterAuxM_append_right [Monad m] [LawfulMonad m] {as acc₁ acc₂ : List α} {p : α → m Bool} : + filterAuxM p as (acc₁ ++ acc₂) = (· ++ acc₂) <$> filterAuxM p as acc₁ := by + induction as generalizing acc₁ with + | nil => simp [filterAuxM] + | cons a as ih => + simp only [filterAuxM, map_bind] + congr 1 + ext pa + cases pa <;> simp only [← cons_append, cond_true, cond_false, ih] + +theorem filterAuxM_eq_map [Monad m] [LawfulMonad m] {as acc : List α} {p : α → m Bool} : + filterAuxM p as acc = (· ++ acc) <$> filterAuxM p as [] := by + simpa using filterAuxM_append_right (acc₁ := []) + /-- Applies the monadic predicate `p` to every element in the list, in order from left to right, and returns the list of elements for which `p` returns `true`. @@ -153,6 +167,41 @@ def filterM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as let as ← filterAuxM p as [] pure as.reverse +@[simp] +theorem filterM_nil {m : Type → Type v} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) : + filterM p [] = pure [] := by + simp [filterM, filterAuxM] + +theorem filterM_cons {m : Type → Type v} [Monad m] [LawfulMonad m] {a : α} {as : List α} {p : α → m Bool} : + filterM p (a :: as) = + (do let pa ← p a; let as ← filterM p as; return if pa then a :: as else as) := by + simp only [filterM, filterAuxM, bind_pure_comp, map_bind, Functor.map_map] + congr 1; ext pa + cases pa + · simp + rw [filterAuxM_eq_map] + simp + +theorem filterM_append {m : Type → Type v} [Monad m] [LawfulMonad m] {as bs : List α} {p : α → m Bool} : + filterM p (as ++ bs) = HAppend.hAppend <$> filterM p as <*> filterM p bs := by + induction as with + | nil => + have : HAppend.hAppend ([] : List α) = id := funext List.nil_append + simp [pure_seq, this] + | cons a' as ih => + simp only [cons_append, filterM_cons, ih, bind_pure_comp, map_bind, Functor.map_map, bind_assoc, + bind_map_left, seq_eq_bind_map] + congr; ext pa; congr; ext as'; congr; ext bs' + split <;> simp + +theorem filterM_concat {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} : + filterM p (as ++ [a]) = + (do let as ← filterM p as; let pa ← p a; return if pa then as ++ [a] else as) := by + rw [filterM_append, filterM_cons, filterM_nil, seq_eq_bind_map] + simp only [bind_pure_comp, map_pure, Functor.map_map, bind_map_left] + congr; ext as'; congr; ext pa + split <;> simp + /-- Applies the monadic predicate `p` on every element in the list in reverse order, from right to left, and returns those elements for which `p` returns `true`. The elements of the returned list are in @@ -180,6 +229,31 @@ Checking 1 def filterRevM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α) := filterAuxM p as.reverse [] +theorem filterRevM_eq_reverse_map_filterM_reverse {m : Type → Type v} [Monad m] [LawfulMonad m] {α : Type} (p : α → m Bool) (as : List α): + filterRevM p as = reverse <$> filterM p as.reverse := by + simp [filterRevM, filterM] + +@[simp] +theorem filterRevM_nil {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) : + filterRevM p [] = pure [] := by + simp [filterRevM, filterAuxM] + +@[simp] +theorem filterRevM_concat {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} : + filterRevM p (as ++ [a]) = + (do let pa ← p a; let as ← filterRevM p as; return if pa then as ++ [a] else as) := by + simp only [filterRevM_eq_reverse_map_filterM_reverse, reverse_append, reverse_cons, reverse_nil, + nil_append, cons_append, filterM_cons, bind_pure_comp, map_bind, Functor.map_map] + congr; ext pa; congr; ext as' + split <;> simp + +theorem filterRevM_cons {m : Type → Type v} [Monad m] [LawfulMonad m] {as : List α} {a : α} {p : α → m Bool} : + filterRevM p (a :: as) = + (do let as ← filterRevM p as; let pa ← p a; return if pa then a :: as else as) := by + simp [filterRevM_eq_reverse_map_filterM_reverse, filterM_concat] + congr; ext as'; congr; ext pa + split <;> simp + /-- Applies a monadic function that returns an `Option` to each element of a list, collecting the non-`none` values. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 7735f1c12591..32c7dbe9c78e 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -2414,15 +2414,6 @@ theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) : rw [← getElem?_eq_getElem, ← getElem?_eq_getElem] rw [getElem?_reverse (by simpa using h)] -theorem reverseAux_reverseAux_nil {as bs : List α} : reverseAux (reverseAux as bs) [] = reverseAux bs as := by - induction as generalizing bs with - | nil => rfl - | cons a as ih => simp [reverseAux, ih] - --- The argument `as : List α` is explicit to allow rewriting from right to left. -@[simp, grind =] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by - simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl - theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse := by constructor <;> (rintro rfl; simp) @@ -2476,28 +2467,10 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) : simp only [reverse_cons, filterMap_append, filterMap_cons, ih] split <;> simp_all -@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by - induction as <;> simp_all - -grind_pattern reverse_append => (as ++ bs).reverse where - as =/= [] - bs =/= [] -grind_pattern reverse_append => bs.reverse ++ as.reverse where - as =/= [] - bs =/= [] - @[simp] theorem reverse_eq_append_iff {xs ys zs : List α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by rw [reverse_eq_iff, reverse_append] -theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by - rw [reverse_append]; rfl - -grind_pattern reverse_concat => (l ++ [a]).reverse where - l =/= [] -grind_pattern reverse_concat => a :: l.reverse where - l =/= [] - theorem reverse_eq_concat {xs ys : List α} {a : α} : xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by rw [reverse_eq_iff, reverse_concat]