From fd4469907923f66ce9e6bca002bffa6eed9bd59c 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 | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Batteries/Data/DArray/Lemmas.lean b/Batteries/Data/DArray/Lemmas.lean index bea7603e67..9df9ed2853 100644 --- a/Batteries/Data/DArray/Lemmas.lean +++ b/Batteries/Data/DArray/Lemmas.lean @@ -73,3 +73,14 @@ theorem umodify_eq_modify (a : DArray n α) (i : USize) (h : i.toNat < n) @[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]