Skip to content

Commit

Permalink
fix: use auto-implicit
Browse files Browse the repository at this point in the history
  • Loading branch information
@fgdorais
fgdorais committed Dec 3, 2024
1 parent 5339692 commit 5c0e5be
Showing 1 changed file with 28 additions and 36 deletions.
64 changes: 28 additions & 36 deletions Batteries/Data/Fin/Fold.lean
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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 =
Expand All @@ -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]
Expand All @@ -58,20 +57,20 @@ 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 =
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] {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 =
Expand All @@ -85,42 +84,38 @@ 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]
| succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih]

/-! ### 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
Expand All @@ -132,21 +127,19 @@ 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]
induction n with
| 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]
Expand All @@ -156,20 +149,20 @@ 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 =
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 {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 =
Expand All @@ -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]
Expand Down

0 comments on commit 5c0e5be

Please sign in to comment.