Documentation

Lean.Meta.Tactic.Simp.Main

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

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.

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

            We use withNewlemmas whenever updating the local context.

            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

                      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

                          Returns true if e is of the form @letFun _ (fun _ => β) _ _

                          β must not contain loose bound variables. Recall that simp does not have support for let_funs where resulting type depends on the let-value. Example:

                          let_fun n := 10;
                          BitVec.zero n
                          
                          Instances For

                            Simplifies a sequence of let_fun declarations. It attempts to minimize the quadratic overhead imposed by the locally nameless discipline.

                            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
                                @[export lean_simp]
                                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
                                    @[inline]
                                    Instances For
                                      def Lean.Meta.Simp.main (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) (methods : Lean.Meta.Simp.Methods := { pre := fun (x : Lean.Expr) => pure Lean.Meta.Simp.Step.continue, post := fun (e : Lean.Expr) => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, cache := true }), dpre := fun (x : Lean.Expr) => pure Lean.TransformStep.continue, dpost := fun (e : Lean.Expr) => pure (Lean.TransformStep.done e), discharge? := fun (x : Lean.Expr) => pure none, wellBehavedDischarge := true }) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def Lean.Meta.Simp.dsimpMain (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) (methods : Lean.Meta.Simp.Methods := { pre := fun (x : Lean.Expr) => pure Lean.Meta.Simp.Step.continue, post := fun (e : Lean.Expr) => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, cache := true }), dpre := fun (x : Lean.Expr) => pure Lean.TransformStep.continue, dpost := fun (e : Lean.Expr) => pure (Lean.TransformStep.done e), discharge? := fun (x : Lean.Expr) => pure none, wellBehavedDischarge := true }) :
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def Lean.Meta.simp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Lean.Meta.dsimp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Lean.Meta.simpTargetCore (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :

                                                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 : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :

                                                  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.

                                                  Instances For

                                                    Apply the result r for 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.simpStep (mvarId : Lean.MVarId) (proof prop : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :

                                                        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

                                                          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 : Lean.MVarId) (fvarId : Lean.FVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Lean.Meta.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array Lean.FVarId := #[]) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                                              Instances For
                                                                def Lean.Meta.simpTargetStar (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (discharge? : Option Lean.Meta.Simp.Discharge := none) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  def Lean.Meta.dsimpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array Lean.FVarId := #[]) (stats : Lean.Meta.Simp.Stats := { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :
                                                                  Instances For