We define discrimination trees for the purpose of unifying local expressions with library results.

This structure is based on Lean.Meta.DiscrTree. I document here what features are not in the original:

• The keys Key.lam, Key.forall and Key.bvar have been introduced in order to allow for matching under lambda and forall binders. Key.lam has arity 1 and indexes the body. Key.forall has arity 2 and indexes the domain and the body. The reason for not indexing the domain of a lambda expression is that it is usually already determined, for example in ∃ a : α, p, which is @Exists α fun a : α => p, we don't want to index the domain α twice. In a forall expression it is necessary to index the domain, because in an implication p → q we need to index both p and q. Key.bvar works the same as Key.fvar, but stores the De Bruijn index to identify it.

  For example, this allows for more specific matching with the left hand side of ∑ i ∈ range n, i = n * (n - 1) / 2, which is indexed by [⟨Finset.sum, 5⟩, ⟨Nat, 0⟩, ⟨Nat, 0⟩, *0, ⟨Finset.Range, 1⟩, *1, λ, ⟨#0, 0⟩].

• The key Key.star takes a Nat identifier as an argument. For example, the library pattern ?a + ?a is encoded as [⟨HAdd.hAdd, 6⟩, *0, *0, *0, *1, *2, *2]. *0 corresponds to the type of a, *1 to the HAdd instance, and *2 to a. This means that it will only match an expression x + y if x is definitionally equal to y. The matching algorithm requires that the same stars from the discrimination tree match with the same patterns in the lookup expression, and similarly requires that the same metavariables form the lookup expression match with the same pattern in the discrimination tree.

• The key Key.opaque has been introduced in order to index existential variables in lemmas like Nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n, where the part Prime p gets the pattern [⟨Nat.Prime, 1⟩, ◾]. (◾ represents Key.opaque) When matching, Key.opaque can only be matched by Key.star.

  Using the WhnfCoreConfig argument, it is possible to disable β-reduction and ζ-reduction. As a result, we may get a lambda expression applied to an argument or a let-expression. Since there is no support for indexing these, they will be indexed by Key.opaque.

• We keep track of the matching score of a unification. This score represents the number of keys that had to be the same for the unification to succeed. For example, matching (1 + 2) + 3 with add_comm gives a score of 2, since the pattern of commutativity is [⟨HAdd.hAdd, 6⟩, *0, *0, *0, *1, *2, *3], so matching ⟨HAdd.hAdd, 6⟩ gives 1 point, and matching *0 after its first appearance gives another point, but the third argument is an outParam, so this gets ignored. Similarly, matching it with add_assoc gives a score of 5.

• Patterns that have the potential to be η-reduced are put into the RefinedDiscrTree under all possible reduced key sequences. This is for terms of the form fun x => f (?m x₁ .. xₙ), where ?m is a metavariable, and one of x₁, .., xₙ in x. For example, the pattern Continuous fun y => Real.exp (f y)]) is indexed by both [⟨Continuous, 5⟩, *0, ⟨Real, 0⟩, *1, *2, λ, ⟨Real.exp⟩, *3] and [⟨Continuous, 5⟩, *0, ⟨Real, 0⟩, *1, *2, ⟨Real.exp⟩] so that it also comes up if you search with Continuous Real.exp. Similarly, Continuous fun x => f x + g x is indexed by both [⟨Continuous, 1⟩, λ, ⟨HAdd.hAdd, 6⟩, *0, *0, *0, *1, *2, *3] and [⟨Continuous, 1⟩, ⟨HAdd.hAdd, 5⟩, *0, *0, *0, *1, *2].

• For sub-expressions not at the root of the original expression we have some additional reductions:

  • Any combination of ofNat, Nat.zero, Nat.succ and number literals is stored as just a number literal.
  • The expression fun a : α => a is stored as @id α.
    • This makes lemmata such as continuous_id' redundant, which is the same as continuous_id, with id replaced by fun x => x.
  • Any expressions involving +, *, -, / or ⁻¹ is normalized to not have a lambda in front and to always have the default amount of arguments. e.g. (f + g) a is stored as f a + g a and fun x => f x + g x is stored as f + g.
    • This makes lemmata such as MeasureTheory.integral_integral_add' redundant, which is the same as MeasureTheory.integral_integral_add, with f a + g a replaced by (f + g) a
    • it also means that a lemma like Continuous.mul can be stated as talking about f * g instead of fun x => f x + g x.

I have also made some changes in the implementation:

• Instead of directly converting from Expr to Array Key during insertion, and directly looking up from an Expr during lookup, I defined the intermediate structure DTExpr, which is a form of Expr that only contains information relevant for the discrimination tree. Each Expr is transformed into a DTExpr before insertion or lookup. For insertion there could be multiple DTExpr representations due to potential η-reductions as mentioned above.

TODO:

• More thought could be put into the matching algorithm for non-trivial unifications. For example, when looking up the expression ?a + ?a (for rewriting), there will only be results like n + n = 2 * n or a + b = b + a, but not like n + 1 = n.succ, even though this would still unify.

• The reason why implicit arguments are not ignored by the discrimination tree is that they provide important type information. Because of this it seems more natural to index the types of expressions instead of indexing the implicit type arguments. Then each key would additionally index the type of that expression. So instead of indexing ?a + ?b as [⟨HAdd.hAdd, 6⟩, *0, *0, *0, *1, *2, *3], it would be indexed by something like [(*0, ⟨HAdd.hAdd, 6⟩), _, _, _, _, (*0, *1), (*0, *2)]. The advantage of this would be that there will be less duplicate indexing of types, because many functions index the types of their arguments and their return type with implicit arguments, meaning that types unnecessarily get indexed multiple times. This modification can be explored, but it could very well not be an improvement.

Definitions

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.Key : Type

Discrimination tree key.

• star: ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A metavariable. This key matches with anything. It stores an index.

• opaque: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  An opaque variable. This key only matches with itself or Key.star.

• const: Lean.Name → ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A constant. It stores the name and the arity.

• fvar: Lean.FVarId → ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A free variable. It stores the FVarId and the arity.

• bvar: ℕ → ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A bound variable, from a lambda or forall binder. It stores the De Bruijn index and the arity.

• lit: Lean.Literal → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A literal.

• sort: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A sort. Universe levels are ignored.

• lam: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A lambda function.

• forall: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A dependent arrow.

• proj: Lean.Name → ℕ → ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A projection. It stores the structure name, the projection index and the arity.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedKey : Inhabited Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedKey = { default := Mathlib.Meta.FunProp.RefinedDiscrTree.Key.star default }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqKey : BEq Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqKey = { beq := Mathlib.Meta.FunProp.RefinedDiscrTree.beqKey✝ }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instReprKey : Repr Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instReprKey = { reprPrec := Mathlib.Meta.FunProp.RefinedDiscrTree.reprKey✝ }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instHashableKey : Hashable Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instHashableKey = { hash := Mathlib.Meta.FunProp.RefinedDiscrTree.Key.hash }

def Mathlib.Meta.FunProp.RefinedDiscrTree.Key.ctorIdx : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → ℕ

Constructor index used for ordering Key. Note that the index of the star pattern is 0, so that when looking up in a Trie, we can look at the start of the sorted array for all .star patterns.

Equations

• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.star a).ctorIdx = 0
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.opaque.ctorIdx = 1
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.const a a_1).ctorIdx = 2
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.fvar a a_1).ctorIdx = 3
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.bvar a a_1).ctorIdx = 4
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lit a).ctorIdx = 5
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.sort.ctorIdx = 6
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lam.ctorIdx = 7
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.forall.ctorIdx = 8
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.proj a a_1 a_2).ctorIdx = 9

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instLTKey : LT Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instLTKey = { lt := fun (a b : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) => Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lt a b = true }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instDecidableLtKey (a : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (b : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : Decidable (a < b)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instDecidableLtKey a b = inferInstanceAs (Decidable (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lt a b = true))

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatKey : Lean.ToFormat Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatKey = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.Key.format }

def Mathlib.Meta.FunProp.RefinedDiscrTree.Key.arity : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → ℕ

Return the number of arguments that the Key takes.

Equations

• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.const a a_1).arity = a_1
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.fvar a a_1).arity = a_1
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.bvar a a_1).arity = a_1
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lam.arity = 1
• Mathlib.Meta.FunProp.RefinedDiscrTree.Key.forall.arity = 2
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.proj a a_1 a_2).arity = 1 + a_2
• x.arity = 0

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.Trie (α : Type) : Type

Discrimination tree trie. See RefinedDiscrTree.

• node: {α : Type} → Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

  Map from Key to Trie. Children is an Array of size at least 2, sorted in increasing order using Key.lt.

• path: {α : Type} → Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

  Sequence of nodes with only one child. keys is an Array of size at least 1.

• values: {α : Type} → Array α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

  Leaf of the Trie. values is an Array of size at least 1.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedTrie {α : Type} : Inhabited (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedTrie = { default := Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.node #[] }

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mkPath {α : Type} (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (child : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

Trie.path constructor that only inserts the path if it is non-empty.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mkPath keys child = if keys.isEmpty = true then child else Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.path keys child

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.singleton {α : Type} (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (value : α) (i : ℕ) : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

Trie constructor for a single value, taking the keys starting at index i.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mkNode2 {α : Type} (k1 : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (t1 : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) (k2 : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (t2 : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

Trie.node constructor for combining two Key, Trie α pairs.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.values! {α : Type} : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Array α

Return the values from a Trie α, assuming that it is a leaf

Equations

• (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.values vs).values! = vs
• x.values! = panicWithPosWithDecl "Mathlib.Tactic.FunProp.RefinedDiscrTree" "Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.values!" 235 9 "expected .values constructor"

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.children! {α : Type} : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the children of a Trie α, assuming that it is not a leaf. The result is sorted by the Key's

Equations

• One or more equations did not get rendered due to their size.
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.node cs).children! = cs
• (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.path ks c).children! = #[(ks[0]!, Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mkPath (let a := ks; ↑(a.toSubarray 1)) c)]

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatTrie {α : Type} [Lean.ToFormat α] : Lean.ToFormat (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatTrie = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.format }

structure Mathlib.Meta.FunProp.RefinedDiscrTree (α : Type) : Type

Discrimination tree. It is an index from expressions to values of type α.

• root : Lean.PersistentHashMap Mathlib.Meta.FunProp.RefinedDiscrTree.Key (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

  The underlying PersistentHashMap of a RefinedDiscrTree.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabited {α : Type} : Inhabited (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabited = { default := { root := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } } }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormat {α : Type} [Lean.ToFormat α] : Lean.ToFormat (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormat = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.format }

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr : Type

DTExpr is a simplified form of Expr. It is the intermediate step for converting from Expr to Array Key.

• star: Option Lean.MVarId → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A metavariable. It optionally stores an MVarId.

• opaque: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  An opaque variable or a let-expression in the case WhnfCoreConfig.zeta := false.

• const: Lean.Name → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A constant. It stores the name and the arguments.

• fvar: Lean.FVarId → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A free variable. It stores the FVarId and the arguments

• bvar: ℕ → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A bound variable. It stores the De Bruijn index and the arguments

• lit: Lean.Literal → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A literal.

• sort: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A sort.

• lam: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A lambda function. It stores the body.

• forall: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A dependent arrow. It stores the domain and body.

• proj: Lean.Name → ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A projection. It stores the structure name, projection index, struct body and arguments.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedDTExpr : Inhabited Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedDTExpr = { default := Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.star default }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqDTExpr : BEq Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqDTExpr = { beq := Mathlib.Meta.FunProp.RefinedDiscrTree.beqDTExpr✝ }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instReprDTExpr : Repr Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instReprDTExpr = { reprPrec := Mathlib.Meta.FunProp.RefinedDiscrTree.reprDTExpr✝ }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatDTExpr : Lean.ToFormat Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatDTExpr = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.format }

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.size : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → ℕ

Return the size of the DTExpr. This is used for calculating the matching score when two expressions are equal. The score is not incremented at a lambda, which is so that the expressions ∀ x, p[x] and ∃ x, p[x] get the same size.

Encoding an Expr

def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flatten (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (initCapacity : optParam ℕ 16) : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Given a DTExpr, return the linearized encoding in terms of Key, which is used for RefinedDiscrTree indexing.

Equations

• e.flatten initCapacity = StateT.run' (Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flattenAux (Array.mkEmpty initCapacity) e) { stars := #[] }

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.reduce (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM Lean.Expr

Reduction procedure for the RefinedDiscrTree indexing.

@[specialize #[]]

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.lambdaTelescopeReduce {α : Type} {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] [MonadControlT Lean.MetaM m] [Nonempty α] (e : Lean.Expr) (fvars : List Lean.FVarId) (config : Lean.Meta.WhnfCoreConfig) (k : Lean.Expr → List Lean.FVarId → m α) : m α

Repeatedly apply reduce while stripping lambda binders and introducing their variables

def Mathlib.Meta.FunProp.RefinedDiscrTree.isStar : Lean.Expr → Bool

Check whether the expression is represented by Key.star.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar (Lean.Expr.mvar mvarId) = true
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar (f.app arg) = Mathlib.Meta.FunProp.RefinedDiscrTree.isStar f
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar x = false

def Mathlib.Meta.FunProp.RefinedDiscrTree.isStarWithArg (arg : Lean.Expr) : Lean.Expr → Bool

Check whether the expression is represented by Key.star and has arg as an argument.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStarWithArg arg x = false

def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.hasLooseBVars (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) : Bool

Return true if e contains a loose bound variable.

Equations

• e.hasLooseBVars = Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.hasLooseBVarsAux 0 e

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.getIgnores (fn : Lean.Expr) (args : Array Lean.Expr) : Lean.MetaM (Array Bool)

Return for each argument whether it should be ignored.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.getIgnores.isIgnoredArg (arg : Lean.Expr) (domain : Lean.Expr) (binderInfo : Lean.BinderInfo) : Lean.MetaM Bool

Return whether the argument should be ignored.

Equations

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

@[irreducible, specialize #[]]

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.etaExpand {α : Type} (args : Array Lean.Expr) (type : Lean.Expr) (lambdas : List Lean.FVarId) (goalArity : ℕ) (k : Array Lean.Expr → List Lean.FVarId → Lean.MetaM α) : Lean.MetaM α

Introduce new lambdas by η-expansion.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceHBinOpAux (args : Array Lean.Expr) (lambdas : List Lean.FVarId) (instH : Lean.Name) (instPi : Lean.Name) : OptionT Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.FVarId)

Normalize an application of a heterogeneous binary operator like HAdd.hAdd, using:

• f = fun x => f x to increase the arity to 6
• (f + g) a = f a + g a to decrease the arity to 6
• (fun x => f x + g x) = f + g to get rid of any lambdas in front

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceHBinOpAux.distributeLambdas (lambdas : List Lean.FVarId) (type : Lean.Expr) (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.FVarId)

use that (fun x => f x + g x) = f + g

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceHBinOpAux.distributeLambdas [] type lhs rhs = pure (type, lhs, rhs, [])

@[inline]

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceHBinOp (n : Lean.Name) (args : Array Lean.Expr) (lambdas : List Lean.FVarId) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.FVarId))

Normalize an application if the head is +, *, - or /. Optionally return the (type, lhs, rhs, lambdas).

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOpAux (args : Array Lean.Expr) (lambdas : List Lean.FVarId) (instPi : Lean.Name) : OptionT Lean.MetaM (Lean.Expr × Lean.Expr × List Lean.FVarId)

Normalize an application of a unary operator like Inv.inv, using:

• f⁻¹ a = (f a)⁻¹ to decrease the arity to 3
• (fun x => (f a)⁻¹) = f⁻¹ to get rid of any lambdas in front

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOpAux.distributeLambdas (lambdas : List Lean.FVarId) (type : Lean.Expr) (arg : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × List Lean.FVarId)

use that (fun x => (f x)⁻¹) = f⁻¹

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOpAux.distributeLambdas [] type arg = pure (type, arg, [])

@[inline]

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOp (n : Lean.Name) (args : Array Lean.Expr) (lambdas : List Lean.FVarId) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × List Lean.FVarId))

Normalize an application if the head is ⁻¹ or -. Optionally return the (type, arg, lambdas).

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOp `Neg.neg args lambdas = Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOpAux args lambdas `Pi.instNeg
• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOp `Inv.inv args lambdas = Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOpAux args lambdas `Pi.instInv
• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.reduceUnOp n args lambdas = pure none

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprAux (e : Lean.Expr) (root : Bool) : ReaderT Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.Context Lean.MetaM Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return the encoding of e as a DTExpr. If root = false, then e is a strict sub expression of the original expression.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.instMonadCacheExprDTExprM : Lean.MonadCache Lean.Expr Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M

Equations

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

@[specialize #[]]

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.etaPossibilities {α : Type} (e : Lean.Expr) (lambdas : List Lean.FVarId) (k : Lean.Expr → List Lean.FVarId → Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M α) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M α

Return all pairs of body, bound variables that could possibly appear due to η-reduction

@[specialize #[]]

def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.cacheEtaPossibilities (e : Lean.Expr) (original : Lean.Expr) (lambdas : List Lean.FVarId) (k : Lean.Expr → List Lean.FVarId → Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

run etaPossibilities, and cache the result if there are multiple possibilities.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.cacheEtaPossibilities e original lambdas k = k e lambdas

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprsAux (original : Lean.Expr) (root : Bool) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return all encodings of e as a DTExpr, taking possible η-reductions into account. If root = false, then e is a strict sub expression of the original expression.

def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.isSpecific : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Bool

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.mkDTExpr (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return the encoding of e as a DTExpr.

Warning: to account for potential η-reductions of e, use mkDTExprs instead.

The argument fvarInContext allows you to specify which free variables in e will still be in the context when the RefinedDiscrTree is being used for lookup. It should return true only if the RefinedDiscrTree is built and used locally.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.mkDTExprs (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) (onlySpecific : Bool) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM (List Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr)

Similar to mkDTExpr. Return all encodings of e as a DTExpr, taking potential further η-reductions into account.

Equations

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

Inserting intro a RefinedDiscrTree

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.insertInTrie {α : Type} [BEq α] (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (v : α) (i : ℕ) : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

Insert the value v at index keys : Array Key in a Trie.

def Mathlib.Meta.FunProp.RefinedDiscrTree.insertInRefinedDiscrTree {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (v : α) : Mathlib.Meta.FunProp.RefinedDiscrTree α

Insert the value v at index keys : Array Key in a RefinedDiscrTree.

Warning: to account for η-reduction, an entry may need to be added at multiple indexes, so it is recommended to use RefinedDiscrTree.insert for insertion.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.insertDTExpr {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (v : α) : Mathlib.Meta.FunProp.RefinedDiscrTree α

Insert the value v at index e : DTExpr in a RefinedDiscrTree.

Warning: to account for η-reduction, an entry may need to be added at multiple indexes, so it is recommended to use RefinedDiscrTree.insert for insertion.

Equations

• d.insertDTExpr e v = d.insertInRefinedDiscrTree e.flatten v

def Mathlib.Meta.FunProp.RefinedDiscrTree.insert {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Lean.Expr) (v : α) (onlySpecific : optParam Bool true) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Insert the value v at index e : Expr in a RefinedDiscrTree. The argument fvarInContext allows you to specify which free variables in e will still be in the context when the RefinedDiscrTree is being used for lookup. It should return true only if the RefinedDiscrTree is built and used locally.

if onlySpecific := true, then we filter out the patterns * and Eq * * *.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.insertEqn {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (lhs : Lean.Expr) (rhs : Lean.Expr) (vLhs : α) (vRhs : α) (onlySpecific : optParam Bool true) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Insert the value vLhs at index lhs, and if rhs is indexed differently, then also insert the value vRhs at index rhs.

Equations

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

Matching with a RefinedDiscrTree

We use a very simple unification algorithm. For all star/metavariable patterns in the RefinedDiscrTree and in the target, we store the assignment, and when it is assigned again, we check that it is the same assignment.

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.findKey {α : Type} (children : Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)) (k : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : Option (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

If k is a key in children, return the corresponding Trie α. Otherwise return none.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.skipEntries {α : Type} (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) (skipped : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : ℕ → Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with n metavariable.

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchTargetStar {α : Type} (mvarId? : Option Lean.MVarId) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with anything. We add 1 to the matching score when the key is .opaque, since this pattern is "harder" to match with.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchTreeStars {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that come from a Key.star, while keeping track of the Key.star assignments.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchExpr {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with e.

@[specialize #[]]

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.exactMatch {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (find? : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Option (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

If e is not a metavariable, return the possible Trie α that exactly match with e.

def Mathlib.Meta.FunProp.RefinedDiscrTree.getMatchWithScore {α : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Lean.Expr) (unify : Bool) (config : Lean.Meta.WhnfCoreConfig) (allowRootStar : optParam Bool false) : Lean.MetaM (Array (Array α × ℕ))

Return the results from the RefinedDiscrTree that match the given expression, together with their matching scores, in decreasing order of score.

Each entry of type Array α × Nat corresponds to one pattern.

If unify := false, then metavariables in e are treated as opaque variables. This is for when you don't want to instantiate metavariables in e.

If allowRootStar := false, then we don't allow e or the matched key in d to be a star pattern.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.getMatchWithScoreWithExtra {α : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Lean.Expr) (unify : Bool) (config : Lean.Meta.WhnfCoreConfig) (allowRootStar : optParam Bool false) : Lean.MetaM (Array (Array α × ℕ × ℕ))

Similar to getMatchWithScore, but also returns matches with prefixes of e. We store the score, followed by the number of ignored arguments.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.getMatchWithScoreWithExtra.go {α : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (unify : Bool) (config : Lean.Meta.WhnfCoreConfig) (allowRootStar : optParam Bool false) (e : Lean.Expr) (numIgnored : ℕ) : Lean.MetaM (Array (Array α × ℕ × ℕ))

go

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mapArraysM {α : Type} {β : Type} {m : Type → Type} [Monad m] (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) (f : Array α → m (Array β)) : m (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie β)

Apply a monadic function to the array of values at each node in a RefinedDiscrTree.

def Mathlib.Meta.FunProp.RefinedDiscrTree.mapArraysM {α : Type} {β : Type} {m : Type → Type} [Monad m] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (f : Array α → m (Array β)) : m (Mathlib.Meta.FunProp.RefinedDiscrTree β)

Apply a monadic function to the array of values at each node in a RefinedDiscrTree.

Equations

• d.mapArraysM f = do let __do_lift ← d.root.mapM fun (x : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) => x.mapArraysM f pure { root := __do_lift }

def Mathlib.Meta.FunProp.RefinedDiscrTree.mapArrays {α : Type} {β : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (f : Array α → Array β) : Mathlib.Meta.FunProp.RefinedDiscrTree β

Apply a function to the array of values at each node in a RefinedDiscrTree.

Equations

• d.mapArrays f = d.mapArraysM f