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

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq LambdaTheoremArgs

Equations

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

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr LambdaTheoremArgs

Equations

• Mathlib.Meta.FunProp.instReprLambdaTheoremArgs = { reprPrec := Mathlib.Meta.FunProp.reprLambdaTheoremArgs✝ }

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable LambdaTheoremArgs

Equations

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

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

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq LambdaTheoremType

Equations

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

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr LambdaTheoremType

Equations

• Mathlib.Meta.FunProp.instReprLambdaTheoremType = { reprPrec := Mathlib.Meta.FunProp.reprLambdaTheoremType✝ }

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable LambdaTheoremType

Equations

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

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.

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited LambdaTheorem

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq LambdaTheorem

Equations

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

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 := { 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

instance Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited TheoremForm

Equations

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

instance Mathlib.Meta.FunProp.instBEqTheoremForm : BEq TheoremForm

Equations

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

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr TheoremForm

Equations

• Mathlib.Meta.FunProp.instReprTheoremForm = { reprPrec := Mathlib.Meta.FunProp.reprTheoremForm✝ }

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 ℕ

  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

Equations

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

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq FunctionTheorem

Equations

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

structure Mathlib.Meta.FunProp.FunctionTheorems : Type

• theorems : Batteries.RBMap Lean.Name (Batteries.RBMap 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 := { 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.

structure Mathlib.Meta.FunProp.GeneralTheorem : Type

General theorem about 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

Equations

• Mathlib.Meta.FunProp.instInhabitedGeneralTheorem = { default := { funPropName := default, thmName := default, keys := default, priority := default } }

instance Mathlib.Meta.FunProp.instBEqGeneralTheorem : BEq GeneralTheorem

Equations

• Mathlib.Meta.FunProp.instBEqGeneralTheorem = { beq := Mathlib.Meta.FunProp.beqGeneralTheorem✝ }

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

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

Equations

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

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.GeneralTheoremsExt : Type

Extendions 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 : ℕ := 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 : ℕ := 1000) : Lean.MetaM Unit

Register theorem declName with fun_prop.

Equations

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