From 67b3afd21fef08a8c4d88535265d2efd89a93708 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 3 Dec 2024 13:16:56 -0500 Subject: [PATCH] fix: style --- Batteries/Data/Fin/Fold.lean | 138 ++++++++++++++--------------------- 1 file changed, 53 insertions(+), 85 deletions(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 7514f13690..c55ca5e87c 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -10,28 +10,21 @@ namespace Fin /-! ### dfoldlM -/ -theorem dfoldlM_loop_lt [Monad m] - (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) - (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = - (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by +theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) : + dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = + (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by rw [dfoldlM.loop, dif_pos h] -theorem dfoldlM_loop_eq [Monad m] - (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x : α ⟨n, Nat.le_refl _⟩) : - dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by +theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) : + dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldlM_zero [Monad m] - (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : - dfoldlM 0 α f x = pure x := - dfoldlM_loop_eq .. +@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM 0 α f x = pure x := dfoldlM_loop_eq .. -theorem dfoldlM_loop [Monad m] - (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) - (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by +theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1) + (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by if h' : i < n then rw [dfoldlM_loop_lt _ h _] congr; funext @@ -42,9 +35,8 @@ theorem dfoldlM_loop [Monad m] congr; funext rw [dfoldlM_loop_eq, dfoldlM_loop_eq] -theorem dfoldlM_succ [Monad m] - (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x : α 0) : - dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := +theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := dfoldlM_loop .. theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : @@ -57,24 +49,19 @@ theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : /-! ### dfoldrM -/ -theorem dfoldrM_loop_zero [Monad m] - (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α 0) : - dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by +theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) : + dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldrM_loop_succ [Monad m] - (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : - dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = - f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by +theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) + (x) : dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = + f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by rw [dfoldrM.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, castSucc_mk, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldrM_loop [Monad m] [LawfulMonad m] - (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (h : i+1 ≤ n+1) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : - dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = - dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by +theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) + (h : i+1 ≤ n+1) (x) : dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = + dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by induction i with | zero => rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind] @@ -84,41 +71,35 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] congr; funext; exact ih .. -@[simp] theorem dfoldrM_zero [Monad m] - (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α 0) : - dfoldrM 0 α f x = pure x := - dfoldrM_loop_zero .. +@[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x) : + dfoldrM 0 α f x = pure x := dfoldrM_loop_zero .. -theorem dfoldrM_succ [Monad m] [LawfulMonad m] - (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (x : α (last (n+1))) : - dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := - dfoldrM_loop .. +theorem dfoldrM_succ [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) + (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldrM_loop .. -theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] - (f : (i : Fin n) → α → m α) (x : α) : dfoldrM n (fun _ => α) f x = foldrM n f x := by +theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x : α) : + dfoldrM n (fun _ => α) f x = foldrM n f x := by induction n generalizing x with | zero => simp only [dfoldrM_zero, foldrM_zero] | succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih] /-! ### dfoldl -/ -theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = - dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by +theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x) : + dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by rw [dfoldl.loop, dif_pos h] -theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : - dfoldl.loop n α f n (Nat.le_refl _) x = x := by +theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x) : + dfoldl.loop n α f n (Nat.le_refl _) x = x := by rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) - (x : α 0) : dfoldl 0 α f x = x := - dfoldl_loop_eq .. +@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x) : + dfoldl 0 α f x = x := dfoldl_loop_eq .. -theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) - (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by +theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) (x) : + dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by if h' : i < n then rw [dfoldl_loop_lt _ h _] rw [dfoldl_loop_lt _ h' _, dfoldl_loop]; rfl @@ -127,13 +108,11 @@ theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i rw [dfoldl_loop_lt] rw [dfoldl_loop_eq, dfoldl_loop_eq] -theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : - dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := - dfoldl_loop .. +theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) : + dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := dfoldl_loop .. -theorem dfoldl_succ_last - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : - dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by +theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) : + dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by rw [dfoldl_succ] induction n with | zero => simp [dfoldl_succ, last] @@ -149,22 +128,17 @@ theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : /-! ### dfoldr -/ -theorem dfoldr_loop_zero - (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α 0) : - dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by +theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : + dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldr_loop_succ - (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : +theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) : dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := by rw [dfoldr.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldr_loop - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : +theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) : dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by induction i with @@ -172,29 +146,23 @@ theorem dfoldr_loop | succ i ih => rw [dfoldr_loop_succ _ h, dfoldr_loop_succ _ (Nat.succ_lt_succ_iff.mp h), ih (Nat.le_of_succ_le h)]; rfl -@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) - (x : α 0) : dfoldr 0 α f x = x := - dfoldr_loop_zero .. +@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) : + dfoldr 0 α f x = x := dfoldr_loop_zero .. -theorem dfoldr_succ - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : - dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := - dfoldr_loop .. +theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : + dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop .. -theorem dfoldr_succ_last - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : - dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by +theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : + dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by induction n with | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr -theorem dfoldr_eq_dfoldrM - (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : - dfoldr n α f x = dfoldrM (m:=Id) n α f x := by +theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : + dfoldr n α f x = dfoldrM (m:=Id) n α f x := by induction n <;> simp [dfoldr_succ, dfoldrM_succ, *] -theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : - dfoldr n (fun _ => α) f x = foldr n f x := by +theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by induction n with | zero => simp only [dfoldr_zero, foldr_zero] | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih]