From 45c0a2fa40736902e6daa61af716abc303cd2dbc Mon Sep 17 00:00:00 2001 From: L Date: Wed, 5 Jun 2024 14:07:28 -0700 Subject: [PATCH] feat: add lemma `Fin.list_reverse` (#819) --- Batteries/Data/Fin/Lemmas.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 2cd8effde9..c11054ce58 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -36,6 +36,22 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x = theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by apply List.ext_get; simp; intro i; cases i <;> simp +theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by + rw [list_succ] + induction n with + | zero => rfl + | succ n ih => + rw [list_succ, List.map_cons castSucc, ih] + simp [Function.comp_def, succ_castSucc] + +theorem list_reverse (n) : (list n).reverse = (list n).map rev := by + induction n with + | zero => rfl + | succ n ih => + conv => lhs; rw [list_succ_last] + conv => rhs; rw [list_succ] + simp [List.reverse_map, ih, Function.comp_def, rev_succ] + /-! ### foldl -/ theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : m < n) :