We use this auxiliary constant to mark delayed congruence proofs.
Equations
Instances For
Returns true
if e
is True
, False
, or a literal value.
See Lean.Meta.LitValues
for supported literals.
Equations
Instances For
Context for GrindM
monad.
- simp : Simp.Context
- simpMethods : Simp.Methods
- config : Grind.Config
- cheapCases : Bool
If
cheapCases
istrue
,grind
only appliescases
to types that contain at most one minor premise. Recall thatgrind
appliescases
when introducing types tagged with[grind cases eager]
, and atSplit.lean
Remark: We add this option to implement thelookahead
feature, we don't want to create several subgoals when performing lookahead. - reportMVarIssue : Bool
Instances For
Key for the congruence theorem cache.
Instances For
Equations
- 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
State for the GrindM
monad.
- scState : AlphaShareCommon.State
ShareCommon
(akaHashconsing
) state. - congrThms : PHashMap CongrTheoremCacheKey CongrTheorem
Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e.,
mkHCongrWithArityForConst?
). Remark: we currently do not reuse congruence theorems - simp : Simp.State
- trueExpr : Expr
- falseExpr : Expr
- natZExpr : Expr
- btrueExpr : Expr
- bfalseExpr : Expr
- lastTag : Name
Used to generate trace messages of the for
[grind] working on <tag>
, and implement the 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
withoutReportingMVarIssues x
executes x
without reporting metavariables found during internalization.
See comment at Grind.Context.reportMVarIssue
for additional details.
Equations
Instances For
Returns the user-defined configuration options
Equations
Instances For
Returns true
if declName
is the name of a match
equation or a match
congruence equation.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Returns maximum term generation that is considered during ematching.
Equations
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
Key for the congruence table.
We need access to the enodes
to be able to retrieve the equivalence class roots.
- e : Expr
Instances For
Equations
Equations
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
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.
match
auxiliary functions whose equations have already been created and activated.
Instances For
Case-split information.
- default
(e : Expr)
: SplitInfo
Term
e
may be an inductive predicate,match
-expression,if
-expression, implication, etc. - imp
(e : Expr)
(h : e.isForall = true)
: SplitInfo
e
is an implication and we want to split on its antecedent. - arg
(a b : Expr)
(i : Nat)
(eq : Expr)
: SplitInfo
Given applications
a
andb
, case-split on whether the correspondingi
-th arguments are equal or not. The split is only performed if all other arguments are already known to be equal or are also tagged as split candidates.
Instances For
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
Case-split candidates.
- added : Std.HashSet SplitInfo
Case-splits that have been inserted at
candidates
at some point. Case-splits that have already been performed, or that do not have to be performed anymore.
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 forcases
applications that generated only 1 subgoal.Lookahead "case-splits".
A mapping
(a, b) ↦ is
s.t. for eachSplitInfo.arg a b i eq
incandidates
orlookaheads
we havei ∈ is
. We use this information to decide whether the split/lookahead is "ready" to be tried or not.
Instances For
The grind
goal.
- mvarId : MVarId
- canon : Canon.State
- enodeMap : Lean.Meta.Grind.ENodeMap
- parents : ParentMap
- congrTable : CongrTable (Lean.Meta.Grind.Goal.enodeMap✝ self)
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 and propositions to be processed.
- inconsistent : Bool
inconsistent := true
ifENode
s forTrue
andFalse
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.
Asserted facts
- extThms : PHashMap ENodeKey (Array Ext.ExtTheorem)
Cached extensionality theorems for types.
- ematch : EMatch.State
State of the E-matching module.
- split : Split.State
State of the case-splitting module.
- arith : Arith.State
State of arithmetic procedures.
- clean : Clean.State
State of the clean name generator.
Instances For
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
Instances For
Adds a new theorem instance produced using E-matching.
Equations
Instances For
Returns true
if the maximum number of instances has been reached.
Equations
Instances For
Returns true
if the maximum number of case-splits has been reached.
Equations
Instances For
Returns true
if the maximum number of E-matching rounds has been reached.
Equations
Instances For
Equations
Instances For
Returns the generation of the given term. Is assumes it has been internalized
Equations
Instances For
Returns true
if a
and b
are in the same equivalence class.
Equations
Instances For
Returns true
if the root of its equivalence class.
Equations
Instances For
Return true
if a
and b
have the same type.
Equations
Instances For
Equations
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
Instances For
Notifies the offset constraint module that a = b
where
a
and b
are terms that have been internalized by this module.
Notifies the cutsat module that a = b
where
a
and b
are terms that have been internalized by this module.
Notifies the cutsat module that a ≠ b
where
a
and b
are terms that have been internalized by this module.
Returns true
if type of t
is definitionally equal to α
Equations
Instances For
Given lhs
and rhs
that are known to be disequal, checks whether
lhs
and rhs
have cutsat terms e₁
and e₂
attached to them,
and invokes process Arith.Cutsat.processNewDiseq e₁ e₂
Equations
Instances For
Notifies the comm ring module that a = b
where
a
and b
are terms that have been internalized by this module.
Notifies the comm ring module that a ≠ b
where
a
and b
are terms that have been internalized by this module.
Given lhs
and rhs
that are known to be disequal, checks whether
lhs
and rhs
have ring terms e₁
and e₂
attached to them,
and invokes process Arith.CommRing.processNewDiseq e₁ e₂
Equations
Instances For
Return true
if the goal is inconsistent.
Equations
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 = Bool.false
.
It assumes a
and Bool.false
are in the same equivalence class.
Equations
Instances For
Returns all enodes in the goal
Equations
Instances For
- propagateUp : Propagator
- propagateDown : Propagator
- fallback : Fallback
Instances For
Equations
Instances For
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
Instances For
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
Instances For
Returns extensionality theorems for the given type if available.
If Config.ext
is false
, the result is #[]
.
Equations
Instances For
Add a new lookahead candidate.