Modify proof terms so that they don't rely on unfolding certain constants

This file defines a procedure for inserting casts into (proof) terms in order to make them well typed in a setting where certain constants aren't allowed to be unfolded.

We make use of withCanUnfoldPred in order to modify which constants can and cannot be unfolded. This way, whnf and isDefEq do not unfold these constants.

So, the procedure is to check that an expression is well typed, analogous to Meta.check, and at each type mismatch, we try to insert a cast.

There are two kinds of casts:

• Equality casts. This is for propositions and terms, where it is possible to prove that one is equal to the other. For example Monotone.
• Explicit casting functions, both for unfolding and refolding. This is for types, where we cannot express their equivalence with an equality. For example DecidableLE.

structure Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries : Type

UnfoldBoundaries stores abstraction boundaries for definitions that shouldn't be unfolded.

• unfolds : Lean.NameMap Lean.Meta.SimpTheorem

  For propositions and terms of types, we store a rewrite theorem that unfolds it.

• casts : Lean.NameMap (Lean.Name × Lean.Name)

  For types, we store a cast for translating from and to the type respectively.

• insertionFuns : Lean.NameSet

  The functions that we want to unfold again after the translation has happened.

instance Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries : Inhabited UnfoldBoundaries

Equations

• Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries = { default := Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries.default }

def Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries.default : UnfoldBoundaries

Equations

• Mathlib.Tactic.UnfoldBoundary.instInhabitedUnfoldBoundaries.default = { unfolds := default, casts := default, insertionFuns := default }

inductive Mathlib.Tactic.UnfoldBoundary.UnfoldEntry : Type

An entry for the UnfoldBoundaries environment extension.

• unfold (declName unfold : Lean.Name) : UnfoldEntry
• cast (declName unfold refold unfold' refold' : Lean.Name) : UnfoldEntry

@[reducible, inline]

abbrev Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt : Type

Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded.

Equations

• Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt = Lean.SimplePersistentEnvExtension Mathlib.Tactic.UnfoldBoundary.UnfoldEntry Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries

def Mathlib.Tactic.UnfoldBoundary.registerUnfoldBoundaryExt : IO UnfoldBoundaryExt

Register a new UnfoldBoundaryExt.

Equations

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

def Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt.cast (b : UnfoldBoundaryExt) (e expectedType : Lean.Expr) (attr : Lean.Name) : Lean.MetaM Lean.Expr

Modify e so that it has type expectedType if the constants in b cannot be unfolded.

Equations

• b.cast e expectedType attr = do let __do_lift ← Lean.getEnv Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.cast✝ (Lean.SimplePersistentEnvExtension.getState b __do_lift) e expectedType attr

def Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Lean.Expr) (attr : Lean.Name) : Lean.MetaM Lean.Expr

Modify e so that it is well typed if the constants in b cannot be unfolded.

Note: it may be that e contains some constant whose type is not well typed in this setting. We don't make an effort to replace such constants. It seems that this approximation works well enough.

Equations

• b.insertBoundaries e attr = do let __do_lift ← Lean.getEnv Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.insertBoundaries✝ (Lean.SimplePersistentEnvExtension.getState b __do_lift) e attr

def Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt.unfoldInsertions (e : Lean.Expr) (b : UnfoldBoundaryExt) : Lean.CoreM Lean.Expr

Unfold all of the auxiliary functions that were inserted as unfold boundaries.

Equations

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