Documentation

Lean.Meta.Tactic.Simp.Rewrite

source
inductive Lean.Meta.Simp.DischargeResult :
Type

Helper type for implementing discharge?'

source
instance Lean.Meta.Simp.instDecidableEqDischargeResult :
DecidableEq DischargeResult
Equations
source
def Lean.Meta.Simp.discharge?' (thmId : Origin) (x type : Expr) :
SimpM Bool

Wrapper for invoking discharge? method. It checks for maximum discharge depth, create trace nodes, and ensure the generated proof was successfully assigned to x.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.synthesizeArgs (thmId : Origin) (bis : Array BinderInfo) (xs : Array Expr) :
SimpM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.synthesizeArgs.synthesizeInstance (thmId : Origin) (x type : Expr) :
SimpM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) :
SimpM (Option Result)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.tryTheorem? (e : Expr) (thm : SimpTheorem) :
SimpM (Option Result)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) :
SimpM (Option Result)

Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite?.rewriteUsingIndex? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) :
SimpM (Option Result)

For (← getConfig).index := true, use discrimination tree structure when collecting simp theorem candidates.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite?.rewriteNoIndex? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) :
SimpM (Option Result)

For (← getConfig).index := false, Lean 3 style simp theorem retrieval. Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite?.diagnoseWhenNoIndex (e : Expr) (s : SimpTheoremTree) (thm : SimpTheorem) :
SimpM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite?.inErasedSet (erased : PHashSet Origin) (thm : SimpTheorem) :
Bool
Equations
source
@[inline]
def Lean.Meta.Simp.simpUsingDecide :
Simproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpArith (e : Expr) :
SimpM Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpMatchDiscrs? (info : MatcherInfo) (e : Expr) :
SimpM (Option Result)

Given a match-application e with MatcherInfo info, return some result if at least of one of the discriminants has been simplified.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpMatchCore (matcherName : Name) (e : Expr) :
SimpM Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpMatch :
Simproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewritePre (rflOnly : Bool := false) :
Simproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewritePost (rflOnly : Bool := false) :
Simproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.drewritePre :
DSimproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.drewritePost :
DSimproc
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.dpreDefault (s : SimprocsArray) :
DSimproc
Equations
source
def Lean.Meta.Simp.dpostDefault (s : SimprocsArray) :
DSimproc
Equations
source
def Lean.Meta.Simp.dischargeGround (e : Expr) :
SimpM (Option Expr)

Discharge procedure for the ground/symbolic evaluator.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.sevalGround :
Simproc

Try to unfold ground term in the ground/symbolic evaluator.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.preSEval (s : SimprocsArray) :
Simproc
Equations
source
def Lean.Meta.Simp.postSEval (s : SimprocsArray) :
Simproc
Equations
source
def Lean.Meta.Simp.mkSEvalMethods :
CoreM Methods
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.mkSEvalContext :
MetaM Context
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.seval (e : Expr) :
SimpM Result

Invoke ground/symbolic evaluator from simp. It uses the seval theorems and simprocs.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpGround :
Simproc

Try to unfold ground term in the ground/symbolic evaluator.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.preDefault (s : SimprocsArray) :
Simproc
Equations
source
def Lean.Meta.Simp.postDefault (s : SimprocsArray) :
Simproc
Equations
source
def Lean.Meta.Simp.isEqnThmHypothesis (e : 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
source
partial def Lean.Meta.Simp.isEqnThmHypothesis.go (e : Expr) :
Bool
source
def Lean.Meta.Simp.dischargeEqnThmHypothesis? (e : Expr) :
MetaM (Option 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 : MVarId) :
MetaM (Option MVarId)
source
def Lean.Meta.Simp.dischargeRfl (e : Expr) :
SimpM (Option Expr)

Discharges assumptions of the form ∀ …, a = b using rfl. This is particularly useful for higher order assumptions of the form ∀ …, e = ?g x y to instaniate a parameter g even if that does not appear on the lhs of the rule.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.dischargeDefault? (e : Expr) :
SimpM (Option Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev Lean.Meta.Simp.Discharge :
Type
Equations
source
def Lean.Meta.Simp.mkMethods (s : SimprocsArray) (discharge? : Discharge) (wellBehavedDischarge : Bool) :
Methods
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.mkDefaultMethodsCore (simprocs : SimprocsArray) :
Methods
Equations
source
def Lean.Meta.Simp.mkDefaultMethods :
CoreM Methods
Equations
  • One or more equations did not get rendered due to their size.