def
Lean.Meta.substCore
(mvarId : Lean.MVarId)
(hFVarId : Lean.FVarId)
(symm : optParam Bool false)
(fvarSubst : optParam Lean.Meta.FVarSubst { map := ∅ })
(clearH : optParam Bool true)
(tryToSkip : optParam Bool false)
:
Equations
- Lean.Meta.substCore mvarId hFVarId symm fvarSubst clearH tryToSkip = Lean.Meta.withMVarContext mvarId do let tag ← Lean.Meta.getMVarTag mvarId Lean.Meta.checkNotAssigned mvarId `subst let hFVarIdOriginal : Lean.FVarId := hFVarId let hLocalDecl ← Lean.Meta.getLocalDecl hFVarId let a ← Lean.Meta.matchEq? (Lean.LocalDecl.type hLocalDecl) match a with | none => Lean.Meta.throwTacticEx `subst mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "argument must be an equality proof") Lean.Syntax.missing | some (α, lhs, rhs) => do let a ← Lean.Meta.instantiateMVars (if symm = true then rhs else lhs) let b ← Lean.Meta.instantiateMVars (if symm = true then lhs else rhs) match a with | Lean.Expr.fvar aFVarId x => let aFVarIdOriginal := aFVarId; let cls := `Meta.Tactic.subst; do let a_1 ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => do let mctx ← Lean.getMCtx let _do_jp : PUnit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => do let _ ← Lean.Meta.getLocalDecl aFVarId let discr ← Lean.Meta.revert mvarId #[aFVarId, hFVarId] true let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (vars, mvarId) => let cls := `Meta.Tactic.subst; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => do let discr ← Lean.Meta.introNP mvarId 2 let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (twoVars, mvarId) => let cls := `Meta.Tactic.subst; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => let cls := `Meta.Tactic.subst; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => let aFVarId := Array.getOp twoVars 0; let a := Lean.mkFVar aFVarId; let hFVarId := Array.getOp twoVars 1; let h := Lean.mkFVar hFVarId; let _do_jp := fun skip => if skip = true then if clearH = true then do let mvarId ← Lean.Meta.clear mvarId hFVarId let mvarId ← Lean.Meta.clear mvarId aFVarId pure ({ map := ∅ }, mvarId) else pure ({ map := ∅ }, mvarId) else Lean.Meta.withMVarContext mvarId do let mvarDecl ← Lean.Meta.getMVarDecl mvarId let type : Lean.Expr := mvarDecl.type let hLocalDecl ← Lean.Meta.getLocalDecl hFVarId let a_2 ← Lean.Meta.matchEq? (Lean.LocalDecl.type hLocalDecl) match a_2 with | none => panicWithPosWithDecl "Lean.Meta.Tactic.Subst" "Lean.Meta.substCore" 66 22 "unreachable code has been reached" | some (α, lhs, rhs) => do let b ← Lean.Meta.instantiateMVars (if symm = true then lhs else rhs) let mctx ← Lean.getMCtx let depElim : Bool := Lean.MetavarContext.exprDependsOn mctx mvarDecl.type hFVarId let cont : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun motive newType => let _do_jp := fun major => do let newMVar ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar newType tag let minor : Lean.Expr := newMVar let _do_jp : Lean.Expr → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun newVal => do Lean.Meta.assignExprMVar mvarId newVal let mvarId : Lean.MVarId := Lean.Expr.mvarId! newMVar let _do_jp : Lean.MVarId → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun mvarId => do let discr ← Lean.Meta.introNP mvarId (Array.size vars - 2) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (newFVars, mvarId) => let cls := `Meta.Tactic.subst; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Meta.FVarSubst × Lean.MVarId) := fun y => do let fvarSubst ← Nat.foldM (fun i fvarSubst => let var := Array.getOp vars (i + 2); let newFVar := Array.getOp newFVars i; pure (Lean.Meta.FVarSubst.insert fvarSubst var (Lean.mkFVar newFVar))) fvarSubst (Array.size newFVars) let fvarSubst : Lean.Meta.FVarSubst := Lean.Meta.FVarSubst.insert fvarSubst aFVarIdOriginal (if clearH = true then b else Lean.mkFVar aFVarId) let fvarSubst : Lean.Meta.FVarSubst := Lean.Meta.FVarSubst.insert fvarSubst hFVarIdOriginal (Lean.mkFVar hFVarId) pure (fvarSubst, mvarId) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "after intro rest " ++ Lean.toMessageData (Array.size vars - 2) ++ Lean.toMessageData " " ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if clearH = true then do let mvarId ← Lean.Meta.clear mvarId hFVarId let y ← Lean.Meta.clear mvarId aFVarId _do_jp y else do let y ← pure mvarId _do_jp y if depElim = true then do let y ← Lean.Meta.mkEqRec motive minor major _do_jp y else do let y ← Lean.Meta.mkEqNDRec motive minor major _do_jp y; if symm = true then do let y ← pure h _do_jp y else do let y ← Lean.Meta.mkEqSymm h _do_jp y if depElim = true then let newType := Lean.Expr.replaceFVar type a b; do let reflB ← Lean.Meta.mkEqRefl b let newType : Lean.Expr := Lean.Expr.replaceFVar newType h reflB if symm = true then do let motive ← Lean.Meta.mkLambdaFVars #[a, h] type false true cont motive newType else do let hAuxType ← Lean.Meta.mkEq b a let motive ← Lean.Meta.withLocalDeclD `_h hAuxType fun hAux => do let hAuxSymm ← Lean.Meta.mkEqSymm hAux let newType : Lean.Expr := Lean.Expr.replaceFVar type h hAuxSymm Lean.Meta.mkLambdaFVars #[a, hAux] newType false true cont motive newType else do let motive ← Lean.Meta.mkLambdaFVars #[a] type false true let newType : Lean.Expr := Lean.Expr.replaceFVar type a b cont motive newType; if (!tryToSkip || Array.size vars != 2) = true then do let y ← pure false _do_jp y else do let mvarType ← Lean.Meta.getMVarType mvarId let mctx ← Lean.getMCtx let y ← pure (!Lean.MetavarContext.exprDependsOn mctx mvarType aFVarId && !Lean.MetavarContext.exprDependsOn mctx mvarType hFVarId) _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "reverted variables " ++ Lean.toMessageData (Array.map (fun a => a.name) vars) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "after intro2 " ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "after revert " ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if Lean.MetavarContext.exprDependsOn mctx b aFVarId = true then do let y ← Lean.Meta.throwTacticEx `subst mvarId (Lean.toMessageData "'" ++ Lean.toMessageData a ++ Lean.toMessageData "' occurs at" ++ Lean.toMessageData (Lean.indentExpr b) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y if a_1 = true then do let y ← Lean.addTrace cls (Lean.toMessageData "substituting " ++ Lean.toMessageData a ++ Lean.toMessageData " (id: " ++ Lean.toMessageData aFVarId.name ++ Lean.toMessageData ") with " ++ Lean.toMessageData b ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => let eqMsg := if symm = true then "(t = x)" else "(x = t)"; Lean.Meta.throwTacticEx `subst mvarId (Lean.toMessageData "invalid equality proof, it is not of the form " ++ Lean.toMessageData eqMsg ++ Lean.toMessageData "" ++ Lean.toMessageData (Lean.indentExpr (Lean.LocalDecl.type hLocalDecl)) ++ Lean.toMessageData "\nafter WHNF, variable expected, but obtained" ++ Lean.toMessageData (Lean.indentExpr a) ++ Lean.toMessageData "") Lean.Syntax.missing
Equations
- Lean.Meta.subst mvarId hFVarId = Lean.Meta.withMVarContext mvarId do let hLocalDecl ← Lean.Meta.getLocalDecl hFVarId let a ← Lean.Meta.matchEq? (Lean.LocalDecl.type hLocalDecl) match a with | some (α, lhs, rhs) => let substReduced := fun newType symm => do let mvarId ← Lean.Meta.assert mvarId (Lean.LocalDecl.userName hLocalDecl) newType (Lean.mkFVar hFVarId) let discr ← Lean.Meta.intro1P mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (hFVarId', mvarId) => do let mvarId ← Lean.Meta.clear mvarId hFVarId let a ← Lean.Meta.substCore mvarId hFVarId' symm { map := ∅ } true true pure a.snd; do let rhs' ← Lean.Meta.whnf rhs if Lean.Expr.isFVar rhs' = true then if (rhs != rhs') = true then do let a ← Lean.Meta.mkEq lhs rhs' substReduced a true else do let a ← Lean.Meta.substCore mvarId hFVarId true { map := ∅ } true true pure a.snd else do let lhs' ← Lean.Meta.whnf lhs if Lean.Expr.isFVar lhs' = true then if (lhs != lhs') = true then do let a ← Lean.Meta.mkEq lhs' rhs substReduced a false else do let a ← Lean.Meta.substCore mvarId hFVarId false { map := ∅ } true true pure a.snd else Lean.Meta.throwTacticEx `subst mvarId (Lean.toMessageData "invalid equality proof, it is not of the form (x = t) or (t = x)" ++ Lean.toMessageData (Lean.indentExpr (Lean.LocalDecl.type hLocalDecl)) ++ Lean.toMessageData "") Lean.Syntax.missing | none => let _do_jp := fun y => do let mctx ← Lean.getMCtx let lctx ← Lean.getLCtx let discr ← Lean.LocalContext.findDeclM? lctx fun localDecl => if Lean.LocalDecl.isAuxDecl localDecl = true then pure none else do let a ← Lean.Meta.matchEq? (Lean.LocalDecl.type localDecl) match a with | some (α, lhs, rhs) => if (Lean.Expr.isFVar rhs && Lean.Expr.fvarId! rhs == hFVarId && !Lean.MetavarContext.exprDependsOn mctx lhs hFVarId) = true then pure (some (Lean.LocalDecl.fvarId localDecl, true)) else if (Lean.Expr.isFVar lhs && Lean.Expr.fvarId! lhs == hFVarId && !Lean.MetavarContext.exprDependsOn mctx rhs hFVarId) = true then pure (some (Lean.LocalDecl.fvarId localDecl, false)) else pure none | x => pure none match discr with | some (fvarId, symm) => do let a ← Lean.Meta.substCore mvarId fvarId symm { map := ∅ } true true pure a.snd | x => Lean.Meta.throwTacticEx `subst mvarId (Lean.toMessageData "did not find equation for eliminating '" ++ Lean.toMessageData (Lean.mkFVar hFVarId) ++ Lean.toMessageData "'") Lean.Syntax.missing; if Lean.LocalDecl.isLet hLocalDecl = true then do let y ← Lean.Meta.throwTacticEx `subst mvarId (Lean.toMessageData "variable '" ++ Lean.toMessageData (Lean.mkFVar hFVarId) ++ Lean.toMessageData "' is a let-declaration") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Meta.subst? mvarId hFVarId = Lean.observing? (Lean.Meta.subst mvarId hFVarId)
Equations
- Lean.Meta.trySubst mvarId hFVarId = do let a ← Lean.Meta.subst? mvarId hFVarId match a with | some mvarId => pure mvarId | none => pure mvarId
Equations
- Lean.Meta.substSomeVar? 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 ← Lean.Meta.subst? mvarId (Lean.LocalDecl.fvarId localDecl) match a with | some mvarId => pure (ForInStep.done { fst := some (some mvarId), snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (Option Lean.MVarId) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a