Skip to content

Commit 5785ebb

Browse files
benbrastmckieclaude
benbrastmckie
and
claude
committed
feat(Logics): add FutureTemporalConnectives typeclass layer and LTL.Formula type
Split TemporalConnectives into FutureTemporalConnectives + TemporalConnectives. Add HasNext typeclass and LTLConnectives bundle. Create LTL.Formula with {atom, bot, imp, next, untl} and derived connectives. Add LTL.Formula.toTemporal embedding. Add basic LTL satisfaction over omega-words. Remove Encodable/Countable/Infinite/Denumerable and BEq instances from Temporal.Formula (deferred to completeness PR). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 0afc9d6 commit 5785ebb

6 files changed

Lines changed: 267 additions & 193 deletions

File tree

‎Cslib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
137137
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
138138
public import Cslib.Logics.HML.Basic
139139
public import Cslib.Logics.HML.LogicalEquivalence
140+
public import Cslib.Logics.LTL.Semantics.Satisfies
141+
public import Cslib.Logics.LTL.Syntax.Formula
140142
public import Cslib.Logics.LinearLogic.CLL.Basic
141143
public import Cslib.Logics.LinearLogic.CLL.CutElimination
142144
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion

‎Cslib/Foundations/Logic/Connectives.lean‎

Lines changed: 25 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,11 @@ class HasSince (F : Type*) where
7070
/-- The since temporal operator. -/
7171
snce : F → F → F
7272

73+
/-- A type has a next-step temporal operator. -/
74+
class HasNext (F : Type*) where
75+
/-- The next-step temporal operator. -/
76+
next : F → F
77+
7378
/-- A type has a conjunction connective. -/
7479
class HasAnd (F : Type*) where
7580
/-- The conjunction connective. -/
@@ -87,7 +92,25 @@ When all four connectives are needed, use
8792
`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/
8893
class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
8994

90-
/-- Temporal connectives: propositional connectives plus until and since. -/
91-
class TemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F, HasSince F
95+
/-- Future temporal connectives: propositional connectives plus until (no since, no next).
96+
97+
This bundle is shared by both `LTLConnectives` (which adds `HasNext`) and
98+
`TemporalConnectives` (which adds `HasSince`). Factoring out the future fragment
99+
allows code generic over future-only temporal logics without committing to past or
100+
next-step operators. -/
101+
class FutureTemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F
102+
103+
/-- LTL connectives: future temporal connectives plus a primitive next-step operator.
104+
105+
Linear Temporal Logic uses `next` as a primitive rather than deriving it from `until`
106+
(the encoding `next φ = φ U ⊥` does not hold in all models). `FutureTemporalConnectives`
107+
provides `bot`, `imp`, and `untl`; this bundle adds `next`. -/
108+
class LTLConnectives (F : Type*) extends FutureTemporalConnectives F, HasNext F
109+
110+
/-- Temporal connectives: propositional connectives plus until and since.
111+
112+
Extends `FutureTemporalConnectives` with the `since` operator, forming the standard
113+
two-sorted temporal signature (future + past). -/
114+
class TemporalConnectives (F : Type*) extends FutureTemporalConnectives F, HasSince F
92115

93116
end Cslib.Logic

‎Cslib/Logics/LTL/Semantics/Satisfies.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Logics.LTL.Syntax.Formula
10+
11+
/-! # LTL Satisfaction over Omega-Words
12+
13+
This module defines a basic satisfaction relation for LTL formulas over omega-words.
14+
An omega-word is represented as a valuation `v : ℕ → (Atom → Prop)`, assigning to
15+
each time point `i : ℕ` the set of atoms that hold at that point.
16+
17+
The semantics follow the standard Kripke/Pnueli definition of LTL over ω-sequences.
18+
Connection to `OmegaExecution` from the LTS library is deferred to future work.
19+
20+
## Main definitions
21+
22+
- `Satisfies v i φ` : formula `φ` holds at time `i` in valuation `v`
23+
- `Valid v φ` : `φ` holds at all time points in `v`
24+
- `Satisfiable φ` : `φ` holds at some time point in some valuation
25+
26+
## References
27+
28+
* [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977]
29+
* [M. Y. Vardi, P. Wolper,
30+
*An automata-theoretic approach to automatic program verification*][VardiWolper1986]
31+
-/
32+
33+
@[expose] public section
34+
35+
namespace Cslib.Logic.LTL
36+
37+
variable {Atom : Type*}
38+
39+
/-- Satisfaction relation for LTL over omega-words.
40+
41+
`Satisfies v i φ` means formula `φ` holds at time point `i` in the omega-word `v`,
42+
where `v : ℕ → (Atom → Prop)` assigns a set of true atoms to each time point.
43+
44+
The `untl` case uses the Burgess convention: `φ U ψ` holds at `i` when there exists
45+
a future time `j ≥ i` where φ holds (the event), and ψ holds at all intermediate
46+
points `i ≤ k < j` (the guard). -/
47+
def Satisfies (v : ℕ → (Atom → Prop)) (i : ℕ) : Formula Atom → Prop
48+
| .atom p => v i p
49+
| .bot => False
50+
| .imp φ ψ => Satisfies v i φ → Satisfies v i ψ
51+
| .next φ => Satisfies v (i + 1) φ
52+
| .untl φ ψ => ∃ j ≥ i, Satisfies v j φ ∧ ∀ k, i ≤ k → k < j → Satisfies v k ψ
53+
54+
/-- A formula holds at all time points in a given omega-word. -/
55+
def Valid (v : ℕ → (Atom → Prop)) (φ : Formula Atom) : Prop :=
56+
∀ i, Satisfies v i φ
57+
58+
/-- A formula is satisfiable: it holds at some time point in some omega-word. -/
59+
def Satisfiable (φ : Formula Atom) : Prop :=
60+
∃ (v : ℕ → (Atom → Prop)) (i : ℕ), Satisfies v i φ
61+
62+
end Cslib.Logic.LTL
63+
64+
end

‎Cslib/Logics/LTL/Syntax/Formula.lean‎

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Cslib.Foundations.Logic.Connectives
11+
public import Cslib.Logics.Temporal.Syntax.Formula
12+
13+
/-! # LTL Formula Type
14+
15+
This module defines the formula type for Linear Temporal Logic with primitives
16+
`{atom, bot, imp, next, untl}`. The primitive `next` operator is kept separate from
17+
`untl` following the Burgess convention: in full temporal logic, `next φ` is sometimes
18+
encoded as `φ U ⊥`, but this encoding does not hold in all models (it relies on
19+
discreteness and non-triviality). An independent primitive `next` avoids this coupling.
20+
21+
## Main definitions
22+
23+
- `Formula` : Inductive type for LTL formulas with constructors
24+
`atom`, `bot`, `imp`, `next`, `untl`
25+
- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point
26+
- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points
27+
- `Formula.toTemporal` : Embedding of `LTL.Formula` into `Temporal.Formula`
28+
29+
## Notation
30+
31+
Propositional connectives (scoped to `Cslib.Logic.LTL`):
32+
- `¬` (prefix, 40) : negation (`Formula.neg`)
33+
- `∧` (infix, 36) : conjunction (`Formula.and`)
34+
- `∨` (infix, 35) : disjunction (`Formula.or`)
35+
- `→` (infix, 30) : implication (`Formula.imp`)
36+
- `↔` (infix, 30) : biconditional (`Formula.iff`)
37+
38+
Temporal operators (scoped to `Cslib.Logic.LTL`):
39+
- `U` (infix, 40) : until (`Formula.untl`)
40+
- `X` (prefix, 40) : next-step (`Formula.next`)
41+
- `𝐅` (prefix, 40) : some future / eventually (`Formula.someFuture`)
42+
- `𝐆` (prefix, 40) : all future / globally (`Formula.allFuture`)
43+
44+
## Derived Operators
45+
46+
Derived operators follow the Burgess convention: in `untl event guard`, the first argument
47+
is the **event** (holds at the witness point) and the second is the **guard** (holds at all
48+
intermediate points). `someFuture φ` is `φ U ⊤` (φ is the event, ⊤ is the trivial guard).
49+
50+
## References
51+
52+
* [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977]
53+
* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968]
54+
* [J. P. Burgess, *Basic Tense Logic*][Burgess1984]
55+
* [M. Y. Vardi, P. Wolper,
56+
*An automata-theoretic approach to automatic program verification*][VardiWolper1986]
57+
-/
58+
59+
@[expose] public section
60+
61+
namespace Cslib.Logic.LTL
62+
63+
/-- LTL formula type. Primitives: atoms, falsum, implication, next-step, and until.
64+
65+
`next` is a primitive constructor and is not derived from `untl`. The encoding
66+
`next φ = φ U ⊥` holds on discrete non-ending sequences but fails in general temporal
67+
models; keeping `next` primitive supports broader model classes. -/
68+
inductive Formula (Atom : Type u) : Type u where
69+
/-- Atomic proposition. -/
70+
| atom (p : Atom)
71+
/-- Falsum / bottom. -/
72+
| bot
73+
/-- Implication. -/
74+
| imp (φ₁ φ₂ : Formula Atom)
75+
/-- Next-step operator: Xφ holds at t iff φ holds at t+1. -/
76+
| next (φ : Formula Atom)
77+
/-- Until temporal operator: φ₁ U φ₂ (Burgess: event U guard). -/
78+
| untl (φ₁ φ₂ : Formula Atom)
79+
deriving DecidableEq, BEq
80+
81+
/-- Negation: ¬φ := φ → ⊥ -/
82+
abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot
83+
84+
/-- Verum / top: ⊤ := ⊥ → ⊥ -/
85+
abbrev Formula.top : Formula Atom := .imp .bot .bot
86+
87+
/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/
88+
abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom :=
89+
.imp (.imp φ₁ .bot) φ₂
90+
91+
/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/
92+
abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom :=
93+
.imp (.imp φ₁ (.imp φ₂ .bot)) .bot
94+
95+
/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/
96+
abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom :=
97+
(φ₁.imp φ₂).and (φ₂.imp φ₁)
98+
99+
/-- Some future (eventually): F φ := φ U ⊤.
100+
Uses Burgess convention: φ is the event (holds at witness), ⊤ is the trivial guard. -/
101+
abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom :=
102+
.untl φ .top
103+
104+
/-- All future (globally): G φ := ¬F ¬φ -/
105+
abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom :=
106+
.neg (.someFuture (.neg φ))
107+
108+
@[inherit_doc] scoped prefix:40 "¬" => Formula.neg
109+
@[inherit_doc] scoped infix:36 " ∧ " => Formula.and
110+
@[inherit_doc] scoped infix:35 " ∨ " => Formula.or
111+
@[inherit_doc] scoped infix:30 " → " => Formula.imp
112+
@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff
113+
@[inherit_doc] scoped infix:40 " U " => Formula.untl
114+
@[inherit_doc] scoped prefix:40 "X" => Formula.next
115+
@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture
116+
@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture
117+
118+
/-- Register `LTL.Formula` as an instance of `LTLConnectives`. -/
119+
instance : LTLConnectives (Formula Atom) where
120+
bot := .bot
121+
imp := .imp
122+
untl := .untl
123+
next := .next
124+
125+
instance : Bot (Formula Atom) := ⟨.bot⟩
126+
instance : Top (Formula Atom) := ⟨.top⟩
127+
128+
/-- Embed `LTL.Formula` into `Temporal.Formula`.
129+
130+
`LTL.Satisfies` uses reflexive (non-strict) until: `∃ j ≥ i, ...`. The BX tense logic
131+
uses strict until: `∃ s > t, ...`. To preserve semantics, `untl` maps to
132+
`reflexiveUntl` (the derived non-strict operator), while `next` maps to the strict
133+
`untl · bot` which forces the witness to be the immediate successor on ℕ. -/
134+
def Formula.toTemporal : Formula Atom → Temporal.Formula Atom
135+
| .atom p => .atom p
136+
| .bot => .bot
137+
| .imp φ ψ => .imp (toTemporal φ) (toTemporal ψ)
138+
| .next φ => .untl (toTemporal φ) .bot
139+
| .untl φ ψ => (toTemporal φ).reflexiveUntl (toTemporal ψ)
140+
141+
end Cslib.Logic.LTL
142+
143+
end

0 commit comments

Comments
 (0)