From 5c0e5befa438aa8d9698da560999932b4f373ecf Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 2 Dec 2024 21:33:15 -0500 Subject: [PATCH] fix: use auto-implicit --- Batteries/Data/Fin/Fold.lean | 64 ++++++++++++++++-------------------- 1 file changed, 28 insertions(+), 36 deletions(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index a7923ca34f..7514f13690 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 François G. Dorais. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: François G. Dorais +Authors: François G. Dorais, Quang Dao -/ import Batteries.Data.List.FinRange import Batteries.Data.Fin.Basic @@ -10,24 +10,24 @@ namespace Fin /-! ### dfoldlM -/ -theorem dfoldlM_loop_lt [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +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 rw [dfoldlM.loop, dif_pos h] -theorem dfoldlM_loop_eq [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +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 rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldlM_zero [Monad m] {α : Fin 1 → Type _} +@[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 .. -theorem dfoldlM_loop [Monad m] {n : Nat} {α : Fin (n+2) → Type _} +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 = @@ -42,13 +42,12 @@ theorem dfoldlM_loop [Monad m] {n : Nat} {α : Fin (n+2) → Type _} congr; funext rw [dfoldlM_loop_eq, dfoldlM_loop_eq] -theorem dfoldlM_succ [Monad m] {n : Nat} {α : Fin (n+2) → Type _} +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 ·) .) := dfoldlM_loop .. -/-- Dependent version `dfoldlM` equals non-dependent version `foldlM` -/ -theorem dfoldlM_eq_foldlM [Monad m] {n : Nat} {α : Type _} (f : (i : Fin n) → α → m α) (x : α) : +theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by induction n generalizing x with | zero => simp only [dfoldlM_zero, foldlM_zero] @@ -58,12 +57,12 @@ theorem dfoldlM_eq_foldlM [Monad m] {n : Nat} {α : Type _} (f : (i : Fin n) → /-! ### dfoldrM -/ -theorem dfoldrM_loop_zero [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +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 rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldrM_loop_succ [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +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 = @@ -71,7 +70,7 @@ theorem dfoldrM_loop_succ [Monad m] {n : Nat} {α : Fin (n+1) → Type _} 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] {n : Nat} {α : Fin (n+2) → Type _} +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 = @@ -85,18 +84,17 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Typ 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] {α : Fin 1 → Type _} +@[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 .. -theorem dfoldrM_succ [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Type _} +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 .. -/-- Dependent version `dfoldrM` equals non-dependent version `foldrM` -/ -theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] {n : Nat} {α : Type _} +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] @@ -104,23 +102,20 @@ theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] {n : Nat} {α : Type _} /-! ### dfoldl -/ -theorem dfoldl_loop_lt {n : Nat} {α : Fin (n+1) → Sort _} - (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : +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 rw [dfoldl.loop, dif_pos h] -theorem dfoldl_loop_eq {n : Nat} {α : Fin (n+1) → Sort _} - (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : +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 rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldl_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → α i.succ) +@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x : α 0) : dfoldl 0 α f x = x := dfoldl_loop_eq .. -theorem dfoldl_loop {n : Nat} {α : Fin (n+2) → Sort _} - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) +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 @@ -132,12 +127,11 @@ theorem dfoldl_loop {n : Nat} {α : Fin (n+2) → Sort _} rw [dfoldl_loop_lt] rw [dfoldl_loop_eq, dfoldl_loop_eq] -theorem dfoldl_succ {n : Nat} {α : Fin (n+2) → Sort _} - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : +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_last {n : Nat} {α : Fin (n+2) → Sort _} +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 rw [dfoldl_succ] @@ -145,8 +139,7 @@ theorem dfoldl_succ_last {n : Nat} {α : Fin (n+2) → Sort _} | zero => simp [dfoldl_succ, last] | succ n ih => rw [dfoldl_succ, @ih (α ∘ succ) (f ·.succ ·), dfoldl_succ]; congr -/-- Dependent version `dfoldl` equals non-dependent version `foldl` -/ -theorem dfoldl_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : +theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x := by induction n generalizing x with | zero => simp only [dfoldl_zero, foldl_zero] @@ -156,12 +149,12 @@ theorem dfoldl_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : /-! ### dfoldr -/ -theorem dfoldr_loop_zero {n : Nat} {α : Fin (n+1) → Sort _} +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 rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldr_loop_succ {n : Nat} {α : Fin (n+1) → Sort _} +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⟩) : dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -169,7 +162,7 @@ theorem dfoldr_loop_succ {n : Nat} {α : Fin (n+1) → Sort _} 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 {n : Nat} {α : Fin (n+2) → Sort _} +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⟩) : dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -179,29 +172,28 @@ theorem dfoldr_loop {n : Nat} {α : Fin (n+2) → Sort _} | 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 {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.succ → α i.castSucc) +@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x : α 0) : dfoldr 0 α f x = x := dfoldr_loop_zero .. -theorem dfoldr_succ {n : Nat} {α : Fin (n+2) → Sort _} +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 {n : Nat} {α : Fin (n+2) → Sort _} +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 {n : Nat} {α : Fin (n+1) → Type _} +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, *] -/-- Dependent version `dfoldr` equals non-dependent version `foldr` -/ -theorem dfoldr_eq_foldr {n : Nat} {α : Sort _} (f : Fin n → α → α) (x : α) : +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]