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.

instance Mathlib.Meta.FunProp.instInhabitedOrigin : Inhabited Origin

Equations

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

instance Mathlib.Meta.FunProp.instBEqOrigin : BEq Origin

Equations

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

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

• One or more equations did not get rendered due to their size.
• 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 : ℕ

  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 smoothenss.

  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.

instance Mathlib.Meta.FunProp.instInhabitedConfig : Inhabited Config

Equations

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

instance Mathlib.Meta.FunProp.instBEqConfig : BEq Config

Equations

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

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.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.

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 if theys shoulds be unfolded.

Equations

• Mathlib.Meta.FunProp.unfoldNamePred = do let __do_lift ← read let 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.