Documentation

Lean.Meta.Tactic.Grind.EMatchTheorem

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

                    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

                          A unique identifier corresponding to the origin.

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

                                Set of E-matching theorems.

                                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

                                      Mark 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
                                          @[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

                                                      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) :

                                                                      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.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (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
                                                                              def Lean.Meta.Grind.mkEMatchTheoremWithKind?.go (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (groundPatterns : Bool := true) (showInfo : Bool := false) (xs searchPlaces : Array Expr) :
                                                                              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) (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