Documentation

Mathlib.Tactic.FunProp.Types

funProp #

this file defines environment extension for funProp

Indicated origin of a function or a statement.

Instances For

    Name of the origin.

    Equations
      Instances For

        Get the expression specified by origin.

        Equations
          Instances For

            Pretty print FunProp.Origin.

            Equations
              Instances For

                Pretty print FunProp.Origin. Returns string unlike ppOrigin.

                Equations
                  Instances For

                    Get origin of the head function.

                    Equations
                      Instances For

                        Default names to be considered reducible by fun_prop

                        Equations
                          Instances For

                            fun_prop configuration

                            • maxTransitionDepth :

                              Maximum number of transitions between function properties. For example inferring continuity from differentiability and then differentiability from smoothness (ContDiff ℝ ∞) requires maxTransitionDepth = 2. The default value of one expects that transition theorems are transitively closed e.g. there is a transition theorem that infers continuity directly from smoothenss.

                              Setting maxTransitionDepth to zero will disable all transition theorems. This can be very useful when fun_prop should fail quickly. For example when using fun_prop as discharger in simp.

                            • maxSteps :

                              Maximum number of steps fun_prop can take.

                            Instances For

                              fun_prop context

                              Instances For

                                fun_prop state

                                • Simp's cache is used as the fun_prop tactic is designed to be used inside of simp and utilize its cache. It holds successful goals.

                                • failureCache : Lean.ExprSet

                                  Cache storing failed goals such that they are not tried again.

                                • numSteps :

                                  Count the number of steps and stop when maxSteps is reached.

                                • msgLog : List String

                                  Log progress and failures messages that should be displayed to the user at the end.

                                Instances For

                                  Increase depth

                                  Equations
                                    Instances For
                                      @[reducible, inline]

                                      Monad to run fun_prop tactic in.

                                      Equations
                                        Instances For

                                          Result of funProp, it is a proof of function property P f

                                          Instances For

                                            Default names to unfold

                                            Equations
                                              Instances For

                                                Get predicate on names indicating if theys shoulds be unfolded.

                                                Equations
                                                  Instances For

                                                    Increase heartbeat, throws error when maxSteps was reached

                                                    Equations
                                                      Instances For

                                                        Increase transition depth. Return none if maximum transition depth has been reached.

                                                        Equations
                                                          Instances For

                                                            Log error message that will displayed to the user at the end.

                                                            Messages are logged only when transitionDepth = 0 i.e. when fun_prop is not trying to infer function property like continuity from another property like differentiability. The main reason is that if the user forgets to add a continuity theorem for function foo then fun_prop should report that there is a continuity theorem for foo missing. If we would log messages transitionDepth > 0 then user will see messages saying that there is a missing theorem for differentiability, smoothness, ... for foo.

                                                            Equations
                                                              Instances For