We use this auxiliary constant to mark delayed congruence proofs.
Equations
- Lean.Meta.Grind.congrPlaceholderProof = Lean.mkConst (Lean.Name.mkSimple "[congruence]")
Instances For
Returns true
if e
is True
, False
, or a literal value.
See Lean.Meta.LitValues
for supported literals.
Equations
Instances For
Key for the congruence theorem cache.
Instances For
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 }
Equations
- One or more equations did not get rendered due to their size.
- origin : Origin
- kind : EMatchTheoremKind
Instances For
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
Instances For
Equations
- Lean.Meta.Grind.instInhabitedTrace = { default := { thms := default, eagerCases := default, cases := default } }
Equations
- Lean.Meta.Grind.instInhabitedCounters = { default := { thm := default, case := default } }
State for the GrindM
monad.
- scState : ShareCommon.State ShareCommon.objectFactory
ShareCommon
(akaHashconsing
) state. - nextThmIdx : Nat
Next index for creating auxiliary theorems.
- 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 - simpStats : Simp.Stats
- trueExpr : Expr
- falseExpr : Expr
- natZExpr : Expr
- btrueExpr : Expr
- bfalseExpr : Expr
- lastTag : Name
Used to generate trace messages of the for
[grind] working on <tag>
, and implement the macrotrace_goal
. - issues : List MessageData
Issues found during the proof search. These issues are reported to users when
grind
fails. - trace : Trace
trace
forgrind?
- counters : Counters
Performance counters
Instances For
Equations
Instances For
Returns the user-defined configuration options
Equations
- Lean.Meta.Grind.getConfig = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.config
Instances For
Returns the internalized Bool.false
.
Equations
- Lean.Meta.Grind.getBoolFalseExpr = do let __do_lift ← get pure __do_lift.bfalseExpr
Instances For
Equations
- Lean.Meta.Grind.getMainDeclName = do let __do_lift ← readThe Lean.Meta.Grind.Context pure __do_lift.mainDeclName
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
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
Instances For
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)
Instances For
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)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- 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
The
offset?
field is used to propagate equalities from thegrind
congruence closure module to the offset constraints module. Whengrind
merges two equivalence classes, and both have an associatedoffset?
set tosome e
, the equality is propagated. This field is assigned during the internalization of offset terms.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.Grind.instReprENode = { reprPrec := Lean.Meta.Grind.reprENode✝ }
Equations
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Grind.congrHash.go enodes (f.app a) r = Lean.Meta.Grind.congrHash.go enodes f (mixHash r (Lean.Meta.Grind.hashRoot✝ enodes a))
- Lean.Meta.Grind.congrHash.go enodes e r = mixHash r (Lean.Meta.Grind.hashRoot✝ enodes e)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Grind.instHashableCongrKey = { hash := fun (k : Lean.Meta.Grind.CongrKey enodes) => Lean.Meta.Grind.congrHash enodes k.e }
Equations
- Lean.Meta.Grind.instBEqCongrKey = { beq := fun (k1 k2 : Lean.Meta.Grind.CongrKey enodes) => Lean.Meta.Grind.isCongruent enodes k1.e k2.e }
Equations
- Lean.Meta.Grind.CongrTable enodes = Lean.PHashSet (Lean.Meta.Grind.CongrKey enodes)
Instances For
Instances For
Equations
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Grind.instInhabitedNewFact = { default := { proof := default, prop := default, generation := default } }
Equations
- Lean.Meta.Grind.Canon.instInhabitedState = { default := { argMap := default, canon := default, proofCanon := default } }
Equations
- Lean.Meta.Grind.instInhabitedCaseTrace = { default := { expr := default, i := default, num := default } }
- mvarId : MVarId
- canon : Canon.State
- enodes : ENodeMap
- parents : ParentMap
- congrTable : CongrTable self.enodes
A mapping from each function application index (
HeadIndex
) to a list of applications with that index. Recall that theHeadIndex
for a constant is its constant name, and for a free variable, it is its unique id.Equations to be processed.
- inconsistent : Bool
inconsistent := true
ifENode
s forTrue
andFalse
are in the same equivalence class. - gmt : Nat
Goal modification time.
- nextIdx : Nat
Next unique index for creating ENodes
- arith : Arith.State
State of arithmetic procedures
- casesTypes : CasesTypes
Inductive datatypes marked for case-splitting
- 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.
- 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
. - numInstances : Nat
Number of theorem instances generated so far
- numEmatch : 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.
new facts to be processed.
match
auxiliary functions whose equations have already been created and activated.Case-split candidates.
- numSplits : Nat
Number of splits performed to get to this goal.
Case-splits that have already been performed, or that do not have to be performed anymore.
- nextThmIdx : Nat
Next local E-match theorem idx.
Asserted facts
- extThms : PHashMap ENodeKey (Array Ext.ExtTheorem)
Cached extensionality theorems for types.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- Lean.Meta.Grind.GoalM.run goal x = goal.mvarId.withContext (StateRefT'.run x goal)
Instances For
Equations
- Lean.Meta.Grind.GoalM.run' goal x = goal.mvarId.withContext ((x *> get).run' goal)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
Adds a new theorem instance produced using E-matching.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.numInstances ≥ __do_lift_1.instances))
Instances For
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.numSplits ≥ __do_lift_1.splits))
Instances For
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.numEmatch ≥ __do_lift_1.ematch))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns node associated with e
. It assumes e
has already been internalized.
Equations
- goal.getENode e = match Lean.PersistentHashMap.find? goal.enodes { expr := e } with | some n => pure n | x => Lean.Meta.Grind.throwNonInternalizedExpr e
Instances For
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
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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.
Instances For
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
Instances For
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
Instances For
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
Instances For
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.enodes { expr := e })
Instances For
Equations
- Lean.Meta.Grind.getTarget? e = do let __do_lift ← get pure (__do_lift.getTarget? e)
Instances For
Return true
if a
and b
have the same type.
Equations
- Lean.Meta.Grind.hasSameType a b = Lean.Meta.withDefault do let __do_lift ← Lean.Meta.inferType a let __do_lift_1 ← Lean.Meta.inferType b Lean.Meta.isDefEq __do_lift __do_lift_1
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pushes lhs = rhs
with proof
to newEqs
.
Equations
- Lean.Meta.Grind.pushEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof false
Instances For
Pushes HEq lhs rhs
with proof
to newEqs
.
Equations
- Lean.Meta.Grind.pushHEq lhs rhs proof = Lean.Meta.Grind.pushEqCore lhs rhs proof true
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
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.
Instances For
Returns the set of expressions e
is a child of, or an expression in
e
s 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 ∅
Instances For
Notify the offset constraint module that a = b
where
a
and b
are terms that have been internalized by this module.
Notify the offset constraint module that a = k
where
a
is term that has been internalized by this module,
and k
is a numeral.
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
Instances For
Return true
if the goal is inconsistent.
Equations
- Lean.Meta.Grind.isInconsistent = do let __do_lift ← get pure __do_lift.inconsistent
Instances For
Returns a proof that a = b
.
It assumes a
and b
are in the same equivalence class, and have the same type.
Returns a proof that a = b
if they have the same type. Otherwise, returns a proof of HEq a b
.
It assumes a
and b
are in the same equivalence class.
Equations
- Lean.Meta.Grind.mkEqHEqProof a b = do let __do_lift ← liftM (Lean.Meta.Grind.hasSameType a b) if __do_lift = true then Lean.Meta.Grind.mkEqProof a b else Lean.Meta.Grind.mkHEqProof a b
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
Marks current goal as inconsistent without assigning mvarId
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns all enodes in the goal
Equations
- Lean.Meta.Grind.getENodes = do let __do_lift ← get pure __do_lift.getENodes
Instances For
Equations
Instances For
Instances For
- propagateUp : Propagator
- propagateDown : Propagator
- fallback : Fallback
Instances For
Equations
- Lean.Meta.Grind.instInhabitedMethods = { default := { propagateUp := default, propagateDown := default, fallback := default } }
Instances For
Equations
- Lean.Meta.Grind.getMethods = do let __do_lift ← Lean.Meta.Grind.getMethodsRef pure __do_lift.toMethods
Instances For
Equations
- Lean.Meta.Grind.propagateUp e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateUp e
Instances For
Equations
- Lean.Meta.Grind.propagateDown e = do let __do_lift ← liftM Lean.Meta.Grind.getMethods __do_lift.propagateDown e
Instances For
Equations
- Lean.Meta.Grind.applyFallback = do let __do_lift ← liftM Lean.Meta.Grind.getMethods let fallback : Lean.Meta.Grind.GoalM Unit := __do_lift.fallback fallback
Instances For
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.resolvedSplits { expr := e })
Instances For
Mark 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.
Instances For
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.
Instances For
Helper function for instantiating a type class type
, and
then using the result to perform isDefEq x val
.
Equations
- One or more equations did not get rendered due to their size.