Documentation

Init.Grind.Attr

source
def Lean.Grind.genPattern {α : Sort u} (_h : Prop) (x _val : α) :
α

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
source
def Lean.Grind.genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) :
α

Similar to genPattern but for the heterogeneous case

Equations
source
def Lean.Parser.resetGrindAttrs :
ParserDescr

Reset all grind attributes. This command is intended for testing purposes only and should not be used in applications.

Equations
source
def Lean.Parser.Attr.grindGen :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindEq :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindEqBoth :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindEqRhs :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindEqBwd :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindBwd :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindFwd :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindRL :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindLR :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindUsr :
ParserDescr
Equations
source
def Lean.Parser.Attr.grindCases :
ParserDescr
Equations
source
def Lean.Parser.Attr.grindCasesEager :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindIntro :
ParserDescr
Equations
source
def Lean.Parser.Attr.grindExt :
ParserDescr
Equations
source
def Lean.Parser.Attr.grindSym :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grindMod :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grind :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Attr.grind? :
ParserDescr
Equations
  • One or more equations did not get rendered due to their size.