LeanPool.Lentil.Basic

A Shallow-Embedding of TLA #

NOTE: There are multiple ways to formalize the concept of infinite sequences. Here, we follow the definition from coq-tla, while an alternative is to define infinite sequence as a coinductive datatype (like Stream in Rocq/Agda).

Lean also comes with a definition of `Stream`, but it is a type class instead of
a datatype, and the sequences generated from it are not necessarily infinite
(in the sense that it may generate finite sequences). So here we do not use it.

source

def TLA.exec (σ : Type u) :

Type u

An execution: an infinite sequence of states indexed by Nat.

Equations

TLA.exec σ = (Nat → σ)

Instances For

source

def TLA.pred (σ : Type u) :

Type u

A temporal predicate: a property of executions.

Equations

TLA.pred σ = (TLA.exec σ → Prop)

Instances For

source

def TLA.statePred {σ : Type u} (f : σ → Prop) :

pred σ

Lift a state property to the temporal predicate that holds at the first state.

Equations

e |=tla= ⌜ f ⌝ = f (e 0)

Instances For

source

def TLA.action (σ : Type u) :

Type u

An action: a binary relation between the current and next state.

Equations

TLA.action σ = (σ → σ → Prop)

Instances For

source

def TLA.actionPred {σ : Type u} (a : action σ) :

pred σ

Lift an action to the temporal predicate that holds on the first two states.

Equations

e |=tla= ⟨ a ⟩ = a (e 0) (e 1)

Instances For

source

def TLA.purePred {α : Type u} (p : Prop) :

pred α

Lift a Prop to the temporal predicate that holds iff the Prop does.

Equations

(⌞ p ⌟) =tla= (⌜ fun (x : α) => p ⌝)

Instances For

source

def TLA.tlaTrue {α : Type u} :

pred α

The temporal predicate that always holds.

Equations

(⊤) =tla= (⌞ True ⌟)

Instances For

source

def TLA.tlaFalse {α : Type u} :

pred α

The temporal predicate that never holds.

Equations

(⊥) =tla= (⌞ False ⌟)

Instances For

source

def TLA.tlaAnd {α : Type u} (p q : pred α) :

pred α

Conjunction of temporal predicates.

Equations

σ |=tla= p ∧ q = (p σ ∧ q σ)

Instances For

source

def TLA.tlaOr {α : Type u} (p q : pred α) :

pred α

Disjunction of temporal predicates.

Equations

σ |=tla= p ∨ q = (p σ ∨ q σ)

Instances For

source

def TLA.tlaImplies {α : Type u} (p q : pred α) :

pred α

Implication of temporal predicates.

Equations

σ |=tla= p → q = (p σ → q σ)

Instances For

source

def TLA.tlaNot {α : Type u} (p : pred α) :

pred α

Negation of a temporal predicate.

Equations

σ |=tla= ¬p = ¬p σ

Instances For

source

def TLA.tlaForall {α : Sort u} {β : Type v} (p : α → pred β) :

pred β

Universal quantification over temporal predicates.

Equations

σ |=tla= ∀ x, (p x) = ∀ (x : α), p x σ

Instances For

source

def TLA.tlaExists {α : Sort u} {β : Type v} (p : α → pred β) :

pred β

Existential quantification over temporal predicates.

Equations

σ |=tla= ∃ x, (p x) = ∃ (x : α), p x σ

Instances For

source

instance TLA.instCommutativePredTlaAnd {α : Type u} :

Std.Commutative tlaAnd

source

instance TLA.instAssociativePredTlaAnd {α : Type u} :

Std.Associative tlaAnd

source

instance TLA.instCommutativePredTlaOr {α : Type u} :

Std.Commutative tlaOr

source

instance TLA.instAssociativePredTlaOr {α : Type u} :

Std.Associative tlaOr

source

def TLA.exec.drop {α : Type u} (k : Nat) (σ : exec α) :

exec α

Drop the first k states of an execution.

Equations

TLA.exec.drop k σ n = σ (n + k)

Instances For

source

def TLA.exec.take {α : Type u} (k : Nat) (σ : exec α) :

List α

The list of the first k states of an execution.

Equations

TLA.exec.take k σ = List.map σ (List.range k)

Instances For

source

def TLA.exec.takeFrom {α : Type u} (start k : Nat) (σ : exec α) :

List α

The list of k states of an execution starting at index start.

Equations

TLA.exec.takeFrom start k σ = List.map σ (List.range' start k)

Instances For

source

def TLA.always {α : Type u} (p : pred α) :

pred α

The always (box) modality: p holds on every suffix.

Equations

σ |=tla= □p = ∀ (k : Nat), p (TLA.exec.drop k σ)

Instances For

source

def TLA.eventually {α : Type u} (p : pred α) :

pred α

The eventually (diamond) modality: p holds on some suffix.

Equations

σ |=tla= ◇p = ∃ (k : Nat ), p (TLA.exec.drop k σ)

Instances For

source

def TLA.later {α : Type u} (p : pred α) :

pred α

The later (next) modality: p holds on the suffix dropping one state.

Equations

σ |=tla= ◯p = p (TLA.exec.drop 1 σ)

Instances For

source

def TLA.exec.satisfies {α : Type u} (p : pred α) (σ : exec α) :

Prop

An execution satisfies a temporal predicate.

Equations

σ |=tla= p = p σ

Instances For

source

def TLA.valid {α : Type u} (p : pred α) :

Prop

A temporal predicate is valid: it holds on every execution.

Equations

|-tla- (p ) = ∀ (σ : TLA.exec α), σ |=tla= p

Instances For

source

def TLA.predImplies {α : Type u} (p q : pred α) :

Prop

Entailment between temporal predicates over all executions.

Equations

(p ) |-tla- (q ) = ∀ (σ : TLA.exec α), σ |=tla= p → σ |=tla= q

Instances For

source

def TLA.enabled {α : Type u} (a : action α) (s : α) :

Prop

An action is enabled at a state if some successor state exists.

Equations

TLA.enabled a s = ∃ (s' : α), a s s'

Instances For

source

def TLA.tlaEnabled {α : Type u} (a : action α) :

pred α

The temporal predicate asserting that an action is enabled.

Equations

(Enabled a) =tla= (⌜ TLA.enabled a ⌝)

Instances For

source

def TLA.tlaBigwedge {α : Type u} {β : Type v} {c : Type v → Type u_1} [Foldable c] (f : β → pred α) (s : c β) :

pred α

Big conjunction of temporal predicates over a foldable collection.

Equations

(⋀ x ∈ s, (f x)) =tla= ((TLA.Foldable.fold TLA.tlaAnd [tlafml|⊤] f s))

Instances For

source

def TLA.tlaBigvee {α : Type u} {β : Type v} {c : Type v → Type u_1} [Foldable c] (f : β → pred α) (s : c β) :

pred α

Big disjunction of temporal predicates over a foldable collection.

Equations

(⋁ x ∈ s, (f x)) =tla= ((TLA.Foldable.fold TLA.tlaOr [tlafml|⊥] f s))

Instances For

source

def TLA.tlaUntil {α : Type u} (p q : pred α) :

pred α

The until modality: p holds until q becomes true.

Equations

σ |=tla= p 𝑈 q = ∃ (i : Nat ), q (TLA.exec.drop i σ) ∧ ∀ (j : Nat), j < i → p (TLA.exec.drop j σ)

Instances For

Syntax for TLA Notations #

Our notations for TLA formulas intersect with those for plain Lean terms,
so to avoid potentially ambiguity(?), we define a new syntax category `tlafml`
for TLA formulas and define macro rules for expanding formulas in `tlafml` into
Lean terms.

source

def tlafml.quot :

Lean.ParserDescr

Equations

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

Instances For

source

def Lean.Parser.Category.tlafml :

Pretty-Printing for TLA Notations #

source

def TLA.syntaxTermToTlafml {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (stx : Lean.TSyntax `term) :

m (Lean.TSyntax `tlafml)

Converting a syntax in term category into tlafml. This is useful in the cases where we want to eliminate the redundant [tlafml| ... ] wrapper of some sub-formula when it is inside a tlafml.

Equations

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

Instances For

source

def TLA.syntaxTlafmlToTerm {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (stx : Lean.TSyntax `tlafml) :

m (Lean.TSyntax `term)

Converting a syntax in term category into tlafml, by inserting [tlafml| ... ] wrapper if needed.

Equations

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

Instances For

source

def TLA.annAsTerm {any : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax any) :

Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax any)

Annotate the syntax with term info for the delaborator.

Equations

TLA.annAsTerm stx = (fun (x : Lean.Syntax) => { raw := x }) <$> do let a ← Lean.PrettyPrinter.Delaborator.annotateTermInfo { raw := stx.raw } pure a.raw

Instances For

source

def TLA.delabTlafmlAux (fuel : Nat) :

Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `tlafml)

Delaborate the current expression into tlafml syntax. fuel bounds the recursion depth; each recursive call descends into a strict subexpression, so seeding it with the expression's depth always suffices.

Instances For

source

def TLA.delabTlafmlAux.getBindernameFunbody (body : Lean.Term) :

Lean.PrettyPrinter.Delaborator.DelabM (Lean.Ident × Lean.TSyntax `tlafml)

Extract the binder name and body of a delaborated lambda.

Equations