From dd22447afdfc0c930234d3cb6749596966708dfe Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Mon, 26 Aug 2024 15:44:54 +0800
Subject: [PATCH] chore: `@[elab_as_elim]` additions (#5147)

This adds `@[elab_as_elim]` to `Quot.rec`, `Nat.strongInductionOn` and
`Nat.casesStrongInductionOn`, and also renames the latter two to
`Nat.strongRecOn` and `Nat.casesStrongRecOn`.

The first change resolves the todos in
[`Mathlib.Init.Quot`](https://github.com/leanprover-community/mathlib4/blob/ca6a6fdc075f392d6d38c787d5f02f1aa61acfbc/Mathlib/Init/Quot.lean)
while the other two are based on a suggestion of @YaelDillies on [the
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Technical.20Debt.20Counters/near/464804567)
and related to
https://github.com/leanprover-community/mathlib4/pull/16096.
---
 src/Init/Core.lean                    |  2 +-
 src/Init/Data/Nat/Bitwise/Lemmas.lean | 11 +++++------
 src/Init/Data/Nat/Div.lean            |  4 ++--
 src/Init/Data/Nat/Gcd.lean            |  2 +-
 src/Init/WF.lean                      |  6 +++---
 5 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index fb2a781754..4a34ff2270 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1564,7 +1564,7 @@ so you should consider the simpler versions if they apply:
 * `Quot.recOnSubsingleton`, when the target type is a `Subsingleton`
 * `Quot.hrecOn`, which uses `HEq (f a) (f b)` instead of a `sound p ▸ f a = f b` assummption
 -/
-protected abbrev rec
+@[elab_as_elim] protected abbrev rec
     (f : (a : α) → motive (Quot.mk r a))
     (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
     (q : Quot r) : motive q :=
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 94946e1737..7959708e68 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -40,7 +40,7 @@ An induction principal that works on divison by two.
 -/
 noncomputable def div2Induction {motive : Nat → Sort u}
     (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
-  induction n using Nat.strongInductionOn with
+  induction n using Nat.strongRecOn with
   | ind n hyp =>
     apply ind
     intro n_pos
@@ -258,7 +258,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
-  induction x using Nat.strongInductionOn generalizing j i with
+  induction x using Nat.strongRecOn generalizing j i with
   | ind x hyp =>
     rw [mod_eq]
     rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j
@@ -337,10 +337,9 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
 
 /-! ### bitwise -/
 
-theorem testBit_bitwise
-  (false_false_axiom : f false false = false) (x y i : Nat)
-: (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
-  induction i using Nat.strongInductionOn generalizing x y with
+theorem testBit_bitwise (false_false_axiom : f false false = false) (x y i : Nat) :
+    (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
+  induction i using Nat.strongRecOn generalizing x y with
   | ind i hyp =>
     unfold bitwise
     if x_zero : x = 0 then
diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index ed27dd428d..788d5d4f2b 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -48,7 +48,7 @@ def div.inductionOn.{u}
 decreasing_by apply div_rec_lemma; assumption
 
 theorem div_le_self (n k : Nat) : n / k ≤ n := by
-  induction n using Nat.strongInductionOn with
+  induction n using Nat.strongRecOn with
   | ind n ih =>
     rw [div_eq]
     -- Note: manual split to avoid Classical.em which is not yet defined
@@ -334,7 +334,7 @@ theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
   else if z0 : z = 0 then by
     rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
   else by
-    induction x using Nat.strongInductionOn with
+    induction x using Nat.strongRecOn with
     | _ n IH =>
       have y0 : y > 0 := Nat.pos_of_ne_zero y0
       have z0 : z > 0 := Nat.pos_of_ne_zero z0
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index 9aa3e558c6..540c0f8267 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -75,7 +75,7 @@ theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
     (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
-  Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
+  Nat.strongRecOn (motive := fun m => ∀ n, P m n) m
     (fun
     | 0, _ => H0
     | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 4ad3a6f170..b932f5f730 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -190,18 +190,18 @@ def lt_wfRel : WellFoundedRelation Nat where
       | Or.inl e => subst e; assumption
       | Or.inr e => exact Acc.inv ih e
 
-protected noncomputable def strongInductionOn
+@[elab_as_elim] protected noncomputable def strongRecOn
     {motive : Nat → Sort u}
     (n : Nat)
     (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
   Nat.lt_wfRel.wf.fix ind n
 
-protected noncomputable def caseStrongInductionOn
+@[elab_as_elim] protected noncomputable def caseStrongRecOn
     {motive : Nat → Sort u}
     (a : Nat)
     (zero : motive 0)
     (ind : ∀ n, (∀ m, m ≤ n → motive m) → motive (succ n)) : motive a :=
-  Nat.strongInductionOn a fun n =>
+  Nat.strongRecOn a fun n =>
     match n with
     | 0   => fun _  => zero
     | n+1 => fun h₁ => ind n (λ _ h₂ => h₁ _ (lt_succ_of_le h₂))