Documentation

Lean.Meta.Tactic.Simp.SimpTheorems

An Origin is an identifier for simp theorems which indicates roughly what action the user took which lead to this theorem existing in the simp set.

  • decl: Lake.NameoptParam Bool trueoptParam Bool falseLean.Meta.Origin

    A global declaration in the environment.

  • fvar: Lean.FVarIdLean.Meta.Origin

    A local hypothesis. When contextual := true is enabled, this fvar may exist in an extension of the current local context; it will not be used for rewriting by simp once it is out of scope but it may end up in the usedSimps trace.

  • stx: Lake.NameLean.SyntaxLean.Meta.Origin

    A proof term provided directly to a call to simp [ref, ...] where ref is the provided simp argument (of kind Parser.Tactic.simpLemma). The id is a unique identifier for the call.

  • other: Lake.NameLean.Meta.Origin

    Some other origin. name should not collide with the other types for erasure to work correctly, and simp trace will ignore this lemma. The other origins should be preferred if possible.

Instances For

    A unique identifier corresponding to the origin.

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

        The fields levelParams and proof are used to encode the proof of the simp theorem. If the proof is a global declaration c, we store Expr.const c [] at proof without the universe levels, and levelParams is set to #[] When using the lemma, we create fresh universe metavariables. Motivation: most simp theorems are global declarations, and this approach is faster and saves memory.

        The field levelParams is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables. Then, we use abstractMVars to abstract the universe metavariables and create new fresh universe parameters that are stored at the field levelParams.

        • levelParams : Array Lake.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 : Lean.Expr
        • priority : Nat
        • post : Bool
        • perm : Bool

          perm is true if lhs and rhs are identical modulo permutation of variables.

        • origin is mainly relevant for producing trace messages. It is also viewed an id used to "erase" simp theorems from SimpTheorems.

        • rfl : Bool

          rfl is true if proof is by Eq.refl or rfl.

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

                Configuration for the discrimination tree.

                Equations
                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

                        Return true if declName is tagged to be unfolded using unfoldDefinition? (i.e., without using equational theorems).

                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For

                              Register the equational theorems for the given definition.

                              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
                                  Instances For
                                    def Lean.Meta.addSimpTheorem (ext : Lean.Meta.SimpExtension) (declName : Lake.Name) (post : Bool) (inv : Bool) (attrKind : Lean.AttributeKind) (prio : Nat) :
                                    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
                                        Instances For

                                          Auxiliary method for adding a global declaration to a SimpTheorems datastructure.

                                          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 method for creating simp theorems from a proof term val.

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

                                                Auxiliary method for adding a local simp theorem to a SimpTheorems datastructure.

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

                                                  Reducible functions and projection functions should always be put in toUnfold, instead of trying to use equational theorems.

                                                  The simplifiers has special support for structure and class projections, and gets confused when they suddenly rewrite, so ignore equations for them

                                                  Equations
                                                  Instances For

                                                    Even if a function has equation theorems, we also store it in the toUnfold set in the following two cases: 1- It was defined by structural recursion and has a smart-unfolding associated declaration. 2- It is non-recursive.

                                                    Reason: unfoldPartialApp := true or conditional equations may not apply.

                                                    Remark: In the future, we are planning to disable this behavior unless unfoldPartialApp := true. Moreover, users will have to use f.eq_def if they want to force the definition to be unfolded.

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