From d87b4cd773ee619e11e00abb54880c8b2345cf91 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 29 May 2024 21:44:40 -0400 Subject: [PATCH] feat: more lemmas --- Batteries/Data/DArray/Lemmas.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Batteries/Data/DArray/Lemmas.lean b/Batteries/Data/DArray/Lemmas.lean index bea7603e67..551c7d17ab 100644 --- a/Batteries/Data/DArray/Lemmas.lean +++ b/Batteries/Data/DArray/Lemmas.lean @@ -71,5 +71,28 @@ theorem umodifyF_eq_modifyF [Functor f] (a : DArray n α) (i : USize) (h : i.toN theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n) (t : α ⟨i.toNat, h⟩ → α ⟨i.toNat, h⟩) : a.umodify i h t = a.modify ⟨i.toNat, h⟩ t := rfl +theorem foldlM_eq_fin_foldlM [Monad m] (a : DArray n α) (f : β → {i : Fin n} → α i → m β) (init) : + a.foldlM f init = Fin.foldlM n (f · <| a.get ·) init := rfl + +theorem foldl_eq_foldlM (a : DArray n α) (f : β → {i : Fin n} → α i → β) (init) : + a.foldl f init = a.foldlM (m:=Id) f init := rfl + +theorem foldrM_eq_fin_foldrM [Monad m] (a : DArray n α) (f : {i : Fin n} → α i → β → m β) (init) : + a.foldrM f init = Fin.foldrM n (f <| a.get ·) init := rfl + +theorem foldr_eq_foldrM (a : DArray n α) (f : {i : Fin n} → α i → β → β) (init) : + a.foldr f init = a.foldrM (m:=Id) f init := rfl + @[simp] theorem copy_eq (a : DArray n α) : a.copy = a := rfl + +theorem get_map {β : Fin n → Type _} (f : {i : Fin n} → α i → β i) (a : DArray n α) (i : Fin n) : + (a.map f).get i = f (a.get i) := rfl + +@[simp] +theorem size_amap (f : {i : Fin n} → α i → β) (a : DArray n α) : + (a.amap f).size = n := Array.size_ofFn .. + +theorem getElem_amap (f : {i : Fin n} → α i → β) (a : DArray n α) (i : Fin n) + (h : i.val < (a.amap f).size := (a.size_amap f).symm ▸ i.is_lt) : + (a.amap f)[i] = f (a.get i) := by simp [amap]