Lean.Meta.Tactic.Simp.Main

Equations

Lean.Meta.Simp.throwCongrHypothesisFailed = throw (Lean.Exception.internal Lean.Meta.Simp.congrHypothesisExceptionId)

source

def Lean.Meta.Simp.Result.getProof (r : Lean.Meta.Simp.Result) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.Simp.Result.getProof r = match r.proof? with | some p => pure p | none => Lean.Meta.mkEqRefl r.expr

source

def Lean.Meta.Simp.mkCongrFun (r : Lean.Meta.Simp.Result) (a : Lean.Expr) :

Lean.MetaM Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.mkCongrFun r a = match r.proof? with | none => pure { expr := Lean.mkApp r.expr a, proof? := none } | some h => do let a ← Lean.Meta.mkCongrFun h a pure { expr := Lean.mkApp r.expr a, proof? := some a }

source

def Lean.Meta.Simp.mkCongr (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) :

Lean.MetaM Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.mkCongr r₁ r₂ = let e := Lean.mkApp r₁.expr r₂.expr; let _discr := r₂.proof?; match r₁.proof?, r₂.proof? with | none, none => pure { expr := e, proof? := none } | some h, none => do let a ← Lean.Meta.mkCongrFun h r₂.expr pure { expr := e, proof? := some a } | none, some h => do let a ← Lean.Meta.mkCongrArg r₁.expr h pure { expr := e, proof? := some a } | some h₁, some h₂ => do let a ← Lean.Meta.mkCongr h₁ h₂ pure { expr := e, proof? := some a }

source

def Lean.Meta.Simp.isOfNatNatLit (e : Lean.Expr) :

Bool

Equations

Lean.Meta.Simp.isOfNatNatLit e = (Lean.Expr.isAppOfArity e `OfNat.ofNat 3 && Lean.Expr.isNatLit (Lean.Expr.appArg! (Lean.Expr.appFn! e)))

source

inductive Lean.Meta.Simp.SimpLetCase :

Type

dep: Lean.Meta.Simp.SimpLetCase
nondepDepVar: Lean.Meta.Simp.SimpLetCase
nondep: Lean.Meta.Simp.SimpLetCase

source

def Lean.Meta.Simp.getSimpLetCase (n : Lean.Name) (t : Lean.Expr) (v : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Meta.Simp.SimpLetCase

Equations

Lean.Meta.Simp.getSimpLetCase n t v b = Lean.Meta.withLocalDeclD n t fun x => let bx := Lean.Expr.instantiate1 b x; do let a ← Lean.Meta.isTypeCorrect bx if a = true then do let a ← Lean.Meta.inferType bx let bxType ← Lean.Meta.whnf a let a ← Lean.Meta.dependsOn bxType (Lean.Expr.fvarId! x) if a = true then pure Lean.Meta.Simp.SimpLetCase.nondepDepVar else pure Lean.Meta.Simp.SimpLetCase.nondep else pure Lean.Meta.Simp.SimpLetCase.dep

source

partial def Lean.Meta.Simp.simp (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpLoop (e : Lean.Expr) (r : Lean.Meta.Simp.Result) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpStep (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

def Lean.Meta.Simp.simp.simpLit (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.simp.simpLit e = match Lean.Expr.natLit? e with | some n => do let a ← Lean.Meta.Simp.getSimpLemmas if Lean.Meta.SimpLemmas.isDeclToUnfold a `OfNat.ofNat = true then pure { expr := e, proof? := none } else do let a ← liftM (Lean.Meta.mkNumeral (Lean.mkConst `Nat) n) pure { expr := a, proof? := none } | none => pure { expr := e, proof? := none }

source

partial def Lean.Meta.Simp.simp.simpProj (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.congrArgs (r : Lean.Meta.Simp.Result) (args : Array Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.congrDefault (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.processCongrHypothesis (h : Lean.Expr) :

Lean.Meta.Simp.M Bool

source

partial def Lean.Meta.Simp.simp.tryCongrLemma? (c : Lean.Meta.CongrLemma) (e : Lean.Expr) :

Lean.Meta.Simp.M (Option Lean.Meta.Simp.Result)

source

partial def Lean.Meta.Simp.simp.congr (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpApp (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

def Lean.Meta.Simp.simp.simpConst (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.simp.simpConst e = do let a ← liftM (Lean.Meta.Simp.reduce e) pure { expr := a, proof? := none }

source

def Lean.Meta.Simp.simp.withNewLemmas {α : Type} (xs : Array Lean.Expr) (f : Lean.Meta.Simp.M α) :

Lean.Meta.Simp.M α

Equations

Lean.Meta.Simp.simp.withNewLemmas xs f = do let a ← Lean.Meta.Simp.getConfig if a.contextual = true then do let s ← Lean.Meta.Simp.getSimpLemmas let updated : Bool := false let r ← forIn xs { fst := s, snd := updated } fun x r => let s := r.fst; let updated := r.snd; do let a ← liftM (Lean.Meta.isProof x) if a = true then do let r ← liftM (Lean.Meta.SimpLemmas.add s #[] x false true 1000 none) let s : Lean.Meta.SimpLemmas := r let updated : Bool := true pure PUnit.unit pure (ForInStep.yield { fst := s, snd := updated }) else do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := updated }) let x : MProd Lean.Meta.SimpLemmas Bool := r match x with | { fst := s, snd := updated } => if updated = true then Lean.Meta.Simp.withSimpLemmas s f else f else f

source

partial def Lean.Meta.Simp.simp.simpLambda (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpArrow (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpForall (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

partial def Lean.Meta.Simp.simp.simpLet (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

source

def Lean.Meta.Simp.simp.cacheResult (e : Lean.Expr) (cfg : Lean.Meta.Simp.Config) (r : Lean.Meta.Simp.Result) :

Lean.Meta.Simp.M Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.simp.cacheResult e cfg r = let _do_jp := fun y => pure r; if cfg.memoize = true then do let y ← modify fun s => { cache := Std.HashMap.insert s.cache e r, numSteps := s.numSteps } _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.Simp.main (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (methods : optParam Lean.Meta.Simp.Methods { pre := fun e => pure (Lean.Meta.Simp.Step.visit { expr := e, proof? := none }), post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none }), discharge? := fun e => pure none }) :

Lean.MetaM Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.main e ctx methods = Lean.Meta.withConfig (fun c => { foApprox := c.foApprox, ctxApprox := c.ctxApprox, quasiPatternApprox := c.quasiPatternApprox, constApprox := c.constApprox, isDefEqStuckEx := c.isDefEqStuckEx, transparency := c.transparency, zetaNonDep := c.zetaNonDep, trackZeta := c.trackZeta, unificationHints := c.unificationHints, proofIrrelevance := c.proofIrrelevance, assignSyntheticOpaque := c.assignSyntheticOpaque, ignoreLevelMVarDepth := c.ignoreLevelMVarDepth, offsetCnstrs := c.offsetCnstrs, etaStruct := ctx.config.etaStruct }) (Lean.Meta.withReducible (StateRefT'.run' (Lean.Meta.Simp.simp e methods ctx) { cache := ∅, numSteps := 0 }))

source

def Lean.Meta.Simp.isEqnThmHypothesis (e : Lean.Expr) :

Bool

Equations

Lean.Meta.Simp.isEqnThmHypothesis e = (fun go => Lean.Expr.isForall e && go e) Lean.Meta.Simp.isEqnThmHypothesis.go

source

partial def Lean.Meta.Simp.isEqnThmHypothesis.go (e : Lean.Expr) :

Bool

source

@[inline]

abbrev Lean.Meta.Simp.Discharge :

Type

Equations

Lean.Meta.Simp.Discharge = (Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))

source

def Lean.Meta.Simp.dischargeUsingAssumption (e : Lean.Expr) :

Lean.Meta.SimpM (Option Lean.Expr)

Equations

Lean.Meta.Simp.dischargeUsingAssumption e = do let a ← Lean.getLCtx Lean.LocalContext.findDeclRevM? a fun localDecl => if Lean.LocalDecl.isAuxDecl localDecl = true then pure none else do let a ← liftM (Lean.Meta.isDefEq e (Lean.LocalDecl.type localDecl)) if a = true then pure (some (Lean.LocalDecl.toExpr localDecl)) else pure none

source

partial def Lean.Meta.Simp.DefaultMethods.discharge? (e : Lean.Expr) :

Lean.Meta.SimpM (Option Lean.Expr)

source

partial def Lean.Meta.Simp.DefaultMethods.pre (e : Lean.Expr) :

Lean.Meta.SimpM Lean.Meta.Simp.Step

source

partial def Lean.Meta.Simp.DefaultMethods.post (e : Lean.Expr) :

Lean.Meta.SimpM Lean.Meta.Simp.Step

source

def Lean.Meta.Simp.DefaultMethods.methods :

Lean.Meta.Simp.Methods

Equations

Lean.Meta.Simp.DefaultMethods.methods = { pre := Lean.Meta.Simp.DefaultMethods.pre, post := Lean.Meta.Simp.DefaultMethods.post, discharge? := Lean.Meta.Simp.DefaultMethods.discharge? }

source

def Lean.Meta.simp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) :

Lean.MetaM Lean.Meta.Simp.Result

Equations

Lean.Meta.simp e ctx discharge? = do let a ← Lean.getOptions Lean.profileitM Lean.Exception "simp" a (match discharge? with | none => Lean.Meta.Simp.main e ctx Lean.Meta.Simp.DefaultMethods.methods | some d => Lean.Meta.Simp.main e ctx { pre := fun a => Lean.Meta.Simp.preDefault a d, post := fun a => Lean.Meta.Simp.postDefault a d, discharge? := d })

source

def Lean.Meta.applySimpResultToTarget (mvarId : Lean.MVarId) (target : Lean.Expr) (r : Lean.Meta.Simp.Result) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.applySimpResultToTarget mvarId target r = match r.proof? with | some proof => Lean.Meta.replaceTargetEq mvarId r.expr proof | none => if (target != r.expr) = true then Lean.Meta.replaceTargetDefEq mvarId r.expr else pure mvarId

source

def Lean.Meta.simpTargetCore (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) :

Lean.MetaM (Option Lean.MVarId)

Equations

Lean.Meta.simpTargetCore mvarId ctx discharge? = do let a ← Lean.Meta.getMVarType mvarId let target ← Lean.Meta.instantiateMVars a let r ← Lean.Meta.simp target ctx discharge? if Lean.Expr.isConstOf r.expr `True = true then let _do_jp := fun y => pure none; match r.proof? with | some proof => do let a ← Lean.Meta.mkOfEqTrue proof let y ← Lean.Meta.assignExprMVar mvarId a _do_jp y | none => do let y ← Lean.Meta.assignExprMVar mvarId (Lean.mkConst `True.intro) _do_jp y else Lean.Internal.coeM (Lean.Meta.applySimpResultToTarget mvarId target r)

source

def Lean.Meta.simpTarget (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) :

Lean.MetaM (Option Lean.MVarId)

Equations

Lean.Meta.simpTarget mvarId ctx discharge? = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `simp Lean.Meta.simpTargetCore mvarId ctx discharge?

source

def Lean.Meta.applySimpResultToProp (mvarId : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (r : Lean.Meta.Simp.Result) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

Lean.Meta.applySimpResultToProp mvarId proof prop r = if Lean.Expr.isConstOf r.expr `False = true then let _do_jp := fun y => pure none; match r.proof? with | some eqProof => do let a ← Lean.Meta.getMVarType mvarId let a_1 ← Lean.Meta.mkEqMP eqProof proof let a ← Lean.Meta.mkFalseElim a a_1 let y ← Lean.Meta.assignExprMVar mvarId a _do_jp y | none => do let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.mkFalseElim a proof let y ← Lean.Meta.assignExprMVar mvarId a _do_jp y else match r.proof? with | some eqProof => do let a ← Lean.Meta.mkEqMP eqProof proof pure (some (a, r.expr)) | none => if (r.expr != prop) = true then do let a ← Lean.Meta.mkExpectedTypeHint proof r.expr pure (some (a, r.expr)) else pure (some (proof, r.expr))

source

def Lean.Meta.applySimpResultToFVarId (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (r : Lean.Meta.Simp.Result) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

Lean.Meta.applySimpResultToFVarId mvarId fvarId r = do let localDecl ← Lean.Meta.getLocalDecl fvarId Lean.Meta.applySimpResultToProp mvarId (Lean.mkFVar fvarId) (Lean.LocalDecl.type localDecl) r

source

def Lean.Meta.simpStep (mvarId : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

Lean.Meta.simpStep mvarId proof prop ctx discharge? = do let r ← Lean.Meta.simp prop ctx discharge? Lean.Meta.applySimpResultToProp mvarId proof prop r

source

def Lean.Meta.applySimpResultToLocalDeclCore (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (r : Option (Lean.Expr × Lean.Expr)) :

Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))

Equations

Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId r = match r with | none => pure none | some (value, type') => do let localDecl ← Lean.Meta.getLocalDecl fvarId if (Lean.LocalDecl.type localDecl != type') = true then do let mvarId ← Lean.Meta.assert mvarId (Lean.LocalDecl.userName localDecl) type' value let mvarId ← Lean.Meta.tryClear mvarId (Lean.LocalDecl.fvarId localDecl) let discr ← Lean.Meta.intro1P mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarId, mvarId) => pure (some (fvarId, mvarId)) else pure (some (fvarId, mvarId))

source

def Lean.Meta.applySimpResultToLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (r : Lean.Meta.Simp.Result) :

Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))

Equations

Lean.Meta.applySimpResultToLocalDecl mvarId fvarId r = do let a ← Lean.Meta.applySimpResultToFVarId mvarId fvarId r Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId a

source

def Lean.Meta.simpLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) :

Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))

Equations

Lean.Meta.simpLocalDecl mvarId fvarId ctx discharge? = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `simp let localDecl ← Lean.Meta.getLocalDecl fvarId let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let a ← Lean.Meta.simpStep mvarId (Lean.mkFVar fvarId) type ctx discharge? Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId a

source

@[inline]

abbrev Lean.Meta.FVarIdToLemmaId :

Type

Equations

Lean.Meta.FVarIdToLemmaId = Lean.FVarIdMap Lean.Name

source

def Lean.Meta.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (fvarIdToLemmaId : optParam Lean.Meta.FVarIdToLemmaId ∅) :

Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId))

Equations

Lean.Meta.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp fvarIdToLemmaId = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `simp let mvarId : Lean.MVarId := mvarId let toAssert : Array Lean.Meta.Hypothesis := #[] let r ← forIn fvarIdsToSimp { fst := none, snd := toAssert } fun fvarId r => let r := r.snd; let toAssert := r; do let localDecl ← Lean.Meta.getLocalDecl fvarId let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let _do_jp : Array Lean.Meta.Hypothesis → Lean.Meta.Simp.Context → Lean.MetaM (ForInStep (MProd (Option (Option (Array Lean.FVarId × Lean.MVarId))) (Array Lean.Meta.Hypothesis))) := fun toAssert ctx => do let a ← Lean.Meta.simpStep mvarId (Lean.mkFVar fvarId) type ctx discharge? match a with | none => pure (ForInStep.done { fst := some none, snd := toAssert }) | some (value, type) => let toAssert := Array.push toAssert { userName := Lean.LocalDecl.userName localDecl, type := type, value := value }; do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := toAssert }) match Std.RBMap.find? fvarIdToLemmaId (Lean.LocalDecl.fvarId localDecl) with | none => do let y ← pure ctx _do_jp toAssert y | some lemmaId => do let a ← pure (Lean.Meta.SimpLemmas.eraseCore ctx.simpLemmas lemmaId) let y ← pure { config := ctx.config, simpLemmas := a, congrLemmas := ctx.congrLemmas, parent? := ctx.parent?, dischargeDepth := ctx.dischargeDepth } _do_jp toAssert y let x : Array Lean.Meta.Hypothesis := r.snd let toAssert : Array Lean.Meta.Hypothesis := x let _do_jp : Lean.MVarId → PUnit → Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId)) := fun mvarId y => let _do_jp := fun mvarId y => do let discr ← Lean.Meta.assertHypotheses mvarId toAssert let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIdsNew, mvarIdNew) => do let mvarIdNew ← Lean.Meta.tryClearMany mvarIdNew fvarIdsToSimp pure (some (fvarIdsNew, mvarIdNew)); if simplifyTarget = true then do let a ← Lean.Meta.simpTarget mvarId ctx discharge? match a with | none => pure none | some mvarIdNew => let mvarId := mvarIdNew; do let y ← pure PUnit.unit _do_jp mvarId y else do let y ← pure PUnit.unit _do_jp mvarId y match r.fst with | none => do let y ← pure PUnit.unit _do_jp mvarId y | some a => pure a