From 133191e2887554432ae34b6711ed27dfd8d64ee7 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 29 Sep 2025 13:32:30 -0400 Subject: [PATCH 1/3] feat: add `Fin.any` and `Fin.all` --- Batteries/Data/Fin/Basic.lean | 14 ++++++++++++++ Batteries/Data/Fin/Lemmas.lean | 19 +++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 2d6058a6ce..73157cabf8 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -96,3 +96,17 @@ 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 diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index a0e1ae9a98..6ef169efef 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -139,6 +139,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?] @@ -191,3 +192,21 @@ theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] : (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by 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 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 + +-- 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) From 48005a657ec14a663a7ddaa993f459fe30defab6 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 30 Sep 2025 07:47:23 -0400 Subject: [PATCH 2/3] feat: tie `Fin.all`/`Fin.any` with `List.all`/`List.any` --- Batteries/Data/Fin/Lemmas.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 6ef169efef..aceba371e2 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -199,10 +199,19 @@ theorem any_eq_true_iff {p : Fin n → Bool} : Fin.any p = true ↔ ∃ i, p i = theorem any_eq_false_iff {p : Fin n → Bool} : Fin.any p = false ↔ ∀ i, p i = false := by simp +theorem any_eq_all_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) From 6ce32409e42491c7e3131264fdc07f8a4acf6e6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Sun, 5 Oct 2025 13:48:04 -0400 Subject: [PATCH 3/3] fix: typo --- Batteries/Data/Fin/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index aceba371e2..4ed20ad199 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -199,7 +199,7 @@ theorem any_eq_true_iff {p : Fin n → Bool} : Fin.any p = true ↔ ∃ i, p i = theorem any_eq_false_iff {p : Fin n → Bool} : Fin.any p = false ↔ ∀ i, p i = false := by simp -theorem any_eq_all_finRange {p : Fin n → Bool} : Fin.any p = (List.finRange n).any p := by +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]