Documentation

Mathlib.Tactic.FunProp.RefinedDiscrTree

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:

I have also made some changes in the implementation:

TODO:

Definitions #

Discrimination tree key.

Instances For

    Discrimination tree trie. See RefinedDiscrTree.

    Instances For
      Equations

      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.
      Instances For

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

        Equations
        Instances For

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

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

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

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

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

              Instances For

                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 #

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

                Equations
                Instances For
                  @[specialize #[]]

                  Repeatedly apply reduce while stripping lambda binders and introducing their variables

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

                  Equations
                  Instances For

                    Return for each argument whether it should be ignored.

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

                      Return whether the argument should be ignored.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[irreducible, specialize #[]]

                        Introduce new lambdas by η-expansion.

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

                          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.
                          Instances For

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

                            Equations
                            Instances For
                              @[inline]

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

                              Instances For

                                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.
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    @[specialize #[]]

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

                                    Instances For

                                      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.

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

                                        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.
                                        Instances For

                                          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.
                                          Instances For

                                            Inserting intro a 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.
                                            Instances For

                                              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
                                              Instances For

                                                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.
                                                Instances For
                                                  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.FVarIdBool) fun (x : Lean.FVarId) => false) :

                                                  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.
                                                  Instances For

                                                    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.

                                                    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.
                                                    Instances For

                                                      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.
                                                      Instances For

                                                        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.
                                                        Instances For

                                                          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.
                                                          Instances For

                                                            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.
                                                            Instances For

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

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

                                                              Equations
                                                              Instances For

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

                                                                Equations
                                                                • d.mapArrays f = d.mapArraysM f
                                                                Instances For