Lean.Meta.Tactic.Cases

source

def Lean.Meta.getInductiveUniverseAndParams (type : Lean.Expr) :

Lean.MetaM (List Lean.Level × Array Lean.Expr)

Equations

Lean.Meta.getInductiveUniverseAndParams type = do let type ← Lean.Meta.whnfD type Lean.matchConstInduct (Lean.Expr.getAppFn type) (fun x => Lean.Meta.throwInductiveTypeExpected type) fun val us => let I := Lean.Expr.getAppFn type; let Iargs := Lean.Expr.getAppArgs type; let params := Array.extract Iargs 0 val.numParams; pure (us, params)

source

def Lean.Meta.generalizeTargetsEq (mvarId : Lean.MVarId) (motiveType : Lean.Expr) (targets : Array Lean.Expr) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.generalizeTargetsEq mvarId motiveType targets = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `generalizeTargets let discr ← Lean.Meta.forallTelescopeReducing motiveType fun targetsNew x => let _do_jp := fun y => Lean.Meta.withNewEqs targets targetsNew fun eqs eqRefls => do let type ← Lean.Meta.getMVarType mvarId let typeNew ← Lean.Meta.mkForallFVars eqs type false true let typeNew ← Lean.Meta.mkForallFVars targetsNew typeNew false true pure (typeNew, eqRefls); if (Array.size targetsNew == Array.size targets) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid number of targets #" ++ Lean.toMessageData (Array.size targets) ++ Lean.toMessageData ", motive expects #" ++ Lean.toMessageData (Array.size targetsNew) ++ Lean.toMessageData "") _do_jp y let x : Lean.Expr × Array Lean.Expr := discr match x with | (typeNew, eqRefls) => do let a ← Lean.Meta.getMVarTag mvarId let mvarNew ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar typeNew a Lean.Meta.assignExprMVar mvarId (Lean.mkAppN (Lean.mkAppN mvarNew targets) eqRefls) pure (Lean.Expr.mvarId! mvarNew)

source

structure Lean.Meta.GeneralizeIndicesSubgoal :

Type

mvarId : Lean.MVarId
indicesFVarIds : Array Lean.FVarId
fvarId : Lean.FVarId
numEqs : Nat

source

def Lean.Meta.generalizeIndices (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :

Lean.MetaM Lean.Meta.GeneralizeIndicesSubgoal

Equations

Lean.Meta.generalizeIndices mvarId fvarId = Lean.Meta.withMVarContext mvarId do let lctx ← Lean.getLCtx let localInsts ← Lean.Meta.getLocalInstances Lean.Meta.checkNotAssigned mvarId `generalizeIndices let fvarDecl ← Lean.Meta.getLocalDecl fvarId let type ← Lean.Meta.whnf (Lean.LocalDecl.type fvarDecl) Lean.Expr.withApp type fun f args => Lean.matchConstInduct f (fun x => Lean.Meta.throwTacticEx `generalizeIndices mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "inductive type expected") Lean.Syntax.missing) fun val x => let _do_jp := fun y => let _do_jp := fun y => let indices := Array.extract args (Array.size args - val.numIndices) (Array.size args); let IA := Lean.mkAppN f (Array.extract args 0 val.numParams); do let IAType ← Lean.Meta.inferType IA Lean.Meta.forallTelescopeReducing IAType fun newIndices x => let newType := Lean.mkAppN IA newIndices; Lean.Meta.withLocalDeclD (Lean.LocalDecl.userName fvarDecl) newType fun h' => Lean.Meta.withNewEqs indices newIndices fun newEqs newRefls => do let discr ← Lean.Meta.mkEqAndProof (Lean.LocalDecl.toExpr fvarDecl) h' let x : Lean.Expr × Lean.Expr := discr match x with | (newEqType, newRefl) => let newRefls := Array.push newRefls newRefl; Lean.Meta.withLocalDeclD `h newEqType fun newEq => let newEqs := Array.push newEqs newEq; do let target ← Lean.Meta.getMVarType mvarId let tag ← Lean.Meta.getMVarTag mvarId let auxType ← Lean.Meta.mkForallFVars newEqs target false true let auxType ← Lean.Meta.mkForallFVars #[h'] auxType false true let auxType ← Lean.Meta.mkForallFVars newIndices auxType false true let newMVar ← Lean.Meta.mkFreshExprMVarAt lctx localInsts auxType Lean.MetavarKind.syntheticOpaque tag 0 Lean.Meta.assignExprMVar mvarId (Lean.mkAppN (Lean.mkApp (Lean.mkAppN newMVar indices) (Lean.LocalDecl.toExpr fvarDecl)) newRefls) let discr ← Lean.Meta.introNP (Lean.Expr.mvarId! newMVar) (Array.size newIndices) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (indicesFVarIds, newMVarId) => do let discr ← Lean.Meta.intro1P newMVarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarId, newMVarId) => pure { mvarId := newMVarId, indicesFVarIds := indicesFVarIds, fvarId := fvarId, numEqs := Array.size newEqs }; if (Array.size args == val.numIndices + val.numParams) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `generalizeIndices mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "ill-formed inductive datatype") Lean.Syntax.missing _do_jp y; if val.numIndices > 0 then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `generalizeIndices mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "indexed inductive type expected") Lean.Syntax.missing _do_jp y

source

structure Lean.Meta.CasesSubgoal extends Lean.Meta.InductionSubgoal :

Type

ctorName : Lean.Name

source

structure Lean.Meta.Cases.Context :

Type

inductiveVal : Lean.InductiveVal
casesOnVal : Lean.DefinitionVal
nminors : Nat
majorDecl : Lean.LocalDecl
majorTypeFn : Lean.Expr
majorTypeArgs : Array Lean.Expr
majorTypeIndices : Array Lean.Expr

source

partial def Lean.Meta.Cases.unifyEqs (numEqs : Nat) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (caseName? : optParam (Option Lean.Name) none) :

Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))

source

partial def Lean.Meta.Cases.unifyEqs.substEq (numEqs : Nat) (subst : Lean.Meta.FVarSubst) (caseName? : optParam (Option Lean.Name) none) (eqFVarId : Lean.FVarId) (mvarId : Lean.MVarId) (eqDecl : Lean.LocalDecl) (a : Lean.Expr) (b : Lean.Expr) (symm : Bool) :

Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))

source

partial def Lean.Meta.Cases.unifyEqs.injection (numEqs : Nat) (subst : Lean.Meta.FVarSubst) (caseName? : optParam (Option Lean.Name) none) (eqFVarId : Lean.FVarId) (mvarId : Lean.MVarId) (eqDecl : Lean.LocalDecl) (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))

source

def Lean.Meta.Cases.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :

Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Equations

Lean.Meta.Cases.cases mvarId majorFVarId givenNames = tryCatch (Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `cases let context? ← Lean.Meta.Cases.mkCasesContext? majorFVarId match context? with | none => Lean.Meta.throwTacticEx `cases mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "not applicable to the given hypothesis") Lean.Syntax.missing | some ctx => if (ctx.inductiveVal.numIndices == 0) = true then Lean.Meta.Cases.inductionCasesOn mvarId majorFVarId givenNames ctx else do let s₁ ← Lean.Meta.generalizeIndices mvarId majorFVarId let cls : Lean.Name := `Meta.Tactic.cases let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Array Lean.Meta.CasesSubgoal) := fun y => do let s₂ ← Lean.Meta.Cases.inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx let s₂ ← Lean.Meta.Cases.elimAuxIndices s₁ s₂ Lean.Meta.Cases.unifyCasesEqs s₁.numEqs s₂ if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "after generalizeIndices\n" ++ Lean.toMessageData (Lean.MessageData.ofGoal s₁.mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) fun ex => Lean.Meta.throwNestedTacticEx `cases ex

source

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

Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Equations

Lean.Meta.cases mvarId majorFVarId givenNames = Lean.Meta.Cases.cases mvarId majorFVarId givenNames

source

def Lean.Meta.casesRec (mvarId : Lean.MVarId) (p : Lean.LocalDecl → Lean.MetaM Bool) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.casesRec mvarId p = Lean.Meta.saturate mvarId fun mvarId => Lean.Meta.withMVarContext mvarId do let a ← Lean.getLCtx let r ← let col := a; forIn col { fst := none, snd := PUnit.unit } fun localDecl r => let r := r.snd; do let a ← p localDecl if a = true then do let r? ← Lean.observing? do let r ← Lean.Meta.cases mvarId (Lean.LocalDecl.fvarId localDecl) #[] pure (List.map (fun a => a.toInductionSubgoal.mvarId) (Array.toList r)) if Option.isSome r? = true then pure (ForInStep.done { fst := some r?, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (Option (List Lean.MVarId)) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

def Lean.Meta.casesAnd (mvarId : Lean.MVarId) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.casesAnd mvarId = do let mvarIds ← Lean.Meta.casesRec mvarId fun localDecl => do let a ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) pure (Lean.Expr.isAppOfArity a `And 2) Lean.Meta.exactlyOne mvarIds (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected number of goals")

source

def Lean.Meta.substEqs (mvarId : Lean.MVarId) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.substEqs mvarId = do let mvarIds ← Lean.Meta.casesRec mvarId fun localDecl => do let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) pure (Lean.Expr.isEq type || Lean.Expr.isHEq type) Lean.Meta.exactlyOne mvarIds (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected number of goals")

source

structure Lean.Meta.ByCasesSubgoal :

Type

mvarId : Lean.MVarId
fvarId : Lean.FVarId

source

def Lean.Meta.byCases (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : optParam Lean.Name `h) :

Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)

Equations

Lean.Meta.byCases mvarId p hName = (fun toByCasesSubgoal => do let mvarId ← Lean.Meta.assert mvarId `hByCases (Lean.mkOr p (Lean.mkNot p)) (Lean.mkEM p) let discr ← Lean.Meta.intro1 mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarId, mvarId) => do let discr ← Lean.Meta.cases mvarId fvarId #[{ explicit := false, varNames := [hName] }, { explicit := false, varNames := [hName] }] match discr with | #[s₁, s₂] => do let a ← toByCasesSubgoal s₁ let a_1 ← toByCasesSubgoal s₂ pure (a, a_1) | x => Lean.throwError (Lean.toMessageData "'byCases' tactic failed, unexpected number of subgoals")) Lean.Meta.byCases.toByCasesSubgoal

source

def Lean.Meta.byCases.toByCasesSubgoal (s : Lean.Meta.CasesSubgoal) :

Lean.MetaM Lean.Meta.ByCasesSubgoal

Equations

Lean.Meta.byCases.toByCasesSubgoal s = do let discr ← pure s.toInductionSubgoal.fields match discr with | #[Lean.Expr.fvar fvarId x] => pure { mvarId := s.toInductionSubgoal.mvarId, fvarId := fvarId } | x => Lean.throwError (Lean.toMessageData "'byCases' tactic failed, unexpected new hypothesis")