inductive TLA.ProofMode.CoalesceBinderMode : Type

How tla_coalesce_to_ptl treats binders while collecting PTL atoms.

• block : CoalesceBinderMode

  Abstract quantifiers and big operators as single coalescing atoms.

• ignore : CoalesceBinderMode

  Keep binders in the PTL skeleton and collect atoms inside their bodies.

@[implicit_reducible]

instance TLA.ProofMode.instBEqCoalesceBinderMode : BEq CoalesceBinderMode

Equations

• TLA.ProofMode.instBEqCoalesceBinderMode = { beq := TLA.ProofMode.instBEqCoalesceBinderMode.beq }

def TLA.ProofMode.instBEqCoalesceBinderMode.beq : CoalesceBinderMode → CoalesceBinderMode → Bool

Equations

• TLA.ProofMode.instBEqCoalesceBinderMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance TLA.ProofMode.instInhabitedCoalesceBinderMode : Inhabited CoalesceBinderMode

Equations

• TLA.ProofMode.instInhabitedCoalesceBinderMode = { default := TLA.ProofMode.instInhabitedCoalesceBinderMode.default }

inductive TLA.ProofMode.CoalesceAbstractLevel : Type

How much temporal structure tla_coalesce_to_ptl preserves.

• leaves : CoalesceAbstractLevel

  Abstract only first-order leaves such as state, action, pure, and enabled predicates.

• modal : CoalesceAbstractLevel

  Abstract the immediate arguments of modal operators.

• formula : CoalesceAbstractLevel

  Abstract each whole formula position as one atom.

@[implicit_reducible]

instance TLA.ProofMode.instBEqCoalesceAbstractLevel : BEq CoalesceAbstractLevel

Equations

• TLA.ProofMode.instBEqCoalesceAbstractLevel = { beq := TLA.ProofMode.instBEqCoalesceAbstractLevel.beq }

def TLA.ProofMode.instBEqCoalesceAbstractLevel.beq : CoalesceAbstractLevel → CoalesceAbstractLevel → Bool

Equations

• TLA.ProofMode.instBEqCoalesceAbstractLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance TLA.ProofMode.instInhabitedCoalesceAbstractLevel : Inhabited CoalesceAbstractLevel

Equations

• TLA.ProofMode.instInhabitedCoalesceAbstractLevel = { default := TLA.ProofMode.instInhabitedCoalesceAbstractLevel.default }

structure TLA.ProofMode.CoalesceConfig : Type

Configuration controlling where tla_coalesce_to_ptl abstracts blocks.

• binders : CoalesceBinderMode

  Whether quantifiers and big operators are abstracted as atoms or traversed.

• level : CoalesceAbstractLevel

  How much temporal structure to keep before abstracting subformulas.

• abstractOpaque : Bool

  Also abstract opaque pred σ terms that are not recognized first-order leaves.

def TLA.ProofMode.elabCoalesceConfig (cfg : Lean.Syntax) (init : CoalesceConfig := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM CoalesceConfig

Elaborator for CoalesceConfig options.

Equations

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

def TLA.ProofMode.tlaCoalesceToPTLTac : Lean.ParserDescr

tla_coalesce_to_ptl abstracts formula blocks from a TLA goal and keeps the requested amount of propositional temporal skeleton.

It supports raw validity goals, raw TLA sequents, and proof-mode Entails goals. The resulting fresh atoms are arbitrary pred σ values, so subsequent steps can reason propositionally about the remaining temporal structure.

Granularity options:

• level := .leaves abstracts concrete first-order leaves. This is the default.
• level := .modal abstracts immediate arguments of temporal operators.
• level := .formula abstracts each whole hypothesis/goal formula.
• binders := .block abstracts quantifiers and big operators as blocks. This is the default.
• binders := .ignore keeps quantifiers and big operators while coalescing blocks inside their bodies.
• abstractOpaque := true also abstracts opaque pred σ leaves.
• unfoldDerived := false leaves derived temporal definitions opaque.

Equations

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