Gadget for representing generalization steps h : x = val
in patterns
This gadget is used to represent patterns in theorems that have been generalized to reduce the
number of casts introduced during E-matching based instantiation.
For example, consider the theorem
Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
{f : (a_1 : α1) → some a = some a_1 → Option α2}
: (some a).pbind f = f a rfl
Now, suppose we have a goal containing the term c.pbind g
and the equivalence class
{c, some b}
. The E-matching module generates the instance
(some b).pbind (cast ⋯ g)
The cast
is necessary because g
's type contains c
instead of some b. This
cast` problematic because we don't have a systematic way of pushing casts over functions
to its arguments. Moreover, heterogeneous equality is not effective because the following theorem
is not provable in DTT:
theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b) : f a ≍ g b := ...
The standard solution is to generalize the theorem above and write it as
theorem Option.pbind_some'
{α1 : Type u_1} {a : α1} {α2 : Type u_2}
{x : Option α1}
{f : (a_1 : α1) → x = some a_1 → Option α2}
(h : x = some a)
: x.pbind f = f a h := by
subst h
apply Option.pbind_some
Internally, we use this gadget to mark the E-matching pattern as
(genPattern h x (some a)).pbind f
This pattern is matched in the same way we match (some a).pbind f
, but it saves the proof
for the actual term to the some
-application in f
, and the actual term in x
.
In the example above, c.pbind g
also matches the pattern (genPattern h x (some a)).pbind f
,
and stores c
in x
, b
in a
, and the proof that c = some b
in h
.
Equations
- Lean.Grind.genPattern _h x _val = x
Instances For
Similar to genPattern
but for the heterogenous case
Equations
- Lean.Grind.genHEqPattern _h x _val = x
Instances For
Reset all grind
attributes. This command is intended for testing purposes only and should not be used in applications.
Equations
- Lean.Parser.resetGrindAttrs = Lean.ParserDescr.node `Lean.Parser.resetGrindAttrs 1024 (Lean.ParserDescr.symbol "reset_grind_attrs%")
Instances For
Equations
- Lean.Parser.Attr.grindGen = Lean.ParserDescr.nodeWithAntiquot "grindGen" `Lean.Parser.Attr.grindGen (Lean.ParserDescr.nonReservedSymbol "gen " false)
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
- 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
- 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.Parser.Attr.grindUsr = Lean.ParserDescr.nodeWithAntiquot "grindUsr" `Lean.Parser.Attr.grindUsr (Lean.ParserDescr.nonReservedSymbol "usr " false)
Instances For
Equations
- Lean.Parser.Attr.grindCases = Lean.ParserDescr.nodeWithAntiquot "grindCases" `Lean.Parser.Attr.grindCases (Lean.ParserDescr.nonReservedSymbol "cases " false)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Attr.grindIntro = Lean.ParserDescr.nodeWithAntiquot "grindIntro" `Lean.Parser.Attr.grindIntro (Lean.ParserDescr.nonReservedSymbol "intro " false)
Instances For
Equations
- Lean.Parser.Attr.grindExt = Lean.ParserDescr.nodeWithAntiquot "grindExt" `Lean.Parser.Attr.grindExt (Lean.ParserDescr.nonReservedSymbol "ext " false)
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
The configuration for grind
.
Passed to grind
using, for example, the grind (config := { matchEqs := true })
syntax.
- trace : Bool
- splits : Nat
Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization.
- ematch : Nat
Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split.
- gen : Nat
Maximum term generation. The input goal terms have generation 0. When we instantiate a theorem using a term from generation
n
, the new terms have generationn+1
. Thus, this parameter limits the length of an instantiation chain. - instances : Nat
Maximum number of theorem instances generated using E-matching in a proof search tree branch.
- matchEqs : Bool
- splitMatch : Bool
If
splitMatch
istrue
,grind
performs case-splitting onmatch
-expressions during the search. - splitIte : Bool
- splitIndPred : Bool
If
splitIndPred
istrue
,grind
performs case-splitting on inductive predicates. Otherwise, it performs case-splitting only on types marked with[grind cases]
attribute. - splitImp : Bool
- canonHeartbeats : Nat
Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test.
- ext : Bool
- extAll : Bool
- etaStruct : Bool
- funext : Bool
- lookahead : Bool
TODO
- verbose : Bool
If
verbose
isfalse
, additional diagnostics information is not collected. - clean : Bool
- qlia : Bool
- mbtc : Bool
- zetaDelta : Bool
When set to
true
(default:true
), local definitions are unfolded during normalization and internalization. In other words, given a local context with an entryx : t := e
, the free variablex
is reduced toe
. Note that this behavior is also available insimp
, but there its default isfalse
becausesimp
is not always used as a terminal tactic, and it important to preserve the abstractions introduced by users. Additionally, ingrind
we observed thatzetaDelta
is particularly important when combined with function induction. In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the corresponding definition. We want to avoid a situation in whichzetaDelta
is not applied to let-declarations introduced by function induction whilezeta
unfolds the definition, causing a mismatch. Finally, note that congruence closure is less effective on terms containing many binders such aslambda
andlet
expressions. - zeta : Bool
When
true
(default:true
), performs zeta reduction of let expressions during normalization. That is,let x := v; e[x]
reduces toe[v]
. See alsozetaDelta
. - ring : Bool
When
true
(default:false
), uses procedure for handling equalities over commutative rings. - ringSteps : Nat
- ringNull : Bool
When
true
(default:false
), the commutative ring procedure ingrind
constructs stepwise proof terms, instead of a single-step Nullstellensatz certificate
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
grind
tactic and related tactics.
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
- 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.