def Lean.Meta.Grind.congrPlaceholderProof : Expr

We use this auxiliary constant to mark delayed congruence proofs.

Equations

• Lean.Meta.Grind.congrPlaceholderProof = Lean.mkConst (Lean.Name.mkSimple "[congruence]")

def Lean.Meta.Grind.isInterpreted (e : Expr) : MetaM Bool

Returns true if e is True, False, or a literal value. See Lean.Meta.LitValues for supported literals.

Equations

• Lean.Meta.Grind.isInterpreted e = if (e.isTrue || e.isFalse) = true then pure true else do let y ← pure PUnit.unit (fun (y : PUnit) => Lean.Meta.isLitValue e) y

opaque Lean.Meta.Grind.grind.debug : Lean.Option Bool

opaque Lean.Meta.Grind.grind.debug.proofs : Lean.Option Bool

opaque Lean.Meta.Grind.grind.warning : Lean.Option Bool

structure Lean.Meta.Grind.Context : Type

Context for GrindM monad.

• simp : Simp.Context
• simpMethods : Simp.Methods
• config : Grind.Config
• cheapCases : Bool

  If cheapCases is true, grind only applies cases to types that contain at most one minor premise. Recall that grind applies cases when introducing types tagged with [grind cases eager], and at Split.lean Remark: We add this option to implement the lookahead feature, we don't want to create several subgoals when performing lookahead.

• reportMVarIssue : Bool

structure Lean.Meta.Grind.CongrTheoremCacheKey : Type

Key for the congruence theorem cache.

• f : Expr
• numArgs : Nat

Instances For

• Lean.Meta.Grind.instBEqCongrTheoremCacheKey
• Lean.Meta.Grind.instHashableCongrTheoremCacheKey

instance Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq CongrTheoremCacheKey

Equations

• Lean.Meta.Grind.instBEqCongrTheoremCacheKey = { beq := fun (a b : Lean.Meta.Grind.CongrTheoremCacheKey) => Lean.Meta.Grind.isSameExpr a.f b.f && a.numArgs == b.numArgs }

instance Lean.Meta.Grind.instHashableCongrTheoremCacheKey : Hashable CongrTheoremCacheKey

Equations

• Lean.Meta.Grind.instHashableCongrTheoremCacheKey = { hash := fun (a : Lean.Meta.Grind.CongrTheoremCacheKey) => mixHash (Lean.Meta.Grind.hashPtrExpr a.f) (hash a.numArgs) }

structure Lean.Meta.Grind.EMatchTheoremTrace : Type

• origin : Origin
• kind : EMatchTheoremKind

Instances For

• Lean.Meta.Grind.instBEqEMatchTheoremTrace
• Lean.Meta.Grind.instHashableEMatchTheoremTrace

instance Lean.Meta.Grind.instBEqEMatchTheoremTrace : BEq EMatchTheoremTrace

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremTrace = { beq := Lean.Meta.Grind.beqEMatchTheoremTrace✝ }

instance Lean.Meta.Grind.instHashableEMatchTheoremTrace : Hashable EMatchTheoremTrace

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremTrace = { hash := Lean.Meta.Grind.hashEMatchTheoremTrace✝ }

structure Lean.Meta.Grind.Trace : Type

E-match theorems and case-splits performed by grind. Note that it may contain elements that are not needed by the final proof. For example, grind instantiated the theorem, but theorem instance was not actually used in the proof.

• thms : PHashSet EMatchTheoremTrace
• eagerCases : PHashSet Name
• cases : PHashSet Name

Instances For

• Lean.Meta.Grind.instInhabitedTrace

instance Lean.Meta.Grind.instInhabitedTrace : Inhabited Trace

Equations

• Lean.Meta.Grind.instInhabitedTrace = { default := { thms := default, eagerCases := default, cases := default } }

structure Lean.Meta.Grind.Counters : Type

• thm : PHashMap Origin Nat

  Number of times E-match theorem has been instantiated.

• case : PHashMap Name Nat

  Number of times a cases has been performed on an inductive type/predicate

Instances For

• Lean.Meta.Grind.instInhabitedCounters

instance Lean.Meta.Grind.instInhabitedCounters : Inhabited Counters

Equations

• Lean.Meta.Grind.instInhabitedCounters = { default := { thm := default, case := default } }

structure Lean.Meta.Grind.State : Type

State for the GrindM monad.

• scState : AlphaShareCommon.State

  ShareCommon (aka Hashconsing) state.

• congrThms : PHashMap CongrTheoremCacheKey CongrTheorem

  Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e., mkHCongrWithArityForConst?). Remark: we currently do not reuse congruence theorems

• simp : Simp.State
• trueExpr : Expr
• falseExpr : Expr
• natZExpr : Expr
• btrueExpr : Expr
• bfalseExpr : Expr
• lastTag : Name

  Used to generate trace messages of the for [grind] working on <tag>, and implement the macro trace_goal.

• issues : List MessageData

  Issues found during the proof search. These issues are reported to users when grind fails.

• trace : Trace

  trace for grind?

• counters : Counters

  Performance counters

instance Lean.Meta.Grind.instNonemptyMethodsRef : Nonempty Lean.Meta.Grind.MethodsRef✝

@[reducible, inline]

abbrev Lean.Meta.Grind.GrindM (α : Type) : Type

Equations

• Lean.Meta.Grind.GrindM = ReaderT Lean.Meta.Grind.MethodsRef✝ (ReaderT Lean.Meta.Grind.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.State Lean.MetaM))

@[inline]

def Lean.Meta.Grind.mapGrindM {m : Type → Type u_1} [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α : Type} (x : m α) : m α

Equations

• Lean.Meta.Grind.mapGrindM f x = controlAt Lean.Meta.Grind.GrindM fun (runInBase : {β : Type} → m β → Lean.Meta.Grind.GrindM (stM Lean.Meta.Grind.GrindM m β)) => f (runInBase x)

def Lean.Meta.Grind.withoutReportingMVarIssues {m : Type → Type u_1} {α : Type} [MonadControlT GrindM m] [Monad m] : m α → m α

withoutReportingMVarIssues x executes x without reporting metavariables found during internalization. See comment at Grind.Context.reportMVarIssue for additional details.

Equations

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

def Lean.Meta.Grind.getConfig : GrindM Grind.Config

Returns the user-defined configuration options

Equations

• Lean.Meta.Grind.getConfig = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.config

def Lean.Meta.Grind.getTrueExpr : GrindM Expr

Returns the internalized True constant.

Equations

• Lean.Meta.Grind.getTrueExpr = do let __do_lift ← get pure __do_lift.trueExpr

def Lean.Meta.Grind.getFalseExpr : GrindM Expr

Returns the internalized False constant.

Equations

• Lean.Meta.Grind.getFalseExpr = do let __do_lift ← get pure __do_lift.falseExpr

def Lean.Meta.Grind.getBoolTrueExpr : GrindM Expr

Returns the internalized Bool.true.

Equations

• Lean.Meta.Grind.getBoolTrueExpr = do let __do_lift ← get pure __do_lift.btrueExpr

def Lean.Meta.Grind.getBoolFalseExpr : GrindM Expr

Returns the internalized Bool.false.

Equations

• Lean.Meta.Grind.getBoolFalseExpr = do let __do_lift ← get pure __do_lift.bfalseExpr

def Lean.Meta.Grind.getNatZeroExpr : GrindM Expr

Returns the internalized 0 : Nat numeral.

Equations

• Lean.Meta.Grind.getNatZeroExpr = do let __do_lift ← get pure __do_lift.natZExpr

def Lean.Meta.Grind.cheapCasesOnly : GrindM Bool

Equations

• Lean.Meta.Grind.cheapCasesOnly = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.cheapCases

def Lean.Meta.Grind.reportMVarInternalization : GrindM Bool

Equations

• Lean.Meta.Grind.reportMVarInternalization = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.reportMVarIssue

def Lean.Meta.Grind.isMatchEqLikeDeclName (declName : Name) : CoreM Bool

Returns true if declName is the name of a match equation or a match congruence equation.

Equations

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

def Lean.Meta.Grind.saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit

Equations

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

def Lean.Meta.Grind.saveCases (declName : Name) (eager : Bool) : GrindM Unit

Equations

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

@[inline]

def Lean.Meta.Grind.getMethodsRef : GrindM Lean.Meta.Grind.MethodsRef✝

Equations

• Lean.Meta.Grind.getMethodsRef = read

def Lean.Meta.Grind.getMaxGeneration : GrindM Nat

Returns maximum term generation that is considered during ematching.

Equations

• Lean.Meta.Grind.getMaxGeneration = do let __do_lift ← Lean.Meta.Grind.getConfig pure __do_lift.gen

def Lean.Meta.Grind.abstractNestedProofs (e : Expr) : GrindM Expr

Abstracts nested proofs in e. This is a preprocessing step performed before internalization.

Equations

• Lean.Meta.Grind.abstractNestedProofs e = liftM (Lean.Meta.abstractNestedProofs e)

def Lean.Meta.Grind.shareCommon (e : Expr) : GrindM Expr

Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

Equations

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

def Lean.Meta.Grind.isTrueExpr (e : Expr) : GrindM Bool

Returns true if e is the internalized True expression.

Equations

• Lean.Meta.Grind.isTrueExpr e = do let __do_lift ← Lean.Meta.Grind.getTrueExpr pure (Lean.Meta.Grind.isSameExpr e __do_lift)

def Lean.Meta.Grind.isFalseExpr (e : Expr) : GrindM Bool

Returns true if e is the internalized False expression.

Equations

• Lean.Meta.Grind.isFalseExpr e = do let __do_lift ← Lean.Meta.Grind.getFalseExpr pure (Lean.Meta.Grind.isSameExpr e __do_lift)

def Lean.Meta.Grind.mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem

Creates a congruence theorem for a f-applications with numArgs arguments.

Equations

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

def Lean.Meta.Grind.reportIssue (msg : MessageData) : GrindM Unit

Equations

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

def Lean.Meta.Grind.doElemReportIssue!__ : ParserDescr

Equations

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

structure Lean.Meta.Grind.ENode : Type

Stores information for a node in the egraph. Each internalized expression e has an ENode associated with it.

• self : Expr

  Node represented by this ENode.

• next : Expr

  Next element in the equivalence class.

• root : Expr

  Root (aka canonical representative) of the equivalence class

• congr : Expr

  congr is the term self is congruent to. We say self is the congruence class root if isSameExpr congr self. This field is initialized to self even if e is not an application.

• target? : Option Expr

  When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

• proof? : Option Expr
• flipped : Bool

  Proof has been flipped.

• size : Nat

  Number of elements in the equivalence class, this field is meaningless if node is not the root.

• interpreted : Bool

  interpreted := true if node should be viewed as an abstract value.

• ctor : Bool

  ctor := true if the head symbol is a constructor application.

• hasLambdas : Bool

  hasLambdas := true if the equivalence class contains lambda expressions.

• heqProofs : Bool

  If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

• idx : Nat

  Unique index used for pretty printing and debugging purposes.

• generation : Nat

  The generation in which this enode was created.

• mt : Nat

  Modification time

• offset? : Option Expr

  The offset? field is used to propagate equalities from the grind congruence closure module to the offset constraints module. When grind merges two equivalence classes, and both have an associated offset? set to some e, the equality is propagated. This field is assigned during the internalization of offset terms.

• cutsat? : Option Expr

  The cutsat? field is used to propagate equalities from the grind congruence closure module to the cutsat module. Its implementation is similar to the offset? field.

• ring? : Option Expr

  The ring? field is used to propagate equalities from the grind congruence closure module to the comm ring module. Its implementation is similar to the offset? field.

Instances For

• Lean.Meta.Grind.instInhabitedENode
• Lean.Meta.Grind.instReprENode

instance Lean.Meta.Grind.instInhabitedENode : Inhabited ENode

Equations

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

instance Lean.Meta.Grind.instReprENode : Repr ENode

Equations

• Lean.Meta.Grind.instReprENode = { reprPrec := Lean.Meta.Grind.reprENode✝ }

def Lean.Meta.Grind.ENode.isRoot (n : ENode) : Bool

Equations

• n.isRoot = Lean.Meta.Grind.isSameExpr n.self n.root

def Lean.Meta.Grind.ENode.isCongrRoot (n : ENode) : Bool

Equations

• n.isCongrRoot = Lean.Meta.Grind.isSameExpr n.self n.congr

inductive Lean.Meta.Grind.NewFact : Type

New equalities and facts to be processed.

• eq (lhs rhs proof : Expr) (isHEq : Bool) : NewFact
• fact (prop proof : Expr) (generation : Nat) : NewFact

@[reducible, inline]

abbrev Lean.Meta.Grind.ENodeMap : Type

Equations

• Lean.Meta.Grind.ENodeMap = Lean.PHashMap Lean.Meta.Grind.ENodeKey Lean.Meta.Grind.ENode

structure Lean.Meta.Grind.CongrKey (enodes : ENodeMap) : Type

Key for the congruence table. We need access to the enodes to be able to retrieve the equivalence class roots.

• e : Expr

Instances For

• Lean.Meta.Grind.instBEqCongrKey
• Lean.Meta.Grind.instHashableCongrKey

instance Lean.Meta.Grind.instHashableCongrKey {enodeMap : ENodeMap} : Hashable (CongrKey enodeMap)

Equations

• Lean.Meta.Grind.instHashableCongrKey = { hash := fun (k : Lean.Meta.Grind.CongrKey enodeMap) => Lean.Meta.Grind.congrHash✝ enodeMap k.e }

instance Lean.Meta.Grind.instBEqCongrKey {enodeMap : ENodeMap} : BEq (CongrKey enodeMap)

Equations

• Lean.Meta.Grind.instBEqCongrKey = { beq := fun (k1 k2 : Lean.Meta.Grind.CongrKey enodeMap) => Lean.Meta.Grind.isCongruent✝ enodeMap k1.e k2.e }

@[reducible, inline]

abbrev Lean.Meta.Grind.CongrTable (enodeMap : ENodeMap) : Type

Equations

• Lean.Meta.Grind.CongrTable enodeMap = Lean.PHashSet (Lean.Meta.Grind.CongrKey enodeMap)

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentSet : Type

Equations

• Lean.Meta.Grind.ParentSet = Std.TreeSet Lean.Expr Lean.Expr.quickComp

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentMap : Type

Equations

• Lean.Meta.Grind.ParentMap = Lean.PHashMap Lean.Meta.Grind.ENodeKey Lean.Meta.Grind.ParentSet

structure Lean.Meta.Grind.PreInstance : Type

The E-matching module instantiates theorems using the EMatchTheorem proof and a (partial) assignment. We want to avoid instantiating the same theorem with the same assignment more than once. Therefore, we store the (pre-)instance information in set. Recall that the proofs of activated theorems have been hash-consed. The assignment contains internalized expressions, which have also been hash-consed.

• proof : Expr
• assignment : Array Expr

Instances For

• Lean.Meta.Grind.instBEqPreInstance
• Lean.Meta.Grind.instHashablePreInstance

instance Lean.Meta.Grind.instHashablePreInstance : Hashable PreInstance

Equations

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

instance Lean.Meta.Grind.instBEqPreInstance : BEq PreInstance

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.PreInstanceSet : Type

Equations

• Lean.Meta.Grind.PreInstanceSet = Lean.PHashSet Lean.Meta.Grind.PreInstance

structure Lean.Meta.Grind.NewRawFact : Type

New raw fact to be preprocessed, and then asserted.

• proof : Expr
• prop : Expr
• generation : Nat

Instances For

• Lean.Meta.Grind.instInhabitedNewRawFact

instance Lean.Meta.Grind.instInhabitedNewRawFact : Inhabited NewRawFact

Equations

• Lean.Meta.Grind.instInhabitedNewRawFact = { default := { proof := default, prop := default, generation := default } }

structure Lean.Meta.Grind.Canon.State : Type

Canonicalizer state. See Canon.lean for additional details.

• argMap : PHashMap (Expr × Nat) (List (Expr × Expr))
• canon : PHashMap Expr Expr
• proofCanon : PHashMap Expr Expr

Instances For

• Lean.Meta.Grind.Canon.instInhabitedState

instance Lean.Meta.Grind.Canon.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Canon.instInhabitedState = { default := { argMap := default, canon := default, proofCanon := default } }

structure Lean.Meta.Grind.CaseTrace : Type

Trace information for a case split.

• expr : Expr
• i : Nat
• num : Nat

Instances For

• Lean.Meta.Grind.instInhabitedCaseTrace

instance Lean.Meta.Grind.instInhabitedCaseTrace : Inhabited CaseTrace

Equations

• Lean.Meta.Grind.instInhabitedCaseTrace = { default := { expr := default, i := default, num := default } }

structure Lean.Meta.Grind.EMatch.State : Type

E-matching related fields for the grind goal.

• thmMap : EMatchTheorems

  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into newThms.

• gmt : Nat

  Goal modification time.

• thms : PArray EMatchTheorem

  Active theorems that we have performed ematching at least once.

• newThms : PArray EMatchTheorem

  Active theorems that we have not performed any round of ematching yet.

• numInstances : Nat

  Number of theorem instances generated so far

• num : Nat

  Number of E-matching rounds performed in this goal since the last case-split.

• preInstances : PreInstanceSet

  (pre-)instances found so far. It includes instances that failed to be instantiated.

• nextThmIdx : Nat

  Next local E-match theorem idx.

• matchEqNames : PHashSet Name

  match auxiliary functions whose equations have already been created and activated.

Instances For

• Lean.Meta.Grind.EMatch.instInhabitedState

instance Lean.Meta.Grind.EMatch.instInhabitedState : Inhabited State

Equations

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

inductive Lean.Meta.Grind.SplitInfo : Type

Case-split information.

• default (e : Expr) : SplitInfo

  Term e may be an inductive predicate, match-expression, if-expression, implication, etc.

• imp (e : Expr) (h : e.isForall = true) : SplitInfo

  e is an implication and we want to split on its antecedent.

• arg (a b : Expr) (i : Nat) (eq : Expr) : SplitInfo

  Given applications a and b, case-split on whether the corresponding i-th arguments are equal or not. The split is only performed if all other arguments are already known to be equal or are also tagged as split candidates.

Instances For

• Lean.Meta.Grind.instBEqSplitInfo
• Lean.Meta.Grind.instHashableSplitInfo
• Lean.Meta.Grind.instInhabitedSplitInfo

instance Lean.Meta.Grind.instHashableSplitInfo : Hashable SplitInfo

Equations

• Lean.Meta.Grind.instHashableSplitInfo = { hash := Lean.Meta.Grind.hashSplitInfo✝ }

instance Lean.Meta.Grind.instInhabitedSplitInfo : Inhabited SplitInfo

Equations

• Lean.Meta.Grind.instInhabitedSplitInfo = { default := Lean.Meta.Grind.SplitInfo.default default }

def Lean.Meta.Grind.SplitInfo.beq : SplitInfo → SplitInfo → Bool

Equations

• (Lean.Meta.Grind.SplitInfo.default e₁).beq (Lean.Meta.Grind.SplitInfo.default e₂) = (e₁ == e₂)
• (Lean.Meta.Grind.SplitInfo.imp e₁ h).beq (Lean.Meta.Grind.SplitInfo.imp e₂ h_1) = (e₁ == e₂)
• (Lean.Meta.Grind.SplitInfo.arg a₁ b₁ i₁ eq₁).beq (Lean.Meta.Grind.SplitInfo.arg a₂ b₂ i₂ eq₂) = (a₁ == a₂ && b₁ == b₂ && i₁ == i₂ && eq₁ == eq₂)
• x✝¹.beq x✝ = false

instance Lean.Meta.Grind.instBEqSplitInfo : BEq SplitInfo

Equations

• Lean.Meta.Grind.instBEqSplitInfo = { beq := Lean.Meta.Grind.SplitInfo.beq }

def Lean.Meta.Grind.SplitInfo.getExpr : SplitInfo → Expr

Equations

• (Lean.Meta.Grind.SplitInfo.default a).getExpr = a
• (Lean.Meta.Grind.SplitInfo.imp a a_1).getExpr = a.forallDomain a_1
• (Lean.Meta.Grind.SplitInfo.arg a a_1 a_2 a_3).getExpr = a_3

def Lean.Meta.Grind.SplitInfo.lt : SplitInfo → SplitInfo → Bool

Equations

• (Lean.Meta.Grind.SplitInfo.default e₁).lt (Lean.Meta.Grind.SplitInfo.default e₂) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.imp e₁ h).lt (Lean.Meta.Grind.SplitInfo.imp e₂ h_1) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.arg a b i e₁).lt (Lean.Meta.Grind.SplitInfo.arg a_1 b_1 i_1 e₂) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.default e).lt x✝ = true
• (Lean.Meta.Grind.SplitInfo.imp e h).lt x✝ = true
• x✝¹.lt x✝ = false

structure Lean.Meta.Grind.SplitArg : Type

Argument arg : type of an application app in SplitInfo.

• arg : Expr
• type : Expr
• app : Expr

structure Lean.Meta.Grind.Split.State : Type

Case splitting related fields for the grind goal.

• num : Nat

  Number of splits performed to get to this goal.

• casesTypes : CasesTypes

  Inductive datatypes marked for case-splitting

• candidates : List SplitInfo

  Case-split candidates.

• added : Std.HashSet SplitInfo

  Case-splits that have been inserted at candidates at some point.

• resolved : PHashSet ENodeKey

  Case-splits that have already been performed, or that do not have to be performed anymore.

• trace : List CaseTrace

  Sequence of cases steps that generated this goal. We only use this information for diagnostics. Remark: casesTrace.length ≥ numSplits because we don't increase the counter for cases applications that generated only 1 subgoal.

• lookaheads : List SplitInfo

  Lookahead "case-splits".

• argPosMap : Std.HashMap (Expr × Expr) (List Nat)

  A mapping (a, b) ↦ is s.t. for each SplitInfo.arg a b i eq in candidates or lookaheads we have i ∈ is. We use this information to decide whether the split/lookahead is "ready" to be tried or not.

• argsAt : PHashMap (Expr × Nat) (List SplitArg)

  Mapping from pairs (f, i) to a list of arguments. Each argument occurs as the i-th of an f-application. We use this information to add splits/lookaheads for triggering extensionality theorems and model-based theory combination. See addSplitCandidatesForExt.

Instances For

• Lean.Meta.Grind.Split.instInhabitedState

instance Lean.Meta.Grind.Split.instInhabitedState : Inhabited State

Equations

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

structure Lean.Meta.Grind.Clean.State : Type

Clean name generator.

• used : PHashSet Name
• next : PHashMap Name Nat

Instances For

• Lean.Meta.Grind.Clean.instInhabitedState

instance Lean.Meta.Grind.Clean.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Clean.instInhabitedState = { default := { used := default, next := default } }

structure Lean.Meta.Grind.Goal : Type

The grind goal.

• mvarId : MVarId
• canon : Canon.State
• enodeMap : Lean.Meta.Grind.ENodeMap
• exprs : PArray Expr
• parents : ParentMap
• congrTable : CongrTable (Lean.Meta.Grind.Goal.enodeMap✝ self)
• appMap : PHashMap HeadIndex (List Expr)

  A mapping from each function application index (HeadIndex) to a list of applications with that index. Recall that the HeadIndex for a constant is its constant name, and for a free variable, it is its unique id.

• newFacts : Array NewFact

  Equations and propositions to be processed.

• inconsistent : Bool

  inconsistent := true if ENodes for True and False are in the same equivalence class.

• nextIdx : Nat

  Next unique index for creating ENodes

• newRawFacts : Std.Queue NewRawFact

  new facts to be preprocessed and then asserted.

• facts : PArray Expr

  Asserted facts

• extThms : PHashMap ENodeKey (Array Ext.ExtTheorem)

  Cached extensionality theorems for types.

• ematch : EMatch.State

  State of the E-matching module.

• split : Split.State

  State of the case-splitting module.

• arith : Arith.State

  State of arithmetic procedures.

• clean : Clean.State

  State of the clean name generator.

Instances For

• Lean.Meta.Grind.instInhabitedGoal

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Goal

Equations

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

def Lean.Meta.Grind.Goal.hasSameRoot (g : Goal) (a b : Expr) : Bool

Equations

• g.hasSameRoot a b = Lean.Meta.Grind.hasSameRoot✝ (Lean.Meta.Grind.Goal.enodeMap✝ g) a b

def Lean.Meta.Grind.Goal.isCongruent (g : Goal) (a b : Expr) : Bool

Equations

• g.isCongruent a b = Lean.Meta.Grind.isCongruent✝ (Lean.Meta.Grind.Goal.enodeMap✝ g) a b

def Lean.Meta.Grind.Goal.admit (goal : Goal) : MetaM Unit

Equations

• goal.admit = goal.mvarId.admit

@[reducible, inline]

abbrev Lean.Meta.Grind.GoalM (α : Type) : Type

Equations

• Lean.Meta.Grind.GoalM = StateRefT' IO.RealWorld Lean.Meta.Grind.Goal Lean.Meta.Grind.GrindM

Instances For

• Lean.Meta.Grind.instMonadLiftGoalMSearchM

@[inline]

def Lean.Meta.Grind.GoalM.runCore {α : Type} (goal : Goal) (x : GoalM α) : GrindM (α × Goal)

Equations

• Lean.Meta.Grind.GoalM.runCore goal x = StateRefT'.run x goal

@[inline]

def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Goal) (x : GoalM α) : GrindM (α × Goal)

Equations

• Lean.Meta.Grind.GoalM.run goal x = goal.mvarId.withContext (Lean.Meta.Grind.GoalM.runCore goal x)

@[inline]

def Lean.Meta.Grind.GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal

Equations

• Lean.Meta.Grind.GoalM.run' goal x = goal.mvarId.withContext ((x *> get).run' goal)

def Lean.Meta.Grind.updateLastTag : GoalM Unit

Equations

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

def Lean.Meta.Grind.«doElemTrace_goal[_]__» : ParserDescr

Macro similar to trace[...], but it includes the trace message trace[grind] "working on <current goal>" if the tag has changed since the last trace message.

Equations

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

def Lean.Meta.Grind.markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool

A helper function used to mark a theorem instance found by the E-matching module. It returns true if it is a new instance and false otherwise.

Equations

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

def Lean.Meta.Grind.addNewRawFact (proof prop : Expr) (generation : Nat) : GoalM Unit

Adds a new fact prop with proof proof to the queue for preprocessing and the assertion.

Equations

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

def Lean.Meta.Grind.addTheoremInstance (thm : EMatchTheorem) (proof prop : Expr) (generation : Nat) : GoalM Unit

Adds a new theorem instance produced using E-matching.

Equations

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

def Lean.Meta.Grind.checkMaxInstancesExceeded : GoalM Bool

Returns true if the maximum number of instances has been reached.

Equations

• Lean.Meta.Grind.checkMaxInstancesExceeded = do let __do_lift ← get let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.ematch.numInstances ≥ __do_lift_1.instances))

def Lean.Meta.Grind.checkMaxCaseSplit : GoalM Bool

Returns true if the maximum number of case-splits has been reached.

Equations

• Lean.Meta.Grind.checkMaxCaseSplit = do let __do_lift ← get let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.split.num ≥ __do_lift_1.splits))

def Lean.Meta.Grind.checkMaxEmatchExceeded : GoalM Bool

Returns true if the maximum number of E-matching rounds has been reached.

Equations

• Lean.Meta.Grind.checkMaxEmatchExceeded = do let __do_lift ← get let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.ematch.num ≥ __do_lift_1.ematch))

def Lean.Meta.Grind.Goal.getENode? (goal : Goal) (e : Expr) : Option ENode

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

Equations

• goal.getENode? e = Lean.PersistentHashMap.find? (Lean.Meta.Grind.Goal.enodeMap✝ goal) { expr := e }

@[inline]

def Lean.Meta.Grind.getENode? (e : Expr) : GoalM (Option ENode)

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

Equations

• Lean.Meta.Grind.getENode? e = do let __do_lift ← get pure (__do_lift.getENode? e)

def Lean.Meta.Grind.throwNonInternalizedExpr {α : Type} (e : Expr) : CoreM α

Equations

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

def Lean.Meta.Grind.Goal.getENode (goal : Goal) (e : Expr) : CoreM ENode

Returns node associated with e. It assumes e has already been internalized.

Equations

• goal.getENode e = match Lean.PersistentHashMap.find? (Lean.Meta.Grind.Goal.enodeMap✝ goal) { expr := e } with | some n => pure n | x => Lean.Meta.Grind.throwNonInternalizedExpr e

@[inline]

def Lean.Meta.Grind.getENode (e : Expr) : GoalM ENode

Returns node associated with e. It assumes e has already been internalized.

Equations

• Lean.Meta.Grind.getENode e = do let __do_lift ← get liftM (__do_lift.getENode e)

def Lean.Meta.Grind.getGeneration (e : Expr) : GoalM Nat

Returns the generation of the given term. Is assumes it has been internalized

Equations

• Lean.Meta.Grind.getGeneration e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure n.generation | x => pure 0

def Lean.Meta.Grind.isEqTrue (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of True.

Equations

• Lean.Meta.Grind.isEqTrue e = do let __do_lift ← Lean.Meta.Grind.getENode e let __do_lift_1 ← liftM Lean.Meta.Grind.getTrueExpr pure (Lean.Meta.Grind.isSameExpr __do_lift.root __do_lift_1)

def Lean.Meta.Grind.isEqFalse (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of False.

Equations

• Lean.Meta.Grind.isEqFalse e = do let __do_lift ← Lean.Meta.Grind.getENode e let __do_lift_1 ← liftM Lean.Meta.Grind.getFalseExpr pure (Lean.Meta.Grind.isSameExpr __do_lift.root __do_lift_1)

def Lean.Meta.Grind.isEqBoolTrue (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of Bool.true.

Equations

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

def Lean.Meta.Grind.isEqBoolFalse (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of Bool.false.

Equations

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

def Lean.Meta.Grind.isEqv (a b : Expr) : GoalM Bool

Returns true if a and b are in the same equivalence class.

Equations

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

def Lean.Meta.Grind.isRoot (e : Expr) : GoalM Bool

Returns true if the root of its equivalence class.

Equations

• Lean.Meta.Grind.isRoot e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => pure (Lean.Meta.Grind.isSameExpr n.root e) | x => pure false

def Lean.Meta.Grind.Goal.getRoot? (goal : Goal) (e : Expr) : Option Expr

Returns the root element in the equivalence class of e IF e has been internalized.

Equations

• goal.getRoot? e = (do let __discr ← goal.getENode? e match __discr with | some n => pure (some n.root) | x => pure none).run

@[inline]

def Lean.Meta.Grind.getRoot? (e : Expr) : GoalM (Option Expr)

Returns the root element in the equivalence class of e IF e has been internalized.

Equations

• Lean.Meta.Grind.getRoot? e = do let __do_lift ← get pure (__do_lift.getRoot? e)

def Lean.Meta.Grind.Goal.getRoot (goal : Goal) (e : Expr) : CoreM Expr

Returns the root element in the equivalence class of e.

Equations

• goal.getRoot e = do let __do_lift ← goal.getENode e pure __do_lift.root

@[inline]

def Lean.Meta.Grind.getRoot (e : Expr) : GoalM Expr

Returns the root element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getRoot e = do let __do_lift ← get liftM (__do_lift.getRoot e)

def Lean.Meta.Grind.getRootENode (e : Expr) : GoalM ENode

Returns the root enode in the equivalence class of e.

Equations

• Lean.Meta.Grind.getRootENode e = do let __do_lift ← Lean.Meta.Grind.getRoot e Lean.Meta.Grind.getENode __do_lift

def Lean.Meta.Grind.getRootENode? (e : Expr) : GoalM (Option ENode)

Returns the root enode in the equivalence class of e if it is in an equivalence class.

Equations

• Lean.Meta.Grind.getRootENode? e = do let __discr ← Lean.Meta.Grind.getENode? e match __discr with | some n => Lean.Meta.Grind.getENode? n.root | x => pure none

def Lean.Meta.Grind.Goal.getNext? (goal : Goal) (e : Expr) : Option Expr

Returns the next element in the equivalence class of e if e has been internalized in the given goal.

Equations

• goal.getNext? e = (do let __discr ← goal.getENode? e match __discr with | some n => pure (some n.next) | x => pure none).run

def Lean.Meta.Grind.Goal.getNext (goal : Goal) (e : Expr) : CoreM Expr

Returns the next element in the equivalence class of e.

Equations

• goal.getNext e = do let __do_lift ← goal.getENode e pure __do_lift.next

@[inline]

def Lean.Meta.Grind.getNext (e : Expr) : GoalM Expr

Returns the root element in the equivalence class of e.

Equations

• Lean.Meta.Grind.getNext e = do let __do_lift ← get liftM (__do_lift.getNext e)

def Lean.Meta.Grind.alreadyInternalized (e : Expr) : GoalM Bool

Returns true if e has already been internalized.

Equations

• Lean.Meta.Grind.alreadyInternalized e = do let __do_lift ← get pure (Lean.PersistentHashMap.contains (Lean.Meta.Grind.Goal.enodeMap✝ __do_lift) { expr := e })

def Lean.Meta.Grind.Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr

Equations

• goal.getTarget? e = (do let __discr ← goal.getENode? e match __discr with | some n => pure n.target? | x => pure none).run

@[inline]

def Lean.Meta.Grind.getTarget? (e : Expr) : GoalM (Option Expr)

Equations

• Lean.Meta.Grind.getTarget? e = do let __do_lift ← get pure (__do_lift.getTarget? e)

def Lean.Meta.Grind.pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit

If isHEq is false, it pushes lhs = rhs with proof to newEqs. Otherwise, it pushes HEq lhs rhs.

Equations

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

def Lean.Meta.Grind.hasSameType (a b : Expr) : MetaM Bool

Return true if a and b have the same type.

Equations

• Lean.Meta.Grind.hasSameType a b = Lean.Meta.withDefault do let __do_lift ← Lean.Meta.inferType a let __do_lift_1 ← Lean.Meta.inferType b Lean.Meta.isDefEq __do_lift __do_lift_1

@[inline]

def Lean.Meta.Grind.pushEqHEq (lhs rhs proof : Expr) : GoalM Unit

Equations

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

@[inline]

def Lean.Meta.Grind.pushEq (lhs rhs proof : Expr) : GoalM Unit

Pushes lhs = rhs with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof false

@[inline]

def Lean.Meta.Grind.pushHEq (lhs rhs proof : Expr) : GoalM Unit

Pushes HEq lhs rhs with proof to newEqs.

Equations

• Lean.Meta.Grind.pushHEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof true

def Lean.Meta.Grind.pushEqTrue (a proof : Expr) : GoalM Unit

Pushes a = True with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqTrue a proof = do let __do_lift ← liftM Lean.Meta.Grind.getTrueExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.pushEqFalse (a proof : Expr) : GoalM Unit

Pushes a = False with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqFalse a proof = do let __do_lift ← liftM Lean.Meta.Grind.getFalseExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.pushEqBoolTrue (a proof : Expr) : GoalM Unit

Pushes a = Bool.true with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqBoolTrue a proof = do let __do_lift ← liftM Lean.Meta.Grind.getBoolTrueExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.pushEqBoolFalse (a proof : Expr) : GoalM Unit

Pushes a = Bool.false with proof to newEqs.

Equations

• Lean.Meta.Grind.pushEqBoolFalse a proof = do let __do_lift ← liftM Lean.Meta.Grind.getBoolFalseExpr Lean.Meta.Grind.pushEq a __do_lift proof

def Lean.Meta.Grind.registerParent (parent child : Expr) : GoalM Unit

Records that parent is a parent of child. This function actually stores the information in the root (aka canonical representative) of child.

Equations

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

def Lean.Meta.Grind.getParents (e : Expr) : GoalM ParentSet

Returns the set of expressions e is a child of, or an expression in es equivalence class is a child of. The information is only up to date if e is the root (aka canonical representative) of the equivalence class.

Equations

• Lean.Meta.Grind.getParents e = do let __do_lift ← get match Lean.PersistentHashMap.find? __do_lift.parents { expr := e } with | some parents => pure parents | x => pure ∅

def Lean.Meta.Grind.resetParentsOf (e : Expr) : GoalM Unit

Removes the entry e ↦ parents from the parent map.

Equations

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

def Lean.Meta.Grind.copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit

Copy parents to the parents of root. root must be the root of its equivalence class.

Equations

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

def Lean.Meta.Grind.mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM Unit

Equations

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

def Lean.Meta.Grind.mkENode (e : Expr) (generation : Nat) : GoalM Unit

Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

Equations

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

def Lean.Meta.Grind.setENode (e : Expr) (n : ENode) : GoalM Unit

Equations

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

@[extern lean_process_new_offset_eq]

opaque Lean.Meta.Grind.Arith.Offset.processNewEq (a b : Expr) : GoalM Unit

Notifies the offset constraint module that a = b where a and b are terms that have been internalized by this module.

def Lean.Meta.Grind.isNatNum (e : Expr) : Bool

Returns true if e is a numeral and has type Nat.

Equations

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

def Lean.Meta.Grind.markAsOffsetTerm (e : Expr) : GoalM Unit

Marks e as a term of interest to the offset constraint module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the offset module.

Equations

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

@[extern lean_process_cutsat_eq]

opaque Lean.Meta.Grind.Arith.Cutsat.processNewEq (a b : Expr) : GoalM Unit

Notifies the cutsat module that a = b where a and b are terms that have been internalized by this module.

@[extern lean_process_cutsat_diseq]

opaque Lean.Meta.Grind.Arith.Cutsat.processNewDiseq (a b : Expr) : GoalM Unit

Notifies the cutsat module that a ≠ b where a and b are terms that have been internalized by this module.

def Lean.Meta.Grind.isNonnegIntNum (e : Expr) : Bool

Returns true if e is a nonegative numeral and has type Int.

Equations

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

def Lean.Meta.Grind.isIntNum (e : Expr) : Bool

Returns true if e is a numeral and has type Int.

Equations

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

def Lean.Meta.Grind.isNum (e : Expr) : Bool

Returns true if e is a numeral supported by cutsat.

Equations

• Lean.Meta.Grind.isNum e = (Lean.Meta.Grind.isNatNum e || Lean.Meta.Grind.isIntNum e)

def Lean.Meta.Grind.hasType (t α : Expr) : MetaM Bool

Returns true if type of t is definitionally equal to α

Equations

• Lean.Meta.Grind.hasType t α = Lean.Meta.withDefault do let __do_lift ← Lean.Meta.inferType t Lean.Meta.isDefEq __do_lift α

@[inline]

def Lean.Meta.Grind.forEachDiseq (parents : ParentSet) (k : Expr → Expr → GoalM Unit) : GoalM Unit

For each equality b = c in parents, executes k b c IF

• b = c is equal to False, and

Equations

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

def Lean.Meta.Grind.propagateCutsatDiseq (lhs rhs : Expr) : GoalM Unit

Given lhs and rhs that are known to be disequal, checks whether lhs and rhs have cutsat terms e₁ and e₂ attached to them, and invokes process Arith.Cutsat.processNewDiseq e₁ e₂

Equations

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

def Lean.Meta.Grind.propagateCutsatDiseq.get? (a : Expr) : GoalM (Option Expr)

Equations

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

def Lean.Meta.Grind.propagateCutsatDiseqs (parents : ParentSet) : GoalM Unit

Traverses disequalities in parents, and propagate the ones relevant to the cutsat module.

Equations

• Lean.Meta.Grind.propagateCutsatDiseqs parents = Lean.Meta.Grind.forEachDiseq parents Lean.Meta.Grind.propagateCutsatDiseq

def Lean.Meta.Grind.markAsCutsatTerm (e : Expr) : GoalM Unit

Marks e as a term of interest to the cutsat module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the cutsat module.

Equations

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

@[extern lean_process_ring_eq]

opaque Lean.Meta.Grind.Arith.CommRing.processNewEq (a b : Expr) : GoalM Unit

Notifies the comm ring module that a = b where a and b are terms that have been internalized by this module.

@[extern lean_process_ring_diseq]

opaque Lean.Meta.Grind.Arith.CommRing.processNewDiseq (a b : Expr) : GoalM Unit

Notifies the comm ring module that a ≠ b where a and b are terms that have been internalized by this module.

def Lean.Meta.Grind.propagateCommRingDiseq (lhs rhs : Expr) : GoalM Unit

Given lhs and rhs that are known to be disequal, checks whether lhs and rhs have ring terms e₁ and e₂ attached to them, and invokes process Arith.CommRing.processNewDiseq e₁ e₂

Equations

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

def Lean.Meta.Grind.propagateCommRingDiseq.get? (a : Expr) : GoalM (Option Expr)

Equations

• Lean.Meta.Grind.propagateCommRingDiseq.get? a = do let __do_lift ← Lean.Meta.Grind.getRootENode a pure __do_lift.ring?

def Lean.Meta.Grind.propagateCommRingDiseqs (parents : ParentSet) : GoalM Unit

Traverses disequalities in parents, and propagate the ones relevant to the comm ring module.

Equations

• Lean.Meta.Grind.propagateCommRingDiseqs parents = Lean.Meta.Grind.forEachDiseq parents Lean.Meta.Grind.propagateCommRingDiseq

def Lean.Meta.Grind.markAsCommRingTerm (e : Expr) : GoalM Unit

Marks e as a term of interest to the ring module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the ring module.

Equations

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

def Lean.Meta.Grind.isCongrRoot (e : Expr) : GoalM Bool

Returns true is e is the root of its congruence class.

Equations

• Lean.Meta.Grind.isCongrRoot e = do let __do_lift ← Lean.Meta.Grind.getENode e pure __do_lift.isCongrRoot

partial def Lean.Meta.Grind.getCongrRoot (e : Expr) : GoalM Expr

Returns the root of the congruence class containing e.

def Lean.Meta.Grind.isInconsistent : GoalM Bool

Return true if the goal is inconsistent.

Equations

• Lean.Meta.Grind.isInconsistent = do let __do_lift ← get pure __do_lift.inconsistent

@[extern lean_grind_mk_eq_proof]

opaque Lean.Meta.Grind.mkEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b. It assumes a and b are in the same equivalence class, and have the same type.

@[extern lean_grind_mk_heq_proof]

opaque Lean.Meta.Grind.mkHEqProof (a b : Expr) : GoalM Expr

Returns a proof that HEq a b. It assumes a and b are in the same equivalence class.

@[extern lean_grind_internalize]

opaque Lean.Meta.Grind.internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit

@[extern lean_grind_process_new_facts]

opaque Lean.Meta.Grind.processNewFacts : GoalM Unit

def Lean.Meta.Grind.mkEqHEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b if they have the same type. Otherwise, returns a proof of HEq a b. It assumes a and b are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqHEqProof a b = do let __do_lift ← liftM (Lean.Meta.Grind.hasSameType a b) if __do_lift = true then Lean.Meta.Grind.mkEqProof a b else Lean.Meta.Grind.mkHEqProof a b

def Lean.Meta.Grind.mkEqTrueProof (a : Expr) : GoalM Expr

Returns a proof that a = True. It assumes a and True are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqTrueProof a = do let __do_lift ← liftM Lean.Meta.Grind.getTrueExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.mkEqFalseProof (a : Expr) : GoalM Expr

Returns a proof that a = False. It assumes a and False are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqFalseProof a = do let __do_lift ← liftM Lean.Meta.Grind.getFalseExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.mkEqBoolTrueProof (a : Expr) : GoalM Expr

Returns a proof that a = Bool.true. It assumes a and Bool.true are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqBoolTrueProof a = do let __do_lift ← liftM Lean.Meta.Grind.getBoolTrueExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.mkEqBoolFalseProof (a : Expr) : GoalM Expr

Returns a proof that a = Bool.false. It assumes a and Bool.false are in the same equivalence class.

Equations

• Lean.Meta.Grind.mkEqBoolFalseProof a = do let __do_lift ← liftM Lean.Meta.Grind.getBoolFalseExpr Lean.Meta.Grind.mkEqProof a __do_lift

def Lean.Meta.Grind.markAsInconsistent : GoalM Unit

Marks current goal as inconsistent without assigning mvarId.

Equations

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

def Lean.MVarId.assignFalseProof (mvarId : MVarId) (falseProof : Expr) : MetaM Unit

Assign the mvarId using the given proof of False. If type of mvarId is not False, then use False.elim.

Equations

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

def Lean.Meta.Grind.closeGoal (falseProof : Expr) : GoalM Unit

Closes the current goal using the given proof of False and marks it as inconsistent if it is not already marked so.

Equations

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

def Lean.Meta.Grind.getExprs : GoalM (PArray Expr)

Returns all enodes in the goal

Equations

• Lean.Meta.Grind.getExprs = do let __do_lift ← get pure __do_lift.exprs

@[inline]

def Lean.Meta.Grind.traverseEqc (e : Expr) (f : ENode → GoalM Unit) : GoalM Unit

Executes f to each term in the equivalence class containing e

Equations

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

@[inline]

def Lean.Meta.Grind.foldEqc {α : Type} (e : Expr) (init : α) (f : ENode → α → GoalM α) : GoalM α

Folds using f and init over the equivalence class containing e

Equations

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

def Lean.Meta.Grind.forEachENode (f : ENode → GoalM Unit) : GoalM Unit

Equations

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

def Lean.Meta.Grind.filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode)

Equations

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

def Lean.Meta.Grind.forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Propagator : Type

Equations

• Lean.Meta.Grind.Propagator = (Lean.Expr → Lean.Meta.Grind.GoalM Unit)

@[reducible, inline]

abbrev Lean.Meta.Grind.Fallback : Type

Equations

• Lean.Meta.Grind.Fallback = Lean.Meta.Grind.GoalM Unit

structure Lean.Meta.Grind.Methods : Type

• propagateUp : Propagator
• propagateDown : Propagator
• fallback : Fallback

Instances For

• Lean.Meta.Grind.instInhabitedMethods

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Methods

Equations

• Lean.Meta.Grind.instInhabitedMethods = { default := { propagateUp := default, propagateDown := default, fallback := default } }

def Lean.Meta.Grind.Methods.toMethodsRef (m : Methods) : Lean.Meta.Grind.MethodsRef✝

Equations

• m.toMethodsRef = Lean.Meta.Grind.Methods.toMethodsRef.unsafe_impl_3 m

@[inline]

def Lean.Meta.Grind.getMethods : GrindM Methods

Equations

• Lean.Meta.Grind.getMethods = do let __do_lift ← Lean.Meta.Grind.getMethodsRef pure __do_lift.toMethods

def Lean.Meta.Grind.propagateUp (e : Expr) : GoalM Unit

Equations

• Lean.Meta.Grind.propagateUp e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateUp e

def Lean.Meta.Grind.propagateDown (e : Expr) : GoalM Unit

Equations

• Lean.Meta.Grind.propagateDown e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateDown e

def Lean.Meta.Grind.applyFallback : GoalM Unit

Equations

• Lean.Meta.Grind.applyFallback = do let __do_lift ← liftM Lean.Meta.Grind.getMethods let fallback : Lean.Meta.Grind.GoalM Unit := __do_lift.fallback fallback

def Lean.Meta.Grind.Goal.getEqc (goal : Goal) (e : Expr) : List Expr

Returns expressions in the given expression equivalence class.

Equations

• goal.getEqc e = Lean.Meta.Grind.Goal.getEqc.go goal e e []

partial def Lean.Meta.Grind.Goal.getEqc.go (goal : Goal) (first e : Expr) (acc : List Expr) : List Expr

@[inline]

def Lean.Meta.Grind.getEqc (e : Expr) : GoalM (List Expr)

Returns expressions in the given expression equivalence class.

Equations

• Lean.Meta.Grind.getEqc e = do let __do_lift ← get pure (__do_lift.getEqc e)

def Lean.Meta.Grind.Goal.getEqcs (goal : Goal) : List (List Expr)

Returns all equivalence classes in the current goal.

Equations

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

@[inline]

def Lean.Meta.Grind.getEqcs : GoalM (List (List Expr))

Returns all equivalence classes in the current goal.

Equations

• Lean.Meta.Grind.getEqcs = do let __do_lift ← get pure __do_lift.getEqcs

def Lean.Meta.Grind.isKnownCaseSplit (s : SplitInfo) : GoalM Bool

Returns true if s has been already added to the case-split list at one point. Remark: this function returns true even if the split has already been resolved and is not in the list anymore.

Equations

• Lean.Meta.Grind.isKnownCaseSplit s = do let __do_lift ← get pure (__do_lift.split.added.contains s)

def Lean.Meta.Grind.isResolvedCaseSplit (e : Expr) : GoalM Bool

Returns true if e is a case-split that does not need to be performed anymore.

Equations

• Lean.Meta.Grind.isResolvedCaseSplit e = do let __do_lift ← get pure (Lean.PersistentHashSet.contains __do_lift.split.resolved { expr := e })

def Lean.Meta.Grind.markCaseSplitAsResolved (e : Expr) : GoalM Unit

Marks e as a case-split that does not need to be performed anymore. Remark: we currently use this feature to disable match-case-splits. Remark: we also use this feature to record the case-splits that have already been performed.

Equations

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

def Lean.Meta.Grind.addSplitCandidate (sinfo : SplitInfo) : GoalM Unit

Inserts e into the list of case-split candidates if it was not inserted before.

Equations

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

def Lean.Meta.Grind.getExtTheorems (type : Expr) : GoalM (Array Ext.ExtTheorem)

Returns extensionality theorems for the given type if available. If Config.ext is false, the result is #[].

Equations

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

def Lean.Meta.Grind.synthesizeInstanceAndAssign (x type : Expr) : MetaM Bool

Helper function for instantiating a type class type, and then using the result to perform isDefEq x val.

Equations

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

def Lean.Meta.Grind.addLookaheadCandidate (sinfo : SplitInfo) : GoalM Unit

Add a new lookahead candidate.

Equations

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

def Lean.Meta.Grind.withoutModifyingState {α : Type} (x : GoalM α) : GoalM α

Helper function for executing x with a fresh newFacts and without modifying the goal state.

Equations

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