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

    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
    • One or more equations did not get rendered due to their size.
    Instances For

      Return the number of arguments that the Key takes.

      Equations
      • One or more equations did not get rendered due to their size.
      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
            • One or more equations did not get rendered due to their size.
            Instances For

              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.
              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 heterogenous 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).

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  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
                                        @[inline]

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        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
                                            @[specialize #[]]

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

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            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 accound 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 accound 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