From f817d5a706ed39a33bd63c4e701036dcb3510183 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 28 Apr 2024 22:28:41 +0200 Subject: [PATCH] feat: use structural recursion in Fin.induction (#4010) this should help with reducing mathlib's vector notation (`![a,b,c] 2`), and reduce fallout from #4002 --- src/Init/Data/Fin/Lemmas.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 6b09f91d23..3f9fc0f431 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -602,6 +602,7 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/ @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by cases i; rfl + /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value. This function has two arguments: `zero` handles the base case on `motive 0`, and `succ` defines the inductive step using `motive i.castSucc`. @@ -610,8 +611,12 @@ and `succ` defines the inductive step using `motive i.castSucc`. @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0) (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) : ∀ i : Fin (n + 1), motive i - | ⟨0, hi⟩ => by rwa [Fin.mk_zero] - | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩) + | ⟨i, hi⟩ => go i hi +where + -- Use a curried function so that this is structurally recursive + go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩ + | 0, hi => by rwa [Fin.mk_zero] + | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi)) @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0) (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :