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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedOrigin : Inhabited Origin

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqOrigin : BEq Origin

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

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

Name of the origin.

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

Get the expression specified by origin.

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

Pretty print FunProp.Origin.

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

Pretty print FunProp.Origin. Returns string unlike ppOrigin.

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

Get origin of the head function.

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

Default names to be considered reducible by fun_prop

structure Mathlib.Meta.FunProp.Config : Type

fun_prop configuration

• maxTransitionDepth : ℕ

  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 : ℕ

  Maximum number of steps fun_prop can take.

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedConfig : Inhabited Config

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqConfig : BEq Config

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

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 : ℕ

  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 : ℕ

  priority

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorem : Inhabited GeneralTheorem

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

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.

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

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorems : Inhabited GeneralTheorems

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 : ℕ

  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

@[reducible, inline]

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

Monad to run fun_prop tactic in.

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

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

Get predicate on names indicating whether they should be unfolded.

def Mathlib.Meta.FunProp.increaseSteps : FunPropM Unit

Increase heartbeat, throws error when maxSteps was reached

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

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

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.