From 04c6d77cb8c94fbdac2ac19ac5dec94434becf41 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Tue, 26 Dec 2023 22:33:54 +0000 Subject: [PATCH] chore: use elab_as_elim directly, now that lean4#1900 is fixed (#9288) Adds the attribute `elab_as_elim` directly to the declarations of `strongSubRecursion` and `pincerRecursion`, rather than in separate commands. This change was made possible by https://github.com/leanprover/lean4/commit/8a573b5d87a42bd19307522ee747aaed44d9d71c, which fixed https://github.com/leanprover/lean4/issues/1900. --- Mathlib/Data/Nat/Basic.lean | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean index 1cd9067d80f1b..6770f954b07a0 100644 --- a/Mathlib/Data/Nat/Basic.lean +++ b/Mathlib/Data/Nat/Basic.lean @@ -560,21 +560,18 @@ theorem decreasingInduction_succ_left {P : ℕ → Sort*} (h : ∀ n, P (n + 1) strictly below `(a,b)` to `P a b`, then we have `P n m` for all `n m : ℕ`. Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas. -/ +@[elab_as_elim] def strongSubRecursion {P : ℕ → ℕ → Sort*} (H : ∀ a b, (∀ x y, x < a → y < b → P x y) → P a b) : ∀ n m : ℕ, P n m | n, m => H n m fun x y _ _ => strongSubRecursion H x y #align nat.strong_sub_recursion Nat.strongSubRecursion --- Porting note: --- we can't put this on the definition itself because of --- https://github.com/leanprover/lean4/issues/1900 -attribute [elab_as_elim] strongSubRecursion - /-- Given `P : ℕ → ℕ → Sort*`, if we have `P i 0` and `P 0 i` for all `i : ℕ`, and for any `x y : ℕ` we can extend `P` from `(x,y+1)` and `(x+1,y)` to `(x+1,y+1)` then we have `P n m` for all `n m : ℕ`. Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas. -/ +@[elab_as_elim] def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ a : ℕ, P a 0) (H0b : ∀ b : ℕ, P 0 b) (H : ∀ x y : ℕ, P x y.succ → P x.succ y → P x.succ y.succ) : ∀ n m : ℕ, P n m | a, 0 => Ha0 a @@ -583,11 +580,6 @@ def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ a : ℕ, P a 0) (H0b termination_by pincerRecursion Ha0 Hab H n m => n + m #align nat.pincer_recursion Nat.pincerRecursion --- Porting note: --- we can't put this on the definition itself because of --- https://github.com/leanprover/lean4/issues/1900 -attribute [elab_as_elim] pincerRecursion - /-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`, there is a map from `C n` to each `C m`, `n ≤ m`. -/ @[elab_as_elim]