Gadgets for providing different variants of a proven theorem.

def TLA.Deriving.assembleUnderCommonContextShape (σ : Lean.Expr) (ps : List Lean.Expr) (q : Lean.Expr) : Lean.MetaM Lean.Expr

Assemble premises and a conclusion under a shared context Γ.

Equations

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

def TLA.Deriving.assembleSeparatedPredImplications (ps : List Lean.Expr) (q : Lean.Expr) : Lean.MetaM Lean.Expr

Assemble a list of premise predicates and a conclusion into the arrow chain of separated predImplies/valid statements used by tla_derive.

Equations

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

def TLA.Deriving.deriveForPredImpliesOrValid (nm : Lean.Name) : Lean.CoreM Unit

For a TLA theorem whose conclusion is a single TLA.predImplies or TLA.valid, this function automatically derives its several equivalent or weakened versions, which might be easier to use elsewhere.

For example, consider the following statement:

|-tla- ((p' ⇒ p) → (q ⇒ q') → (p ↝ q) ⇒ (p' ↝ q'))

One useful, but weaker version is:

(p') |-tla- (p) → (q) |-tla- (q') → (p ↝ q) |-tla- (p' ↝ q')

which is derived by repeatly applying impl_decouple, impl_intro and always_intro.

Another useful and equivalent version is:

∀ Γ, (Γ) |-tla- (p' ⇒ p) → (Γ) |-tla- (q ⇒ q') → (Γ) |-tla- ((p ↝ q) ⇒ (p' ↝ q'))

which can be used in case we want to keep the context Γ.

Equations

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

def tlaDerive : Lean.ParserDescr

For a TLA theorem with this attribute in the form of a single TLA.predImplies or TLA.valid, its different variants will be derived. See the docstring of TLA.Deriving.deriveForPredImpliesOrValid for more details.

Equations

• tlaDerive = Lean.ParserDescr.node `tlaDerive 1024 (Lean.ParserDescr.nonReservedSymbol "tla_derive" false)