Documentation

Mathlib.Tactic.FunProp.Core

Tactic fun_prop for proving function properties like Continuous f, Differentiable ℝ f, ... #

Synthesize instance of type type and

  1. assign it to x if x is meta variable
  2. check it is equal to x
Equations
    Instances For

      Synthesize arguments xs either with typeclass synthesis, with fun_prop or with discharger.

      Equations
        Instances For

          Try to apply theorem - core function

          Equations
            Instances For
              def Mathlib.Meta.FunProp.tryTheoremWithHint? (e : Lean.Expr) (thmOrigin : Origin) (hint : Array ( × Lean.Expr)) (funProp : Lean.ExprFunPropM (Option Result)) (newMCtxDepth : Bool := false) :

              Try to apply a theorem provided some of the theorem arguments.

              Equations
                Instances For
                  def Mathlib.Meta.FunProp.tryTheorem? (e : Lean.Expr) (thmOrigin : Origin) (funProp : Lean.ExprFunPropM (Option Result)) (newMCtxDepth : Bool := false) :

                  Try to apply a theorem thmOrigin to the goal e.

                  Equations
                    Instances For

                      Try to prove e using using identity lambda theorem.

                      For example, e = q(Continuous fun x => x) and funPropDecl is FunPropDecl for Continuous.

                      Equations
                        Instances For

                          Try to prove e using using constant lambda theorem.

                          For example, e = q(Continuous fun x => y) and funPropDecl is FunPropDecl for Continuous.

                          Equations
                            Instances For

                              Try to prove e using using apply lambda theorem.

                              For example, e = q(Continuous fun f => f x) and funPropDecl is FunPropDecl for Continuous.

                              Equations
                                Instances For

                                  Try to prove e using composition lambda theorem.

                                  For example, e = q(Continuous fun x => f (g x)) and funPropDecl is FunPropDecl for Continuous

                                  You also have to provide the functions f and g.

                                  Equations
                                    Instances For

                                      Try to prove e using pi lambda theorem.

                                      For example, e = q(Continuous fun x y => f x y) and funPropDecl is FunPropDecl for Continuous

                                      Equations
                                        Instances For

                                          Try to prove e = q(P (fun x => let y := φ x; ψ x y).

                                          For example,

                                          • funPropDecl is FunPropDecl for Continuous
                                          • e = q(Continuous fun x => let y := φ x; ψ x y)
                                          • f = q(fun x => let y := φ x; ψ x y)
                                          Equations
                                            Instances For

                                              Prove function property of using morphism theorems.

                                              Equations
                                                Instances For

                                                  Prove function property of using transition theorems.

                                                  Equations
                                                    Instances For

                                                      Try to remove applied argument i.e. prove P (fun x => f x y) from P (fun x => f x).

                                                      For example

                                                      • funPropDecl is FunPropDecl for Continuous
                                                      • e = q(Continuous fun x => foo (bar x) y)
                                                      • fData contains info on fun x => foo (bar x) y This tries to prove Continuous fun x => foo (bar x) y from Continuous fun x => foo (bar x)
                                                      Equations
                                                        Instances For

                                                          Prove function property of fun f => f x₁ ... xₙ.

                                                          Equations
                                                            Instances For
                                                              def Mathlib.Meta.FunProp.getDeclTheorems (funPropDecl : FunPropDecl) (funName : Lean.Name) (mainArgs : Array ) (appliedArgs : ) :

                                                              Get candidate theorems from the environment for function property funPropDecl and function funName.

                                                              Equations
                                                                Instances For
                                                                  def Mathlib.Meta.FunProp.getLocalTheorems (funPropDecl : FunPropDecl) (funOrigin : Origin) (mainArgs : Array ) (appliedArgs : ) :

                                                                  Get candidate theorems from the local context for function property funPropDecl and function funName.

                                                                  Equations
                                                                    Instances For

                                                                      Try to apply function theorems thms to e.

                                                                      Equations
                                                                        Instances For

                                                                          Prove function property of fun x => f x₁ ... xₙ where f is free variable.

                                                                          Equations
                                                                            Instances For

                                                                              Prove function property of fun x => f x₁ ... xₙ where f is declared function.

                                                                              Equations
                                                                                Instances For

                                                                                  Cache result if it does not have any subgoals.

                                                                                  Equations
                                                                                    Instances For

                                                                                      Cache for failed goals such that fun_prop can fail fast next time.

                                                                                      Equations
                                                                                        Instances For

                                                                                          Main funProp function. Returns proof of e.