From 550fa6994e7853d2673d7373c99e46f79a6220f1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jan 2024 17:57:41 +0100 Subject: [PATCH] feat: induction using (#3188) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit right now, the `induction` tactic accepts a custom eliminator using the `using ` 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 | 6 +- src/Lean/Elab/App.lean | 6 +- src/Lean/Elab/Tactic/Induction.lean | 61 +++-- src/Lean/Elab/Term.lean | 13 ++ src/Lean/Meta/AbstractMVars.lean | 26 ++- src/Lean/Meta/Tactic/ElimInfo.lean | 77 ++++--- tests/lean/indUsingTerm.lean | 225 +++++++++++++++++++ tests/lean/indUsingTerm.lean.expected.out | 0 tests/lean/indimpltarget.lean | 13 ++ tests/lean/indimpltarget.lean.expected.out | 7 +- tests/lean/inductionErrors.lean.expected.out | 2 +- 11 files changed, 369 insertions(+), 67 deletions(-) create mode 100644 tests/lean/indUsingTerm.lean create mode 100644 tests/lean/indUsingTerm.lean.expected.out diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 3a769b5592..46dfed3be8 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -559,7 +559,7 @@ 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. @@ -567,7 +567,7 @@ You can use `with` to provide the variables names for each constructor. - 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 diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 9d9169350d..aa0e473205 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index ab070547ba..f4a638aa9f 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/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 '), 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) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 8eea10b980..7ce6f963ea 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index a362566d56..d5d7597c1f 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 58fb1fa4ff..94601b2379 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -15,16 +15,24 @@ structure ElimAltInfo where numFields : Nat deriving Repr, Inhabited +/-- +Information about an eliminator as used by `induction` or `cases`. + +Created from an expression by `getElimInfo`. This typically contains level metavariables that +are instantiated as we go (e.g. in `addImplicitTargets`), so this is single use. +-/ structure ElimInfo where - name : Name + elimExpr : Expr + elimType : Expr motivePos : Nat targetsPos : Array Nat := #[] altsInfo : Array ElimAltInfo := #[] deriving Repr, Inhabited -def getElimInfo (declName : Name) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do - let declInfo ← getConstInfo declName - forallTelescopeReducing declInfo.type fun xs type => do +def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do + let elimType ← inferType elimExpr + trace[Elab.induction] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}" + forallTelescopeReducing elimType fun xs type => do let motive := type.getAppFn let targets := type.getAppArgs unless motive.isFVar && targets.all (·.isFVar) && targets.size > 0 do @@ -36,10 +44,10 @@ def getElimInfo (declName : Name) (baseDeclName? : Option Name := none) : MetaM unless motiveResultType.isSort do throwError "motive result type must be a sort{indentExpr motiveType}" let some motivePos ← pure (xs.indexOf? motive) | - throwError "unexpected eliminator type{indentExpr declInfo.type}" + throwError "unexpected eliminator type{indentExpr elimType}" let targetsPos ← targets.mapM fun target => do match xs.indexOf? target with - | none => throwError "unexpected eliminator type{indentExpr declInfo.type}" + | none => throwError "unexpected eliminator type{indentExpr elimType}" | some targetPos => pure targetPos.val let mut altsInfo := #[] let env ← getEnv @@ -55,55 +63,60 @@ def getElimInfo (declName : Name) (baseDeclName? : Option Name := none) : MetaM let altDeclName := base ++ name if env.contains altDeclName then some altDeclName else none altsInfo := altsInfo.push { name, declName?, numFields } - pure { name := declName, motivePos, targetsPos, altsInfo } + pure { elimExpr, elimType, motivePos, targetsPos, altsInfo } + +def getElimInfo (elimName : Name) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do + getElimExprInfo (← mkConstWithFreshMVarLevels elimName) baseDeclName? /-- Eliminators/recursors may have implicit targets. For builtin recursors, all indices are implicit targets. Given an eliminator and the sequence of explicit targets, this methods returns a new sequence containing implicit and explicit targets. -/ -partial def addImplicitTargets (elimInfo : ElimInfo) (targets : Array Expr) : MetaM (Array Expr) := - withNewMCtxDepth do - let f ← mkConstWithFreshMVarLevels elimInfo.name - let targets ← collect (← inferType f) 0 0 #[] - let targets ← targets.mapM instantiateMVars - for target in targets do - if (← hasAssignableMVar target) then - throwError "failed to infer implicit target, it contains unresolved metavariables{indentExpr target}" - return targets +partial def addImplicitTargets (elimInfo : ElimInfo) (targets : Array Expr) : MetaM (Array Expr) := do + let (implicitMVars, targets) ← collect elimInfo.elimType 0 0 #[] #[] + for mvar in implicitMVars do + unless ← mvar.isAssigned do + let name := (←mvar.getDecl).userName + if name.isAnonymous || name.hasMacroScopes then + throwError "failed to infer implicit target" + else + throwError "failed to infer implicit target {(←mvar.getDecl).userName}" + targets.mapM instantiateMVars where - collect (type : Expr) (argIdx targetIdx : Nat) (targets' : Array Expr) : MetaM (Array Expr) := do + collect (type : Expr) (argIdx targetIdx : Nat) (implicits : Array MVarId) (targets' : Array Expr) : + MetaM (Array MVarId × Array Expr) := do match (← whnfD type) with - | Expr.forallE _ d b bi => + | Expr.forallE n d b bi => if elimInfo.targetsPos.contains argIdx then if bi.isExplicit then unless targetIdx < targets.size do - throwError "insufficient number of targets for '{elimInfo.name}'" + throwError "insufficient number of targets for '{elimInfo.elimExpr}'" let target := targets[targetIdx]! let targetType ← inferType target unless (← isDefEq d targetType) do throwError "target{indentExpr target}\n{← mkHasTypeButIsExpectedMsg targetType d}" - collect (b.instantiate1 target) (argIdx+1) (targetIdx+1) (targets'.push target) + collect (b.instantiate1 target) (argIdx+1) (targetIdx+1) implicits (targets'.push target) else - let implicitTarget ← mkFreshExprMVar d - collect (b.instantiate1 implicitTarget) (argIdx+1) targetIdx (targets'.push implicitTarget) + let implicitTarget ← mkFreshExprMVar (type? := d) (userName := n) + collect (b.instantiate1 implicitTarget) (argIdx+1) targetIdx (implicits.push implicitTarget.mvarId!) (targets'.push implicitTarget) else - collect (b.instantiate1 (← mkFreshExprMVar d)) (argIdx+1) targetIdx targets' + collect (b.instantiate1 (← mkFreshExprMVar d)) (argIdx+1) targetIdx implicits targets' | _ => - return targets' + return (implicits, targets') structure CustomEliminator where typeNames : Array Name - elimInfo : ElimInfo + elimName : Name -- NB: Do not store the ElimInfo, it can contain MVars deriving Inhabited, Repr structure CustomEliminators where - map : SMap (Array Name) ElimInfo := {} + map : SMap (Array Name) Name := {} deriving Inhabited, Repr def addCustomEliminatorEntry (es : CustomEliminators) (e : CustomEliminator) : CustomEliminators := match es with - | { map := map } => { map := map.insert e.typeNames e.elimInfo } + | { map := map } => { map := map.insert e.typeNames e.elimName } builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminator CustomEliminators ← registerSimpleScopedEnvExtension { @@ -112,9 +125,9 @@ builtin_initialize customEliminatorExt : SimpleScopedEnvExtension CustomEliminat finalizeImport := fun { map := map } => { map := map.switch } } -def mkCustomEliminator (declName : Name) : MetaM CustomEliminator := do - let info ← getConstInfo declName - let elimInfo ← getElimInfo declName +def mkCustomEliminator (elimName : Name) : MetaM CustomEliminator := do + let elimInfo ← getElimInfo elimName + let info ← getConstInfo elimName forallTelescopeReducing info.type fun xs _ => do let mut typeNames := #[] for i in [:elimInfo.targetsPos.size] do @@ -134,7 +147,7 @@ def mkCustomEliminator (declName : Name) : MetaM CustomEliminator := do let xType ← inferType x let .const typeName .. := xType.getAppFn | throwError "unexpected eliminator target type{indentExpr xType}" typeNames := typeNames.push typeName - return { typeNames, elimInfo } + return { typeNames, elimName} def addCustomEliminator (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do let e ← mkCustomEliminator declName @@ -151,7 +164,7 @@ builtin_initialize def getCustomEliminators : CoreM CustomEliminators := do return customEliminatorExt.getState (← getEnv) -def getCustomEliminator? (targets : Array Expr) : MetaM (Option ElimInfo) := do +def getCustomEliminator? (targets : Array Expr) : MetaM (Option Name) := do let mut key := #[] for target in targets do let targetType := (← instantiateMVars (← inferType target)).headBeta diff --git a/tests/lean/indUsingTerm.lean b/tests/lean/indUsingTerm.lean new file mode 100644 index 0000000000..223be3e8de --- /dev/null +++ b/tests/lean/indUsingTerm.lean @@ -0,0 +1,225 @@ +namespace Ex0 + +-- NB: no parameter +theorem elim_without_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n := + case1 _ + +example (n : Nat) : n = n := by + induction n using elim_without_param + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using @elim_without_param + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using (elim_without_param) -- Error: unexpected eliminator resulting type + case case1 n => rfl + +end Ex0 + +namespace Ex1 + +-- NB: p before motive +theorem elim_with_param (p : Bool) {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n := + if p then case1 _ else case1 _ + +example (n : Nat) : n = n := by + induction n using elim_with_param + case p => exact true -- uninstantiated parameters becomes goal + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using @elim_with_param + case p => exact true -- uninstantiated parameters becomes goal + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using elim_with_param (p := true) + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using elim_with_param true + case case1 n => rfl + +example (n : Nat) : n = n := by + -- not really a useful idiom, but it better works: + induction n using fun motive case1 n => @elim_with_param true motive case1 n + case case1 n => rfl + +example (n : Nat) : n = n := by + -- NB: no renaming of cases this way? + induction n using fun motive the_case n => @elim_with_param true motive the_case n + case case1 n => rfl + +end Ex1 + +namespace Ex2 + +-- NB: p after motive +theorem elim_with_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) (p : Bool) : motive n := + if p then case1 _ else case1 _ + +example (n : Nat) : n = n := by + induction n using elim_with_param + case p => exact true + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using @elim_with_param + case p => exact true + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using elim_with_param (p := true) + case case1 n => rfl + +example (n : Nat) : n = n := by + induction n using @elim_with_param (p := true) + case case1 n => rfl + +example (n : Nat) : n = n := by + -- This renames the cases with unhelpful names + induction n using elim_with_param _ _ true + case x_1 n => rfl + +example (n : Nat) : n = n := by + -- We can put in custom names + induction n using elim_with_param ?case2 _ true + case case2 n => rfl + +example (n : Nat) : n = n := by + -- not really a useful idiom, but it works: + induction n using fun motive case1 n => @elim_with_param motive case1 n true + case case1 n => rfl + +end Ex2 + +namespace Ex3 + +-- Mutual induction, multiple motives + +mutual +inductive A : Type u where | mkA : B → A | A : A +inductive B : Type u where | mkB : A → B +end + +-- NB: A.rec is configured as elab_as_elim, +-- but in `using` it should not matter + +-- For comparision, a copy without that attribute +noncomputable def A_rec := @A.rec + +set_option linter.unusedVariables false + +example (a : A) : True := by + -- motive_2 becomes a mvar + induction a using A.rec + case mkA b IH => + refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar + exact trivial + case A => exact trivial + case mkB b IH => show True; exact trivial + +example (a : A) : True := by + -- motive_2 becomes a mvar + induction a using A_rec + case mkA b IH => + refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar + exact trivial + case A => exact trivial + case mkB b IH => show True; exact trivial -- Error: type mismatch + +example (a : A) : True := by + -- motive_2 becomes a mvar + induction a using @A.rec + case mkA b IH => + refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar + exact trivial + case A => exact trivial + case mkB b IH => show True; exact trivial + +example (a : A) : True := by + -- motive_2 becomes a mvar + induction a using @A_rec + case mkA b IH => + refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar + exact trivial + case A => exact trivial + case mkB b IH => show True; exact trivial + +example (a : A) : True := by + induction a using fun motive_1 => @A.rec motive_1 (motive_2 := fun b => True) + case mkA b IH => exact trivial + case A => exact trivial + case mkB b IH => exact trivial + +example (a : A) : True := by + induction a using fun motive_1 => @A_rec motive_1 (motive_2 := fun b => True) + case mkA b IH => exact trivial + case A => exact trivial + case mkB b IH => exact trivial + +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 + +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 + +example (a : A) : True := by + -- A.rec is marked elab_as_elim, and normally elaborating + -- #check A.rec (motive_2 := fun b => True) + -- fails with + -- > failed to elaborate eliminator, expected type is not available + -- so we elaborate with heedElabAsElim := false + 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 + +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 + +end Ex3 + +namespace Ex4 + +-- We can use parameters as elaborators + +set_option linter.unusedVariables false in +example + (α : Type u) + (ela : ∀ {motive : α → Prop} (case1 : ∀ (x : α), motive x) (x : α), motive x) + (x : α) + : x = x := by + induction x using ela + case case1 x => rfl + +end Ex4 + +namespace Ex5 + +-- Multiple motives, different number of extra assumptions + +mutual +inductive A : Type u where | mkA : B → A | A : A +inductive B : Type u where | mkB : A → B +end + +set_option linter.unusedVariables false in +example (a : A) : True := by + induction a using A.rec (motive_2 := fun b => (heq : b = b) -> True) + case mkA b IH => exact trivial + case A => exact trivial + case mkB b IH h => exact trivial + +end Ex5 diff --git a/tests/lean/indUsingTerm.lean.expected.out b/tests/lean/indUsingTerm.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/lean/indimpltarget.lean b/tests/lean/indimpltarget.lean index 3008fd14a1..634b7d5b5b 100644 --- a/tests/lean/indimpltarget.lean +++ b/tests/lean/indimpltarget.lean @@ -28,3 +28,16 @@ example (n : Nat) (m : Fin n) : n ≤ m := by case case1 => sorry end Ex3 + +namespace Ex4 + +-- anonymous implicit target + +theorem elim_with_implicit_target (motive : Bool → Nat → Prop) + (case1 : ∀ m k, motive m k) {_ : Bool} (m : Nat) : motive ‹Bool› m := case1 _ _ + +example (n m : Nat) : n ≤ m := by + induction m using elim_with_implicit_target + case case1 => sorry + +end Ex4 diff --git a/tests/lean/indimpltarget.lean.expected.out b/tests/lean/indimpltarget.lean.expected.out index 797357e144..7ccfe0aa0e 100644 --- a/tests/lean/indimpltarget.lean.expected.out +++ b/tests/lean/indimpltarget.lean.expected.out @@ -1,5 +1,4 @@ -indimpltarget.lean:6:2-6:45: error: failed to infer implicit target, it contains unresolved metavariables - ?m -indimpltarget.lean:16:2-16:45: error: failed to infer implicit target, it contains unresolved metavariables - ?m +indimpltarget.lean:6:2-6:45: error: failed to infer implicit target m +indimpltarget.lean:16:2-16:45: error: failed to infer implicit target n indimpltarget.lean:26:0-26:7: warning: declaration uses 'sorry' +indimpltarget.lean:40:2-40:45: error: failed to infer implicit target diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out index ffe26b71ac..502af53f15 100644 --- a/tests/lean/inductionErrors.lean.expected.out +++ b/tests/lean/inductionErrors.lean.expected.out @@ -6,7 +6,7 @@ inductionErrors.lean:12:12-12:27: error: unsolved goals case upper.h q d : Nat ⊢ q + Nat.succ d > q -inductionErrors.lean:16:19-16:26: error: unknown constant 'elimEx2' +inductionErrors.lean:16:19-16:26: error: unknown identifier 'elimEx2' inductionErrors.lean:22:2-25:45: error: insufficient number of targets for 'elimEx' inductionErrors.lean:28:16-28:23: error: unexpected eliminator resulting type Nat