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

source
def Mathlib.Meta.FunProp.synthesizeInstance (thmId : Origin) (x type : Lean.Expr) :
Lean.MetaM Bool

Synthesize instance of type `type` and

1. assign it to `x` if `x` is meta variable
2. check it is equal to `x`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.synthesizeArgs (thmId : Origin) (xs : Array Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM Bool

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.tryTheoremCore (xs : Array Lean.Expr) (val type e : Lean.Expr) (thmId : Origin) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Try to apply theorem - core function

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.tryTheoremWithHint? (e : Lean.Expr) (thmOrigin : Origin) (hint : Array (Nat × Lean.Expr)) (funProp : Lean.Expr → FunPropM (Option Result)) (newMCtxDepth : Bool := false) :
FunPropM (Option Result)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.tryTheorem? (e : Lean.Expr) (thmOrigin : Origin) (funProp : Lean.Expr → FunPropM (Option Result)) (newMCtxDepth : Bool := false) :
FunPropM (Option Result)

Try to apply a theorem `thmOrigin` to the goal `e`.

Equations

- Mathlib.Meta.FunProp.tryTheorem? e thmOrigin funProp newMCtxDepth = Mathlib.Meta.FunProp.tryTheoremWithHint? e thmOrigin #[] funProp newMCtxDepth

Instances For

source
def Mathlib.Meta.FunProp.applyIdRule (funPropDecl : FunPropDecl) (e : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Try to prove `e` using the identity lambda theorem.

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.applyConstRule (funPropDecl : FunPropDecl) (e : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Try to prove `e` using the constant lambda theorem.

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.applyApplyRule (funPropDecl : FunPropDecl) (e : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Try to prove `e` using the apply lambda theorem.

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.applyCompRule (funPropDecl : FunPropDecl) (e f g : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.applyPiRule (funPropDecl : FunPropDecl) (e : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.letCase (funPropDecl : FunPropDecl) (e f : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

- One or more equations did not get rendered due to their size.
- Mathlib.Meta.FunProp.letCase funPropDecl e f funProp = Lean.throwError (Lean.toMessageData "expected expression of the form `fun x => lam y := ..; ..`")

Instances For

source
def Mathlib.Meta.FunProp.applyMorRules (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Prove function property of using morphism theorems.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.applyTransitionRules (e : Lean.Expr) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Prove function property of using transition theorems.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.removeArgRule (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.bvarAppCase (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.getDeclTheorems (funPropDecl : FunPropDecl) (funName : Lean.Name) (mainArgs : Array Nat) (appliedArgs : Nat) :
Lean.MetaM (Array FunctionTheorem)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.getLocalTheorems (funPropDecl : FunPropDecl) (funOrigin : Origin) (mainArgs : Array Nat) (appliedArgs : Nat) :
FunPropM (Array FunctionTheorem)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.tryTheorems (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (thms : Array FunctionTheorem) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

Try to apply function theorems `thms` to `e`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.fvarAppCase (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.constAppCase (funPropDecl : FunPropDecl) (e : Lean.Expr) (fData : FunctionData) (funProp : Lean.Expr → FunPropM (Option Result)) :
FunPropM (Option Result)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.cacheResult (e : Lean.Expr) (r : Result) :
FunPropM Result

Cache result if it does not have any subgoals.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.FunProp.cacheFailure (e : Lean.Expr) :
FunPropM Unit

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Mathlib.Meta.FunProp.funProp (e : Lean.Expr) :
FunPropM (Option Result)

Main `funProp` function. Returns proof of `e`.