feat: add Fin.any and Fin.all

Batteries/Data/Fin/Basic.lean

@@ -98,6 +98,20 @@ The function `p` is not evaluated on further inputs after the first `i` is found
 @[inline] def find? (p : Fin n → Bool) : Option (Fin n) :=
   findSome? <| Option.guard fun i => p i
 
+/--
+Returns true if `p i` is true for some `i`.
+
+Short-circuits upon encountering the first true.
+-/
+protected abbrev any (p : Fin n → Bool) := find? p |>.isSome
+
+/--
+Returns true if `p i` is true for every `i`.
+
+Short-circuits upon encountering the first false.
+-/
+protected abbrev all (p : Fin n → Bool) := find? (! p ·) |>.isNone
+
 /-- Compute `i / n`, where `n` is a `Nat` and inferred the type of `i`. -/
 def divNat (i : Fin (m * n)) : Fin m :=
   ⟨i / n, Nat.div_lt_of_lt_mul <| Nat.mul_comm m n ▸ i.is_lt⟩

Batteries/Data/Fin/Lemmas.lean

@@ -150,6 +150,7 @@ theorem find?_succ {p : Fin (n+1) → Bool} :
 theorem find?_eq_some_iff {p : Fin n → Bool} :
     find? p = some i ↔ p i ∧ ∀ j, j < i → p j = false := by simp [find?, and_assoc]
 
+@[simp]
 theorem isSome_find?_iff {p : Fin n → Bool} :
     (find? p).isSome ↔ ∃ i, p i := by simp [find?]
 
@@ -203,6 +204,33 @@ theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] :
   simpa only [decide_eq_true_iff, decide_eq_false_iff_not] using
     exists_eq_true_iff_exists_minimal_eq_true (p ·)
 
+/-! ### any/all -/
+
+theorem any_eq_true_iff {p : Fin n → Bool} : Fin.any p = true ↔ ∃ i, p i = true := by simp
+
+theorem any_eq_false_iff {p : Fin n → Bool} : Fin.any p = false ↔ ∀ i, p i = false := by simp
+
+theorem any_eq_any_finRange {p : Fin n → Bool} : Fin.any p = (List.finRange n).any p := by
+  rw [Bool.eq_iff_iff]
+  simp only [Fin.any, find?_eq_find?_finRange, List.find?_isSome, List.any_eq, decide_eq_true_eq]
+
+theorem all_eq_true_iff {p : Fin n → Bool} : Fin.all p = true ↔ ∀ i, p i = true := by simp
+
+theorem all_eq_false_iff {p : Fin n → Bool} : Fin.all p = false ↔ ∃ i, p i = false := by simp
+
+theorem all_eq_all_finRange {p : Fin n → Bool} : Fin.all p = (List.finRange n).all p := by
+  rw [Bool.eq_iff_iff]
+  simp only [Fin.all, find?_eq_find?_finRange, Option.isNone_iff_eq_none, List.find?_eq_none,
+    Bool.not_eq_eq_eq_not, Bool.not_true, Bool.not_eq_false, List.all_eq, decide_eq_true_eq]
+
+-- The instance in Lean is not tail recursive and leads to stack overflow.
+instance (p : Fin n → Prop) [DecidablePred p] : Decidable (∃ i, p i) :=
+  decidable_of_iff (Fin.any (p ·) = true) (by simp)
+
+-- The instance in Lean is not tail recursive and leads to stack overflow.
+instance (p : Fin n → Prop) [DecidablePred p] : Decidable (∀ i, p i) :=
+  decidable_of_iff (Fin.all (p ·) = true) (by simp)
+
 /-! ### divNat / modNat / mkDivMod -/
 
 @[simp] theorem coe_divNat (i : Fin (m * n)) : (i.divNat : Nat) = i / n := rfl