Documentation

Lean.Meta.Tactic.Grind.EMatchTheorem

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

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

                                Equations
                                  Instances For
                                    def Lean.Meta.Grind.preprocessPattern (pat : Expr) (normalizePattern : Bool := true) :
                                    Equations
                                      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
                                              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

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

                                                                            Returns theorems associated with the given origin.

                                                                            Equations
                                                                              Instances For

                                                                                Returns true if declName has been tagged as an E-match theorem using [grind].

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

                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                              Instances For
                                                                                                @[reducible, inline]
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    • 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
                                                                                                        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
                                                                                                              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
                                                                                                                  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
                                                                                                                      Instances For
                                                                                                                        def Lean.Meta.Grind.mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo : Bool := false) :
                                                                                                                        Equations
                                                                                                                          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
                                                                                                                              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
                                                                                                                                  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
                                                                                                                                              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
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                          Instances For
                                                                                                                                                            def Lean.Meta.Grind.addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (showInfo : Bool := false) :
                                                                                                                                                            Equations
                                                                                                                                                              Instances For
                                                                                                                                                                Equations
                                                                                                                                                                  Instances For