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 : Nat) : 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

@[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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr LambdaTheoremArgs

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

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

@[implicit_reducible]

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

@[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

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr LambdaTheoremType

@[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.instBEqLambdaTheorem.beq : LambdaTheorem → LambdaTheorem → Bool

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr TheoremForm

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instToStringTheoremForm : ToString TheoremForm

TheoremForm to string

def Mathlib.Meta.FunProp.DecompositionResult.toTheoremForm : DecompositionResult → TheoremForm

Gives the theorem form using the result of FunctionData.decomposition.

Note that this returns TheoremForm.comp even when the decomposition failed (usually due to dependent types). This means that the theorem will be applied directly without trying to write the goal as a composition.

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 Nat

  array of argument indices about which this theorem is about

• appliedArgs : Nat

  total number of arguments applied to the function

• priority : Nat

  priority

• form : TheoremForm

  form of the theorem, see documentation of TheoremForm

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited FunctionTheorem

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq FunctionTheorem

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

@[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 : Nat := 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 : Nat := 1000) : Lean.MetaM Unit

Register theorem declName with fun_prop.