refactor: induction

src/Lean/Elab/Tactic/Induction.lean

@@ -49,11 +49,11 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (remainingGoals : Array MVarId) : T
         let gs' ← getMVarsNoDelayed val
         tagUntaggedGoals mvarDecl.userName `induction gs'.toList
         pure gs'
-      pure (remainingGoals ++ gs')
+      return remainingGoals ++ gs'
     else
       setGoals [mvarId]
       closeUsingOrAdmit rhs
-      pure remainingGoals
+      return remainingGoals
 
 /-
   Helper method for creating an user-defined eliminator/recursor application.
@@ -70,13 +70,10 @@ structure State where
   f         : Expr
   fType     : Expr
   alts      : Array (Name × MVarId) := #[]
-  instMVars : Array MVarId := #[]
+  insts     : Array MVarId := #[]
 
 abbrev M := ReaderT Context $ StateRefT State TermElabM
 
-private def addInstMVar (mvarId : MVarId) : M Unit :=
-  modify fun s => { s with instMVars := s.instMVars.push mvarId }
-
 private def addNewArg (arg : Expr) : M Unit :=
   modify fun s => { s with argPos := s.argPos+1, f := mkApp s.f arg, fType := s.fType.bindingBody!.instantiate1 arg }
 
@@ -93,6 +90,7 @@ private def getFType : M Expr := do
 structure Result where
   elimApp : Expr
   alts    : Array (Name × MVarId) := #[]
+  others  : Array MVarId := #[]
 
 partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
   let rec loop : M Unit := do
@@ -122,21 +120,29 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
           let arg ← mkFreshExprMVar (← getArgExpectedType)
           addNewArg arg
         | BinderInfo.instImplicit =>
-          let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
-          addInstMVar arg.mvarId!
+          let arg ← mkFreshExprMVar (← getArgExpectedType) (kind := MetavarKind.synthetic) (userName := appendTag tag binderName)
+          modify fun s => { s with insts := s.insts.push arg.mvarId! }
           addNewArg arg
         | _ =>
-          let alt ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
-          modify fun s => { s with alts := s.alts.push (← getBindingName, alt.mvarId!) }
-          addNewArg alt
+          let arg ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
+          modify fun s => { s with alts := s.alts.push (← getBindingName, arg.mvarId!) }
+          addNewArg arg
       loop
     | _ =>
       pure ()
   let f ← Term.mkConst elimName
   let fType ← inferType f
   let (_, s) ← loop.run { elimInfo := elimInfo, targets := targets } |>.run { f := f, fType := fType }
-  Lean.Elab.Term.synthesizeAppInstMVars s.instMVars
-  pure { elimApp := (← instantiateMVars s.f), alts := s.alts }
+  let mut others := #[]
+  for mvarId in s.insts do
+    try
+      unless (← Term.synthesizeInstMVarCore mvarId) do
+        setMVarKind mvarId MetavarKind.syntheticOpaque
+        others := others.push mvarId
+    catch _ =>
+      setMVarKind mvarId MetavarKind.syntheticOpaque
+      others := others.push mvarId
+  pure { elimApp := (← instantiateMVars s.f), alts := s.alts, others := others }
 
 /- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign
   `motiveArg := fun targets => C[targets]` -/
@@ -440,31 +446,30 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do
     let target ← withMainMVarContext <| elabTerm target none
     generalizeTerm target
   let n ← generalizeVars stx targets
-  if targets.size == 1 then
-    let recInfo ← getRecInfo stx targets[0]
-    let (mvarId, _) ← getMainGoal
-    let altVars := recInfo.alts.map fun alt =>
-      { explicit := altHasExplicitModifier alt, varNames := (getAltVarNames alt).toList : AltVarNames }
-    let result ← Meta.induction mvarId targets[0].fvarId! recInfo.recName altVars
-    processResult recInfo.alts result (numToIntro := n)
-  else
+  let (elimName, elimInfo) ←
     if stx[2].isNone then
-      throwError! "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>')"
-    let elimId := stx[2][1]
-    let elimName ← withRef elimId do resolveGlobalConstNoOverload elimId.getId.eraseMacroScopes
-    let elimInfo ← withRef elimId do getElimInfo elimName
-    let (mvarId, _) ← getMainGoal
-    let tag ← getMVarTag mvarId
-    withMVarContext mvarId do
-      let result ← withRef stx[1] do -- use target position as reference
-        ElimApp.mkElimApp elimName elimInfo targets tag
-      assignExprMVar mvarId result.elimApp
-      let elimArgs := result.elimApp.getAppArgs
-      let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
-      let targetFVarIds := targets.map (·.fvarId!)
-      ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
-      let optInductionAlts := stx[4]
-      ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numGeneralized := n) (toClear := targetFVarIds)
+      unless targets.size == 1 do
+        throwError! "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>')"
+      let indVal ← getInductiveValFromMajor targets[0]
+      let elimName := mkRecName indVal.name
+      pure (elimName, ← getElimInfo elimName)
+    else
+      let elimId := stx[2][1]
+      let elimName ← withRef elimId do resolveGlobalConstNoOverload elimId.getId.eraseMacroScopes
+      pure (elimName, ← withRef elimId do getElimInfo elimName)
+  let (mvarId, _) ← getMainGoal
+  let tag ← getMVarTag mvarId
+  withMVarContext mvarId do
+    let result ← withRef stx[1] do -- use target position as reference
+      ElimApp.mkElimApp elimName elimInfo targets tag
+    assignExprMVar mvarId result.elimApp
+    let elimArgs := result.elimApp.getAppArgs
+    let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
+    let targetFVarIds := targets.map (·.fvarId!)
+    ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
+    let optInductionAlts := stx[4]
+    ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numGeneralized := n) (toClear := targetFVarIds)
+    appendGoals result.others.toList
 
 private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (alts : Array Syntax) : TacticM Unit := do
   let rec loop (i j : Nat) : TacticM Unit :=

tests/lean/run/ac_expr.lean

@@ -42,8 +42,8 @@ def Expr.flat : Expr → Expr
 
 theorem Expr.denote_flat (ctx : Context α) (e : Expr) : denote ctx (flat e) = denote ctx e := by
   induction e with
-  | Expr.var i => rfl
-  | Expr.op a b ih₁ ih₂ => simp [flat, denote, denote_concat, ih₁, ih₂]
+  | var i => rfl
+  | op a b ih₁ ih₂ => simp [flat, denote, denote_concat, ih₁, ih₂]
 
 theorem Expr.eq_of_flat (ctx : Context α) (a b : Expr) (h : flat a = flat b) : denote ctx a = denote ctx b := by
   have h := congrArg (denote ctx) h

tests/lean/run/flat_expr.lean

@@ -37,8 +37,8 @@ theorem Expr.concat_var (i : Nat) (c : Expr) : concat (Expr.var i) c = Expr.op (
 
 theorem Expr.denote_concat (ctx : Context α) (a b : Expr) : denote ctx (concat a b) = denote ctx (Expr.op a b) := by
   induction a with
-  | Expr.var i => rfl
-  | Expr.op _ _ _ ih => rw [concat_op, denote_op, ih, denote_op, denote_op, denote_op, ctx.assoc]
+  | var i => rfl
+  | op _ _ _ ih => rw [concat_op, denote_op, ih, denote_op, denote_op, denote_op, ctx.assoc]
 
 def Expr.flat : Expr → Expr
   | Expr.op a b => concat (flat a) (flat b)
@@ -49,8 +49,8 @@ theorem Expr.flat_op (a b : Expr) : flat (Expr.op a b) = concat (flat a) (flat b
 
 theorem Expr.denote_flat (ctx : Context α) (a : Expr) : denote ctx (flat a) = denote ctx a := by
   induction a with
-  | Expr.var i => rfl
-  | Expr.op a b ih₁ ih₂ => rw [flat_op, denote_concat, denote_op, denote_op, ih₁, ih₂]
+  | var i => rfl
+  | op a b ih₁ ih₂ => rw [flat_op, denote_concat, denote_op, denote_op, ih₁, ih₂]
 
 theorem Expr.eq_of_flat (ctx : Context α) (a b : Expr) (h : flat a = flat b) : denote ctx a = denote ctx b := by
   rw [← Expr.denote_flat _ a, ← Expr.denote_flat _ b, h]

tests/lean/run/induction1.lean

@@ -1,9 +1,3 @@
-@[recursor 4]
-def Or.elim2 {p q r : Prop} (major : p ∨ q) (left : p → r) (right : q → r) : r :=
-  match  major with
-  | Or.inl h => left h
-  | Or.inr h => right h
-
 theorem tst0 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
   induction h;
@@ -25,36 +19,6 @@ induction h with
 | inr h2 => exact Or.inl h2
 | inl h1 => exact Or.inr h1
 
-theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
-| left _  => apply Or.inr; assumption
-| right _ => apply Or.inl; assumption
-
-theorem tst2b {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
-| left => apply Or.inr; assumption
-| _ => apply Or.inl; assumption
-
-theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
-| right h => exact Or.inl h
-| left h  => exact Or.inr h
-
-theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
-| right h => ?myright
-| left h  => ?myleft
-case myleft  => exact Or.inr h
-case myright => exact Or.inl h
-
-theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2 with
-| right h => _
-| left h  =>
-  refine Or.inr ?_
-  exact h
-case right => exact Or.inl h
-
 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
   cases h with
@@ -64,13 +28,13 @@ by {
 
 theorem tst7 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
 by {
-  induction xs with
+  induction xs generalizing h with
   | nil          => exact rfl
   | cons z zs ih => exact absurd rfl (h z zs)
 }
 
 theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by {
-  induction xs;
+  induction xs generalizing h;
   exact rfl;
   exact absurd rfl $ h _ _
 }
@@ -111,7 +75,7 @@ theorem tst13 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by
   | _     => injection h
 
 theorem tst14 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by
-  induction x with
+  induction x generalizing h with
   | leaf₁ => rfl
   | _     => injection h