Lean.Meta.Tactic.Induction

source

structure Lean.Meta.InductionSubgoal :

Type

mvarId : Lean.MVarId
fields : Array Lean.Expr
subst : Lean.Meta.FVarSubst

source

instance Lean.Meta.instInhabitedInductionSubgoal :

Inhabited Lean.Meta.InductionSubgoal

Equations

Lean.Meta.instInhabitedInductionSubgoal = { default := { mvarId := default, fields := default, subst := default } }

source

structure Lean.Meta.AltVarNames :

Type

explicit : Bool
varNames : List Lean.Name

source

instance Lean.Meta.instInhabitedAltVarNames :

Inhabited Lean.Meta.AltVarNames

Equations

Lean.Meta.instInhabitedAltVarNames = { default := { explicit := default, varNames := default } }

source

def Lean.Meta.induction (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (recursorName : Lean.Name) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :

Lean.MetaM (Array Lean.Meta.InductionSubgoal)

Equations

Lean.Meta.induction mvarId majorFVarId recursorName givenNames = Lean.Meta.withMVarContext mvarId (let cls := `Meta.Tactic.induction; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Array Lean.Meta.InductionSubgoal) := fun y => do Lean.Meta.checkNotAssigned mvarId `induction let majorLocalDecl ← Lean.Meta.getLocalDecl majorFVarId let recursorInfo ← Lean.Meta.mkRecursorInfo recursorName none let discr ← Lean.Meta.whnfUntil (Lean.LocalDecl.type majorLocalDecl) recursorInfo.typeName match discr with | some majorType => Lean.Expr.withApp majorType fun x majorTypeArgs => do List.forM recursorInfo.paramsPos fun paramPos? => match paramPos? with | none => pure () | some paramPos => if paramPos ≥ Array.size majorTypeArgs then Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "major premise type is ill-formed" ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing else pure PUnit.unit let mctx ← Lean.getMCtx let indices ← Array.mapM (fun idxPos => let _do_jp := fun y => let idx := Array.get! majorTypeArgs idxPos; let _do_jp := fun y => do Nat.forM (Array.size majorTypeArgs) fun i => let arg := Array.getOp majorTypeArgs i; let _do_jp := fun y => let _do_jp := fun y => if (decide (i > idxPos) && List.contains recursorInfo.indicesPos i && Lean.Expr.isFVar arg) = true then do let idxDecl ← Lean.Meta.getLocalDecl (Lean.Expr.fvarId! idx) if Lean.MetavarContext.localDeclDependsOn mctx idxDecl (Lean.Expr.fvarId! arg) = true then Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "'" ++ Lean.toMessageData idx ++ Lean.toMessageData "' is an index in major premise, but it depends on index occurring at position #" ++ Lean.toMessageData (i + 1) ++ Lean.toMessageData "") Lean.Syntax.missing else pure PUnit.unit else pure PUnit.unit; if (decide (i < idxPos) && Lean.MetavarContext.exprDependsOn mctx arg (Lean.Expr.fvarId! idx)) = true then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "'" ++ Lean.toMessageData idx ++ Lean.toMessageData "' is an index in major premise, but it occurs in previous arguments" ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y; if (i != idxPos && arg == idx) = true then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "'" ++ Lean.toMessageData idx ++ Lean.toMessageData "' is an index in major premise, but it occurs more than once" ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y pure idx; if Lean.Expr.isFVar idx = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "major premise type index " ++ Lean.toMessageData idx ++ Lean.toMessageData " is not a variable" ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y; if idxPos ≥ Array.size majorTypeArgs then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "major premise type is ill-formed" ++ Lean.toMessageData (Lean.indentExpr majorType) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y) (List.toArray recursorInfo.indicesPos) let target ← Lean.Meta.getMVarType mvarId let _do_jp : PUnit → Lean.MetaM (Array Lean.Meta.InductionSubgoal) := fun y => do let discr ← Lean.Meta.revert mvarId (Array.push (Array.map Lean.Expr.fvarId! indices) majorFVarId) true let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (reverted, mvarId) => do let discr ← Lean.Meta.introNP mvarId (Array.size indices) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (indices', mvarId) => do let discr ← Lean.Meta.intro1P mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (majorFVarId', mvarId) => let baseSubst := Id.run (let subst := { map := ∅ }; let i := 0; do let r ← forIn indices { fst := subst, snd := i } fun index r => let subst := r.fst; let i := r.snd; let subst := Lean.Meta.FVarSubst.insert subst (Lean.Expr.fvarId! index) (Lean.mkFVar (Array.getOp indices' i)); let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := subst, snd := i }) let x : MProd Lean.Meta.FVarSubst Nat := r match x with | { fst := subst, snd := i } => pure subst); let cls := `Meta.Tactic.induction; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Array Lean.Meta.InductionSubgoal) := fun y => let indices := Array.map Lean.mkFVar indices'; let majorFVarId := majorFVarId'; let major := Lean.mkFVar majorFVarId; Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType mvarId let targetLevel ← Lean.Meta.getLevel target let targetLevel ← Lean.Meta.normalizeLevel targetLevel let majorLocalDecl ← Lean.Meta.getLocalDecl majorFVarId let discr ← Lean.Meta.whnfUntil (Lean.LocalDecl.type majorLocalDecl) recursorInfo.typeName match discr with | some majorType => Lean.Expr.withApp majorType fun majorTypeFn majorTypeArgs => match majorTypeFn with | Lean.Expr.const majorTypeFnName majorTypeFnLevels x => let majorTypeFnLevels := List.toArray majorTypeFnLevels; do let discr ← List.foldlM (fun x univPos => match x with | (recursorLevels, foundTargetLevel) => match univPos with | Lean.Meta.RecursorUnivLevelPos.motive => pure (Array.push recursorLevels targetLevel, true) | Lean.Meta.RecursorUnivLevelPos.majorType idx => let _do_jp := fun y => pure (Array.push recursorLevels (Array.get! majorTypeFnLevels idx), foundTargetLevel); if idx ≥ Array.size majorTypeFnLevels then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "ill-formed recursor") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y) (#[], false) recursorInfo.univLevelPos let x : Array Lean.Level × Bool := discr match x with | (recursorLevels, foundTargetLevel) => let _do_jp := fun y => let recursor := Lean.mkConst recursorName (Array.toList recursorLevels); do let recursor ← Lean.Meta.addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor let motive : Lean.Expr := target let _do_jp : Lean.Expr → Lean.MetaM (Array Lean.Meta.InductionSubgoal) := fun motive => do let motive ← Lean.Meta.mkLambdaFVars indices motive false true let recursor : Lean.Expr := Lean.mkApp recursor motive Lean.Meta.finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor if recursorInfo.depElim = true then do let a ← Lean.Meta.inferType major let a_1 ← Lean.Meta.abstract motive #[major] let y ← pure (Lean.mkLambda `x Lean.BinderInfo.default a a_1) _do_jp y else do let y ← pure motive _do_jp y; if (!foundTargetLevel && !Lean.Level.isZero targetLevel) = true then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "recursor '" ++ Lean.toMessageData recursorName ++ Lean.toMessageData "' can only eliminate into Prop") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => Lean.Meta.throwTacticEx `induction mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "major premise is not of the form (C ...)") Lean.Syntax.missing | x => Lean.Meta.throwUnexpectedMajorType mvarId (Lean.LocalDecl.type majorLocalDecl) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "after revert&intro\n" ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if (!recursorInfo.depElim && Lean.MetavarContext.exprDependsOn mctx target majorFVarId) = true then do let y ← Lean.Meta.throwTacticEx `induction mvarId (Lean.toMessageData "recursor '" ++ Lean.toMessageData recursorName ++ Lean.toMessageData "' does not support dependent elimination, but conclusion depends on major premise") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => Lean.Meta.throwUnexpectedMajorType mvarId (Lean.LocalDecl.type majorLocalDecl) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "initial\n" ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y)