Documentation

instance Lean.Meta.Grind.instInhabitedOrigin :

Inhabited Origin

Equations

Lean.Meta.Grind.instInhabitedOrigin = { default := Lean.Meta.Grind.Origin.decl default }

instance Lean.Meta.Grind.instReprOrigin :

Repr Origin

Equations

Lean.Meta.Grind.instReprOrigin = { reprPrec := Lean.Meta.Grind.reprOrigin✝ }

def Lean.Meta.Grind.Origin.key :

Origin → Name

A unique identifier corresponding to the origin.

Equations

(Lean.Meta.Grind.Origin.decl a).key = a
(Lean.Meta.Grind.Origin.fvar a).key = a.name
(Lean.Meta.Grind.Origin.stx a a_1).key = a
(Lean.Meta.Grind.Origin.local a).key = a

def Lean.Meta.Grind.Origin.pp {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (o : Origin) :

m MessageData

Equations

(Lean.Meta.Grind.Origin.decl a).pp = do let __do_lift ← Lean.mkConstWithLevelParams a pure (Lean.MessageData.ofConst __do_lift)
(Lean.Meta.Grind.Origin.fvar a).pp = pure (Lean.MessageData.ofExpr (Lean.mkFVar a))
(Lean.Meta.Grind.Origin.stx a a_1).pp = pure (Lean.MessageData.ofSyntax a_1)
(Lean.Meta.Grind.Origin.local a).pp = pure (Lean.MessageData.ofName a)

instance Lean.Meta.Grind.instBEqOrigin :

BEq Origin

Equations

Lean.Meta.Grind.instBEqOrigin = { beq := fun (a b : Lean.Meta.Grind.Origin) => a.key == b.key }

instance Lean.Meta.Grind.instHashableOrigin :

Hashable Origin

Equations

Lean.Meta.Grind.instHashableOrigin = { hash := fun (a : Lean.Meta.Grind.Origin) => hash a.key }

inductive Lean.Meta.Grind.EMatchTheoremKind :

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

Inhabited EMatchTheoremKind

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind :

Equations

Lean.Meta.Grind.instInhabitedEMatchTheoremKind = { default := Lean.Meta.Grind.EMatchTheoremKind.eqLhs default }

instance Lean.Meta.Grind.instBEqEMatchTheoremKind :

BEq EMatchTheoremKind

Equations

Lean.Meta.Grind.instBEqEMatchTheoremKind = { beq := Lean.Meta.Grind.beqEMatchTheoremKind✝ }

instance Lean.Meta.Grind.instReprEMatchTheoremKind :

Repr EMatchTheoremKind

Equations

Lean.Meta.Grind.instReprEMatchTheoremKind = { reprPrec := Lean.Meta.Grind.reprEMatchTheoremKind✝ }

Hashable EMatchTheoremKind

instance Lean.Meta.Grind.instHashableEMatchTheoremKind :

Equations

Lean.Meta.Grind.instHashableEMatchTheoremKind = { hash := Lean.Meta.Grind.hashEMatchTheoremKind✝ }

def Lean.Meta.Grind.EMatchTheoremKind.isEqLhs :

EMatchTheoremKind → Bool

Equations

(Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen).isEqLhs = true
x✝.isEqLhs = false

def Lean.Meta.Grind.EMatchTheoremKind.isDefault :

EMatchTheoremKind → Bool

Equations

(Lean.Meta.Grind.EMatchTheoremKind.default gen).isDefault = true
x✝.isDefault = false

structure Lean.Meta.Grind.EMatchTheorem :

A theorem for heuristic instantiation based on E-matching.

levelParams : Array Name
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
patterns : List Expr
symbols : List HeadIndex
Contains all symbols used in patterns.
origin : Origin
kind : EMatchTheoremKind
The kind is used for generating the patterns. We save it here to implement grind?.

Instances For

Lean.Meta.Grind.instInhabitedEMatchTheorem

instance Lean.Meta.Grind.instInhabitedEMatchTheorem :

Inhabited EMatchTheorem

Equations

One or more equations did not get rendered due to their size.

structure Lean.Meta.Grind.EMatchTheorems :

Set of E-matching theorems.

smap : Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)
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
omap : Lean.PHashMap Lean.Meta.Grind.Origin (List Lean.Meta.Grind.EMatchTheorem)
Mapping from origin to E-matching theorems associated with this origin.

Instances For

Lean.Meta.Grind.instInhabitedEMatchTheorems

instance Lean.Meta.Grind.instInhabitedEMatchTheorems :

Inhabited EMatchTheorems

Equations

Lean.Meta.Grind.instInhabitedEMatchTheorems = { default := { smap := default, origins := default, erased := default, omap := default } }

def Lean.Meta.Grind.EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) :

EMatchTheorems

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) :

Bool

Returns true if s contains a theorem with the given origin.

Equations

s.contains origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.origins✝ s) origin

def Lean.Meta.Grind.EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) :

EMatchTheorems

Mark the theorem with the given origin as erased

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) :

Bool

Returns true if the theorem has been marked as erased.

Equations

s.isErased origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.erased✝ s) origin

@[inline]

def Lean.Meta.Grind.EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) :

Option (List EMatchTheorem × EMatchTheorems)

Retrieves theorems from s associated with the given symbol. See EMatchTheorem.insert. The theorems are removed from s.

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.EMatchTheorems.find (s : EMatchTheorems) (origin : Origin) :

List EMatchTheorem

Returns theorems associated with the given origin.

Equations

s.find origin = match Lean.PersistentHashMap.find? (Lean.Meta.Grind.EMatchTheorems.omap✝ s) origin with | some thms => thms | x => []

def Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) :

MetaM Expr

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.isEMatchTheorem (declName : Name) :

CoreM Bool

Returns true if declName has been tagged as an E-match theorem using [grind].

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.resetEMatchTheoremsExt :

CoreM Unit

Equations

One or more equations did not get rendered due to their size.

partial def Lean.Meta.Grind.splitWhileForbidden (pat : Expr) :

List Expr

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.

def Lean.Meta.Grind.mkGroundPattern (e : Expr) :

Expr

Equations

Lean.Meta.Grind.mkGroundPattern e = Lean.mkAnnotation `grind.ground_pat e

def Lean.Meta.Grind.groundPattern? (e : Expr) :

Option Expr

Equations

Lean.Meta.Grind.groundPattern? e = Lean.annotation? `grind.ground_pat e

def Lean.Meta.Grind.isPatternDontCare (e : Expr) :

Bool

Equations

Lean.Meta.Grind.isPatternDontCare e = (e == Lean.Meta.Grind.dontCare✝)

partial def Lean.Meta.Grind.ppPattern (pattern : Expr) :

MessageData

partial def Lean.Meta.Grind.ppPattern.ppArg (arg : Expr) :

MessageData

structure Lean.Meta.Grind.NormalizePattern.State :

symbols : Array HeadIndex
symbolSet : Std.HashSet HeadIndex
bvarsFound : Std.HashSet Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.NormalizePattern.M (α : Type) :

Equations

Lean.Meta.Grind.NormalizePattern.M = StateRefT' IO.RealWorld Lean.Meta.Grind.NormalizePattern.State Lean.MetaM

inductive Lean.Meta.Grind.NormalizePattern.PatternArgKind :

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 form C .. where C is inductive type we process it as part of the pattern. Suppose we have as bs : List α, and a pattern candidate expression as ++ 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

Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind

instance Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind :

Repr PatternArgKind

Equations

Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind = { reprPrec := Lean.Meta.Grind.NormalizePattern.reprPatternArgKind✝ }

def Lean.Meta.Grind.NormalizePattern.PatternArgKind.isSupport :

PatternArgKind → Bool

Equations

def Lean.Meta.Grind.NormalizePattern.getPatternArgKinds (f : Expr) (numArgs : Nat) :

MetaM (Array PatternArgKind)

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.NormalizePattern.main (patterns : List Expr) :

MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.NormalizePattern.normalizePattern (e : Expr) :

M Expr

Equations

Lean.Meta.Grind.NormalizePattern.normalizePattern e = Lean.Meta.Grind.NormalizePattern.go✝ e false

inductive Lean.Meta.Grind.CheckCoverageResult :

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

def Lean.Meta.Grind.mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) (showInfo : Bool := false) :

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) :

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern useLhs gen : Bool) (showInfo : Bool := false) :

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo : Bool := false) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.mkEMatchEqTheorem (declName : Name) (normalizePattern useLhs : Bool := true) (gen showInfo : Bool := false) :

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

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) :

MetaM Unit

Adds an E-matching theorem to the environment. See mkEMatchTheorem.

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.addEMatchEqTheorem (declName : Name) :

MetaM Unit

Adds an E-matching equality theorem to the environment. See mkEMatchEqTheorem.

Equations

Lean.Meta.Grind.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift

def Lean.Meta.Grind.getEMatchTheorems :

CoreM EMatchTheorems

Returns the E-matching theorems registered in the environment.

Equations

Lean.Meta.Grind.getEMatchTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift)