def Lean.Meta.Grind.congrPlaceholderProof : Expr

We use this auxiliary constant to mark delayed congruence proofs.

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.

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

inductive Lean.Meta.Grind.SplitSource : Type

Case-split source. That is, where it came from. We store the current source in the grind context.

• ematch (origin : Origin) : SplitSource

  Generated while instantiating a theorem using E-matching.

• ext (declName : Name) : SplitSource

  Generated while instantiating an extensionality theorem with name declName

• mbtc (a b : Expr) (i : Nat) : SplitSource

  Model-based theory combination equality coming from the i-th argument of applications a and b

• beta (e : Expr) : SplitSource

  Beta-reduction.

• forallProp (e : Expr) : SplitSource

  Forall-propagator.

• existsProp (e : Expr) : SplitSource

  Exists-propagator.

• input : SplitSource

  Input goal

instance Lean.Meta.Grind.instInhabitedSplitSource : Inhabited SplitSource

def Lean.Meta.Grind.SplitSource.toMessageData : SplitSource → MetaM MessageData

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
• splitSource : SplitSource

  Current source of case-splits.

• symPrios : SymbolPriorities

  Symbol priorities for inferring E-matching patterns

• trueExpr : Expr
• falseExpr : Expr
• natZExpr : Expr
• btrueExpr : Expr
• bfalseExpr : Expr
• ordEqExpr : Expr
• intExpr : Expr

structure Lean.Meta.Grind.CongrTheoremCacheKey : Type

Key for the congruence theorem cache.

• f : Expr
• numArgs : Nat

instance Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq CongrTheoremCacheKey

instance Lean.Meta.Grind.instHashableCongrTheoremCacheKey : Hashable CongrTheoremCacheKey

structure Lean.Meta.Grind.EMatchTheoremTrace : Type

• origin : Origin
• kind : EMatchTheoremKind

instance Lean.Meta.Grind.instBEqEMatchTheoremTrace : BEq EMatchTheoremTrace

instance Lean.Meta.Grind.instHashableEMatchTheoremTrace : Hashable EMatchTheoremTrace

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

instance Lean.Meta.Grind.instInhabitedTrace : Inhabited Trace

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

• apps : PHashMap Name Nat

  Number of applications per function symbol. This information is only collected if set_option diagnostics true

instance Lean.Meta.Grind.instInhabitedCounters : Inhabited Counters

structure Lean.Meta.Grind.SplitDiagInfo : Type

Case-split diagnostic information

• lctx : LocalContext
• c : Expr
• gen : Nat
• numCases : Nat
• splitSource : SplitSource

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
• 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

• splitDiags : PArray SplitDiagInfo

  Split diagnostic information. This information is only collected when set_option diagnostics true

• lawfulEqCmpMap : PHashMap ExprPtr (Option Expr)

  Mapping from binary functions f to a theorem thm : ∀ a b, f a b = .eq → a = b if it implements the LawfulEqCmp type class.

• reflCmpMap : PHashMap ExprPtr (Option Expr)

  Mapping from binary functions f to a theorem thm : ∀ a, f a a = .eq if it implements the ReflCmp type class.

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

@[reducible, inline]

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

@[inline]

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

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.

def Lean.Meta.Grind.withSplitSource {m : Type → Type u_1} {α : Type} [MonadControlT GrindM m] [Monad m] (splitSource : SplitSource) : m α → m α

withSplitSource s x executes x and uses s as the split source for any case-split registered.

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

Returns the user-defined configuration options

def Lean.Meta.Grind.getTrueExpr : GrindM Expr

Returns the internalized True constant.

def Lean.Meta.Grind.getFalseExpr : GrindM Expr

Returns the internalized False constant.

def Lean.Meta.Grind.getBoolTrueExpr : GrindM Expr

Returns the internalized Bool.true.

def Lean.Meta.Grind.getBoolFalseExpr : GrindM Expr

Returns the internalized Bool.false.

def Lean.Meta.Grind.getNatZeroExpr : GrindM Expr

Returns the internalized 0 : Nat numeral.

def Lean.Meta.Grind.getOrderingEqExpr : GrindM Expr

Returns the internalized Ordering.eq.

def Lean.Meta.Grind.getIntExpr : GrindM Expr

Returns the internalized Int.

def Lean.Meta.Grind.cheapCasesOnly : GrindM Bool

def Lean.Meta.Grind.reportMVarInternalization : GrindM Bool

def Lean.Meta.Grind.getSymbolPriorities : GrindM SymbolPriorities

Returns symbol priorities for inferring E-matching patterns.

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.

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

def Lean.Meta.Grind.saveAppOf (h : HeadIndex) : GrindM Unit

def Lean.Meta.Grind.saveSplitDiagInfo (c : Expr) (gen numCases : Nat) (splitSource : SplitSource) : GrindM Unit

@[inline]

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

def Lean.Meta.Grind.getMaxGeneration : GrindM Nat

Returns maximum term generation that is considered during ematching.

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

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

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.

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

Returns true if e is the internalized True expression.

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

Returns true if e is the internalized False expression.

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

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

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

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

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.

• linarith? : Option Expr

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

instance Lean.Meta.Grind.instInhabitedENode : Inhabited ENode

instance Lean.Meta.Grind.instReprENode : Repr ENode

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

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

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

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

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

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

@[reducible, inline]

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

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentSet : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentMap : Type

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

instance Lean.Meta.Grind.instHashablePreInstance : Hashable PreInstance

instance Lean.Meta.Grind.instBEqPreInstance : BEq PreInstance

@[reducible, inline]

abbrev Lean.Meta.Grind.PreInstanceSet : Type

structure Lean.Meta.Grind.NewRawFact : Type

New raw fact to be preprocessed, and then asserted.

• proof : Expr
• prop : Expr
• generation : Nat
• splitSource : SplitSource

  splitSource to use when internalizing this fact.

instance Lean.Meta.Grind.instInhabitedNewRawFact : Inhabited NewRawFact

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

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

structure Lean.Meta.Grind.CaseTrace : Type

Trace information for a case split.

• expr : Expr
• i : Nat
• num : Nat
• source : SplitSource

instance Lean.Meta.Grind.instInhabitedCaseTrace : Inhabited CaseTrace

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.

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

inductive Lean.Meta.Grind.SplitInfo : Type

Case-split information.

• default (e : Expr) (source : SplitSource) : SplitInfo

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

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

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

• arg (a b : Expr) (i : Nat) (eq : Expr) (source : SplitSource) : 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.

instance Lean.Meta.Grind.instInhabitedSplitInfo : Inhabited SplitInfo

def Lean.Meta.Grind.SplitInfo.hash : SplitInfo → UInt64

instance Lean.Meta.Grind.instHashableSplitInfo : Hashable SplitInfo

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

instance Lean.Meta.Grind.instBEqSplitInfo : BEq SplitInfo

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

def Lean.Meta.Grind.SplitInfo.source : SplitInfo → SplitSource

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

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 ExprPtr

  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.

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

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

Clean name generator.

• used : PHashSet Name
• next : PHashMap Name Nat

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

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 ExprPtr (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.

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Goal

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

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

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

@[reducible, inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

def Lean.Meta.Grind.updateLastTag : GoalM Unit

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.

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.

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

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

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

Adds a new theorem instance produced using E-matching.

def Lean.Meta.Grind.checkMaxInstancesExceeded : GoalM Bool

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

def Lean.Meta.Grind.checkMaxCaseSplit : GoalM Bool

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

def Lean.Meta.Grind.checkMaxEmatchExceeded : GoalM Bool

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

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.

@[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.

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

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

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

@[inline]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Returns true if the root of its equivalence class.

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.

@[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.

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

Returns the root element in the equivalence class of e.

@[inline]

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

Returns the root element in the equivalence class of e.

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

Returns the root enode in the equivalence class of e.

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.

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.

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

Returns the next element in the equivalence class of e.

@[inline]

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

Returns the root element in the equivalence class of e.

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

Returns true if e has already been internalized.

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

@[inline]

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

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 lhs ≍ rhs.

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

Return true if a and b have the same type.

@[inline]

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

@[inline]

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

Pushes lhs = rhs with proof to newEqs.

@[inline]

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

Pushes lhs ≍ rhs with proof to newEqs.

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

Pushes a = True with proof to newEqs.

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

Pushes a = False with proof to newEqs.

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

Pushes a = Bool.true with proof to newEqs.

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

Pushes a = Bool.false with proof to newEqs.

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.

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.

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

Removes the entry e ↦ parents from the parent map.

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.

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

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.

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

@[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.

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.

@[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.

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

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

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

Returns true if e is a numeral supported by cutsat.

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

Returns true if type of t is definitionally equal to α

@[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

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₂

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

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

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

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.

@[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₂

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

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

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

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.

@[extern lean_process_linarith_eq]

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

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

@[extern lean_process_linarith_diseq]

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

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

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

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

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

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

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

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

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

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

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

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.

@[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 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 a ≍ b. It assumes a and b are in the same equivalence class.

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.

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.

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.

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.

def Lean.Meta.Grind.markAsInconsistent : GoalM Unit

Marks current goal as inconsistent without assigning mvarId.

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.

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.

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

Returns all enodes in the goal

@[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

@[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

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

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

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Propagator : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.Fallback : Type

structure Lean.Meta.Grind.Methods : Type

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

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Methods

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

@[inline]

def Lean.Meta.Grind.getMethods : GrindM Methods

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

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

def Lean.Meta.Grind.applyFallback : GoalM Unit

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

def Lean.Meta.Grind.Goal.getEqc (goal : Goal) (e : Expr) (sort : Bool := false) : List Expr

Returns expressions in the given expression equivalence class.

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

@[inline]

def Lean.Meta.Grind.getEqc (e : Expr) (sort : Bool := false) : GoalM (List Expr)

Returns expressions in the given expression equivalence class.

def Lean.Meta.Grind.Goal.getEqcs (goal : Goal) (sort : Bool := false) : List (List Expr)

Returns all equivalence classes in the current goal.

@[inline]

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

Returns all equivalence classes in the current goal.

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.

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.

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.

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

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

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 #[].

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.

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

Add a new lookahead candidate.

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

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