feat: relate Nat.fold/foldRev/any/all to List.finRange (#6235)

This PR relates that operations `Nat.fold`/`foldRev`/`any`/`all` to the
corresponding List operations over `List.finRange`.

src/Init/Data/List/Lemmas.lean

@@ -3357,10 +3357,10 @@ theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!
 theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .) := by
   simp only [not_any_eq_all_not, Bool.not_not]
 
-@[simp] theorem any_map {l : List α} {p : α → Bool} : (l.map f).any p = l.any (p ∘ f) := by
+@[simp] theorem any_map {l : List α} {p : β → Bool} : (l.map f).any p = l.any (p ∘ f) := by
   induction l with simp | cons _ _ ih => rw [ih]
 
-@[simp] theorem all_map {l : List α} {p : α → Bool} : (l.map f).all p = l.all (p ∘ f) := by
+@[simp] theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f) := by
   induction l with simp | cons _ _ ih => rw [ih]
 
 @[simp] theorem any_filter {l : List α} {p q : α → Bool} :

src/Init/Data/Nat/Fold.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Kim Morrison
 -/
 prelude
 import Init.Omega
+import Init.Data.List.FinRange
 
 set_option linter.missingDocs true -- keep it documented
 universe u
@@ -137,6 +138,54 @@ theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bo
       omega
   go n 0 f
 
+@[simp] theorem fold_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
+    fold 0 f init = init := by simp [fold]
+
+@[simp] theorem fold_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1 → α → α) (init : α) :
+    fold (n + 1) f init = f n (by omega) (fold n (fun i h => f i (by omega)) init) := by simp [fold]
+
+theorem fold_eq_finRange_foldl {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
+    fold n f init = (List.finRange n).foldl (fun acc ⟨i, h⟩ => f i h acc) init := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    simp [ih, List.finRange_succ_last, List.foldl_map]
+
+@[simp] theorem foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
+    foldRev 0 f init = init := by simp [foldRev]
+
+@[simp] theorem foldRev_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1 → α → α) (init : α) :
+    foldRev (n + 1) f init = foldRev n (fun i h => f i (by omega)) (f n (by omega) init) := by
+  simp [foldRev]
+
+theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
+    foldRev n f init = (List.finRange n).foldr (fun ⟨i, h⟩ acc => f i h acc) init := by
+  induction n generalizing init with
+  | zero => simp
+  | succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]
+
+@[simp] theorem any_zero {f : (i : Nat) → i < 0 → Bool} : any 0 f = false := by simp [any]
+
+@[simp] theorem any_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
+  any (n + 1) f = (any n (fun i h => f i (by omega)) || f n (by omega)) := by simp [any]
+
+theorem any_eq_finRange_any {n : Nat} (f : (i : Nat) → i < n → Bool) :
+    any n f = (List.finRange n).any (fun ⟨i, h⟩ => f i h) := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [ih, List.finRange_succ_last, List.any_map, Function.comp_def]
+
+@[simp] theorem all_zero {f : (i : Nat) → i < 0 → Bool} : all 0 f = true := by simp [all]
+
+@[simp] theorem all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
+  all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega)) := by simp [all]
+
+theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
+    all n f = (List.finRange n).all (fun ⟨i, h⟩ => f i h) := by
+  induction n with
+  | zero => simp
+  | succ n ih => simp [ih, List.finRange_succ_last, List.all_map, Function.comp_def]
+
 end Nat
 
 namespace Prod