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.isDefEqD (t s : Expr) : MetaM Bool

Similar to isDefEq, but ensures default transparency is used.

Equations

• Lean.Meta.Grind.isDefEqD t s = Lean.Meta.withDefault (Lean.Meta.isDefEq t s)

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

opaque Lean.Meta.Grind.SolverExtensionStateSpec : (α : Type) × Inhabited α

Opaque solver extension state.

def Lean.Meta.Grind.SolverExtensionState : Type

Equations

• Lean.Meta.Grind.SolverExtensionState = Lean.Meta.Grind.SolverExtensionStateSpec.fst

instance Lean.Meta.Grind.instInhabitedSolverExtensionState : Inhabited SolverExtensionState

Equations

• Lean.Meta.Grind.instInhabitedSolverExtensionState = Lean.Meta.Grind.SolverExtensionStateSpec.snd

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

Equations

• Lean.Meta.Grind.instInhabitedSplitSource = { default := Lean.Meta.Grind.instInhabitedSplitSource.default }

def Lean.Meta.Grind.instInhabitedSplitSource.default : SplitSource

Equations

• Lean.Meta.Grind.instInhabitedSplitSource.default = Lean.Meta.Grind.SplitSource.ematch default

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

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Grind.SplitSource.ematch origin).toMessageData = Lean.toMessageData "E-matching " ++ Lean.toMessageData origin.pp
• (Lean.Meta.Grind.SplitSource.ext declName).toMessageData = Lean.toMessageData "Extensionality " ++ Lean.toMessageData declName
• (Lean.Meta.Grind.SplitSource.beta e).toMessageData = Lean.toMessageData "Beta-reduction of" ++ Lean.toMessageData (Lean.indentExpr e)
• (Lean.Meta.Grind.SplitSource.forallProp e).toMessageData = Lean.toMessageData "Forall propagation at" ++ Lean.toMessageData (Lean.indentExpr e)
• (Lean.Meta.Grind.SplitSource.existsProp e).toMessageData = Lean.toMessageData "Exists propagation at" ++ Lean.toMessageData (Lean.indentExpr e)
• Lean.Meta.Grind.SplitSource.input.toMessageData = (Lean.MessageData.ofFormat ∘ Std.format) "Initial goal"

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

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

instance Lean.Meta.Grind.instBEqEMatchTheoremTrace : BEq EMatchTheoremTrace

Equations

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

def Lean.Meta.Grind.instBEqEMatchTheoremTrace.beq : EMatchTheoremTrace → EMatchTheoremTrace → Bool

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremTrace.beq { origin := a, kind := a_1 } { origin := b, kind := b_1 } = (a == b && a_1 == b_1)
• Lean.Meta.Grind.instBEqEMatchTheoremTrace.beq x✝¹ x✝ = false

def Lean.Meta.Grind.instHashableEMatchTheoremTrace.hash : EMatchTheoremTrace → UInt64

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremTrace.hash { origin := a, kind := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Lean.Meta.Grind.instHashableEMatchTheoremTrace : Hashable EMatchTheoremTrace

Equations

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

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

Equations

• Lean.Meta.Grind.instInhabitedTrace = { default := Lean.Meta.Grind.instInhabitedTrace.default }

def Lean.Meta.Grind.instInhabitedTrace.default : 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

• 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

Equations

• Lean.Meta.Grind.instInhabitedCounters = { default := Lean.Meta.Grind.instInhabitedCounters.default }

def Lean.Meta.Grind.instInhabitedCounters.default : Counters

Equations

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

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 Hash-consing) 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.

def Lean.Meta.Grind.MethodsRef : Type

Equations

• Lean.Meta.Grind.MethodsRef = Lean.Meta.Grind.MethodsRefPointed✝.type

instance Lean.Meta.Grind.instNonemptyMethodsRef : Nonempty 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.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.

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 ← readThe Lean.Meta.Grind.Context 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 ← readThe Lean.Meta.Grind.Context 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 ← readThe Lean.Meta.Grind.Context 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 ← readThe Lean.Meta.Grind.Context 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 ← readThe Lean.Meta.Grind.Context pure __do_lift.natZExpr

def Lean.Meta.Grind.getOrderingEqExpr : GrindM Expr

Returns the internalized Ordering.eq.

Equations

• Lean.Meta.Grind.getOrderingEqExpr = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.ordEqExpr

def Lean.Meta.Grind.getIntExpr : GrindM Expr

Returns the internalized Int.

Equations

• Lean.Meta.Grind.getIntExpr = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.intExpr

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.getSymbolPriorities : GrindM SymbolPriorities

Returns symbol priorities for inferring E-matching patterns.

Equations

• Lean.Meta.Grind.getSymbolPriorities = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.symPrios

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.saveCases (declName : Name) (eager : Bool) : GrindM Unit

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.saveAppOf h = do let __do_lift ← liftM Lean.isDiagnosticsEnabled if __do_lift = true then pure () else pure PUnit.unit

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

Equations

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

@[inline]

def Lean.Meta.Grind.getMethodsRef : GrindM 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.

inductive Lean.Meta.Grind.SolverTerms : Type

Each E-node may have "solver terms" attached to them. Each term is an element of the equivalence class that the solver cares about. Each solver is responsible for marking the terms they care about. The grind core propagates equalities and disequalities to the theory solvers using these "marked" terms. The root of the equivalence class contains a list of representatives sorted by solver id. Note that many E-nodes do not have any solver terms attached to them.

"Solver terms" are referenced as "theory variables" in the SMT literature. The SMT solver Z3 uses a similar representation.

• nil : SolverTerms
• next (solverId : Nat) (e : Expr) (rest : SolverTerms) : SolverTerms

instance Lean.Meta.Grind.instInhabitedSolverTerms : Inhabited SolverTerms

Equations

• Lean.Meta.Grind.instInhabitedSolverTerms = { default := Lean.Meta.Grind.instInhabitedSolverTerms.default }

def Lean.Meta.Grind.instInhabitedSolverTerms.default : SolverTerms

Equations

• Lean.Meta.Grind.instInhabitedSolverTerms.default = Lean.Meta.Grind.SolverTerms.nil

instance Lean.Meta.Grind.instReprSolverTerms : Repr SolverTerms

Equations

• Lean.Meta.Grind.instReprSolverTerms = { reprPrec := Lean.Meta.Grind.instReprSolverTerms.repr }

def Lean.Meta.Grind.instReprSolverTerms.repr : SolverTerms → Nat → Format

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 E-graph. 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

• sTerms : SolverTerms

  Solver terms attached to this E-node.

instance Lean.Meta.Grind.instInhabitedENode : Inhabited ENode

Equations

• Lean.Meta.Grind.instInhabitedENode = { default := Lean.Meta.Grind.instInhabitedENode.default }

def Lean.Meta.Grind.instInhabitedENode.default : 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.instReprENode.repr }

def Lean.Meta.Grind.instReprENode.repr : ENode → Nat → Format

Equations

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

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

def Lean.Meta.Grind.ENodeMap : Type

Equations

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

instance Lean.Meta.Grind.instInhabitedENodeMap : Inhabited ENodeMap

Equations

• Lean.Meta.Grind.instInhabitedENodeMap = { default := Lean.Meta.Grind.instInhabitedENodeMap._private_1 }

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)

Equations

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

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.instBEqCongrKey._private_1 k1 k2 }

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

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

  splitSource to use when internalizing this fact.

def Lean.Meta.Grind.instInhabitedNewRawFact.default : NewRawFact

Equations

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

instance Lean.Meta.Grind.instInhabitedNewRawFact : Inhabited NewRawFact

Equations

• Lean.Meta.Grind.instInhabitedNewRawFact = { default := Lean.Meta.Grind.instInhabitedNewRawFact.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

def Lean.Meta.Grind.Canon.instInhabitedState.default : State

Equations

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

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

Equations

• Lean.Meta.Grind.Canon.instInhabitedState = { default := Lean.Meta.Grind.Canon.instInhabitedState.default }

structure Lean.Meta.Grind.CaseTrace : Type

Trace information for a case split.

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

def Lean.Meta.Grind.instInhabitedCaseTrace.default : CaseTrace

Equations

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

instance Lean.Meta.Grind.instInhabitedCaseTrace : Inhabited CaseTrace

Equations

• Lean.Meta.Grind.instInhabitedCaseTrace = { default := Lean.Meta.Grind.instInhabitedCaseTrace.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.

def Lean.Meta.Grind.EMatch.instInhabitedState.default : State

Equations

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

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

Equations

• Lean.Meta.Grind.EMatch.instInhabitedState = { default := Lean.Meta.Grind.EMatch.instInhabitedState.default }

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

Equations

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

def Lean.Meta.Grind.instInhabitedSplitInfo.default : SplitInfo

Equations

• Lean.Meta.Grind.instInhabitedSplitInfo.default = Lean.Meta.Grind.SplitInfo.default default default

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

Equations

• (Lean.Meta.Grind.SplitInfo.default e source).hash = hash e
• (Lean.Meta.Grind.SplitInfo.imp e h source).hash = hash e
• (Lean.Meta.Grind.SplitInfo.arg a b i e source).hash = hash e

instance Lean.Meta.Grind.instHashableSplitInfo : Hashable SplitInfo

Equations

• Lean.Meta.Grind.instHashableSplitInfo = { hash := Lean.Meta.Grind.SplitInfo.hash }

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

Equations

• (Lean.Meta.Grind.SplitInfo.default e₁ source).beq (Lean.Meta.Grind.SplitInfo.default e₂ source_1) = (e₁ == e₂)
• (Lean.Meta.Grind.SplitInfo.imp e₁ h source).beq (Lean.Meta.Grind.SplitInfo.imp e₂ h_1 source_1) = (e₁ == e₂)
• (Lean.Meta.Grind.SplitInfo.arg a₁ b₁ i₁ eq₁ source).beq (Lean.Meta.Grind.SplitInfo.arg a₂ b₂ i₂ eq₂ source_1) = (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 e source).getExpr = e
• (Lean.Meta.Grind.SplitInfo.imp e h source).getExpr = e.forallDomain h
• (Lean.Meta.Grind.SplitInfo.arg a b i e source).getExpr = e

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

Equations

• (Lean.Meta.Grind.SplitInfo.default e source).source = source
• (Lean.Meta.Grind.SplitInfo.imp e h source).source = source
• (Lean.Meta.Grind.SplitInfo.arg a b i e source).source = source

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

Equations

• (Lean.Meta.Grind.SplitInfo.default e₁ source).lt (Lean.Meta.Grind.SplitInfo.default e₂ source_1) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.imp e₁ h source).lt (Lean.Meta.Grind.SplitInfo.imp e₂ h_1 source_1) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.arg a b i e₁ source).lt (Lean.Meta.Grind.SplitInfo.arg a_1 b_1 i_1 e₂ source_1) = e₁.lt e₂
• (Lean.Meta.Grind.SplitInfo.default e source).lt x✝ = true
• (Lean.Meta.Grind.SplitInfo.imp e h source).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 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.

def Lean.Meta.Grind.Split.instInhabitedState.default : State

Equations

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

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

Equations

• Lean.Meta.Grind.Split.instInhabitedState = { default := Lean.Meta.Grind.Split.instInhabitedState.default }

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

Equations

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

def Lean.Meta.Grind.Clean.instInhabitedState.default : State

Equations

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

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

Cache for Unit-like types. It maps the type to its element. We say a type is Unit-like if it is a subsingleton and is inhabited.

• map : PHashMap ExprPtr (Option Expr)

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

Equations

• Lean.Meta.Grind.UnitLike.instInhabitedState = { default := Lean.Meta.Grind.UnitLike.instInhabitedState.default }

def Lean.Meta.Grind.UnitLike.instInhabitedState.default : State

Equations

• Lean.Meta.Grind.UnitLike.instInhabitedState.default = { map := default }

structure Lean.Meta.Grind.Goal : Type

The grind goal.

• mvarId : MVarId
• canon : Canon.State
• enodeMap : ENodeMap
• exprs : PArray Expr
• parents : ParentMap
• congrTable : CongrTable self.enodeMap
• 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.

• clean : Clean.State

  State of the clean name generator.

• sstates : Array SolverExtensionState

  Solver states.

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Goal

Equations

• Lean.Meta.Grind.instInhabitedGoal = { default := Lean.Meta.Grind.instInhabitedGoal.default }

def Lean.Meta.Grind.instInhabitedGoal.default : 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✝ g.enodeMap a b

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

Equations

• g.isCongruent a b = Lean.Meta.Grind.isCongruent✝ g.enodeMap 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

@[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) (splitSource : SplitSource) : 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? goal.enodeMap { 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

• Lean.Meta.Grind.throwNonInternalizedExpr e = Lean.throwError (Lean.toMessageData "internal `grind` error, term has not been internalized" ++ Lean.toMessageData (Lean.indentExpr e))

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? goal.enodeMap { 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 __do_lift.enodeMap { 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 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 = do let __do_lift ← Lean.Meta.inferType a let __do_lift_1 ← Lean.Meta.inferType b Lean.Meta.Grind.isDefEqD __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 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 hash-consed.

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.

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 α = do let __do_lift ← Lean.Meta.inferType t Lean.Meta.Grind.isDefEqD __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.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 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.

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

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Methods

Equations

• Lean.Meta.Grind.instInhabitedMethods = { default := Lean.Meta.Grind.instInhabitedMethods.default }

def Lean.Meta.Grind.instInhabitedMethods.default : Methods

Equations

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

def Lean.Meta.Grind.Methods.toMethodsRef (m : Methods) : 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 (Lean.Meta.Grind.MethodsRef.toMethods✝ __do_lift)

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 have fallback : Lean.Meta.Grind.GoalM Unit := __do_lift.fallback fallback

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

Equations

• goal.getGeneration e = match goal.getENode? e with | some n => n.generation | x => 0

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

Returns expressions in the given expression equivalence class.

Equations

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

@[inline]

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

Returns expressions in the given expression equivalence class.

Equations

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

def Lean.Meta.Grind.Goal.getEqcs (goal : Goal) (sort : Bool := false) : 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.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.

@[extern lean_grind_canon]

opaque Lean.Meta.Grind.canon (e : Expr) : GoalM Expr

Canonicalizes nested types, type formers, and instances in e.

Solver Extensions

structure Lean.Meta.Grind.SolverExtension (σ : Type) : Type

Solver extension, can only be generated by registerSolverExtension that allocates a unique index for this extension into each goal's extension state's array.

• id : Nat
• mkInitial : IO σ
• internalize : Expr → (parent? : Option Expr) → GoalM Unit
• newEq : Expr → Expr → GoalM Unit
• newDiseq : Expr → Expr → GoalM Unit
• mbtc : GoalM Bool
• check : GoalM Bool
• checkInv : GoalM Unit

def Lean.Meta.Grind.instInhabitedSolverExtension.default {a✝ : Type} : SolverExtension a✝

Equations

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

instance Lean.Meta.Grind.instInhabitedSolverExtension {a✝ : Type} : Inhabited (SolverExtension a✝)

Equations

• Lean.Meta.Grind.instInhabitedSolverExtension = { default := Lean.Meta.Grind.instInhabitedSolverExtension.default }

def Lean.Meta.Grind.registerSolverExtension {σ : Type} (mkInitial : IO σ) : IO (SolverExtension σ)

Registers a new solver extension for grind. Solver extensions can only be registered during initialization. Reason: We do not use any synchronization primitive to access solverExtensionsRef.

Equations

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

def Lean.Meta.Grind.SolverExtension.setMethods {σ : Type} (ext : SolverExtension σ) (internalize : Expr → Option Expr → GoalM Unit := fun (x : Expr) (x : Option Expr) => pure ()) (newEq newDiseq : Expr → Expr → GoalM Unit := fun (x x : Expr) => pure ()) (mbtc check : GoalM Bool := pure false) (checkInv : GoalM Unit := pure ()) : IO Unit

Sets methods/handlers for solver extension ext. Solver extension methods can only be registered during initialization. Reason: We do not use any synchronization primitive to access solverExtensionsRef.

Equations

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

def Lean.Meta.Grind.Solvers.mkInitialStates : IO (Array SolverExtensionState)

Returns initial state for registered solvers.

Equations

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

instance Lean.Meta.Grind.instInhabitedGoalM {σ : Type} : Inhabited (GoalM σ)

Equations

• Lean.Meta.Grind.instInhabitedGoalM = { default := Lean.throwError (Lean.toMessageData "<GoalM action default value>") }

@[implemented_by _private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.modifyStateImpl]

opaque Lean.Meta.Grind.SolverExtension.modifyState {σ : Type} (ext : SolverExtension σ) (f : σ → σ) : GoalM Unit

@[implemented_by _private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.getStateCoreImpl]

opaque Lean.Meta.Grind.SolverExtension.getStateCore {σ : Type} (ext : SolverExtension σ) (goal : Goal) : IO σ

def Lean.Meta.Grind.SolverExtension.getState {σ : Type} (ext : SolverExtension σ) : GoalM σ

Equations

• ext.getState = do let __do_lift ← get liftM (ext.getStateCore __do_lift)

def Lean.Meta.Grind.Solvers.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit

Internalizes given expression in all registered solvers.

Equations

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

def Lean.Meta.Grind.Solvers.checkInvariants : GoalM Unit

Checks invariants of all registered solvers.

Equations

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

def Lean.Meta.Grind.Solvers.check : GoalM Bool

Performs (expensive) satisfiability checks in all registered solvers.

Equations

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

def Lean.Meta.Grind.Solvers.mbtc : GoalM Bool

Invokes model-based theory combination extensions in all registered solvers.

Equations

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

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

Given a new disequality lhs ≠ rhs, propagates it to relevant theories.

Equations

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

def Lean.Meta.Grind.isSameSolverTerms (a b : SolverTerms) : Bool

Equations

• Lean.Meta.Grind.isSameSolverTerms a b = Lean.Meta.Grind.isSameSolverTerms.unsafe_impl_3✝ a b

def Lean.Meta.Grind.SolverExtension.markTerm {σ : Type} (ext : SolverExtension σ) (e : Expr) : GoalM Unit

Equations

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

def Lean.Meta.Grind.SolverExtension.getTerm {σ : Type} (ext : SolverExtension σ) (e : ENode) : Option Expr

Returns some t if t is the solver term for ext associated with e.

Equations

• ext.getTerm e = Lean.Meta.Grind.SolverExtension.getTerm.go✝ ext.id e.sTerms

def Lean.Meta.Grind.SolverExtension.hasTermAtRoot {σ : Type} (ext : SolverExtension σ) (e : Expr) : GoalM Bool

Returns true if the root of es equivalence class is already attached to a term of the given solver.

Equations

• ext.hasTermAtRoot e = do let __do_lift ← Lean.Meta.Grind.getRootENode e pure (Lean.Meta.Grind.SolverExtension.hasTermAtRoot.go✝ ext.id __do_lift.sTerms)

structure Lean.Meta.Grind.PendingSolverPropagations : Type

• data : Lean.Meta.Grind.PendingSolverPropagationsData✝

def Lean.Meta.Grind.Solvers.mergeTerms (rhsRoot lhsRoot : ENode) : GoalM PendingSolverPropagations

Equations

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

def Lean.Meta.Grind.PendingSolverPropagations.propagate (p : PendingSolverPropagations) : GoalM Unit

Equations

• p.propagate = Lean.Meta.Grind.PendingSolverPropagations.propagate.go✝ (Lean.Meta.Grind.PendingSolverPropagations.data✝ p)