Lean.Meta.Tactic.Simp.Main

Equations

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

source

def Lean.Meta.Simp.Config.updateArith (c : Lean.Meta.Simp.Config) :

Lean.CoreM Lean.Meta.Simp.Config

Helper method for bootstrapping purposes. It disables arith if support theorems have not been defined yet.

Equations

One or more equations did not get rendered due to their size.

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.Result.getProof' (source : Lean.Expr) (r : Lean.Meta.Simp.Result) :

Lean.MetaM Lean.Expr

Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.MetaM Lean.Meta.Simp.Result

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.MetaM Lean.Meta.Simp.Result

Equations

One or more equations did not get rendered due to their size.

source

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

Bool

Return true if e is of the form ofNat n where n is a kernel Nat literal

Equations

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

source

instance Lean.Meta.Simp.instInhabitedM {α : Type} :

Inhabited (Lean.Meta.Simp.M α)

Equations

Lean.Meta.Simp.instInhabitedM = { default := fun x x x => default }

source

def Lean.Meta.Simp.lambdaTelescopeDSimp {α : Type} (e : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → Lean.Meta.Simp.M α) :

Lean.Meta.Simp.M α

Equations

Lean.Meta.Simp.lambdaTelescopeDSimp e k = Lean.Meta.Simp.lambdaTelescopeDSimp.go k #[] e

source

partial def Lean.Meta.Simp.lambdaTelescopeDSimp.go {α : Type} (k : Array Lean.Expr → Lean.Expr → Lean.Meta.Simp.M α) (xs : Array Lean.Expr) (e : Lean.Expr) :

Lean.Meta.Simp.M α

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) (b : Lean.Expr) :

Lean.MetaM Lean.Meta.Simp.SimpLetCase

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.MetaM Lean.Expr

Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec (e : Lean.Expr) :

Bool

Equations

Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec e = ((Lean.Expr.isAppOfArity e `Eq.rec 6 || Lean.Expr.isAppOfArity e `Eq.ndrec 6) && Lean.Expr.isAppOf (Lean.Expr.appArg! e) `Eq.refl)

source

partial def Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec (e : Lean.Expr) :

Lean.Expr

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

One or more equations did not get rendered due to their size.

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.visitFn (e : Lean.Expr) :

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

source

def Lean.Meta.Simp.simp.mkCongrSimp? (f : Lean.Expr) :

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

Equations

One or more equations did not get rendered due to their size.

source

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

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

Try to use automatically generated congruence theorems. See mkCongrSimp?.

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

Process the given congruence theorem hypothesis. Return true if it made "progress".

source

partial def Lean.Meta.Simp.simp.trySimpCongrTheorem? (c : Lean.Meta.SimpCongrTheorem) (e : Lean.Expr) :

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

Try to rewrite e children using the given congruence theorem

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, dischargeDepth := 0 }

source

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

Lean.Meta.Simp.M α

Equations

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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, dischargeDepth := 0 }), post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }) :

Lean.MetaM Lean.Meta.Simp.Result

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.Simp.dsimpMain (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, dischargeDepth := 0 }), post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

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

Bool

Return true if e is of the form (x : α) → ... → s = t → ... → False

Recall that this kind of proposition is generated by Lean when creating equations for functions and match-expressions with overlapping cases. Example: the following match-expression has overlapping cases.

def f (x y : Nat) :=
  match x, y with
  | Nat.succ n, Nat.succ m => ...
  | _, _ => 0

The second equation is of the form

(x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0

The hypothesis (n m : Nat) → x = Nat.succ n → y = Nat.succ m → False is essentially saying the first case is not applicable.

Equations

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

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

One or more equations did not get rendered due to their size.

source

def Lean.Meta.Simp.dischargeEqnThmHypothesis? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Tries to solve e using unifyEq?. It assumes that isEqnThmHypothesis e is true.

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.Simp.dischargeEqnThmHypothesis?.go? (mvarId : Lean.MVarId) :

Lean.MetaM (Option Lean.MVarId)

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

One or more equations did not get rendered due to their size.

source

def Lean.Meta.dsimp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.dsimp e ctx = do let a ← Lean.getOptions Lean.profileitM Lean.Exception "dsimp" a (Lean.Meta.Simp.dsimpMain e ctx Lean.Meta.Simp.DefaultMethods.methods)

source

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

Lean.MetaM Lean.MVarId

Auxiliary method. Given the current target of mvarId, apply r which is a new target and proof that it is equaal to the current one.

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.MetaM (Option Lean.MVarId)

See simpTarget. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.MetaM (Option Lean.MVarId)

Simplify the given goal target (aka type). Return none if the goal was closed. Return some mvarId' otherwise, where mvarId' is the simplified new goal.

Equations

One or more equations did not get rendered due to their size.

source

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

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

Apply the result r for prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

One or more equations did not get rendered due to their size.

source

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

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

Equations

One or more equations did not get rendered due to their size.

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) (mayCloseGoal : optParam Bool true) :

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

Simplify prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

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

One or more equations did not get rendered due to their size.

source

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

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

Simplify simp result to the given local declaration. Return none if the goal was closed. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations