Gadgets for lifting a propositional theorem to the level of temporal logic.

def TLA.Lifting.liftPropToPurePred (σ p : Lean.Expr) : Lean.MetaM Lean.Expr

If p : Prop, then lift it to ⌞ p ⌟ of type TLA.pred σ; otherwise do nothing and return p (note that in this case, whether p is of type TLA.pred σ is not checked).

Equations

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

@[irreducible]

def TLA.Lifting.convertPropToTLAPredAux (fuel : Nat) (alist : Lean.AssocList Lean.Expr Lean.Expr) (σ p : Lean.Expr) : Lean.MetaM Lean.Expr

Recursively convert a propositional Expr p into the corresponding TLA predicate, replacing leaves via alist. fuel bounds the recursion depth; each recursive call descends into a strict subterm, so seeding it from the expression's depth always suffices.

Equations

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

def TLA.Lifting.convertPropToTLAPred (alist : Lean.AssocList Lean.Expr Lean.Expr) (σ p : Lean.Expr) : Lean.MetaM Lean.Expr

Convert a propositional Expr into the corresponding TLA predicate, seeding the recursion fuel from the expression's approximate depth.

Equations

• TLA.Lifting.convertPropToTLAPred alist σ p = TLA.Lifting.convertPropToTLAPredAux (p.approxDepth.toNat + 1) alist σ p >>= TLA.Lifting.liftPropToPurePred σ

inductive TLA.Lifting.LiftingCase : Type

Which shape a lifted theorem's conclusion takes.

• Iff : LiftingCase

  The case where the conclusion is a single ↔.

• Other : LiftingCase

  The other cases, including those where the conclusion is a series of →.

@[instance_reducible]

instance TLA.Lifting.instInhabitedLiftingCase : Inhabited LiftingCase

Equations

• TLA.Lifting.instInhabitedLiftingCase = { default := TLA.Lifting.instInhabitedLiftingCase.default }

@[instance_reducible]

instance TLA.Lifting.instToStringLiftingCase : ToString LiftingCase

Equations

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

def TLA.Lifting.guessWhereToStart (thmStmt : Lean.Expr) : Lean.MetaM Nat

Given thmStmt being x₁ → x₂ → ⋯ → xₙ, find the longest suffix xₘ → ⋯ → xₙ such that each xᵢ is a Prop and independent.

Equations

• TLA.Lifting.guessWhereToStart thmStmt = Lean.Meta.forallTelescope thmStmt fun (xs : Array Lean.Expr) (body : Lean.Expr) => TLA.Lifting.guessWhereToStartAux✝ [body] xs.reverse.toList

def TLA.Lifting.convertTheoremStatement (thmStmt : Lean.Expr) (uName : Lean.Name) : Lean.MetaM (LiftingCase × Lean.Expr)

Convert a theorem statement to the level of temporal logic. Given the theorem statement and the name of the additional universe level (required by σ in TLA.pred σ), return the case for lifting and the converted statement.

Equations

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

def TLA.Lifting.liftTheorem (thmName : Lean.Name) (liftedThmName : Option Lean.Name) (tactic? : Option (Lean.TSyntax `term)) : Lean.MetaM Unit

Lift the theorem named thmName to the temporal-logic level, optionally renaming the result (liftedThmName) and supplying a proof tactic?.

Equations

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

def tlaLiftTac : Lean.ParserDescr

#tla_lift thm₁ ... thmₙ lifts (typically purely first-order) theorems thm₁, ... ,thmₙ to the temporal logic level. Each new theorem will have the prefix TLA. and the same suffix as before.

For example, after executing #tla_lift Decidable.not_not, there will be a new theorem named TLA.not_not in the environment.

Equations

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

def tlaLiftSingleTac : Lean.ParserDescr

#tla_lift thm => newthm behaves like #tla_lift, but only lifts one theorem, while naming the new theorem as newthm.

Equations

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