fun_prop environment extensions storing theorems for fun_prop

inductive Mathlib.Meta.FunProp.LambdaTheoremArgs : Type

Tag for one of the 5 basic lambda theorems, that also hold extra data for composition theorem

• id : LambdaTheoremArgs

  Identity theorem e.g. Continuous fun x => x

• const : LambdaTheoremArgs

  Constant theorem e.g. Continuous fun x => y

• apply : LambdaTheoremArgs

  Apply theorem e.g. Continuous fun (f : (x : X) → Y x => f x)

• comp (fArgId gArgId : ℕ) : LambdaTheoremArgs

  Composition theorem e.g. Continuous f → Continuous g → Continuous fun x => f (g x)

  The numbers fArgId and gArgId store the argument index for f and g in the composition theorem.

• pi : LambdaTheoremArgs

  Pi theorem e.g. ∀ y, Continuous (f · y) → Continuous fun x y => f x y

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs : Inhabited LambdaTheoremArgs

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq LambdaTheoremArgs

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr LambdaTheoremArgs

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable LambdaTheoremArgs

inductive Mathlib.Meta.FunProp.LambdaTheoremType : Type

Tag for one of the 5 basic lambda theorems

• id : LambdaTheoremType

  Identity theorem e.g. Continuous fun x => x

• const : LambdaTheoremType

  Constant theorem e.g. Continuous fun x => y

• apply : LambdaTheoremType

  Apply theorem e.g. Continuous fun (f : (x : X) → Y x => f x)

• comp : LambdaTheoremType

  Composition theorem e.g. Continuous f → Continuous g → Continuous fun x => f (g x)

• pi : LambdaTheoremType

  Pi theorem e.g. ∀ y, Continuous (f · y) → Continuous fun x y => f x y

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType : Inhabited LambdaTheoremType

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq LambdaTheoremType

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr LambdaTheoremType

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable LambdaTheoremType

def Mathlib.Meta.FunProp.LambdaTheoremArgs.type (t : LambdaTheoremArgs) : LambdaTheoremType

Convert LambdaTheoremArgs to LambdaTheoremType.

def Mathlib.Meta.FunProp.detectLambdaTheoremArgs (f : Lean.Expr) (ctxVars : Array Lean.Expr) : Lean.MetaM (Option LambdaTheoremArgs)

Decides whether f is a function corresponding to one of the lambda theorems.

structure Mathlib.Meta.FunProp.LambdaTheorem : Type

Structure holding information about lambda theorem.

• funPropName : Lean.Name

  Name of function property

• thmName : Lean.Name

  Name of lambda theorem

• thmArgs : LambdaTheoremArgs

  Type and important argument of the theorem.

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited LambdaTheorem

instance Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq LambdaTheorem

structure Mathlib.Meta.FunProp.LambdaTheorems : Type

Collection of lambda theorems

• theorems : Std.HashMap (Lean.Name × LambdaTheoremType) (Array LambdaTheorem)

  map: function property name × theorem type → lambda theorem

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorems : Inhabited LambdaTheorems

def Mathlib.Meta.FunProp.LambdaTheorem.getProof (thm : LambdaTheorem) : Lean.MetaM Lean.Expr

Return proof of lambda theorem

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.LambdaTheoremsExt : Type

Environment extension storing lambda theorems.

opaque Mathlib.Meta.FunProp.lambdaTheoremsExt : LambdaTheoremsExt

Environment extension storing all lambda theorems.

def Mathlib.Meta.FunProp.getLambdaTheorems (funPropName : Lean.Name) (type : LambdaTheoremType) : Lean.CoreM (Array LambdaTheorem)

Get lambda theorems for particular function property funPropName.

inductive Mathlib.Meta.FunProp.TheoremForm : Type

Function theorems are stated in uncurried or compositional form.

uncurried

theorem Continuous_add : Continuous (fun x => x.1 + x.2)

compositional

theorem Continuous_add (hf : Continuous f) (hg : Continuous g) : Continuous (fun x => (f x) + (g x))

• uncurried : TheoremForm
• comp : TheoremForm

instance Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited TheoremForm

instance Mathlib.Meta.FunProp.instBEqTheoremForm : BEq TheoremForm

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr TheoremForm

instance Mathlib.Meta.FunProp.instToStringTheoremForm : ToString TheoremForm

TheoremForm to string

structure Mathlib.Meta.FunProp.FunctionTheorem : Type

theorem about specific function (either declared constant or free variable)

• funPropName : Lean.Name

  function property name

• thmOrigin : Origin

  theorem name

• funOrigin : Origin

  function name

• mainArgs : Array ℕ

  array of argument indices about which this theorem is about

• appliedArgs : ℕ

  total number of arguments applied to the function

• priority : ℕ

  priority

• form : TheoremForm

  form of the theorem, see documentation of TheoremForm

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited FunctionTheorem

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq FunctionTheorem

structure Mathlib.Meta.FunProp.FunctionTheorems : Type

• theorems : Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array FunctionTheorem) compare) compare

  map: function name → function property → function theorem

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorems : Inhabited FunctionTheorems

def Mathlib.Meta.FunProp.FunctionTheorem.getProof (thm : FunctionTheorem) : Lean.MetaM Lean.Expr

return proof of function theorem

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.FunctionTheoremsExt : Type

opaque Mathlib.Meta.FunProp.functionTheoremsExt : FunctionTheoremsExt

Extension storing all function theorems.

def Mathlib.Meta.FunProp.getTheoremsForFunction (funName funPropName : Lean.Name) : Lean.CoreM (Array FunctionTheorem)

structure Mathlib.Meta.FunProp.GeneralTheorem : Type

General theorem about a function property used for transition and morphism theorems

• funPropName : Lean.Name

  function property name

• thmName : Lean.Name

  theorem name

• keys : List Lean.Meta.RefinedDiscrTree.DTExpr

  discrimination tree keys used to index this theorem

• priority : ℕ

  priority

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorem : Inhabited GeneralTheorem

instance Mathlib.Meta.FunProp.instBEqGeneralTheorem : BEq GeneralTheorem

def Mathlib.Meta.FunProp.GeneralTheorem.getProof (thm : GeneralTheorem) : Lean.MetaM Lean.Expr

Get proof of a theorem.

structure Mathlib.Meta.FunProp.GeneralTheorems : Type

Structure holding transition or morphism theorems for fun_prop tactic.

• theorems : Lean.Meta.RefinedDiscrTree GeneralTheorem

  Discrimination tree indexing theorems.

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorems : Inhabited GeneralTheorems

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.GeneralTheoremsExt : Type

Extendions for transition or morphism theorems

opaque Mathlib.Meta.FunProp.transitionTheoremsExt : GeneralTheoremsExt

Environment extension for transition theorems.

def Mathlib.Meta.FunProp.getTransitionTheorems (e : Lean.Expr) : FunPropM (Array GeneralTheorem)

Get transition theorems applicable to e.

For example calling on e equal to Continuous f might return theorems implying continuity from linearity over finite dimensional spaces or differentiability.

opaque Mathlib.Meta.FunProp.morTheoremsExt : GeneralTheoremsExt

Environment extension for morphism theorems.

def Mathlib.Meta.FunProp.getMorphismTheorems (e : Lean.Expr) : FunPropM (Array GeneralTheorem)

Get morphism theorems applicable to e.

For example calling on e equal to Continuous f for f : X→L[ℝ] Y would return theorem inferring continuity from the bundled morphism.

inductive Mathlib.Meta.FunProp.Theorem : Type

There are four types of theorems:

• lam - theorem about basic lambda calculus terms
• function - theorem about a specific function(declared or free variable) in specific arguments
• mor - special theorems talking about bundled morphisms/DFunLike.coe
• transition - theorems inferring one function property from another

Examples:

• lam

  theorem Continuous_id : Continuous fun x => x
  theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f (g x)

• function

  theorem Continuous_add : Continuous (fun x => x.1 + x.2)
  theorem Continuous_add (hf : Continuous f) (hg : Continuous g) :
      Continuous (fun x => (f x) + (g x))

• mor - the head of function body has to be ``DFunLike.code

  theorem ContDiff.clm_apply {f : E → F →L[𝕜] G} {g : E → F}
      (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
      ContDiff 𝕜 n fun x => (f x) (g x)
  theorem clm_linear {f : E →L[𝕜] F} : IsLinearMap 𝕜 f

• transition - the conclusion has to be in the form P f where f is a free variable

  theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
      Continuous f

• lam (thm : LambdaTheorem) : Theorem
• function (thm : FunctionTheorem) : Theorem
• mor (thm : GeneralTheorem) : Theorem
• transition (thm : GeneralTheorem) : Theorem

def Mathlib.Meta.FunProp.getTheoremFromConst (declName : Lean.Name) (prio : ℕ := 1000) : Lean.MetaM Theorem

For a theorem declaration declName return fun_prop theorem. It correctly detects which type of theorem it is.

def Mathlib.Meta.FunProp.addTheorem (declName : Lean.Name) (attrKind : Lean.AttributeKind := Lean.AttributeKind.global) (prio : ℕ := 1000) : Lean.MetaM Unit

Register theorem declName with fun_prop.