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 : Mathlib.Meta.FunProp.LambdaTheoremArgs

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

• const : Mathlib.Meta.FunProp.LambdaTheoremArgs

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

• apply : Mathlib.Meta.FunProp.LambdaTheoremArgs

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

• comp (fArgId gArgId : ℕ) : Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.LambdaTheoremArgs

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

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremArgs : Inhabited Mathlib.Meta.FunProp.LambdaTheoremArgs

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq Mathlib.Meta.FunProp.LambdaTheoremArgs

Equations

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

instance Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr Mathlib.Meta.FunProp.LambdaTheoremArgs

Equations

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

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs : Hashable Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.LambdaTheoremType

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

• const : Mathlib.Meta.FunProp.LambdaTheoremType

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

• apply : Mathlib.Meta.FunProp.LambdaTheoremType

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

• comp : Mathlib.Meta.FunProp.LambdaTheoremType

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

• pi : Mathlib.Meta.FunProp.LambdaTheoremType

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

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType : Inhabited Mathlib.Meta.FunProp.LambdaTheoremType

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheoremType : BEq Mathlib.Meta.FunProp.LambdaTheoremType

Equations

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

instance Mathlib.Meta.FunProp.instReprLambdaTheoremType : Repr Mathlib.Meta.FunProp.LambdaTheoremType

Equations

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

instance Mathlib.Meta.FunProp.instHashableLambdaTheoremType : Hashable Mathlib.Meta.FunProp.LambdaTheoremType

Equations

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

def Mathlib.Meta.FunProp.LambdaTheoremArgs.type (t : Mathlib.Meta.FunProp.LambdaTheoremArgs) : Mathlib.Meta.FunProp.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 Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.LambdaTheoremArgs

  Type and important argument of the theorem.

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorem : Inhabited Mathlib.Meta.FunProp.LambdaTheorem

Equations

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

instance Mathlib.Meta.FunProp.instBEqLambdaTheorem : BEq Mathlib.Meta.FunProp.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 × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem)

  map: function property name × theorem type → lambda theorem

instance Mathlib.Meta.FunProp.instInhabitedLambdaTheorems : Inhabited Mathlib.Meta.FunProp.LambdaTheorems

Equations

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

def Mathlib.Meta.FunProp.LambdaTheorem.getProof (thm : Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.LambdaTheoremsExt

Environment extension storing all lambda theorems.

def Mathlib.Meta.FunProp.getLambdaTheorems (funPropName : Lean.Name) (type : Mathlib.Meta.FunProp.LambdaTheoremType) : Lean.CoreM (Array Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.TheoremForm
• comp : Mathlib.Meta.FunProp.TheoremForm

instance Mathlib.Meta.FunProp.instInhabitedTheoremForm : Inhabited Mathlib.Meta.FunProp.TheoremForm

Equations

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

instance Mathlib.Meta.FunProp.instBEqTheoremForm : BEq Mathlib.Meta.FunProp.TheoremForm

Equations

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

instance Mathlib.Meta.FunProp.instReprTheoremForm : Repr Mathlib.Meta.FunProp.TheoremForm

Equations

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

instance Mathlib.Meta.FunProp.instToStringTheoremForm : ToString Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.Origin

  theorem name

• funOrigin : Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.TheoremForm

  form of the theorem, see documentation of TheoremForm

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorem : Inhabited Mathlib.Meta.FunProp.FunctionTheorem

Equations

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

instance Mathlib.Meta.FunProp.instBEqFunctionTheorem : BEq Mathlib.Meta.FunProp.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 Mathlib.Meta.FunProp.FunctionTheorem) compare) compare

  map: function name → function property → function theorem

instance Mathlib.Meta.FunProp.instInhabitedFunctionTheorems : Inhabited Mathlib.Meta.FunProp.FunctionTheorems

Equations

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

def Mathlib.Meta.FunProp.FunctionTheorem.getProof (thm : Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.FunctionTheoremsExt

Extension storing all function theorems.

def Mathlib.Meta.FunProp.getTheoremsForFunction (funName funPropName : Lean.Name) : Lean.CoreM (Array Mathlib.Meta.FunProp.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 Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  discrimination tree keys used to index this theorem

• priority : ℕ

  priority

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorem : Inhabited Mathlib.Meta.FunProp.GeneralTheorem

Equations

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

instance Mathlib.Meta.FunProp.instBEqGeneralTheorem : BEq Mathlib.Meta.FunProp.GeneralTheorem

Equations

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

def Mathlib.Meta.FunProp.GeneralTheorem.getProof (thm : Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem

  Discrimination tree indexing theorems.

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorems : Inhabited Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.GeneralTheoremsExt

Environment extension for transition theorems.

def Mathlib.Meta.FunProp.getTransitionTheorems (e : Lean.Expr) : Mathlib.Meta.FunProp.FunPropM (Array Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.GeneralTheoremsExt

Environment extension for morphism theorems.

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

Get morphism theorems applicable to e.

For example calling on e equal to Continuous f for f : X→L[ℝ] Y would return theorem infering 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 : Mathlib.Meta.FunProp.LambdaTheorem) : Mathlib.Meta.FunProp.Theorem
• function (thm : Mathlib.Meta.FunProp.FunctionTheorem) : Mathlib.Meta.FunProp.Theorem
• mor (thm : Mathlib.Meta.FunProp.GeneralTheorem) : Mathlib.Meta.FunProp.Theorem
• transition (thm : Mathlib.Meta.FunProp.GeneralTheorem) : Mathlib.Meta.FunProp.Theorem

def Mathlib.Meta.FunProp.getTheoremFromConst (declName : Lean.Name) (prio : ℕ := 1000) : Lean.MetaM Mathlib.Meta.FunProp.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.