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

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

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.

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

def Mathlib.Meta.FunProp.tryTheoremWithHint? (e : Lean.Expr) (thmOrigin : Origin) (hint : Array (ℕ × 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.

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.

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.

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.

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.

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.

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

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)

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.

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

Prove function property of using transition theorems.

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)

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ₙ.

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

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

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

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

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.

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.

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.

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

Cache result if it does not have any subgoals.

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

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

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

Main funProp function. Returns proof of e.