finish

src/Init/Data/Array/Attach.lean

@@ -555,6 +555,10 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Array.map_push]
 
+@[simp] theorem mem_unattach {p : α → Prop} {xs : Array { x // p x }} {a} :
+    a ∈ xs.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ xs := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem size_unattach {p : α → Prop} {xs : Array { x // p x }} :
     xs.unattach.size = xs.size := by
   unfold unattach
@@ -676,6 +680,20 @@ and simplifies these to the function directly taking the value.
   simp
   rw [List.find?_subtype hf]
 
+@[simp] theorem all_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.all f 0 stop = xs.unattach.all g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.any f 0 stop = xs.unattach.any g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {xs : Array { x // p x }}

src/Init/Data/Array/Lemmas.lean

@@ -3496,6 +3496,239 @@ theorem replace_extract {xs : Array α} {i : Nat} :
 
 end replace
 
+/-! ## Logic -/
+
+/-! ### any / all -/
+
+theorem not_any_eq_all_not (xs : Array α) (p : α → Bool) : (!xs.any p) = xs.all fun a => !p a := by
+  rcases xs with ⟨xs⟩
+  simp [List.not_any_eq_all_not]
+
+theorem not_all_eq_any_not (xs : Array α) (p : α → Bool) : (!xs.all p) = xs.any fun a => !p a := by
+  rcases xs with ⟨xs⟩
+  simp [List.not_all_eq_any_not]
+
+theorem and_any_distrib_left (xs : Array α) (p : α → Bool) (q : Bool) :
+    (q && xs.any p) = xs.any fun a => q && p a := by
+  rcases xs with ⟨xs⟩
+  simp [List.and_any_distrib_left]
+
+theorem and_any_distrib_right (xs : Array α) (p : α → Bool) (q : Bool) :
+    (xs.any p && q) = xs.any fun a => p a && q := by
+  rcases xs with ⟨xs⟩
+  simp [List.and_any_distrib_right]
+
+theorem or_all_distrib_left (xs : Array α) (p : α → Bool) (q : Bool) :
+    (q || xs.all p) = xs.all fun a => q || p a := by
+  rcases xs with ⟨xs⟩
+  simp [List.or_all_distrib_left]
+
+theorem or_all_distrib_right (xs : Array α) (p : α → Bool) (q : Bool) :
+    (xs.all p || q) = xs.all fun a => p a || q := by
+  rcases xs with ⟨xs⟩
+  simp [List.or_all_distrib_right]
+
+theorem any_eq_not_all_not (xs : Array α) (p : α → Bool) : xs.any p = !xs.all (!p .) := by
+  simp only [not_all_eq_any_not, Bool.not_not]
+
+/-- Variant of `any_map` with a side condition for the `stop` argument. -/
+@[simp] theorem any_map' {xs : Array α} {p : β → Bool} (w : stop = xs.size):
+    (xs.map f).any p 0 stop = xs.any (p ∘ f) := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.map_toArray]
+  simp [List.any_map]
+
+/-- Variant of `all_map` with a side condition for the `stop` argument. -/
+@[simp] theorem all_map' {xs : Array α} {p : β → Bool} (w : stop = xs.size):
+    (xs.map f).all p 0 stop = xs.all (p ∘ f) := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.map_toArray]
+  simp [List.all_map]
+
+theorem any_map {xs : Array α} {p : β → Bool} : (xs.map f).any p = xs.any (p ∘ f) := by
+  simp
+
+theorem all_map {xs : Array α} {p : β → Bool} : (xs.map f).all p = xs.all (p ∘ f) := by
+  simp
+
+/-- Variant of `any_filter` with a side condition for the `stop` argument. -/
+@[simp] theorem any_filter' {xs : Array α} {p q : α → Bool} (w : stop = (xs.filter p).size) :
+    (xs.filter p).any q 0 stop = xs.any fun a => p a && q a := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.filter_toArray]
+  simp [List.any_filter]
+
+/-- Variant of `all_filter` with a side condition for the `stop` argument. -/
+@[simp] theorem all_filter' {xs : Array α} {p q : α → Bool} (w : stop = (xs.filter p).size) :
+    (xs.filter p).all q 0 stop = xs.all fun a => p a → q a := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.filter_toArray]
+  simp [List.all_filter]
+
+theorem any_filter {xs : Array α} {p q : α → Bool} :
+    (xs.filter p).any q 0 = xs.any fun a => p a && q a := by
+  simp
+
+theorem all_filter {xs : Array α} {p q : α → Bool} :
+    (xs.filter p).all q 0 = xs.all fun a => p a → q a := by
+  simp
+
+/-- Variant of `any_filterMap` with a side condition for the `stop` argument. -/
+@[simp] theorem any_filterMap' {xs : Array α} {f : α → Option β} {p : β → Bool} (w : stop = (xs.filterMap f).size) :
+    (xs.filterMap f).any p 0 stop = xs.any fun a => match f a with | some b => p b | none => false := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.filterMap_toArray]
+  simp [List.any_filterMap]
+  rfl
+
+/-- Variant of `all_filterMap` with a side condition for the `stop` argument. -/
+@[simp] theorem all_filterMap' {xs : Array α} {f : α → Option β} {p : β → Bool} (w : stop = (xs.filterMap f).size) :
+    (xs.filterMap f).all p 0 stop = xs.all fun a => match f a with | some b => p b | none => true := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.filterMap_toArray]
+  simp [List.all_filterMap]
+  rfl
+
+theorem any_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
+    (xs.filterMap f).any p 0 = xs.any fun a => match f a with | some b => p b | none => false := by
+  simp
+
+theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
+    (xs.filterMap f).all p 0 = xs.all fun a => match f a with | some b => p b | none => true := by
+  simp
+
+/-- Variant of `any_append` with a side condition for the `stop` argument. -/
+@[simp] theorem any_append' {xs ys : Array α} (w : stop = (xs ++ ys).size) :
+    (xs ++ ys).any f 0 stop = (xs.any f || ys.any f) := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  rw [List.append_toArray]
+  simp [List.any_append]
+
+/-- Variant of `all_append` with a side condition for the `stop` argument. -/
+@[simp] theorem all_append' {xs ys : Array α} (w : stop = (xs ++ ys).size) :
+    (xs ++ ys).all f 0 stop = (xs.all f && ys.all f) := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  rw [List.append_toArray]
+  simp [List.all_append]
+
+theorem any_append {xs ys : Array α} :
+    (xs ++ ys).any f 0 = (xs.any f || ys.any f) := by
+  simp
+
+theorem all_append {xs ys : Array α} :
+    (xs ++ ys).all f 0 = (xs.all f && ys.all f) := by
+  simp
+
+@[congr] theorem anyM_congr [Monad m]
+    {xs ys : Array α} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) :
+    xs.anyM p start₁ stop₁ = ys.anyM q start₂ stop₂ := by
+  have : p = q := by funext a; apply h
+  subst this
+  subst w
+  subst wstart
+  subst wstop
+  rfl
+
+@[congr] theorem any_congr
+    {xs ys : Array α} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) :
+    xs.any p start₁ stop₁ = ys.any q start₂ stop₂ := by
+  unfold any
+  apply anyM_congr w h wstart wstop
+
+@[congr] theorem allM_congr [Monad m]
+    {xs ys : Array α} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) :
+    xs.allM p start₁ stop₁ = ys.allM q start₂ stop₂ := by
+  have : p = q := by funext a; apply h
+  subst this
+  subst w
+  subst wstart
+  subst wstop
+  rfl
+
+@[congr] theorem all_congr
+    {xs ys : Array α} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) :
+    xs.all p start₁ stop₁ = ys.all q start₂ stop₂ := by
+  unfold all
+  apply allM_congr w h wstart wstop
+
+@[simp] theorem any_flatten' {xss : Array (Array α)} (w : stop = xss.flatten.size) : xss.flatten.any f 0 stop = xss.any (any · f) := by
+  subst w
+  cases xss using array₂_induction
+  simp [Function.comp_def]
+
+@[simp] theorem all_flatten' {xss : Array (Array α)} (w : stop = xss.flatten.size) : xss.flatten.all f 0 stop = xss.all (all · f) := by
+  subst w
+  cases xss using array₂_induction
+  simp [Function.comp_def]
+
+theorem any_flatten {xss : Array (Array α)} : xss.flatten.any f = xss.any (any · f) := by
+  simp
+
+theorem all_flatten {xss : Array (Array α)} : xss.flatten.all f = xss.all (all · f) := by
+  simp
+
+/-- Variant of `any_flatMap` with a side condition for the `stop` argument. -/
+@[simp] theorem any_flatMap' {xs : Array α} {f : α → Array β} {p : β → Bool} (w : stop = (xs.flatMap f).size) :
+    (xs.flatMap f).any p 0 stop = xs.any fun a => (f a).any p := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.flatMap_toArray]
+  simp [List.any_flatMap]
+
+/-- Variant of `all_flatMap` with a side condition for the `stop` argument. -/
+@[simp] theorem all_flatMap' {xs : Array α} {f : α → Array β} {p : β → Bool} (w : stop = (xs.flatMap f).size) :
+    (xs.flatMap f).all p 0 stop = xs.all fun a => (f a).all p := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.flatMap_toArray]
+  simp [List.all_flatMap]
+
+theorem any_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
+    (xs.flatMap f).any p 0 = xs.any fun a => (f a).any p := by
+  simp
+
+theorem all_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
+    (xs.flatMap f).all p 0 = xs.all fun a => (f a).all p := by
+  simp
+
+/-- Variant of `any_reverse` with a side condition for the `stop` argument. -/
+@[simp] theorem any_reverse' {xs : Array α} (w : stop = xs.size) : xs.reverse.any f 0 stop = xs.any f := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.reverse_toArray]
+  simp [List.any_reverse]
+
+/-- Variant of `all_reverse` with a side condition for the `stop` argument. -/
+@[simp] theorem all_reverse' {xs : Array α} (w : stop = xs.size) : xs.reverse.all f 0 stop = xs.all f := by
+  subst w
+  rcases xs with ⟨xs⟩
+  rw [List.reverse_toArray]
+  simp [List.all_reverse]
+
+theorem any_reverse {xs : Array α} : xs.reverse.any f 0 = xs.any f := by
+  simp
+
+theorem all_reverse {xs : Array α} : xs.reverse.all f 0 = xs.all f := by
+  simp
+
+@[simp] theorem any_mkArray {n : Nat} {a : α} :
+    (mkArray n a).any f = if n = 0 then false else f a := by
+  induction n <;> simp_all [mkArray_succ']
+
+@[simp] theorem all_mkArray {n : Nat} {a : α} :
+    (mkArray n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [mkArray_succ']
+
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/

src/Init/Data/List/Attach.lean

@@ -662,6 +662,10 @@ def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) : List α :
 @[simp] theorem unattach_cons {p : α → Prop} {a : { x // p x }} {l : List { x // p x }} :
   (a :: l).unattach = a.val :: l.unattach := rfl
 
+@[simp] theorem mem_unattach {p : α → Prop} {l : List { x // p x }} {a} :
+    a ∈ l.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ l := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem length_unattach {p : α → Prop} {l : List { x // p x }} :
     l.unattach.length = l.length := by
   unfold unattach
@@ -766,6 +770,16 @@ and simplifies these to the function directly taking the value.
     simp [hf, find?_cons]
     split <;> simp [ih]
 
+@[simp] theorem all_subtype {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.all f = l.unattach.all g := by
+  simp [all_eq, hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.any f = l.unattach.any g := by
+  simp [any_eq, hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}

src/Init/Data/Vector/Attach.lean

@@ -473,6 +473,10 @@ def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vect
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Vector.map_push]
 
+@[simp] theorem mem_unattach {p : α → Prop} {xs : Vector { x // p x } n} {a} :
+    a ∈ xs.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ xs := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem unattach_mk {p : α → Prop} {xs : Array { x // p x }} {h : xs.size = n} :
     (mk xs h).unattach = mk xs.unattach (by simpa using h) := by
   simp [unattach]
@@ -552,6 +556,18 @@ and simplifies these to the function directly taking the value.
   simp
   rw [Array.find?_subtype hf]
 
+@[simp] theorem all_subtype {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    xs.all f = xs.unattach.all g := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    xs.any f = xs.unattach.any g := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_reverse {p : α → Prop} {xs : Vector { x // p x } n} :

src/Init/Data/Vector/Lemmas.lean

@@ -2585,6 +2585,161 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
 
 end replace
 
+/-! ## Logic -/
+
+/-! ### any / all -/
+
+theorem not_any_eq_all_not (xs : Vector α n) (p : α → Bool) : (!xs.any p) = xs.all fun a => !p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.not_any_eq_all_not]
+
+theorem not_all_eq_any_not (xs : Vector α n) (p : α → Bool) : (!xs.all p) = xs.any fun a => !p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.not_all_eq_any_not]
+
+theorem and_any_distrib_left (xs : Vector α n) (p : α → Bool) (q : Bool) :
+    (q && xs.any p) = xs.any fun a => q && p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.and_any_distrib_left]
+
+theorem and_any_distrib_right (xs : Vector α n) (p : α → Bool) (q : Bool) :
+    (xs.any p && q) = xs.any fun a => p a && q := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.and_any_distrib_right]
+
+theorem or_all_distrib_left (xs : Vector α n) (p : α → Bool) (q : Bool) :
+    (q || xs.all p) = xs.all fun a => q || p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.or_all_distrib_left]
+
+theorem or_all_distrib_right (xs : Vector α n) (p : α → Bool) (q : Bool) :
+    (xs.all p || q) = xs.all fun a => p a || q := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.or_all_distrib_right]
+
+theorem any_eq_not_all_not (xs : Vector α n) (p : α → Bool) : xs.any p = !xs.all (!p .) := by
+  simp only [not_all_eq_any_not, Bool.not_not]
+
+@[simp] theorem any_map {xs : Vector α n} {p : β → Bool} : (xs.map f).any p = xs.any (p ∘ f) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem all_map {xs : Vector α n} {p : β → Bool} : (xs.map f).all p = xs.all (p ∘ f) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem any_filter {xs : Vector α n} {p q : α → Bool} :
+    (xs.filter p).any q = xs.any fun a => p a && q a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem all_filter {xs : Vector α n} {p q : α → Bool} :
+    (xs.filter p).all q = xs.all fun a => p a → q a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem any_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
+    (xs.filterMap f).any p = xs.any fun a => match f a with | some b => p b | none => false := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+  rfl
+
+@[simp] theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
+    (xs.filterMap f).all p = xs.all fun a => match f a with | some b => p b | none => true := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+  rfl
+
+@[simp] theorem any_append {xs : Vector α n} {ys : Vector α m} :
+    (xs ++ ys).any f = (xs.any f || ys.any f) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp
+
+@[simp] theorem all_append {xs : Vector α n} {ys : Vector α m} :
+    (xs ++ ys).all f = (xs.all f && ys.all f) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp
+
+@[congr] theorem anyM_congr [Monad m]
+    {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) :
+    xs.anyM p = ys.anyM q := by
+  have : p = q := by funext a; apply h
+  subst this
+  subst w
+  rfl
+
+@[congr] theorem any_congr
+    {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) :
+    xs.any p = ys.any q := by
+  unfold any
+  apply anyM_congr w h
+
+@[congr] theorem allM_congr [Monad m]
+    {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) :
+    xs.allM p = ys.allM q := by
+  have : p = q := by funext a; apply h
+  subst this
+  subst w
+  rfl
+
+@[congr] theorem all_congr
+    {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) :
+    xs.all p = ys.all q := by
+  unfold all
+  apply allM_congr w h
+
+@[simp] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
+  cases xss using vector₂_induction
+  simp
+
+@[simp] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
+  cases xss using vector₂_induction
+  simp
+
+@[simp] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+    (xs.flatMap f).any p = xs.any fun a => (f a).any p := by
+  rcases xs with ⟨xs⟩
+  simp only [flatMap_mk, any_mk, Array.size_flatMap, size_toArray, Array.any_flatMap']
+  congr
+  funext
+  congr
+  simp [Vector.size_toArray]
+
+@[simp] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+    (xs.flatMap f).all p = xs.all fun a => (f a).all p := by
+  rcases xs with ⟨xs⟩
+  simp only [flatMap_mk, all_mk, Array.size_flatMap, size_toArray, Array.all_flatMap']
+  congr
+  funext
+  congr
+  simp [Vector.size_toArray]
+
+@[simp] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem any_cast {xs : Vector α n} : (xs.cast h).any f = xs.any f := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem all_cast {xs : Vector α n} : (xs.cast h).all f = xs.all f := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
+@[simp] theorem any_mkVector {n : Nat} {a : α} :
+    (mkVector n a).any f = if n = 0 then false else f a := by
+  induction n <;> simp_all [mkVector_succ']
+
+@[simp] theorem all_mkVector {n : Nat} {a : α} :
+    (mkVector n a).all f = if n = 0 then true else f a := by
+  induction n <;> simp_all +contextual [mkVector_succ']
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in