funProp

this file defines environment extension for funProp

inductive Mathlib.Meta.FunProp.Origin : Type

Indicated origin of a function or a statement.

• decl: Lean.Name → Mathlib.Meta.FunProp.Origin

  It is a constant defined in the environment.

• fvar: Lean.FVarId → Mathlib.Meta.FunProp.Origin

  It is a free variable in the local context.

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

Equations

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

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

Equations

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

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

Name of the origin.

Equations

• origin.name = match origin with | Mathlib.Meta.FunProp.Origin.decl name => name | Mathlib.Meta.FunProp.Origin.fvar id => id.name

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

Get the expression specified by origin.

Equations

• origin.getValue = match origin with | Mathlib.Meta.FunProp.Origin.decl name => Lean.Meta.mkConstWithFreshMVarLevels name | Mathlib.Meta.FunProp.Origin.fvar id => pure (Lean.Expr.fvar id)

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

Pretty print FunProp.Origin.

Equations

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

def Mathlib.Meta.FunProp.ppOrigin' (origin : Mathlib.Meta.FunProp.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.

def Mathlib.Meta.FunProp.FunctionData.getFnOrigin (fData : Mathlib.Meta.FunProp.FunctionData) : Mathlib.Meta.FunProp.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

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

  Name to unfold

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

  Custom discharger to satisfy theorem hypotheses.

• maxDepth : ℕ

  Maximal number of transitions between function properties e.g. inferring differentiability from linearity

• depth : ℕ

  current depth

• thmStack : List Mathlib.Meta.FunProp.Origin

  Stack of used theorem, used to prevent trivial loops.

• maxSteps : ℕ

  Maximum number of steps fun_prop can take.

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

Equations

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

structure Mathlib.Meta.FunProp.State : Type

fun_prop state

• cache : Lean.Meta.Simp.Cache

  Simp's cache is used as the funProp tactic is designed to be used inside of simp and utilize its cache

• 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.Config.addThm (cfg : Mathlib.Meta.FunProp.Config) (thmId : Mathlib.Meta.FunProp.Origin) : Mathlib.Meta.FunProp.Config

Log used theorem

Equations

• cfg.addThm thmId = { constToUnfold := cfg.constToUnfold, disch := cfg.disch, maxDepth := cfg.maxDepth, depth := cfg.depth, thmStack := thmId :: cfg.thmStack, maxSteps := cfg.maxSteps }

def Mathlib.Meta.FunProp.Config.increaseDepth (cfg : Mathlib.Meta.FunProp.Config) : Mathlib.Meta.FunProp.Config

Increase depth

Equations

• cfg.increaseDepth = { constToUnfold := cfg.constToUnfold, disch := cfg.disch, maxDepth := cfg.maxDepth, depth := cfg.depth + 1, thmStack := cfg.thmStack, maxSteps := cfg.maxSteps }

@[reducible, inline]

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

Equations

• Mathlib.Meta.FunProp.FunPropM = ReaderT Mathlib.Meta.FunProp.Config (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.previouslyUsedThm (thmOrigin : Mathlib.Meta.FunProp.Origin) : Mathlib.Meta.FunProp.FunPropM Bool

Check if previously used theorem was thmOrigin.

Equations

• Mathlib.Meta.FunProp.previouslyUsedThm thmOrigin = do let __do_lift ← read match __do_lift.thmStack.head? with | some thmOrigin' => pure (thmOrigin == thmOrigin') | x => pure false

def Mathlib.Meta.FunProp.withTheorem {α : Type} (thmOrigin : Mathlib.Meta.FunProp.Origin) (go : Mathlib.Meta.FunProp.FunPropM α) : Mathlib.Meta.FunProp.FunPropM α

Puts the theorem to the stack of used theorems.

Equations

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

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 : Mathlib.Meta.FunProp.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.RBSet Lean.Name Lean.Name.quickCmp := __do_lift.constToUnfold pure fun (n : Lean.Name) => toUnfold.contains n

def Mathlib.Meta.FunProp.increaseSteps : Mathlib.Meta.FunProp.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.logError (msg : String) : Mathlib.Meta.FunProp.FunPropM Unit

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

Equations

• Mathlib.Meta.FunProp.logError msg = modify fun (s : Mathlib.Meta.FunProp.State) => { cache := s.cache, numSteps := s.numSteps, msgLog := msg :: s.msgLog }