Documentation

Lean.Meta.Tactic.Simp.Main

Return true if e is of the form ofNat n where n is a kernel Nat literal

Equations
Instances For

    If e is a raw Nat literal and OfNat.ofNat is not in the list of declarations to unfold, return an OfNat.ofNat-application.

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

      Return true if e is of the form ofScientific n b m where n and m are kernel Nat literals.

      Equations
      Instances For

        Return true if e is of the form Char.ofNat n where n is a kernel Nat literals.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          partial def Lean.Meta.Simp.lambdaTelescopeDSimp.go {α : Type} (k : Array ExprExprSimpM α) (xs : Array Expr) (e : Expr) :
          def Lean.Meta.Simp.withNewLemmas {α : Type} (xs : Array Expr) (f : SimpM α) :

          We use withNewlemmas whenever updating the local context.

          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
                • 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

                      Information about a single have in a have telescope. Created by getHaveTelescopeInfo.

                      Instances For
                        Equations

                        Information about a have telescope. Created by getHaveTelescopeInfo and used in simpHaveTelescope.

                        The data is used to avoid applying Expr.abstract more than once on any given subexpression when constructing terms and proofs during simplification. Abstraction is linear in the size t of a term, and so in a depth-n telescope it is O(nt), quadratic in n, since n ≤ t. For example, given have x₁ := v₁; ...; have xₙ := vₙ; b and h : b = b', we need to construct

                        have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))
                        

                        We apply Expr.abstract to h once and then build the term, rather than using mkLambdaFVars #[fvarᵢ] pfᵢ at each step.

                        As an additional optimization, we save the fvar-instantiated terms calculated by getHaveTelescopeInfo so that we don't have to compute them again. This is only saving a constant factor.

                        It is also used for computing used haves in computeFixedUsed. In have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b, if xₙ is unused in b, then all the haves are unused. Without a global computation of used haves, the proof term would be quadratic in the number of haves (with n iterations of simp). Knowing which haves are transitively unused lets the proof term be linear in size.

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

                          Efficiently collect dependency information for a have telescope. This is part of a scheme to avoid quadratic overhead from the locally nameless discipline (see HaveTelescopeInfo and simpHaveTelescope).

                          The expression e must not have loose bvars.

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

                              Computes which haves in the telescope are fixed and which are unused. The length of the unused array may be less than the number of haves: use unused.getD i true.

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

                                Routine for simplifying have telescopes. Used by simpLet. This is optimized to be able to handle deep have telescopes while avoiding quadratic complexity arising from the locally nameless expression representations.

                                Overview #

                                Consider a have telescope:

                                have x₁ : T₁ := v₁; ...; have xₙ : Tₙ := vₙ; b
                                

                                We say xᵢ is fixed if it appears in the type of b. If xᵢ is fixed, then it can only be rewritten using definitional equalities. Otherwise, we can freely rewrite the value using a propositional equality vᵢ = vᵢ'. The body b can always be freely rewritten using a propositional equality b = b'. (All the mentioned equalities must be type correct with respect to the obvious local contexts.)

                                If xᵢ neither appears in b nor any Tⱼ nor any vⱼ, then its have is unused. Unused haves can be eliminated, which we do if cfg.zetaUnused is true. We clear haves from the end, to be able to transitively clear chains of unused haves. This is why we honor zetaUnused here even though reduceStep is also responsible for it; reduceStep can only eliminate unused haves at the start of a telescope. Eliminating all transitively unused haves at once like this also avoids quadratic complexity.

                                If debug.simp.check.have is enabled then we typecheck the resulting expression and proof.

                                Proof generation #

                                There are two main complications with generating proofs.

                                1. We work almost exclusively with expressions with loose bound variables, to avoid overhead from instantiating and abstracting free variables, which can lead to complexity quadratic in the telescope length. (See HaveTelescopeInfo.)
                                2. We want to avoid triggering zeta reductions in the kernel.

                                Regarding this second point, the issue is that we cannot organize the proof using congruence theorems in the obvious way. For example, given

                                theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
                                    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
                                    (have x := a; f x) = (have x := a'; f' x)
                                

                                the kernel sees that the type of have_congr (fun x => b) (fun x => b') h₁ h₂ is (have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x), since when instantiating values it does not beta reduce at the same time. Hence, when is_def_eq is applied to the LHS and have x := a; b for example, it will do whnf_core to both sides.

                                Instead, we use the form (fun x => b) a = (fun x => b') a' in the proofs, which we can reliably match up without triggering beta reductions in the kernel. The zeta/beta reductions are then limited to the type hint for the entire telescope, when we convert this back into have form. In the base case, we include an optimization to avoid unnecessary zeta/beta reductions, by detecting a simpHaveTelescope proofs and removing the type hint.

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

                                  Routine for simplifying let expressions.

                                  If it is a have, we use simpHaveTelescope to simplify entire telescopes at once, to avoid quadratic behavior arising from locally nameless expression representations.

                                  We assume that dependent lets are dependent, but if Config.letToHave is enabled then we attempt to transform it into a have. If that does not change it, then it is only dsimped.

                                  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

                                        Process the given congruence theorem hypothesis. Return true if it made "progress".

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

                                          Try to rewrite e children using the given congruence theorem

                                          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
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[export lean_simp]
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[inline]
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Lean.Meta.Simp.mainCore (e : Expr) (ctx : Context) (s : State := { }) (methods : Methods := { }) :
                                                      Equations
                                                      Instances For
                                                        def Lean.Meta.Simp.main (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) :
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          def Lean.Meta.Simp.dsimpMain (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) :
                                                          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.simp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { }) :
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                def Lean.Meta.dsimp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { }) :
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  def Lean.Meta.simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) :

                                                                  See simpTarget. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    def Lean.Meta.simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) :

                                                                    Simplify the given goal target (aka type). Return none if the goal was closed. Return some mvarId' otherwise, where mvarId' is the simplified new goal.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def Lean.Meta.applySimpResult (mvarId : MVarId) (val type : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) :

                                                                      Applies the result r for type (which is inhabited by val). Returns none if the goal was closed. Returns some (val', type') otherwise, where val' : type' and type' is the simplified type.

                                                                      This method assumes mvarId is not assigned, and we are already using mvarIds local context.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[deprecated Lean.Meta.applySimpResult (since := "2025-03-26")]
                                                                        def Lean.Meta.applySimpResultToProp (mvarId : MVarId) (proof prop : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) :
                                                                        Equations
                                                                        Instances For
                                                                          def Lean.Meta.applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) :
                                                                          Equations
                                                                          Instances For
                                                                            def Lean.Meta.simpStep (mvarId : MVarId) (proof prop : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) :

                                                                            Simplify prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

                                                                            This method assumes mvarId is not assigned, and we are already using mvarIds local context.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              Equations
                                                                              Instances For
                                                                                def Lean.Meta.applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) :

                                                                                Simplify simp result to the given local declaration. Return none if the goal was closed. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  def Lean.Meta.simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) :
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    def Lean.Meta.simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { }) :
                                                                                    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.dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { }) :
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For