This file implements a finite-window reduction for local TLA obligations.

The older simp_finite_exec_goal tactic unfolds a TLA formula on an explicit trace, then tries to discover and generalize the finitely many trace cells that remain. That is fragile: the tactic has to rediscover finite dependence from the unfolded goal shape.

Here the finite dependence is part of the certificate. A FiniteWindow p n contains a curried finite predicate core over exactly n states, together with a theorem saying that evaluating p on a trace is equivalent to evaluating core on the first n states of that trace. The tactic uses instance search to find a HasFiniteWindow p n, applies the certificate theorem, introduces the n state variables, and simplifies the resulting core.

For sequents, tlaFiniteWindow first changes p |-tla- q by definitional equality into |-tla- p → q, so the rest of the pipeline only handles validity goals.

def TLA.IteratedHomPred : Nat → Type u → Type u

A curried predicate over n consecutive states.

For example, IteratedHomPred 2 σ reduces to σ → σ → ULift Prop. The ULift in the base case is deliberate: for universe-polymorphic σ : Type u, the successor case lives in Type u, so the base proposition also has to be lifted into Type u. The user-facing goals are later simplified through .down.

Equations

• TLA.IteratedHomPred 0 x✝ = ULift Prop
• TLA.IteratedHomPred n.succ x✝ = (x✝ → TLA.IteratedHomPred n x✝)

def TLA.IteratedHomPred.evalExec {σ : Type u} (n : Nat) : IteratedHomPred n σ → exec σ → Prop

Evaluate a curried finite predicate on the first n states of a trace.

Equations

• TLA.IteratedHomPred.evalExec 0 p x✝ = p.down
• TLA.IteratedHomPred.evalExec n.succ p x✝ = TLA.IteratedHomPred.evalExec n (p (x✝ 0)) (TLA.exec.drop 1 x✝)

def TLA.IteratedHomPred.weaken {σ : Type u} (n m : Nat) : n ≤ m → IteratedHomPred n σ → IteratedHomPred m σ

View an n-state core as an m-state core when n ≤ m, ignoring the additional trailing states. This is used to combine two formulas with different window sizes into a common max window.

Equations

• TLA.IteratedHomPred.weaken 0 0 x_4 p = p
• TLA.IteratedHomPred.weaken 0 m.succ x_4 p = fun (x : σ) => TLA.IteratedHomPred.weaken 0 m ⋯ p
• TLA.IteratedHomPred.weaken n.succ 0 h x_4 = ⋯.elim
• TLA.IteratedHomPred.weaken n.succ m.succ h p = fun (s : σ) => TLA.IteratedHomPred.weaken n m ⋯ (p s)

theorem TLA.IteratedHomPred.evalExec_weaken {σ : Type u} {n m : Nat} (h : n ≤ m) (p : IteratedHomPred n σ) (e : exec σ) : evalExec m (weaken n m h p) e ↔ evalExec n p e

Weakening does not change how a core evaluates on any trace.

def TLA.IteratedHomPred.mkNot {σ : Type u} (n : Nat) : IteratedHomPred n σ → IteratedHomPred n σ

Negate an iterated finite-window predicate.

Equations

• TLA.IteratedHomPred.mkNot 0 p = { down := ¬p.down }
• TLA.IteratedHomPred.mkNot n.succ p = fun (s : σ) => TLA.IteratedHomPred.mkNot n (p s)

theorem TLA.IteratedHomPred.evalExec_mkNot {σ : Type u} (n : Nat) (p : IteratedHomPred n σ) (e : exec σ) : evalExec n (mkNot n p) e ↔ ¬evalExec n p e

def TLA.IteratedHomPred.mkBinary {σ : Type u} (op : Prop → Prop → Prop) (n : Nat) : IteratedHomPred n σ → IteratedHomPred n σ → IteratedHomPred n σ

Combine two iterated finite-window predicates with a binary connective.

Equations

• TLA.IteratedHomPred.mkBinary op 0 p q = { down := op p.down q.down }
• TLA.IteratedHomPred.mkBinary op n.succ p q = fun (s : σ) => TLA.IteratedHomPred.mkBinary op n (p s) (q s)

theorem TLA.IteratedHomPred.evalExec_mkBinary {σ : Type u} (op : Prop → Prop → Prop) (n : Nat) (p q : IteratedHomPred n σ) (e : exec σ) : evalExec n (mkBinary op n p q) e ↔ op (evalExec n p e) (evalExec n q e)

def TLA.IteratedHomPred.mkAnd {σ : Type u} (n : Nat) : IteratedHomPred n σ → IteratedHomPred n σ → IteratedHomPred n σ

Conjoin two iterated finite-window predicates.

Equations

• TLA.IteratedHomPred.mkAnd = TLA.IteratedHomPred.mkBinary fun (p q : Prop) => p ∧ q

theorem TLA.IteratedHomPred.evalExec_mkAnd {σ : Type u} (n : Nat) (p q : IteratedHomPred n σ) (e : exec σ) : evalExec n (mkAnd n p q) e ↔ evalExec n p e ∧ evalExec n q e

def TLA.IteratedHomPred.mkOr {σ : Type u} (n : Nat) : IteratedHomPred n σ → IteratedHomPred n σ → IteratedHomPred n σ

Disjoin two iterated finite-window predicates.

Equations

• TLA.IteratedHomPred.mkOr = TLA.IteratedHomPred.mkBinary fun (p q : Prop) => p ∨ q

theorem TLA.IteratedHomPred.evalExec_mkOr {σ : Type u} (n : Nat) (p q : IteratedHomPred n σ) (e : exec σ) : evalExec n (mkOr n p q) e ↔ evalExec n p e ∨ evalExec n q e

def TLA.IteratedHomPred.mkImplies {σ : Type u} (n : Nat) : IteratedHomPred n σ → IteratedHomPred n σ → IteratedHomPred n σ

Form the implication of two iterated finite-window predicates.

Equations

• TLA.IteratedHomPred.mkImplies = TLA.IteratedHomPred.mkBinary fun (p q : Prop) => p → q

theorem TLA.IteratedHomPred.evalExec_mkImplies {σ : Type u} (n : Nat) (p q : IteratedHomPred n σ) (e : exec σ) : evalExec n (mkImplies n p q) e ↔ evalExec n p e → evalExec n q e

def TLA.IteratedHomPred.mkBinder {σ : Type u} {α : Sort v} (op : (α → Prop) → Prop) (n : Nat) : (α → IteratedHomPred n σ) → IteratedHomPred n σ

Bind a quantifier over an iterated finite-window predicate.

Equations

• TLA.IteratedHomPred.mkBinder op 0 p = { down := op fun (x : α) => (p x).down }
• TLA.IteratedHomPred.mkBinder op n.succ p = fun (s : σ) => TLA.IteratedHomPred.mkBinder op n fun (x : α) => p x s

theorem TLA.IteratedHomPred.evalExec_mkBinder {σ : Type u} {α : Sort v} (op : (α → Prop) → Prop) (n : Nat) (p : α → IteratedHomPred n σ) (e : exec σ) : evalExec n (mkBinder op n p) e ↔ op fun (x : α) => evalExec n (p x) e

def TLA.IteratedHomPred.mkForall {σ : Type u} {α : Sort v} (n : Nat) : (α → IteratedHomPred n σ) → IteratedHomPred n σ

Universally quantify an iterated finite-window predicate.

Equations

• TLA.IteratedHomPred.mkForall = TLA.IteratedHomPred.mkBinder fun (p : α → Prop) => ∀ (x : α), p x

theorem TLA.IteratedHomPred.evalExec_mkForall {σ : Type u} {α : Sort v} (n : Nat) (p : α → IteratedHomPred n σ) (e : exec σ) : evalExec n (mkForall n p) e ↔ ∀ (x : α), evalExec n (p x) e

def TLA.IteratedHomPred.mkExists {σ : Type u} {α : Sort v} (n : Nat) : (α → IteratedHomPred n σ) → IteratedHomPred n σ

Existentially quantify an iterated finite-window predicate.

Equations

• TLA.IteratedHomPred.mkExists = TLA.IteratedHomPred.mkBinder fun (p : α → Prop) => ∃ (x : α), p x

theorem TLA.IteratedHomPred.evalExec_mkExists {σ : Type u} {α : Sort v} (n : Nat) (p : α → IteratedHomPred n σ) (e : exec σ) : evalExec n (mkExists n p) e ↔ ∃ (x : α), evalExec n (p x) e

def TLA.IteratedForall {σ : Type u} (n : Nat) : IteratedHomPred n σ → Prop

Universal closure of a finite core over all its state arguments.

Equations

• TLA.IteratedForall 0 p = p.down
• TLA.IteratedForall n.succ p = ∀ (s : σ), TLA.IteratedForall n (p s)

theorem TLA.IteratedForall.evalExec {σ : Type u} {n : Nat} {p : IteratedHomPred n σ} : IteratedForall n p → ∀ (e : exec σ), IteratedHomPred.evalExec n p e

A universally closed finite core holds on the first n states of every trace.

structure TLA.FiniteWindow {σ : Type u} (p : pred σ) (n : Nat) : Type u

FiniteWindow p n means that p can be represented as a predicate over the first n states of a trace.

• core : IteratedHomPred n σ

  The curried finite core over n states.

• iff_of_eval (e : exec σ) : p e ↔ IteratedHomPred.evalExec n self.core e

class TLA.HasFiniteWindow {σ : Type u} (p : pred σ) (n : outParam Nat) : Type u

A computable finite-window certificate.

The window is an output parameter so that instance synthesis can compute a canonical bound for p. The certificate itself is data, because tlaFiniteWindow uses its core field to produce the finite-state goal.

• finite : FiniteWindow p n

  The finite-window certificate for the predicate.

def TLA.finiteWindowOfHasFiniteWindow {σ : Type u} {p : pred σ} {n : Nat} [h : HasFiniteWindow p n] : FiniteWindow p n

Extract the semantic certificate from the tactic-facing class. Keeping this as a definition, not an instance for FiniteWindow, prevents arbitrary FiniteWindow facts from becoming part of instance search.

Equations

• TLA.finiteWindowOfHasFiniteWindow = TLA.HasFiniteWindow.finite

theorem TLA.FiniteWindow.valid_of_forall {σ : Type u} {p : pred σ} {n : Nat} (h : FiniteWindow p n) : IteratedForall n h.core → |-tla- (p)

Soundness theorem used by tlaFiniteWindow: proving the finite core for all choices of its state arguments proves validity of the original predicate.

theorem TLA.HasFiniteWindow.valid_of_forall {σ : Type u} {p : pred σ} {n : Nat} [h : HasFiniteWindow p n] : IteratedForall n finite.core → |-tla- (p)

def TLA.finiteWindowPure {σ : Type u} (P : Prop) : FiniteWindow [tlafml|⌞ P ⌟] 0

Finite-window certificate for a pure predicate.

Equations

• TLA.finiteWindowPure P = { core := { down := P }, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowPure {σ : Type u} (P : Prop) : HasFiniteWindow [tlafml|⌞ P ⌟] 0

Equations

• TLA.hasFiniteWindowPure P = { finite := TLA.finiteWindowPure P }

def TLA.finiteWindowTrue {σ : Type u} : FiniteWindow [tlafml|⊤] 0

Finite-window certificate for ⊤.

Equations

• TLA.finiteWindowTrue = { core := { down := True }, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowTrue {σ : Type u} : HasFiniteWindow [tlafml|⊤] 0

Equations

• TLA.hasFiniteWindowTrue = { finite := TLA.finiteWindowTrue }

def TLA.finiteWindowFalse {σ : Type u} : FiniteWindow [tlafml|⊥] 0

Finite-window certificate for ⊥.

Equations

• TLA.finiteWindowFalse = { core := { down := False }, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowFalse {σ : Type u} : HasFiniteWindow [tlafml|⊥] 0

Equations

• TLA.hasFiniteWindowFalse = { finite := TLA.finiteWindowFalse }

def TLA.finiteWindowState {σ : Type u} (p : σ → Prop) : FiniteWindow [tlafml|⌜ p ⌝] 1

Finite-window certificate for a state predicate.

Equations

• TLA.finiteWindowState p = { core := fun (s : σ) => { down := p s }, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowState {σ : Type u} (p : σ → Prop) : HasFiniteWindow [tlafml|⌜ p ⌝] 1

Equations

• TLA.hasFiniteWindowState p = { finite := TLA.finiteWindowState p }

def TLA.finiteWindowAction {σ : Type u} (a : action σ) : FiniteWindow [tlafml|⟨ a ⟩] 2

Finite-window certificate for an action predicate.

Equations

• TLA.finiteWindowAction a = { core := fun (s s' : σ) => { down := a s s' }, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowAction {σ : Type u} (a : action σ) : HasFiniteWindow [tlafml|⟨ a ⟩] 2

Equations

• TLA.hasFiniteWindowAction a = { finite := TLA.finiteWindowAction a }

def TLA.finiteWindowEnabled {σ : Type u} (a : action σ) : FiniteWindow [tlafml|Enabled a] 1

Finite-window certificate for an enabledness predicate.

Equations

• TLA.finiteWindowEnabled a = TLA.finiteWindowState (TLA.enabled a)

@[implicit_reducible]

instance TLA.hasFiniteWindowEnabled {σ : Type u} (a : action σ) : HasFiniteWindow [tlafml|Enabled a] 1

Equations

• TLA.hasFiniteWindowEnabled a = { finite := TLA.finiteWindowEnabled a }

def TLA.finiteWindowBinary {σ : Type u} (op : Prop → Prop → Prop) (p q : pred σ) (n m : Nat) (hp : FiniteWindow p n) (hq : FiniteWindow q m) : FiniteWindow (fun (e : exec σ) => op (p e) (q e)) (max n m)

Finite-window certificate for a binary connective of predicates.

Equations

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

def TLA.finiteWindowAnd {σ : Type u} (p q : pred σ) (n m : Nat) (hp : FiniteWindow p n) (hq : FiniteWindow q m) : FiniteWindow [tlafml|p ∧ q] (max n m)

Finite-window certificate for a conjunction.

Equations

• TLA.finiteWindowAnd p q n m hp hq = TLA.finiteWindowBinary (fun (p q : Prop) => p ∧ q) p q n m hp hq

@[implicit_reducible]

instance TLA.hasFiniteWindowAnd {σ : Type u} (p q : pred σ) (n m : Nat) [HasFiniteWindow p n] [HasFiniteWindow q m] : HasFiniteWindow [tlafml|p ∧ q] (max n m)

Equations

• TLA.hasFiniteWindowAnd p q n m = { finite := TLA.finiteWindowAnd p q n m TLA.finiteWindowOfHasFiniteWindow TLA.finiteWindowOfHasFiniteWindow }

def TLA.finiteWindowOr {σ : Type u} (p q : pred σ) (n m : Nat) (hp : FiniteWindow p n) (hq : FiniteWindow q m) : FiniteWindow [tlafml|p ∨ q] (max n m)

Finite-window certificate for a disjunction.

Equations

• TLA.finiteWindowOr p q n m hp hq = TLA.finiteWindowBinary (fun (p q : Prop) => p ∨ q) p q n m hp hq

@[implicit_reducible]

instance TLA.hasFiniteWindowOr {σ : Type u} (p q : pred σ) (n m : Nat) [HasFiniteWindow p n] [HasFiniteWindow q m] : HasFiniteWindow [tlafml|p ∨ q] (max n m)

Equations

• TLA.hasFiniteWindowOr p q n m = { finite := TLA.finiteWindowOr p q n m TLA.finiteWindowOfHasFiniteWindow TLA.finiteWindowOfHasFiniteWindow }

def TLA.finiteWindowNot {σ : Type u} (p : pred σ) (n : Nat) (hp : FiniteWindow p n) : FiniteWindow [tlafml|¬p] n

Finite-window certificate for a negation.

Equations

• TLA.finiteWindowNot p n hp = { core := TLA.IteratedHomPred.mkNot n hp.core, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowNot {σ : Type u} (p : pred σ) (n : Nat) [HasFiniteWindow p n] : HasFiniteWindow [tlafml|¬p] n

Equations

• TLA.hasFiniteWindowNot p n = { finite := TLA.finiteWindowNot p n TLA.finiteWindowOfHasFiniteWindow }

def TLA.finiteWindowImplies {σ : Type u} (p q : pred σ) (n m : Nat) (hp : FiniteWindow p n) (hq : FiniteWindow q m) : FiniteWindow [tlafml|p → q] (max n m)

Finite-window certificate for an implication.

Equations

• TLA.finiteWindowImplies p q n m hp hq = TLA.finiteWindowBinary (fun (p q : Prop) => p → q) p q n m hp hq

@[implicit_reducible]

instance TLA.hasFiniteWindowImplies {σ : Type u} (p q : pred σ) (n m : Nat) [HasFiniteWindow p n] [HasFiniteWindow q m] : HasFiniteWindow [tlafml|p → q] (max n m)

Equations

• TLA.hasFiniteWindowImplies p q n m = { finite := TLA.finiteWindowImplies p q n m TLA.finiteWindowOfHasFiniteWindow TLA.finiteWindowOfHasFiniteWindow }

def TLA.finiteWindowLater {σ : Type u} (p : pred σ) (n : Nat) (hp : FiniteWindow p n) : FiniteWindow [tlafml|◯p] (n + 1)

Finite-window certificate for the ◯ modality.

Equations

• TLA.finiteWindowLater p n hp = { core := fun (x : σ) => hp.core, iff_of_eval := ⋯ }

@[implicit_reducible]

instance TLA.hasFiniteWindowLater {σ : Type u} (p : pred σ) (n : Nat) [HasFiniteWindow p n] : HasFiniteWindow [tlafml|◯p] (n + 1)

Equations

• TLA.hasFiniteWindowLater p n = { finite := TLA.finiteWindowLater p n TLA.finiteWindowOfHasFiniteWindow }

def TLA.finiteWindowBinder {σ : Type u} {α : Sort v} (op : (α → Prop) → Prop) (op_congr : ∀ {p q : α → Prop}, (∀ (x : α), p x ↔ q x) → (op p ↔ op q)) (p : α → pred σ) (n : Nat) (hp : (x : α) → FiniteWindow (p x) n) : FiniteWindow (fun (e : exec σ) => op fun (x : α) => p x e) n

Finite-window certificate for a quantifier binder.

Equations

• TLA.finiteWindowBinder op op_congr p n hp = { core := TLA.IteratedHomPred.mkBinder op n fun (x : α) => (hp x).core, iff_of_eval := ⋯ }

def TLA.finiteWindowForall {σ : Type u} {α : Sort v} (p : α → pred σ) (n : Nat) (hp : (x : α) → FiniteWindow (p x) n) : FiniteWindow [tlafml|∀ x, (p x)] n

Finite-window certificate for a universal quantifier.

Equations

• TLA.finiteWindowForall p n hp = TLA.finiteWindowBinder (fun (r : α → Prop) => ∀ (x : α), r x) ⋯ p n hp

def TLA.finiteWindowExists {σ : Type u} {α : Sort v} (p : α → pred σ) (n : Nat) (hp : (x : α) → FiniteWindow (p x) n) : FiniteWindow [tlafml|∃ x, (p x)] n

Finite-window certificate for an existential quantifier.

Equations

• TLA.finiteWindowExists p n hp = TLA.finiteWindowBinder (fun (r : α → Prop) => ∃ (x : α), r x) ⋯ p n hp

@[implicit_reducible]

instance TLA.hasFiniteWindowForall {σ : Type u} {α : Sort v} (p : α → pred σ) (n : Nat) [hp : (x : α) → HasFiniteWindow (p x) n] : HasFiniteWindow [tlafml|∀ x, (p x)] n

Equations

• TLA.hasFiniteWindowForall p n = { finite := TLA.finiteWindowForall p n fun (x : α) => TLA.finiteWindowOfHasFiniteWindow }

@[implicit_reducible]

instance TLA.hasFiniteWindowExists {σ : Type u} {α : Sort v} (p : α → pred σ) (n : Nat) [hp : (x : α) → HasFiniteWindow (p x) n] : HasFiniteWindow [tlafml|∃ x, (p x)] n

Equations

• TLA.hasFiniteWindowExists p n = { finite := TLA.finiteWindowExists p n fun (x : α) => TLA.finiteWindowOfHasFiniteWindow }

def TLA.tacticTlaFiniteWindow : Lean.ParserDescr

tlaFiniteWindow reduces a finite-window TLA sequent to an ordinary Lean goal over finitely many states.

The tactic uses HasFiniteWindow instances for every predicate in the sequent. It supports local formulas built from state predicates, action predicates, pure predicates, Boolean connectives, implication, negation, and ◯. It deliberately does not peel genuinely temporal structure such as □; use sequent/modal rules first to expose a finite local obligation.

Equations

• TLA.tacticTlaFiniteWindow = Lean.ParserDescr.node `TLA.tacticTlaFiniteWindow 1024 (Lean.ParserDescr.nonReservedSymbol "tlaFiniteWindow" false)