## `funProp` #

this file defines environment extension for `funProp`

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

Instances For

source
instance Mathlib.Meta.FunProp.instInhabitedOrigin :
Inhabited Origin
Equations

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

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

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

Instances For

source
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

Instances For

source
instance Mathlib.Meta.FunProp.instBEqOrigin :
BEq Origin
Equations

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

source
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

Instances For

source
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)

Instances For

source
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))

Instances For

source
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)

Instances For

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

Instances For

source
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]

Instances For

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

Instances For

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

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

Instances For

source
instance Mathlib.Meta.FunProp.instInhabitedConfig :
Inhabited Config
Equations

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

source
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

Instances For

source
instance Mathlib.Meta.FunProp.instBEqConfig :
BEq Config
Equations

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

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

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

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

Instances For

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

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

Instances For

source
instance Mathlib.Meta.FunProp.instInhabitedGeneralTheorems :
Inhabited GeneralTheorems
Equations

- Mathlib.Meta.FunProp.instInhabitedGeneralTheorems = { default := Mathlib.Meta.FunProp.instInhabitedGeneralTheorems.default }

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

Instances For

source
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 }

Instances For

source
@[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)

Instances For

source
structure Mathlib.Meta.FunProp.Result :
Type

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

- proof : Lean.Expr

Instances For

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

Default names to unfold

Equations

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For