Equations
Instances For
Returns true
if declName
is the name of a match
-expression congruence equation.
Equations
Instances For
- decl
(declName : Name)
: Origin
A global declaration in the environment.
- fvar
(fvarId : FVarId)
: Origin
A local hypothesis.
- stx
(id : Name)
(ref : Syntax)
: Origin
A proof term provided directly to a call to
grind
whereref
is the provided grind argument. Theid
is a unique identifier for the call. - local
(id : Name)
: Origin
It is local, but we don't have a local hypothesis for it.
Instances For
A unique identifier corresponding to the origin.
Equations
Instances For
Equations
Instances For
- eqLhs (gen : Bool) : EMatchTheoremKind
- eqRhs (gen : Bool) : EMatchTheoremKind
- eqBoth (gen : Bool) : EMatchTheoremKind
- eqBwd : EMatchTheoremKind
- fwd : EMatchTheoremKind
- bwd (gen : Bool) : EMatchTheoremKind
- leftRight : EMatchTheoremKind
- rightLeft : EMatchTheoremKind
- default (gen : Bool) : EMatchTheoremKind
- user : EMatchTheoremKind
Instances For
Equations
Instances For
A theorem for heuristic instantiation based on E-matching.
It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When
proof
is just a constant, we can use the universe parameter names stored in the declaration.- proof : Expr
- numParams : Nat
Contains all symbols used in
patterns
.- origin : Origin
- kind : EMatchTheoremKind
Instances For
Set of E-matching theorems.
The key is a symbol from
EMatchTheorem.symbols
.- origins : Lean.PHashSet Lean.Meta.Grind.Origin
Set of theorem ids that have been inserted using
insert
. - erased : Lean.PHashSet Lean.Meta.Grind.Origin
Theorems that have been marked as erased
Mapping from origin to E-matching theorems associated with this origin.
Instances For
Inserts a thm
with symbols [s_1, ..., s_n]
to s
.
We add s_1 -> { thm with symbols := [s_2, ..., s_n] }
.
When grind
internalizes a term containing symbol s
, we
process all theorems thm
associated with key s
.
If their thm.symbols
is empty, we say they are activated.
Otherwise, we reinsert into map
.
Equations
Instances For
Returns true
if s
contains a theorem with the given origin.
Equations
Instances For
Mark the theorem with the given origin as erased
Equations
Instances For
Returns true if the theorem has been marked as erased.
Equations
Instances For
Retrieves theorems from s
associated with the given symbol. See EMatchTheorem.insert
.
The theorems are removed from s
.
Equations
Instances For
Returns theorems associated with the given origin.
Equations
Instances For
Equations
Instances For
Returns true
if declName
has been tagged as an E-match theorem using [grind]
.
Equations
Instances For
Auxiliary function to expand a pattern containing forbidden application symbols into a multi-pattern.
This function enhances the usability of the [grind =]
attribute by automatically handling
forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:
getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
Here, the selected pattern is xs.getLast? = some a
, but Eq
is a forbidden pattern symbol.
Instead of producing an error, this function converts the pattern into a multi-pattern,
allowing the attribute to be used conveniently.
The function recursively expands patterns with forbidden symbols by splitting them into their sub-components. If the pattern does not contain forbidden symbols, it is returned as-is.
- symbolSet : Std.HashSet HeadIndex
- bvarsFound : Std.HashSet Nat
Instances For
Equations
Instances For
- relevant : PatternArgKind
Argument is relevant for E-matching.
- instImplicit : PatternArgKind
Instance implicit arguments are considered support and handled using
isDefEq
. - proof : PatternArgKind
Proofs are ignored during E-matching. Lean is proof irrelevant.
- typeFormer : PatternArgKind
Types and type formers are mostly ignored during E-matching, and processed using
isDefEq
. However, if the argument is of the formC ..
whereC
is inductive type we process it as part of the pattern. Suppose we haveas bs : List α
, and a pattern candidate expressionas ++ bs
, i.e.,@HAppend.hAppend (List α) (List α) (List α) inst as bs
. If we completely ignore the types, the pattern will just be@HAppend.hAppend _ _ _ _ #1 #0
This is not ideal because the E-matcher will try it in any goal that contains
++
, even if it does not even mention lists.
Instances For
Equations
Equations
Instances For
Returns an array kinds
s.ts kinds[i]
is the kind of the corresponding argument.
- a type (that is not a proposition) or type former (which has forward dependencies) or
- a proof, or
- an instance implicit argument
When kinds[i].isSupport
is true
, we say the corresponding argument is a "support" argument.
Equations
Instances For
Equations
Instances For
Auxiliary type for the checkCoverage
function.
- ok : CheckCoverageResult
checkCoverage
succeeded - missing
(pos : List Nat)
: CheckCoverageResult
checkCoverage
failed because some of the theorem parameters are missing,pos
contains their positions
Instances For
Creates an E-matching theorem for a theorem with proof proof
, numParams
parameters, and the given set of patterns.
Pattern variables are represented using de Bruijn indices.
Equations
Instances For
Creates an E-matching theorem for declName
with numParams
parameters, and the given set of patterns.
Pattern variables are represented using de Bruijn indices.
Equations
Instances For
Given a theorem with proof proof
and type of the form ∀ (a_1 ... a_n), lhs = rhs
,
creates an E-matching pattern for it using addEMatchTheorem n [lhs]
If normalizePattern
is true, it applies the grind
simplification theorems and simprocs to the pattern.
Equations
Instances For
Given theorem with name declName
and type of the form ∀ (a_1 ... a_n), lhs = rhs
,
creates an E-matching pattern for it using addEMatchTheorem n [lhs]
If normalizePattern
is true, it applies the grind
simplification theorems and simprocs to the
pattern.
Equations
Instances For
Adds an E-matching theorem to the environment.
See mkEMatchTheorem
.
Equations
Instances For
Adds an E-matching equality theorem to the environment.
See mkEMatchEqTheorem
.
Equations
Instances For
Returns the E-matching theorems registered in the environment.
Equations
Instances For
Creates an E-match theorem using the given proof and kind.
If groundPatterns
is true
, it accepts patterns without pattern variables. This is useful for
theorems such as theorem evenZ : Even 0
. For local theorems, we use groundPatterns := false
since the theorem is already in the grind
state and there is nothing to be instantiated.