Documentation

Lean.Meta.Tactic.Simp.Main

Equations
• Lean.Meta.Simp.throwCongrHypothesisFailed =

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.
Equations

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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

Equations
Equations
• Lean.Meta.Simp.instInhabitedM = { default := fun x x x => default }
Equations
partial def Lean.Meta.Simp.lambdaTelescopeDSimp.go {α : Type} (k : ) (xs : ) (e : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.

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.
Equations
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Meta.Simp.simp.congrArgs (args : ) :
Equations
• One or more equations did not get rendered due to their size.

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

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

Try to rewrite e children using the given congruence theorem

Equations
• = do let __do_lift ← pure { expr := __do_lift, proof? := none, dischargeDepth := 0 }
def Lean.Meta.Simp.simp.withNewLemmas {α : Type} (xs : ) (f : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.Simp.main (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : ) (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 }) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.Simp.dsimpMain (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : ) (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 }) :
Equations
• One or more equations did not get rendered due to their size.

Return true if e is of the form (x : α) → ... → s = t → ... → False→ ... → s = t → ... → False→ s = t → ... → False→ ... → False→ 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
→ ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
→ x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
→ y = Nat.succ m → False) → f x y = 0
→ False) → f x y = 0
→ f x y = 0


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

Equations
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.

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.
def Lean.Meta.simp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.dsimp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpTargetCore (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (mayCloseGoal : ) (usedSimps : ) :

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.
def Lean.Meta.simpTarget (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (mayCloseGoal : ) (usedSimps : ) :

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.
def Lean.Meta.applySimpResultToProp (mvarId : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (mayCloseGoal : ) :

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.
def Lean.Meta.applySimpResultToFVarId (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (mayCloseGoal : Bool) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpStep (mvarId : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (mayCloseGoal : ) (usedSimps : ) :

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
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.applySimpResultToLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (mayCloseGoal : Bool) :

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
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (mayCloseGoal : ) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (simplifyTarget : ) (fvarIdsToSimp : optParam () #[]) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.simpTargetStar (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : ) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.dsimpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simplifyTarget : ) (fvarIdsToSimp : optParam () #[]) (usedSimps : ) :
Equations
• One or more equations did not get rendered due to their size.