Equations
- Lean.Meta.getCtorNumPropFields ctorInfo = Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs x => let numProps := 0; do let r ← let col := { start := 0, stop := ctorInfo.numFields, step := 1 }; forIn col numProps fun i r => let numProps := r; do let a ← Lean.Meta.inferType (Array.getOp xs (ctorInfo.numParams + i)) let a ← Lean.Meta.isProp a if a = true then let numProps := numProps + 1; do pure PUnit.unit pure (ForInStep.yield numProps) else do pure PUnit.unit pure (ForInStep.yield numProps) let x : Nat := r let numProps : Nat := x pure numProps
- solved: Lean.Meta.InjectionResultCore
- subgoal: Lean.MVarId → Nat → Lean.Meta.InjectionResultCore
Equations
- Lean.Meta.injectionCore mvarId fvarId = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `injection let decl ← Lean.Meta.getLocalDecl fvarId let type ← Lean.Meta.whnf (Lean.LocalDecl.type decl) match Lean.Expr.eq? type with | none => Lean.Meta.throwTacticEx `injection mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "equality expected") Lean.Syntax.missing | some (α, a, b) => do let a ← Lean.Meta.whnf a let b ← Lean.Meta.whnf b let target ← Lean.Meta.getMVarType mvarId let env ← Lean.getEnv let _discr : Option Lean.ConstructorVal := Lean.Expr.isConstructorApp? env b match Lean.Expr.isConstructorApp? env a, Lean.Expr.isConstructorApp? env b with | some aCtor, some bCtor => do let val ← Lean.Meta.mkNoConfusion target (Lean.mkFVar fvarId) if (aCtor.toConstantVal.name != bCtor.toConstantVal.name) = true then do Lean.Meta.assignExprMVar mvarId val pure Lean.Meta.InjectionResultCore.solved else do let valType ← Lean.Meta.inferType val let valType ← Lean.Meta.whnf valType match valType with | Lean.Expr.forallE x newTarget x_1 x_2 => let newTarget := Lean.Expr.headBeta newTarget; do let tag ← Lean.Meta.getMVarTag mvarId let newMVar ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar newTarget tag Lean.Meta.assignExprMVar mvarId (Lean.mkApp val newMVar) let mvarId ← Lean.Meta.tryClear (Lean.Expr.mvarId! newMVar) fvarId let numPropFields ← Lean.Meta.getCtorNumPropFields aCtor pure (Lean.Meta.InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields)) | x => Lean.Meta.throwTacticEx `injection mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "ill-formed noConfusion auxiliary construction") Lean.Syntax.missing | x, x_1 => Lean.Meta.throwTacticEx `injection mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "equality of constructor applications expected") Lean.Syntax.missing
- solved: Lean.Meta.InjectionResult
- subgoal: Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.Meta.InjectionResult
Equations
- Lean.Meta.heqToEq mvarId fvarId tryToClear = Lean.Meta.withMVarContext mvarId do let decl ← Lean.Meta.getLocalDecl fvarId let type ← Lean.Meta.whnf (Lean.LocalDecl.type decl) match Lean.Expr.heq? type with | none => pure (fvarId, mvarId) | some (α, a, β, b) => do let a_1 ← Lean.Meta.isDefEq α β if a_1 = true then do let pr ← Lean.Meta.mkEqOfHEq (Lean.mkFVar fvarId) let eq ← Lean.Meta.mkEq a b let mvarId ← Lean.Meta.assert mvarId (Lean.LocalDecl.userName decl) eq pr let _do_jp : Lean.MVarId → PUnit → Lean.MetaM (Lean.FVarId × Lean.MVarId) := fun mvarId y => do let discr ← Lean.Meta.intro1P mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarId, mvarId') => pure (fvarId, mvarId') if tryToClear = true then do let r ← Lean.Meta.tryClear mvarId fvarId let mvarId : Lean.MVarId := r let y ← pure PUnit.unit _do_jp mvarId y else do let y ← pure PUnit.unit _do_jp mvarId y else pure (fvarId, mvarId)
def
Lean.Meta.injectionIntro
(mvarId : Lean.MVarId)
(numEqs : Nat)
(newNames : List Lean.Name)
(tryToClear : optParam Bool true)
:
Equations
- Lean.Meta.injectionIntro mvarId numEqs newNames tryToClear = (fun go => go numEqs mvarId #[] newNames) (Lean.Meta.injectionIntro.go tryToClear)
Equations
- Lean.Meta.injectionIntro.go tryToClear 0 x x x = pure (Lean.Meta.InjectionResult.subgoal x x x)
- Lean.Meta.injectionIntro.go tryToClear (Nat.succ n) x x (name :: remainingNames) = do let discr ← Lean.Meta.intro x name let x : Lean.FVarId × Lean.MVarId := discr let discr ← Lean.Meta.heqToEq x.2 x.1 tryToClear let x : Lean.FVarId × Lean.MVarId := discr Lean.Meta.injectionIntro.go tryToClear n x.2 (Array.push x x.1) remainingNames
- Lean.Meta.injectionIntro.go tryToClear (Nat.succ n) x x [] = do let discr ← Lean.Meta.intro1 x let x : Lean.FVarId × Lean.MVarId := discr let discr ← Lean.Meta.heqToEq x.2 x.1 tryToClear let x : Lean.FVarId × Lean.MVarId := discr Lean.Meta.injectionIntro.go tryToClear n x.2 (Array.push x x.1) []
def
Lean.Meta.injection
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(newNames : optParam (List Lean.Name) [])
:
Equations
- Lean.Meta.injection mvarId fvarId newNames = do let a ← Lean.Meta.injectionCore mvarId fvarId match a with | Lean.Meta.InjectionResultCore.solved => pure Lean.Meta.InjectionResult.solved | Lean.Meta.InjectionResultCore.subgoal mvarId numEqs => Lean.Meta.injectionIntro mvarId numEqs newNames true
Equations
- Lean.Meta.injections mvarId maxDepth = (fun go => Lean.Meta.withMVarContext mvarId do let a ← Lean.getLCtx let fvarIds : Array Lean.FVarId := Lean.LocalContext.getFVarIds a go maxDepth (Array.toList fvarIds) mvarId) (Lean.Meta.injections.go mvarId)
partial def
Lean.Meta.injections.go
(mvarId : Lean.MVarId)
:
Nat → List Lean.FVarId → Lean.MVarId → Lean.MetaM (Option Lean.MVarId)