funProp

this file defines environment extension for funProp

inductive Mathlib.Meta.FunProp.Origin : Type

Indicated origin of a function or a statement.

• decl (name : Lean.Name) : Origin

  It is a constant defined in the environment.

• fvar (fvarId : Lean.FVarId) : Origin

  It is a free variable in the local context.

def Mathlib.Meta.FunProp.instInhabitedOrigin.default : Origin

Equations

• Mathlib.Meta.FunProp.instInhabitedOrigin.default = Mathlib.Meta.FunProp.Origin.decl default

instance Mathlib.Meta.FunProp.instInhabitedOrigin : Inhabited Origin

Equations

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

def Mathlib.Meta.FunProp.instBEqOrigin.beq : Origin → Origin → Bool

Equations

• Mathlib.Meta.FunProp.instBEqOrigin.beq (Mathlib.Meta.FunProp.Origin.decl a) (Mathlib.Meta.FunProp.Origin.decl b) = (a == b)
• Mathlib.Meta.FunProp.instBEqOrigin.beq (Mathlib.Meta.FunProp.Origin.fvar a) (Mathlib.Meta.FunProp.Origin.fvar b) = (a == b)
• Mathlib.Meta.FunProp.instBEqOrigin.beq x✝¹ x✝ = false

instance Mathlib.Meta.FunProp.instBEqOrigin : BEq Origin

Equations

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

def Mathlib.Meta.FunProp.Origin.name (origin : Origin) : Lean.Name

Name of the origin.

Equations

• (Mathlib.Meta.FunProp.Origin.decl name).name = name
• (Mathlib.Meta.FunProp.Origin.fvar id).name = id.name

def Mathlib.Meta.FunProp.Origin.getValue (origin : Origin) : Lean.MetaM Lean.Expr

Get the expression specified by origin.

Equations

• (Mathlib.Meta.FunProp.Origin.decl name).getValue = Lean.Meta.mkConstWithFreshMVarLevels name
• (Mathlib.Meta.FunProp.Origin.fvar id).getValue = pure (Lean.Expr.fvar id)

def Mathlib.Meta.FunProp.ppOrigin {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] : Origin → m Lean.MessageData

Pretty print FunProp.Origin.

Equations

• Mathlib.Meta.FunProp.ppOrigin (Mathlib.Meta.FunProp.Origin.decl name) = do let __do_lift ← Lean.mkConstWithLevelParams name pure (Lean.toMessageData __do_lift)
• Mathlib.Meta.FunProp.ppOrigin (Mathlib.Meta.FunProp.Origin.fvar id) = pure (Lean.MessageData.ofExpr (Lean.mkFVar id))

def Mathlib.Meta.FunProp.ppOrigin' (origin : Origin) : Lean.MetaM String

Pretty print FunProp.Origin. Returns string unlike ppOrigin.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.ppOrigin' origin = pure (toString origin.name)

def Mathlib.Meta.FunProp.FunctionData.getFnOrigin (fData : FunctionData) : Origin

Get origin of the head function.

Equations

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

def Mathlib.Meta.FunProp.defaultNamesToUnfold : Array Lean.Name

Default names to be considered reducible by fun_prop

Equations

• Mathlib.Meta.FunProp.defaultNamesToUnfold = #[`id, `Function.comp, `Function.HasUncurry.uncurry, `Function.uncurry]

structure Mathlib.Meta.FunProp.Config : Type

fun_prop configuration

• maxTransitionDepth : Nat

  Maximum number of transitions between function properties. For example inferring continuity from differentiability and then differentiability from smoothness (ContDiff ℝ ∞) requires maxTransitionDepth = 2. The default value of one expects that transition theorems are transitively closed e.g. there is a transition theorem that infers continuity directly from smoothness.

  Setting maxTransitionDepth to zero will disable all transition theorems. This can be very useful when fun_prop should fail quickly. For example when using fun_prop as discharger in simp.

• maxSteps : Nat

  Maximum number of steps fun_prop can take.

instance Mathlib.Meta.FunProp.instInhabitedConfig : Inhabited Config

Equations

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

def Mathlib.Meta.FunProp.instInhabitedConfig.default : Config

Equations

• Mathlib.Meta.FunProp.instInhabitedConfig.default = { maxTransitionDepth := default, maxSteps := default }

def Mathlib.Meta.FunProp.instBEqConfig.beq : Config → Config → Bool

Equations

• Mathlib.Meta.FunProp.instBEqConfig.beq { maxTransitionDepth := a, maxSteps := a_1 } { maxTransitionDepth := b, maxSteps := b_1 } = (a == b && a_1 == b_1)
• Mathlib.Meta.FunProp.instBEqConfig.beq x✝¹ x✝ = false

instance Mathlib.Meta.FunProp.instBEqConfig : BEq Config

Equations

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

structure Mathlib.Meta.FunProp.Context : Type

fun_prop context

• config : Config

  fun_prop config

• constToUnfold : Std.TreeSet Lean.Name Lean.Name.quickCmp

  Name to unfold

• disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)

  Custom discharger to satisfy theorem hypotheses.

• transitionDepth : Nat

  current transition depth

structure Mathlib.Meta.FunProp.GeneralTheorem : Type

General theorem about a function property used for transition and morphism theorems

• funPropName : Lean.Name

  function property name

• thmName : Lean.Name

  theorem name

• keys : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)

  discrimination tree keys used to index this theorem

• priority : Nat

  priority

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorem : Inhabited GeneralTheorem

Equations

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

def Mathlib.Meta.FunProp.instInhabitedGeneralTheorem.default : GeneralTheorem

Equations

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

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 := Mathlib.Meta.FunProp.instInhabitedGeneralTheorems.default }

def Mathlib.Meta.FunProp.instInhabitedGeneralTheorems.default : GeneralTheorems

Equations

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

structure Mathlib.Meta.FunProp.State : Type

fun_prop state

• cache : Lean.Meta.Simp.Cache

  Simp's cache is used as the fun_prop tactic is designed to be used inside of simp and utilize its cache. It holds successful goals.

• failureCache : Lean.ExprSet

  Cache storing failed goals such that they are not tried again.

• numSteps : Nat

  Count the number of steps and stop when maxSteps is reached.

• msgLog : List String

  Log progress and failures messages that should be displayed to the user at the end.

• morTheorems : GeneralTheorems

  RefinedDiscrTree is lazy, so we store the partially evaluated tree.

• transitionTheorems : GeneralTheorems

  RefinedDiscrTree is lazy, so we store the partially evaluated tree.

def Mathlib.Meta.FunProp.Context.increaseTransitionDepth (ctx : Context) : Context

Increase depth

Equations

• ctx.increaseTransitionDepth = { config := ctx.config, constToUnfold := ctx.constToUnfold, disch := ctx.disch, transitionDepth := ctx.transitionDepth + 1 }

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.FunPropM (α : Type) : Type

Monad to run fun_prop tactic in.

Equations

• Mathlib.Meta.FunProp.FunPropM = ReaderT Mathlib.Meta.FunProp.Context (StateT Mathlib.Meta.FunProp.State Lean.MetaM)

structure Mathlib.Meta.FunProp.Result : Type

Result of funProp, it is a proof of function property P f

• proof : Lean.Expr

def Mathlib.Meta.FunProp.defaultUnfoldPred : Lean.Name → Bool

Default names to unfold

Equations

• Mathlib.Meta.FunProp.defaultUnfoldPred = Mathlib.Meta.FunProp.defaultNamesToUnfold.contains

def Mathlib.Meta.FunProp.unfoldNamePred : FunPropM (Lean.Name → Bool)

Get predicate on names indicating whether they should be unfolded.

Equations

• Mathlib.Meta.FunProp.unfoldNamePred = do let __do_lift ← read have toUnfold : Std.TreeSet Lean.Name Lean.Name.quickCmp := __do_lift.constToUnfold pure fun (n : Lean.Name) => toUnfold.contains n

def Mathlib.Meta.FunProp.increaseSteps : FunPropM Unit

Increase heartbeat, throws error when maxSteps was reached

Equations

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

def Mathlib.Meta.FunProp.withIncreasedTransitionDepth {α : Type} (go : FunPropM (Option α)) : FunPropM (Option α)

Increase transition depth. Return none if maximum transition depth has been reached.

Equations

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

def Mathlib.Meta.FunProp.logError (msg : String) : FunPropM Unit

Log error message that will displayed to the user at the end.

Messages are logged only when transitionDepth = 0 i.e. when fun_prop is not trying to infer function property like continuity from another property like differentiability. The main reason is that if the user forgets to add a continuity theorem for function foo then fun_prop should report that there is a continuity theorem for foo missing. If we would log messages transitionDepth > 0 then user will see messages saying that there is a missing theorem for differentiability, smoothness, ... for foo.

Equations

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