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

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs : Inhabited LambdaTheoremArgs

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs = { default := Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs.default }

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

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs.default = Mathlib.Meta.FunProp.LambdaTheoremArgs.id

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

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq Mathlib.Meta.FunProp.LambdaTheoremArgs.id Mathlib.Meta.FunProp.LambdaTheoremArgs.id = true
• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq Mathlib.Meta.FunProp.LambdaTheoremArgs.const Mathlib.Meta.FunProp.LambdaTheoremArgs.const = true
• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq Mathlib.Meta.FunProp.LambdaTheoremArgs.apply Mathlib.Meta.FunProp.LambdaTheoremArgs.apply = true
• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp a a_1) (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp b b_1) = (a == b && a_1 == b_1)
• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq Mathlib.Meta.FunProp.LambdaTheoremArgs.pi Mathlib.Meta.FunProp.LambdaTheoremArgs.pi = true
• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq x✝¹ x✝ = false

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq LambdaTheoremArgs

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs = { beq := Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq }

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr LambdaTheoremArgs

Equations

• Mathlib.Meta.FunProp.instReprLambdaTheoremArgs = { reprPrec := Mathlib.Meta.FunProp.instReprLambdaTheoremArgs.repr }

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

Equations

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

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

Equations

• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash Mathlib.Meta.FunProp.LambdaTheoremArgs.id = 0
• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash Mathlib.Meta.FunProp.LambdaTheoremArgs.const = 1
• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash Mathlib.Meta.FunProp.LambdaTheoremArgs.apply = 2
• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp a a_1) = mixHash (mixHash 3 (hash a)) (hash a_1)
• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash Mathlib.Meta.FunProp.LambdaTheoremArgs.pi = 4

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable LambdaTheoremArgs

Equations

• Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs = { hash := Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash }

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

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType.default = Mathlib.Meta.FunProp.LambdaTheoremType.id

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType : Inhabited LambdaTheoremType

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType = { default := Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType.default }

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

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheoremType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq LambdaTheoremType

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheoremType = { beq := Mathlib.Meta.FunProp.instBEqLambdaTheoremType.beq }

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

Equations

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

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr LambdaTheoremType

Equations

• Mathlib.Meta.FunProp.instReprLambdaTheoremType = { reprPrec := Mathlib.Meta.FunProp.instReprLambdaTheoremType.repr }

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable LambdaTheoremType

Equations

• Mathlib.Meta.FunProp.instHashableLambdaTheoremType = { hash := Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash }

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

Equations

• Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash Mathlib.Meta.FunProp.LambdaTheoremType.id = 0
• Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash Mathlib.Meta.FunProp.LambdaTheoremType.const = 1
• Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash Mathlib.Meta.FunProp.LambdaTheoremType.apply = 2
• Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash Mathlib.Meta.FunProp.LambdaTheoremType.comp = 3
• Mathlib.Meta.FunProp.instHashableLambdaTheoremType.hash Mathlib.Meta.FunProp.LambdaTheoremType.pi = 4

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

Convert LambdaTheoremArgs to LambdaTheoremType.

Equations

• Mathlib.Meta.FunProp.LambdaTheoremArgs.id.type = Mathlib.Meta.FunProp.LambdaTheoremType.id
• Mathlib.Meta.FunProp.LambdaTheoremArgs.const.type = Mathlib.Meta.FunProp.LambdaTheoremType.const
• (Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId).type = Mathlib.Meta.FunProp.LambdaTheoremType.comp
• Mathlib.Meta.FunProp.LambdaTheoremArgs.apply.type = Mathlib.Meta.FunProp.LambdaTheoremType.apply
• Mathlib.Meta.FunProp.LambdaTheoremArgs.pi.type = Mathlib.Meta.FunProp.LambdaTheoremType.pi

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.

Equations

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

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.

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

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheorem.default = { funPropName := default, thmName := default, thmArgs := default }

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited LambdaTheorem

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheorem = { default := Mathlib.Meta.FunProp.instInhabitedLambdaTheorem.default }

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

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheorem.beq { funPropName := a, thmName := a_1, thmArgs := a_2 } { funPropName := b, thmName := b_1, thmArgs := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.Meta.FunProp.instBEqLambdaTheorem.beq x✝¹ x✝ = false

instance Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq LambdaTheorem

Equations

• Mathlib.Meta.FunProp.instBEqLambdaTheorem = { beq := Mathlib.Meta.FunProp.instBEqLambdaTheorem.beq }

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

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheorems = { default := Mathlib.Meta.FunProp.instInhabitedLambdaTheorems.default }

def Mathlib.Meta.FunProp.instInhabitedLambdaTheorems.default : LambdaTheorems

Equations

• Mathlib.Meta.FunProp.instInhabitedLambdaTheorems.default = { theorems := default }

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

Return proof of lambda theorem

Equations

• thm.getProof = Lean.Meta.mkConstWithFreshMVarLevels thm.thmName

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.LambdaTheoremsExt : Type

Environment extension storing lambda theorems.

Equations

• Mathlib.Meta.FunProp.LambdaTheoremsExt = Lean.SimpleScopedEnvExtension Mathlib.Meta.FunProp.LambdaTheorem Mathlib.Meta.FunProp.LambdaTheorems

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.

Equations

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

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

Equations

• Mathlib.Meta.FunProp.instInhabitedTheoremForm.default = Mathlib.Meta.FunProp.TheoremForm.uncurried

instance Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited TheoremForm

Equations

• Mathlib.Meta.FunProp.instInhabitedTheoremForm = { default := Mathlib.Meta.FunProp.instInhabitedTheoremForm.default }

instance Mathlib.Meta.FunProp.instBEqTheoremForm : BEq TheoremForm

Equations

• Mathlib.Meta.FunProp.instBEqTheoremForm = { beq := Mathlib.Meta.FunProp.instBEqTheoremForm.beq }

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

Equations

• Mathlib.Meta.FunProp.instBEqTheoremForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr TheoremForm

Equations

• Mathlib.Meta.FunProp.instReprTheoremForm = { reprPrec := Mathlib.Meta.FunProp.instReprTheoremForm.repr }

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

Equations

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

instance Mathlib.Meta.FunProp.instToStringTheoremForm : ToString TheoremForm

TheoremForm to string

Equations

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

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

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited FunctionTheorem

Equations

• Mathlib.Meta.FunProp.instInhabitedFunctionTheorem = { default := Mathlib.Meta.FunProp.instInhabitedFunctionTheorem.default }

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.instBEqFunctionTheorem.beq x✝¹ x✝ = false

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq FunctionTheorem

Equations

• Mathlib.Meta.FunProp.instBEqFunctionTheorem = { beq := Mathlib.Meta.FunProp.instBEqFunctionTheorem.beq }

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

Equations

• Mathlib.Meta.FunProp.instInhabitedFunctionTheorems = { default := Mathlib.Meta.FunProp.instInhabitedFunctionTheorems.default }

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

Equations

• Mathlib.Meta.FunProp.instInhabitedFunctionTheorems.default = { theorems := default }

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

return proof of function theorem

Equations

• thm.getProof = match thm.thmOrigin with | Mathlib.Meta.FunProp.Origin.decl name => Lean.Meta.mkConstWithFreshMVarLevels name | Mathlib.Meta.FunProp.Origin.fvar id => pure (Lean.Expr.fvar id)

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.FunctionTheoremsExt : Type

Equations

• Mathlib.Meta.FunProp.FunctionTheoremsExt = Lean.SimpleScopedEnvExtension Mathlib.Meta.FunProp.FunctionTheorem Mathlib.Meta.FunProp.FunctionTheorems

opaque Mathlib.Meta.FunProp.functionTheoremsExt : FunctionTheoremsExt

Extension storing all function theorems.

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

Equations

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

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

Get proof of a theorem.

Equations

• thm.getProof = Lean.Meta.mkConstWithFreshMVarLevels thm.thmName

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.GeneralTheoremsExt : Type

Extensions for transition or morphism theorems

Equations

• Mathlib.Meta.FunProp.GeneralTheoremsExt = Lean.SimpleScopedEnvExtension Mathlib.Meta.FunProp.GeneralTheorem Mathlib.Meta.FunProp.GeneralTheorems

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.

Equations

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

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.

Equations

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

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

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

Equations

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

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.

Equations

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