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

def Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs.default : LambdaTheoremArgs

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs : Inhabited LambdaTheoremArgs

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq LambdaTheoremArgs

def Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq : LambdaTheoremArgs → LambdaTheoremArgs → Bool

def Mathlib.Meta.FunProp.instReprLambdaTheoremArgs.repr : LambdaTheoremArgs → ℕ → Std.Format

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr LambdaTheoremArgs

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable LambdaTheoremArgs

def Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash : LambdaTheoremArgs → UInt64

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

def Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType.default : LambdaTheoremType

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType : Inhabited LambdaTheoremType

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq LambdaTheoremType

def Mathlib.Meta.FunProp.instBEqLambdaTheoremType.beq : LambdaTheoremType → LambdaTheoremType → Bool

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr LambdaTheoremType

def Mathlib.Meta.FunProp.instReprLambdaTheoremType.repr : LambdaTheoremType → ℕ → Std.Format

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable LambdaTheoremType

def Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash : LambdaTheoremType → UInt64

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.

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited LambdaTheorem

def Mathlib.Meta.FunProp.instInhabitedLambdaTheorem.default : LambdaTheorem

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq LambdaTheorem

def Mathlib.Meta.FunProp.instBEqLambdaTheorem.beq : LambdaTheorem → LambdaTheorem → Bool

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorems : Inhabited LambdaTheorems

def Mathlib.Meta.FunProp.instInhabitedLambdaTheorems.default : 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

def Mathlib.Meta.FunProp.instInhabitedTheoremForm.default : TheoremForm

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited TheoremForm

def Mathlib.Meta.FunProp.instBEqTheoremForm.beq : TheoremForm → TheoremForm → Bool

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqTheoremForm : BEq TheoremForm

def Mathlib.Meta.FunProp.instReprTheoremForm.repr : TheoremForm → ℕ → Std.Format

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr TheoremForm

@[implicit_reducible]

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

def Mathlib.Meta.FunProp.instInhabitedFunctionTheorem.default : FunctionTheorem

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited FunctionTheorem

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq FunctionTheorem

def Mathlib.Meta.FunProp.instBEqFunctionTheorem.beq : FunctionTheorem → FunctionTheorem → Bool

structure Mathlib.Meta.FunProp.FunctionTheorems : Type

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

  map: function name → function property → function theorem

def Mathlib.Meta.FunProp.instInhabitedFunctionTheorems.default : FunctionTheorems

@[implicit_reducible]

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)

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

Get proof of a theorem.

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.GeneralTheoremsExt : Type

Extensions 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.coe

  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.