Documentation

Lean.Meta.Tactic.Simp.Types

The result of simplifying some expression e.

  • expr : Lean.Expr

    The simplified version of e

  • proof? : Option Lean.Expr

    A proof that $e = $expr, where the simplified expression is on the RHS. If none, the proof is assumed to be refl.

  • cache : Bool

    If cache := true the result is cached. Warning: we will remove this field in the future. It is currently used by arith := true, but we can now refactor the code to avoid the hack.

Instances For
    Equations
    Equations
    Instances For

      Flip the proof in a Simp.Result.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        • maxDischargeDepth : UInt32
        • parent? : Option Lean.Expr

          Stores the "parent" term for the term being simplified. If a simplification procedure result depends on this value, then it is its reponsability to set Result.cache := false.

          Motivation for this field: Suppose we have a simplification procedure for normalizing arithmetic terms. Then, given a term such as t_1 + ... + t_n, we don't want to apply the procedure to every subterm t_1 + ... + t_i for i < n for performance issues. The procedure can accomplish this by checking whether the parent term is also an arithmetical expression and do nothing if it is. However, it should set Result.cache := false to ensure we don't miss simplification opportunities. For example, consider the following:

          example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
            simp_arith only
            ...
          

          If we don't set Result.cache := false for the first x + x, then we get the resulting state:

          ... |- id (2*x + y) = id (x + x)
          

          instead of

          ... |- id (2*x + y) = id (2*x)
          

          as expected.

          Remark: given an application f a b c the "parent" term for f, a, b, and c is f a b c.

        • dischargeDepth : UInt32
        • lctxInitIndices : Nat

          Number of indices in the local context when starting simp. We use this information to decide which assumptions we can use without invalidating the cache.

        • inDSimp : Bool

          If inDSimp := true, then simp is in dsimp mode, and only applying transformations that presereve definitional equality.

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

                    Result type for a simplification procedure. We have pre and post simplification procedures.

                    Instances For
                      @[reducible, inline]

                      A simplification procedure. Recall that we have pre and post procedures. See Step.

                      Equations
                      Instances For
                        @[reducible, inline]
                        Equations
                        Instances For
                          @[reducible, inline]

                          Similar to Simproc, but resulting expression should be definitionally equal to the input one.

                          Equations
                          Instances For
                            Equations
                            Instances For
                              @[always_inline]

                              "Compose" the two given simplification procedures. We use the following semantics.

                              • If f produces done or visit, then return f's result.
                              • If f produces continue, then apply g to new expression returned by f.

                              See Simp.Step type.

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

                                  Simproc .olean entry.

                                  Instances For
                                    Equations

                                    Simproc entry. It is the .olean entry plus the actual function.

                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        @[implemented_by Lean.Meta.Simp.Methods.toMethodsRefImpl]
                                        @[implemented_by Lean.Meta.Simp.MethodsRef.toMethodsImpl]
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            @[inline]
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              Returns true if simp is in dsimp mode. That is, only transformations that preserve definitional equality should be applied.

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

                                                  Save current cache, reset it, execute x, and then restore original cache.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[inline]
                                                    def Lean.Meta.Simp.withDischarger {α : Type} (discharge? : Lean.ExprLean.Meta.SimpM (Option Lean.Expr)) (wellBehavedDischarge : Bool) (x : Lean.Meta.SimpM α) :
                                                    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
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              Equations
                                                              Instances For

                                                                Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

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

                                                                  Construct the Expr cast h e, from a Simp.Result with proof h.

                                                                  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

                                                                          Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

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

                                                                              Given a simplified function result r and arguments args, simplify arguments using simp and dsimp. The resulting proof is built using congr and congrFun theorems.

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

                                                                                Retrieve auto-generated congruence lemma for f.

                                                                                Remark: If all argument kinds are fixed or eq, it returns none because using simple congruence theorems congr, congrArg, and congrFun produces a more compact proof.

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

                                                                                  Try to use automatically generated congruence theorems. See mkCongrSimp?.

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

                                                                                    Return a WHNF configuration for retrieving [simp] from the discrimination tree. If user has disabled zeta and/or beta reduction in the simplifier, or enabled zetaDelta, we must also disable/enable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281

                                                                                    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. Given the current target of mvarId, apply r which is a new target and proof that it is equal to the current one.

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