From 98d86bd9027cfb180756e666b3d6a2b74c32eec3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 12:35:33 -0800
Subject: [PATCH] chore: remove `induction h:e`

Users should use `cases h:e` instead
---
 src/Lean/Elab/Tactic/Induction.lean | 71 ++++++++++++++---------------
 src/Lean/Parser/Tactic.lean         |  4 +-
 2 files changed, 37 insertions(+), 38 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index e27a7e2403..3cfd749a0f 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -174,40 +174,6 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax :
 
 end ElimApp
 
--- Recall that
--- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
-private def getTargetHypothesisName? (target : Syntax) : Option Name :=
-  if target[0].isNone then
-    none
-  else
-    some target[0][0].getId
-
-private def getTargetTerm (target : Syntax) : Syntax :=
-  target[1]
-
-private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
-  match h? with
-  | none   => withMainMVarContext $ elabTerm major none
-  | some h => withMainMVarContext do
-    let lctx ← getLCtx
-    let x ← mkFreshUserName `x
-    let major ← elabTerm major none
-    evalGeneralizeAux h? major x
-    withMainMVarContext do
-      let lctx ← getLCtx
-      match lctx.findFromUserName? x with
-      | some decl => pure decl.toExpr
-      | none      => throwError "failed to generalize"
-
-private def generalizeMajor (major : Expr) : TacticM Expr := do
-  match major with
-  | Expr.fvar _ _ => pure major
-  | _ =>
-    liftMetaTacticAux fun mvarId => do
-      mvarId ← Meta.generalize mvarId major `x false
-      let (fvarId, mvarId) ← Meta.intro1 mvarId
-      pure (mkFVar fvarId, [mvarId])
-
 /-
   Recall that
   ```
@@ -442,12 +408,20 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio
         done
     setGoals gs
 
+private def generalizeMajor (major : Expr) : TacticM Expr := do
+  match major with
+  | Expr.fvar .. => pure major
+  | _ =>
+    liftMetaTacticAux fun mvarId => do
+      mvarId ← Meta.generalize mvarId major `x false
+      let (fvarId, mvarId) ← Meta.intro1 mvarId
+      pure (mkFVar fvarId, [mvarId])
+
 @[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focusAux do
   let targets := stx[1].getSepArgs
   if targets.size == 1 then
     let target := targets[0]
-    let h? := getTargetHypothesisName? target
-    let major ← elabMajor h? (getTargetTerm target)
+    let major ← withMainMVarContext $ elabTerm target none
     let major ← generalizeMajor major
     let n ← generalizeVars stx major
     let recInfo ← getRecInfo stx major
@@ -481,6 +455,31 @@ private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ct
   unless altRHSs.isEmpty do
     loop 0 0
 
+-- Recall that
+-- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
+private def getTargetHypothesisName? (target : Syntax) : Option Name :=
+  if target[0].isNone then
+    none
+  else
+    some target[0][0].getId
+
+private def getTargetTerm (target : Syntax) : Syntax :=
+  target[1]
+
+private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
+  match h? with
+  | none   => withMainMVarContext $ elabTerm major none
+  | some h => withMainMVarContext do
+    let lctx ← getLCtx
+    let x ← mkFreshUserName `x
+    let major ← elabTerm major none
+    evalGeneralizeAux h? major x
+    withMainMVarContext do
+      let lctx ← getLCtx
+      match lctx.findFromUserName? x with
+      | some decl => pure decl.toExpr
+      | none      => throwError "failed to generalize"
+
 /- Default `cases` tactic that uses `casesOn` eliminator -/
 def evalCasesOn (target : Syntax) (withAlts : Syntax) : TacticM Unit := do
   let h?    := getTargetHypothesisName? target
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 5dc4ea9c7e..876e5a8c37 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -64,14 +64,14 @@ def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
 @[builtinTacticParser] def «rewrite»    := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> notSymbol "[" >> rwRule >> optional location
 @[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
 
-def majorPremise := parser! optional («try» (ident >> " : ")) >> termParser
 def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
 def inductionAlts : Parser := withPosition $ "| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
 def withAlts : Parser := optional inductionAlts
 def usingRec : Parser := optional (" using " >> ident)
 def generalizingVars := optional (" generalizing " >> many1 ident)
-@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> sepBy1 majorPremise ", " >> usingRec >> generalizingVars >> withAlts
+@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> withAlts
+def majorPremise := parser! optional («try» (ident >> " : ")) >> termParser
 @[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> sepBy1 majorPremise ", " >> usingRec >> withAlts
 
 def matchAlt  : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS