From eafd2a88ce0af8b54040de3264810cd00a111451 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jul 2022 15:34:06 -0700
Subject: [PATCH] chore: simplify `Prelude.lean` and `Core.lean` using
 `elabAsElim`

---
 src/Init/Core.lean              | 31 ++++++++++++++++++++-----------
 src/Init/Data/String/Extra.lean |  4 ++--
 src/Init/Prelude.lean           | 21 +++++++++------------
 src/Init/WF.lean                | 10 ++++------
 tests/lean/elabAsElim.lean      |  8 ++++++++
 5 files changed, 43 insertions(+), 31 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 28031221f6..9e1451545c 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -292,10 +292,10 @@ section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
 theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b :=
-  @HEq.rec α a (fun b _ => motive b) m β b h
+  h.rec m
 
 theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b :=
-  @HEq.rec α a (fun b _ => motive b) m β b h
+  h.rec m
 
 theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
@@ -304,7 +304,7 @@ theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p 
   HEq.ndrecOn h₁ h₂
 
 theorem HEq.symm (h : HEq a b) : HEq b a :=
-  HEq.ndrecOn (motive := fun x => HEq x a) h (HEq.refl a)
+  h.rec (HEq.refl a)
 
 theorem heq_of_eq (h : a = a') : HEq a a' :=
   Eq.subst h (HEq.refl a)
@@ -319,7 +319,7 @@ theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : HEq a' b) : HEq a b :=
   HEq.trans (heq_of_eq h₁) h₂
 
 def type_eq_of_heq (h : HEq a b) : α = β :=
-  HEq.ndrecOn (motive := @fun (x : Sort u) _ => α = x) h (Eq.refl α)
+  h.rec (Eq.refl α)
 
 end
 
@@ -497,7 +497,7 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
 
 /-- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/
 abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
-  Decidable.casesOn (motive := fun _ => Sort w) (inst (f x) (f y))
+  (inst (f x) (f y)).casesOn
     (fun _ => P)
     (fun _ => P → P)
 
@@ -549,7 +549,7 @@ theorem recSubsingleton
      {h₂ : ¬p → Sort u}
      [h₃ : ∀ (h : p), Subsingleton (h₁ h)]
      [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)]
-     : Subsingleton (Decidable.casesOn (motive := fun _ => Sort u) h h₂ h₁) :=
+     : Subsingleton (h.casesOn h₂ h₁) :=
   match h with
   | isTrue h  => h₃ h
   | isFalse h => h₄ h
@@ -767,6 +767,7 @@ protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot
 protected abbrev liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
   lift f c q
 
+@[elabAsElim]
 protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop}
     (q : Quot r)
     (h : (a : α) → motive (Quot.mk r a))
@@ -774,7 +775,7 @@ protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Q
   ind h q
 
 theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
-  Quot.inductionOn (motive := fun q => Exists (fun a => (Quot.mk r a) = q)) q (fun a => ⟨a, rfl⟩)
+  q.inductionOn (fun a => ⟨a, rfl⟩)
 
 section
 variable {α : Sort u}
@@ -810,7 +811,7 @@ protected abbrev recOn
     (f : (a : α) → motive (Quot.mk r a))
     (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
     : motive q :=
- Quot.rec f h q
+ q.rec f h
 
 protected abbrev recOnSubsingleton
     [h : (a : α) → Subsingleton (motive (Quot.mk r a))]
@@ -858,6 +859,7 @@ protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Pro
 protected abbrev liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
   Quot.liftOn q f c
 
+@[elabAsElim]
 protected theorem inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop}
     (q : Quotient s)
     (h : (a : α) → motive (Quotient.mk s a))
@@ -872,7 +874,7 @@ variable {α : Sort u}
 variable {s : Setoid α}
 variable {motive : Quotient s → Sort v}
 
-@[inline]
+@[inline, elabAsElim]
 protected def rec
     (f : (a : α) → motive (Quotient.mk s a))
     (h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
@@ -880,6 +882,7 @@ protected def rec
     : motive q :=
   Quot.rec f h q
 
+@[elabAsElim]
 protected abbrev recOn
     (q : Quotient s)
     (f : (a : α) → motive (Quotient.mk s a))
@@ -887,6 +890,7 @@ protected abbrev recOn
     : motive q :=
   Quot.recOn q f h
 
+@[elabAsElim]
 protected abbrev recOnSubsingleton
     [h : (a : α) → Subsingleton (motive (Quotient.mk s a))]
     (q : Quotient s)
@@ -894,6 +898,7 @@ protected abbrev recOnSubsingleton
     : motive q :=
   Quot.recOnSubsingleton (h := h) q f
 
+@[elabAsElim]
 protected abbrev hrecOn
     (q : Quotient s)
     (f : (a : α) → motive (Quotient.mk s a))
@@ -925,6 +930,7 @@ protected abbrev liftOn₂
     : φ :=
   Quotient.lift₂ f c q₁ q₂
 
+@[elabAsElim]
 protected theorem ind₂
     {motive : Quotient s₁ → Quotient s₂ → Prop}
     (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))
@@ -935,6 +941,7 @@ protected theorem ind₂
   induction q₂ using Quotient.ind
   apply h
 
+@[elabAsElim]
 protected theorem inductionOn₂
     {motive : Quotient s₁ → Quotient s₂ → Prop}
     (q₁ : Quotient s₁)
@@ -945,6 +952,7 @@ protected theorem inductionOn₂
   induction q₂ using Quotient.ind
   apply h
 
+@[elabAsElim]
 protected theorem inductionOn₃
     {s₃ : Setoid φ}
     {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
@@ -973,7 +981,7 @@ private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
         (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
 
 private theorem rel.refl {s : Setoid α} (q : Quotient s) : rel q q :=
-  Quot.inductionOn (motive := fun q => rel q q) q (fun a => Setoid.refl a)
+  q.inductionOn Setoid.refl
 
 private theorem rel_of_eq {s : Setoid α} {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
   fun h => Eq.ndrecOn h (rel.refl q₁)
@@ -988,6 +996,7 @@ universe uA uB uC
 variable {α : Sort uA} {β : Sort uB}
 variable {s₁ : Setoid α} {s₂ : Setoid β}
 
+@[elabAsElim]
 protected abbrev recOnSubsingleton₂
     {motive : Quotient s₁ → Quotient s₂ → Sort uC}
     [s : (a : α) → (b : β) → Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))]
@@ -1012,7 +1021,7 @@ variable (r : α → α → Prop)
 
 instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
   fun (q₁ q₂ : Quotient s) =>
-    Quotient.recOnSubsingleton₂ (motive := fun a b => Decidable (a = b)) q₁ q₂
+    Quotient.recOnSubsingleton₂ q₁ q₂
       fun a₁ a₂ =>
         match d a₁ a₂ with
         | isTrue h₁  => isTrue (Quotient.sound h₁)
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index d8a19e7a58..7999265084 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -74,9 +74,9 @@ namespace Iterator
   else find it.next p
 
 @[specialize] def foldUntil (it : Iterator) (init : α) (f : α → Char → Option α) : α × Iterator :=
-  if it.atEnd then 
+  if it.atEnd then
     (init, it)
-  else if let some a := f init it.curr then 
+  else if let some a := f init it.curr then
     foldUntil it.next a f
   else
     (init, it)
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index d44eddcffe..d251218239 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -50,16 +50,16 @@ inductive PEmpty : Sort u where
 def Not (a : Prop) : Prop := a → False
 
 @[macroInline] def False.elim {C : Sort u} (h : False) : C :=
-  @False.rec (fun _ => C) h
+  h.rec
 
 @[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
-  False.elim (h₂ h₁)
+  (h₂ h₁).rec
 
 inductive Eq : α → α → Prop where
   | refl (a : α) : Eq a a
 
 @[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
-  Eq.rec (motive := fun α _ => motive α) m h
+  h.rec m
 
 @[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
 
@@ -75,7 +75,7 @@ theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq
   h₂ ▸ h₁
 
 @[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
-  Eq.rec (motive := fun α _ => α) a h
+  h.rec a
 
 theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
   h ▸ rfl
@@ -142,7 +142,6 @@ In fact, the computation principle is declared as a reduction rule.
 -/
 add_decl_doc Quot.lift
 
-
 inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
   | refl (a : α) : HEq a a
 
@@ -151,10 +150,8 @@ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
 
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
   have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
-    fun α _ a _ h₁ =>
-      HEq.rec (motive := fun {β} (b : β) (_ : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
-        (fun (_ : Eq α α) => rfl)
-        h₁
+    fun _ _ _ _ h₁ =>
+      h₁.rec (fun _ => rfl)
   this α α a a' h rfl
 
 structure Prod (α : Type u) (β : Type v) where
@@ -310,7 +307,7 @@ class inductive Decidable (p : Prop) where
   | isTrue  (h : p) : Decidable p
 
 @[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
-  Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true)
+  h.casesOn (fun _ => false) (fun _ => true)
 
 export Decidable (isTrue isFalse decide)
 
@@ -369,12 +366,12 @@ instance [DecidableEq α] : BEq α where
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
 @[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
-  Decidable.casesOn (motive := fun _ => α) h e t
+  h.casesOn e t
 
 /-! # if-then-else -/
 
 @[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
-  Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t)
+  h.casesOn (fun _ => e) (fun _ => t)
 
 @[macroInline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (And p q) :=
   match dp with
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 743309f798..ff9bf3d84f 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -15,20 +15,19 @@ inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
 noncomputable abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
     (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
     {a : α} (n : Acc r a) : C a :=
-Acc.rec (motive := fun α _ => C α) m n
+  n.rec m
 
 noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
     {a : α} (n : Acc r a)
     (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
     : C a :=
-Acc.rec (motive := fun α _ => C α) m n
+  n.rec m
 
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
 def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
-Acc.recOn (motive := fun (x : α) _ => r y x → Acc r y)
-  h₁ (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
+  h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
 
@@ -41,8 +40,7 @@ class WellFoundedRelation (α : Sort u) where
 
 namespace WellFounded
 def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
-  WellFounded.recOn (motive := fun _ => (y : α) → Acc r y)
-    wf (fun p => p) a
+  wf.rec (fun p => p) a
 
 section
 variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
index 80c4a253b9..5fe3ddb43a 100644
--- a/tests/lean/elabAsElim.lean
+++ b/tests/lean/elabAsElim.lean
@@ -75,3 +75,11 @@ protected def znum.bit1 : znum → znum
   | zero    => pos .one
   | pos n => pos (pos_num.bit1 n)
   | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1)
+
+example (h : False) : a = c :=
+  h.rec
+
+example (h : False) : a = c :=
+  h.elim
+
+