Documentation

Lean.Meta.Tactic.Simp.Types

The result of simplifying some expression e.

  • expr : Expr

    The simplified version of e

  • proof? : Option 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
      Instances For
        Equations
          Instances For

            Flip the proof in a Simp.Result.

            Equations
              Instances For
                @[reducible, inline]
                Equations
                  Instances For
                    @[reducible, inline]
                    Equations
                      Instances For
                        • config : Config
                        • zetaDeltaSet : FVarIdSet

                          Local declarations to propagate to Meta.Context

                        • initUsedZetaDelta : FVarIdSet

                          When processing Simp arguments, zetaDelta may be performed if zetaDeltaSet is not empty. We save the local free variable ids in initUsedZetaDelta. initUsedZetaDelta is a subset of zetaDeltaSet.

                        • metaConfig : ConfigWithKey
                        • indexConfig : ConfigWithKey
                        • maxDischargeDepth : UInt32
                        • simpTheorems : SimpTheoremsArray
                        • congrTheorems : SimpCongrTheorems
                        • parent? : Option 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
                          def Lean.Meta.Simp.mkContext (config : Config := { }) (simpTheorems : SimpTheoremsArray := ) (congrTheorems : SimpCongrTheorems := { }) :
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              def Lean.Meta.Simp.Context.setZetaDeltaSet (c : Context) (zetaDeltaSet initUsedZetaDelta : FVarIdSet) :
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            • usedThmCounter : PHashMap Origin Nat

                                                              Number of times each simp theorem has been used/applied.

                                                            • triedThmCounter : PHashMap Origin Nat

                                                              Number of times each simp theorem has been tried.

                                                            • congrThmCounter : PHashMap Name Nat

                                                              Number of times each congr theorem has been tried.

                                                            • thmsWithBadKeys : PArray SimpTheorem

                                                              When using Simp.Config.index := false, and set_option diagnostics true, for every theorem used by simp, we check whether the theorem would be also applied if index := true, and we store it here if it would not have been tried.

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

                                                                                      Executes x using a MetaM configuration for indexing terms. It is inferred from Simp.Config. For example, if the user has set simp (config := { zeta := false }), isDefEq and whnf in MetaM should not perform zeta reduction.

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[inline]

                                                                                          Executes x using a MetaM configuration for inferred from Simp.Config.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[extern lean_simp]
                                                                                              @[extern lean_dsimp]
                                                                                              @[inline]
                                                                                              Equations
                                                                                                Instances For

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

                                                                                                  • done (r : Result) : Step

                                                                                                    For pre procedures, it returns the result without visiting any subexpressions.

                                                                                                    For post procedures, it returns the result.

                                                                                                  • visit (e : Result) : Step

                                                                                                    For pre procedures, the resulting expression is passed to pre again.

                                                                                                    For post procedures, the resulting expression is passed to pre again IF Simp.Config.singlePass := false and resulting expression is not equal to initial expression.

                                                                                                  • continue (e? : Option Result := none) : Step

                                                                                                    For pre procedures, continue transformation by visiting subexpressions, and then executing post procedures.

                                                                                                    For post procedures, this is equivalent to returning visit.

                                                                                                  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
                                                                                                                      Instances For
                                                                                                                        @[always_inline]
                                                                                                                        Equations
                                                                                                                          Instances For

                                                                                                                            Simproc .olean entry.

                                                                                                                            Instances For

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

                                                                                                                              Instances For
                                                                                                                                @[reducible, inline]
                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    Instances For
                                                                                                                                      Instances For
                                                                                                                                        @[implemented_by Lean.Meta.Simp.Methods.toMethodsRefImpl]
                                                                                                                                        @[implemented_by Lean.Meta.Simp.MethodsRef.toMethodsImpl]
                                                                                                                                        Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Lean.Meta.Simp.withParent {α : Type} (parent : Expr) (f : SimpM α) :
                                                                                                                                                            Equations
                                                                                                                                                              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
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]

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

                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Lean.Meta.Simp.withDischarger {α : Type} (discharge? : ExprSimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) :
                                                                                                                                                                            Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        Equations
                                                                                                                                                                                          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
                                                                                                                                                                                                  Instances For

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

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                      Instances For

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

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        def Lean.Meta.Simp.mkImpCongr (src : Expr) (r₁ r₂ : Result) :
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                          Instances For

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

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

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

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