funProp core tactic algorithm

def Mathlib.Meta.FunProp.synthesizeInstance (thmId : Mathlib.Meta.FunProp.Origin) (x : Lean.Expr) (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.

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

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

Equations

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

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

Try to apply theorem - core function

Equations

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

def Mathlib.Meta.FunProp.tryTheoremWithHint? (e : Lean.Expr) (thmOrigin : Mathlib.Meta.FunProp.Origin) (hint : Array (ℕ × Lean.Expr)) (funProp : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) (newMCtxDepth : optParam Bool false) : Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.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.

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

Try to apply a theorem

Equations

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

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

Apply lambda calculus rule P fun x => x`

Equations

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

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

Apply lambda calculus rule P fun x => y`

Equations

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

def Mathlib.Meta.FunProp.applyProjRule (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (e : Lean.Expr) (x : Lean.Expr) (XY : Lean.Expr) (funProp : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) : Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)

Apply lambda calculus rule P fun f => f i`

Equations

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

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

Apply lambda calculus rule P f → P g → P fun x => f (g x)

Equations

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

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

Apply lambda calculus rule ∀ y, P (f · y) → P fun x y => f x y

Equations

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

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

Prove function property of fun x => let y := g x; f x y.

Equations

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

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

Prove function property of using "morphism theorems" e.g. bundled linear map is linear map.

Equations

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

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

Prove function property of using "transition theorems" e.g. continuity from linearity.

Equations

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

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

Try to remove applied argument.

Equations

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

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

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

Equations

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

def Mathlib.Meta.FunProp.getDeclTheorems (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (funName : Lean.Name) (mainArgs : Array ℕ) (appliedArgs : ℕ) : Lean.MetaM (Array Mathlib.Meta.FunProp.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.

def Mathlib.Meta.FunProp.getLocalTheorems (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (funOrigin : Mathlib.Meta.FunProp.Origin) (mainArgs : Array ℕ) (appliedArgs : ℕ) : Mathlib.Meta.FunProp.FunPropM (Array Mathlib.Meta.FunProp.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.

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

Try to apply theorems thms to e

Equations

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

def Mathlib.Meta.FunProp.fvarAppCase (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (e : Lean.Expr) (fData : Mathlib.Meta.FunProp.FunctionData) (funProp : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) : Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.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.

def Mathlib.Meta.FunProp.constAppCase (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (e : Lean.Expr) (fData : Mathlib.Meta.FunProp.FunctionData) (funProp : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) : Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.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.

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

Cache result if it does not have any subgoals.

Equations

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

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

Main funProp function. Returns proof of e.