feat: induction using <term> (leanprover#3188)

right now, the `induction` tactic accepts a custom eliminator using the
`using <ident>` syntax, but is restricted to identifiers. This
limitation becomes annoying when the elminator has explicit parameters
that are not targets, and the user (naturally) wants to be able to write
```
induction a, b, c using foo (x := …)
```

This generalizes the syntax to expressions and changes the code
accordingly.

This can be used to instantiate a multi-motive induction:
```
example (a : A) : True := by
  induction a using A.rec (motive_2 := fun b => True)
  case mkA b IH => exact trivial
  case A => exact trivial
  case mkB b IH => exact trivial
```

For this to work the term elaborator learned the `heedElabAsElim` flag,
`true` by default. But in the default setting, `A.rec (motive_2 := fun b
=> True)`
would fail to elaborate, because there is no expected type. So the
induction
tactic will elaborate in a mode where that attribute is simply ignored.

As a side effect, the “failed to infer implicit target” error message 
is improved and prints the name of the implicit target that could not be
instantiated.

src/Init/Tactics.lean

@@ -559,15 +559,15 @@ You can use `with` to provide the variables names for each constructor.
 - `induction e`, where `e` is an expression instead of a variable,
   generalizes `e` in the goal, and then performs induction on the resulting variable.
 - `induction e using r` allows the user to specify the principle of induction that should be used.
-  Here `r` should be a theorem whose result type must be of the form `C t`,
+  Here `r` should be a term whose result type must be of the form `C t`,
   where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
 - `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context,
   generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal.
   In other words, the net effect is that each inductive hypothesis is generalized.
 - Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂`
   uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.
 -/
-syntax (name := induction) "induction " term,+ (" using " ident)?
+syntax (name := induction) "induction " term,+ (" using " term)?
   (" generalizing" (ppSpace colGt term:max)+)? (inductionAlts)? : tactic
 
 /-- A `generalize` argument, of the form `term = x` or `h : term = x`. -/
@@ -610,7 +610,7 @@ You can use `with` to provide the variables names for each constructor.
   performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis,
   where `...` is the constructor instance for that particular case.
 -/
-syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
+syntax (name := cases) "cases " casesTarget,+ (" using " term)? (inductionAlts)? : tactic
 
 /-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
 syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic

src/Lean/Elab/App.lean

@@ -690,10 +690,10 @@ builtin_initialize elabAsElim : TagAttribute ←
     (applicationTime := .afterCompilation)
     fun declName => do
       let go : MetaM Unit := do
-        discard <| getElimInfo declName
         let info ← getConstInfo declName
         if (← hasOptAutoParams info.type) then
           throwError "[elab_as_elim] attribute cannot be used in declarations containing optional and auto parameters"
+        discard <| getElimInfo declName
       go.run' {} {}
 
 /-! # Eliminator-like function application elaborator -/
@@ -937,6 +937,7 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
 where
   /-- Return `some info` if we should elaborate as an eliminator. -/
   elabAsElim? : TermElabM (Option ElimInfo) := do
+    unless (← read).heedElabAsElim do return none
     if explicit || ellipsis then return none
     let .const declName _ := f | return none
     unless (← shouldElabAsElim declName) do return none
@@ -957,8 +958,7 @@ where
   The idea is that the contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`.
   -/
   getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do
-    let cinfo ← getConstInfo elimInfo.name
-    forallTelescope cinfo.type fun xs type => do
+    forallTelescope elimInfo.elimType fun xs type => do
       let resultArgs := type.getAppArgs
       let mut extraArgsPos := #[]
       for i in [:xs.size] do

src/Lean/Elab/Tactic/Induction.lean

@@ -95,6 +95,7 @@ structure Context where
 structure State where
   argPos    : Nat := 0 -- current argument position
   targetPos : Nat := 0 -- current target at targetsStx
+  motive    : Option MVarId -- motive metavariable
   f         : Expr
   fType     : Expr
   alts      : Array Alt := #[]
@@ -117,6 +118,7 @@ private def getFType : M Expr := do
 
 structure Result where
   elimApp : Expr
+  motive  : MVarId
   alts    : Array Alt := #[]
   others  : Array MVarId := #[]
 
@@ -134,12 +136,13 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
       let argPos := (← get).argPos
       if ctx.elimInfo.motivePos == argPos then
         let motive ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.syntheticOpaque
+        modify fun s => { s with motive := motive.mvarId! }
         addNewArg motive
       else if ctx.elimInfo.targetsPos.contains argPos then
         let s ← get
         let ctx ← read
         unless s.targetPos < ctx.targets.size do
-          throwError "insufficient number of targets for '{elimInfo.name}'"
+          throwError "insufficient number of targets for '{elimInfo.elimExpr}'"
         let target := ctx.targets[s.targetPos]!
         let expectedType ← getArgExpectedType
         let target ← withAssignableSyntheticOpaque <| Term.ensureHasType expectedType target
@@ -166,9 +169,8 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
       loop
     | _ =>
       pure ()
-  let f ← Term.mkConst elimInfo.name
-  let fType ← inferType f
-  let (_, s) ← (loop).run { elimInfo := elimInfo, targets := targets } |>.run { f := f, fType := fType }
+  let (_, s) ← (loop).run { elimInfo := elimInfo, targets := targets }
+    |>.run { f := elimInfo.elimExpr, fType := elimInfo.elimType, motive := none }
   let mut others := #[]
   for mvarId in s.insts do
     try
@@ -179,7 +181,9 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
       mvarId.setKind .syntheticOpaque
       others := others.push mvarId
   let alts ← s.alts.filterM fun alt => return !(← alt.mvarId.isAssigned)
-  return { elimApp := (← instantiateMVars s.f), alts, others := others }
+  let some motive := s.motive |
+      throwError "mkElimApp: motive not found"
+  return { elimApp := (← instantiateMVars s.f), alts, others, motive }
 
 /-- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign
   `motiveArg := fun targets => C[targets]` -/
@@ -499,11 +503,36 @@ def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
       (fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
       (fun val _ => pure val)
 
--- `optElimId` is of the form `("using" ident)?`
+/--
+Elaborates the term in the `using` clause. We want to allow parameters to be instantiated
+(e.g. `using foo (p := …)`), but preserve other paramters, like the motives, as parameters,
+without turning them into MVars. So this uses `abstractMVars` at the end. This is inspired by
+`Lean.Elab.Tactic.addSimpTheorem`.
+
+It also elaborates without `heedElabAsElim` so that users can use constants that are marked
+`elabAsElim` in the `using` clause`.
+-/
+private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
+  -- Short-circuit elaborating plain identifiers
+  if stx.isIdent then
+    if let some e ← Term.resolveId? stx (withInfo := true) then
+      return e
+  Term.withoutErrToSorry <| Term.withoutHeedElabAsElim do
+    let e ← Term.elabTerm stx none (implicitLambda := false)
+    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    let e ← instantiateMVars e
+    let e := e.eta
+    if e.hasMVar then
+      let r ← abstractMVars (levels := false) e
+      return r.expr
+    else
+      return e
+
+-- `optElimId` is of the form `("using" term)?`
 private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool): TacticM ElimInfo := do
   if optElimId.isNone then
-    if let some elimInfo ← getCustomEliminator? targets then
-      return elimInfo
+    if let some elimName ← getCustomEliminator? targets then
+      return ← getElimInfo elimName
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>'), and no default eliminator has been registered using attribute `[eliminator]`"
     let indVal ← getInductiveValFromMajor targets[0]!
@@ -514,12 +543,17 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
     let elimName := if induction then mkRecName indVal.name else mkCasesOnName indVal.name
     getElimInfo elimName indVal.name
   else
-    let elimId := optElimId[1]
-    let elimName ← withRef elimId do resolveGlobalConstNoOverloadWithInfo elimId
+    let elimTerm := optElimId[1]
+    let elimExpr ← withRef elimTerm do elabTermForElim elimTerm
     -- not a precise check, but covers the common cases of T.recOn / T.casesOn
     -- as well as user defined T.myInductionOn to locate the constructors of T
-    let baseName? := if ← isInductive elimName.getPrefix then some elimName.getPrefix else none
-    withRef elimId <| getElimInfo elimName baseName?
+    let baseName? ← do
+      let some elimName := elimExpr.getAppFn.constName? | pure none
+      if ← isInductive elimName.getPrefix then
+        pure (some elimName.getPrefix)
+      else
+        pure none
+    withRef elimTerm <| getElimExprInfo elimExpr baseName?
 
 private def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
   if let .fvar fvarId .. := e then
@@ -557,8 +591,7 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
         let result ← withRef stx[1] do -- use target position as reference
           ElimApp.mkElimApp elimInfo targets tag
         trace[Elab.induction] "elimApp: {result.elimApp}"
-        let elimArgs := result.elimApp.getAppArgs
-        ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds
+        ElimApp.setMotiveArg mvarId result.motive targetFVarIds
         let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
         mvarId.assign result.elimApp
         ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)

src/Lean/Elab/Term.lean

@@ -198,6 +198,8 @@ structure Context where
   sectionFVars       : NameMap Expr    := {}
   /-- Enable/disable implicit lambdas feature. -/
   implicitLambda     : Bool            := true
+  /-- Heed `elab_as_elim` attribute. -/
+  heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
@@ -409,6 +411,17 @@ def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
 def withoutErrToSorry [MonadFunctorT TermElabM m] : m α → m α :=
   monadMap (m := TermElabM) withoutErrToSorryImp
 
+def withoutHeedElabAsElimImp (x : TermElabM α) : TermElabM α :=
+  withReader (fun ctx => { ctx with heedElabAsElim := false }) x
+
+/--
+  Execute `x` without heeding the `elab_as_elim` attribute. Useful when there is
+  no expected type (so `elabAppArgs` would fail), but expect that the user wants
+  to use such constants.
+-/
+def withoutHeedElabAsElim [MonadFunctorT TermElabM m] : m α → m α :=
+  monadMap (m := TermElabM) withoutHeedElabAsElimImp
+
 /--
   Execute `x` but discard changes performed at `Term.State` and `Meta.State`.
   Recall that the `Environment` and `InfoState` are at `Core.State`. Thus, any updates to it will

src/Lean/Meta/AbstractMVars.lean

@@ -16,14 +16,15 @@ structure AbstractMVarsResult where
 namespace AbstractMVars
 
 structure State where
-  ngen         : NameGenerator
-  lctx         : LocalContext
-  mctx         : MetavarContext
-  nextParamIdx : Nat := 0
-  paramNames   : Array Name := #[]
-  fvars        : Array Expr  := #[]
-  lmap         : HashMap LMVarId Level := {}
-  emap         : HashMap MVarId Expr  := {}
+  ngen           : NameGenerator
+  lctx           : LocalContext
+  mctx           : MetavarContext
+  nextParamIdx   : Nat := 0
+  paramNames     : Array Name := #[]
+  fvars          : Array Expr  := #[]
+  lmap           : HashMap LMVarId Level := {}
+  emap           : HashMap MVarId Expr  := {}
+  abstractLevels : Bool -- whether to abstract level mvars
 
 abbrev M := StateM State
 
@@ -42,6 +43,8 @@ def mkFreshFVarId : M FVarId :=
   return { name := (← mkFreshId) }
 
 private partial def abstractLevelMVars (u : Level) : M Level := do
+  if !(← get).abstractLevels then
+    return u
   if !u.hasMVar then
     return u
   else
@@ -124,10 +127,13 @@ end AbstractMVars
   new fresh universe metavariables, and instantiate the `(m_i : A_i)` in the lambda-expression
   with new fresh metavariables.
 
+  If `levels := false`, then level metavariables are not abstracted.
+
   Application: we use this method to cache the results of type class resolution. -/
-def abstractMVars (e : Expr) : MetaM AbstractMVarsResult := do
+def abstractMVars (e : Expr) (levels : Bool := true): MetaM AbstractMVarsResult := do
   let e ← instantiateMVars e
-  let (e, s) := AbstractMVars.abstractExprMVars e { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen) }
+  let (e, s) := AbstractMVars.abstractExprMVars e
+    { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen), abstractLevels := levels }
   setNGen s.ngen
   setMCtx s.mctx
   let e := s.lctx.mkLambda s.fvars e