Documentation

Lean.Meta.Tactic.Grind.EMatchTheorem

grind uses symbol priorities when inferring patterns for E-matching. Symbols not in map are assumed to have default priority (i.e., eval_prio default).

Instances For
    Instances For

      Removes the given declaration from s.

      Equations
      Instances For

        Inserts declNameprio into s.

        Equations
        Instances For

          Returns declName priority for E-matching pattern inference in s.

          Equations
          Instances For

            Returns true, if there is an entry declNameprio in s. Recall that symbols not in s are assumed to have default priority.

            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Lean.Meta.Grind.addSymbolPriorityAttr (declName : Name) (attrKind : AttributeKind) (prio : Nat) :

                Sets declName priority to be used during E-matching pattern inference

                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lean.Meta.Grind.mkGenPattern (u : List Level) (α h x val : Expr) :
                            Equations
                            Instances For
                              def Lean.Meta.Grind.mkGenHEqPattern (u : List Level) (α β h x val : Expr) :
                              Equations
                              Instances For

                                Generalized pattern information. See Grind.genPattern gadget.

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

                                      Returns true if declName is the name of a match-expression congruence equation.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def Lean.Meta.Grind.preprocessPattern (pat : Expr) (normalizePattern : Bool := true) :
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          • decl (declName : Name) : Origin

                                            A global declaration in the environment.

                                          • fvar (fvarId : FVarId) : Origin

                                            A local hypothesis.

                                          • stx (id : Name) (ref : Syntax) : Origin

                                            A proof term provided directly to a call to grind where ref is the provided grind argument. The id is a unique identifier for the call.

                                          • local (id : Name) : Origin

                                            It is local, but we don't have a local hypothesis for it.

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

                                              A unique identifier corresponding to the origin.

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

                                                      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
                                                      • The kind is used for generating the patterns. We save it here to implement grind?.

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

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

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

                                                            Equations
                                                            Instances For

                                                              Marks the theorem with the given origin as erased

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

                                                                Returns true if the theorem has been marked as erased.

                                                                Equations
                                                                Instances For

                                                                  Returns true if there is a theorem with exactly the same pattern is already in s

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

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

                                                                        Returns theorems associated with the given origin.

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

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

                                                                                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.

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

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

                                                                                        Auxiliary type for the checkCoverage function.

                                                                                        Instances For
                                                                                          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.
                                                                                          Instances For
                                                                                            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.
                                                                                            Instances For
                                                                                              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.
                                                                                              Instances For
                                                                                                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.
                                                                                                Instances For
                                                                                                  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.
                                                                                                  Instances For
                                                                                                    def Lean.Meta.Grind.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (attrKind : AttributeKind := AttributeKind.global) :

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

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

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

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Returns the E-matching theorems registered in the environment.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def Lean.Meta.Grind.mkEMatchTheoremUsingSingletonPatterns (origin : Origin) (levelParams : Array Name) (proof : Expr) (minPrio : Nat) (symPrios : SymbolPriorities) (showInfo : Bool := false) :

                                                                                                          Collects all singleton patterns in the type of the given proof. We use this function to implement local forall expressions in a grind goal.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            def Lean.Meta.Grind.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (showInfo : Bool := false) :

                                                                                                            Creates an E-match theorem using the given proof and kind. If groundPatterns is true, it accepts patterns without pattern variables. This is useful for theorems such as theorem evenZ : Even 0. For local theorems, we use groundPatterns := false since the theorem is already in the grind state and there is nothing to be instantiated.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    def Lean.Meta.Grind.addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo : Bool := false) :
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For