From 71bf28895f20cab67354b414eadd645163983763 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 27 Dec 2023 19:55:58 +0000 Subject: [PATCH] feat: add lemmas about `Fin.rev` (#8814) Co-authored-by: Yury G. Kudryashov Co-authored-by: Siddharth Bhat Co-authored-by: Tobias Grosser --- Mathlib/Data/Fin/Basic.lean | 14 ++++++ Mathlib/Data/Fin/Tuple/Basic.lean | 81 +++++++++++++++++++++++++++---- 2 files changed, 86 insertions(+), 9 deletions(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index a1d02bc80f803..c7f05f6268a35 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -347,6 +347,8 @@ theorem pos_iff_ne_zero' [NeZero n] (a : Fin n) : 0 < a ↔ a ≠ 0 := by #align fin.eq_zero_or_eq_succ Fin.eq_zero_or_eq_succ #align fin.eq_succ_of_ne_zero Fin.eq_succ_of_ne_zero +@[simp] lemma cast_eq_self (a : Fin n) : cast rfl a = a := rfl + theorem rev_involutive : Involutive (rev : Fin n → Fin n) := fun i => ext <| by dsimp only [rev] @@ -403,6 +405,10 @@ theorem revOrderIso_symm_apply (i : Fin n) : revOrderIso.symm i = OrderDual.toDu rfl #align fin.rev_order_iso_symm_apply Fin.revOrderIso_symm_apply +theorem cast_rev (i : Fin n) (h : n = m) : + cast h i.rev = (i.cast h).rev := by + subst h; simp + #align fin.last Fin.last #align fin.coe_last Fin.val_last @@ -1571,6 +1577,14 @@ theorem one_succAbove_one {n : ℕ} : (1 : Fin (n + 3)).succAbove 1 = 2 := by exact this #align fin.one_succ_above_one Fin.one_succAbove_one +lemma rev_succAbove (p : Fin (n + 1)) (i : Fin n) : + rev (succAbove p i) = succAbove (rev p) (rev i) := by + cases' lt_or_le (castSucc i) p with h h + · rw [succAbove_below _ _ h, rev_castSucc, succAbove_above] + rwa [← rev_succ, rev_le_rev] + · rw [succAbove_above _ _ h, rev_succ, succAbove_below] + rwa [← rev_succ, rev_lt_rev, lt_def, val_succ, Nat.lt_succ_iff] + end SuccAbove section PredAbove diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean index 7a7b5d2de6ae5..fdf6c08e5b815 100644 --- a/Mathlib/Data/Fin/Tuple/Basic.lean +++ b/Mathlib/Data/Fin/Tuple/Basic.lean @@ -372,19 +372,24 @@ theorem cons_eq_append {α : Type*} (x : α) (xs : Fin n → α) : @[simp] lemma append_cast_left {n m} {α : Type*} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ) (h : n' = n) : Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ (Fin.cast <| by rw [h]) := by - subst h - funext i - simp (config := {unfoldPartialApp := true}) only [Fin.append, Fin.addCases, comp_def, Fin.cast, - Fin.coe_castLT, Fin.subNat_mk, Fin.natAdd_mk, ge_iff_le, eq_rec_constant, Fin.eta, Eq.ndrec, - id_eq, eq_mpr_eq_cast, cast_eq] + subst h; simp @[simp] lemma append_cast_right {n m} {α : Type*} (xs : Fin n → α) (ys : Fin m → α) (m' : ℕ) (h : m' = m) : Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ (Fin.cast <| by rw [h]) := by - subst h - funext i - simp only [append, addCases, cast, subNat_mk, natAdd_mk, Fin.eta, ge_iff_le, comp_apply, - eq_rec_constant] + subst h; simp + +lemma append_rev {m n} {α : Type*} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) : + append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (cast (add_comm _ _) i) := by + rcases rev_surjective i with ⟨i, rfl⟩ + rw [rev_rev] + induction i using Fin.addCases + · simp [rev_castAdd] + · simp [cast_rev, rev_addNat] + +lemma append_comp_rev {m n} {α : Type*} (xs : Fin m → α) (ys : Fin n → α) : + append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ cast (add_comm _ _) := + funext <| append_rev xs ys end Append @@ -439,6 +444,9 @@ theorem repeat_add {α : Type*} (a : Fin n → α) (m₁ m₂ : ℕ) : Fin.repea · simp [modNat, Nat.add_mod] #align fin.repeat_add Fin.repeat_add +proof_wanted repeat_comp_rev {α} (a : Fin n → α) : + (Fin.repeat m a) ∘ Fin.rev = Fin.repeat m (a ∘ Fin.rev) + end Repeat end Tuple @@ -658,6 +666,34 @@ theorem append_right_cons {n m} {α : Type*} (xs : Fin n → α) (y : α) (ys : Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm := by rw [append_left_snoc]; rfl +theorem append_cons {α} (a : α) (as : Fin n → α) (bs : Fin m → α) : + Fin.append (cons a as) bs + = cons a (Fin.append as bs) ∘ (Fin.cast <| Nat.add_right_comm n 1 m) := by + funext i + rcases i with ⟨i, -⟩ + simp only [append, addCases, cons, castLT, cast, comp_apply] + cases' i with i + · simp + · split_ifs with h + · have : i < n := Nat.lt_of_succ_lt_succ h + simp [addCases, this] + · have : ¬i < n := Nat.not_le.mpr <| Nat.lt_succ.mp <| Nat.not_le.mp h + simp [addCases, this] + +theorem append_snoc {α} (as : Fin n → α) (bs : Fin m → α) (b : α) : + Fin.append as (snoc bs b) = snoc (Fin.append as bs) b := by + funext i + rcases i with ⟨i, isLt⟩ + simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, ge_iff_le, snoc._eq_1, + cast_eq, eq_rec_constant, Nat.add_eq, Nat.add_zero, castLT_mk] + split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl) + · have := Nat.lt_add_right m lt_n + contradiction + · obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt + simp [Nat.add_comm n m] at sub_lt + · have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add + contradiction + theorem comp_init {α : Type*} {β : Type*} (g : α → β) (q : Fin n.succ → α) : g ∘ init q = init (g ∘ q) := by ext j @@ -816,6 +852,33 @@ theorem insertNth_zero_right [∀ j, Zero (α j)] (i : Fin (n + 1)) (x : α i) : insertNth_eq_iff.2 <| by simp [succAbove_ne, Pi.zero_def] #align fin.insert_nth_zero_right Fin.insertNth_zero_right +lemma insertNth_rev {α : Type*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) : + insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j := by + induction j using Fin.succAboveCases; exact rev i + · simp + · simp [rev_succAbove] + +theorem insertNth_comp_rev {α} (i : Fin (n + 1)) (x : α) (p : Fin n → α) : + (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev) := by + funext x + apply insertNth_rev + +theorem cons_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) : + cons (α := fun _ => α) a f i.rev = snoc (α := fun _ => α) (f ∘ Fin.rev : Fin _ → α) a i := by + simpa using insertNth_rev 0 a f i + +theorem cons_comp_rev {α n} (a : α) (f : Fin n → α) : + Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a := by + funext i; exact cons_rev .. + +theorem snoc_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) : + snoc (α := fun _ => α) f a i.rev = cons (α := fun _ => α) a (f ∘ Fin.rev : Fin _ → α) i := by + simpa using insertNth_rev (last n) a f i + +theorem snoc_comp_rev {α n} (a : α) (f : Fin n → α) : + Fin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev) := + funext <| snoc_rev a f + theorem insertNth_binop (op : ∀ j, α j → α j → α j) (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) : (i.insertNth (op i x y) fun j ↦ op _ (p j) (q j)) = fun j ↦