Skip to content

Changing the semantics of LTLf to match most papers #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nathanael-fijalkow merged 1 commit into from
Jun 19, 2026
+110 −63
Merged

Changing the semantics of LTLf to match most papers #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions BoltLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
-- This module serves as the root of the `BoltLean` library.
-- Import modules here that should be built as part of the library.
import BoltLean.Basic
import BoltLean.Boolean.Domination
import BoltLean.Boolean.UpperBound
import BoltLean.Ltl.UpperBound
4 changes: 2 additions & 2 deletions BoltLean/Boolean/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,13 +23,13 @@ namespace BoolFormula
| And f1 f2 => f1.accepts v ∧ f2.accepts v
| Or f1 f2 => f1.accepts v ∨ f2.accepts v

/-- A formula satisfies an examples if it is positive and the formula accepts,
/-- A formula satisfies an example if it is positive and the formula accepts,
or if it is negative and the formula rejects.-/
@[simp]
def satisfies (f: BoolFormula n_sets) (v: Valuation n_sets) (positive: Bool) : Prop :=
f.accepts v ↔ positive

/-- A formula `f1` dominates `f2` another if `f1` satisfies a superset
/-- A formula `f1` dominates `f2` if `f1` satisfies a superset
of the elements satisfied by `f2`.-/
def dominates (f1 f2: BoolFormula n_sets): Prop :=
∀ (v: Valuation n_sets) (b: Bool), f2.satisfies v b → f1.satisfies v b
Expand Down
4 changes: 4 additions & 0 deletions BoltLean/Boolean/UpperBound.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,8 @@ namespace Valuation

end Valuation

namespace BoolFormula

/-- Given a list of valuations, construct a formula that accepts exactly these valuations. -/
def UpperBoundFormula (vs: List (Valuation n_var)) : BoolFormula n_var :=
let fs := vs.map Valuation.exact
Expand Down Expand Up @@ -153,3 +155,5 @@ theorem UpperBound (pos: List (Valuation n_var)) (neg: List (Valuation n_var))
rw [Valuation.exact_correct] at hf3
apply h v' hv'.left v hv
exact hf3

end BoolFormula
10 changes: 2 additions & 8 deletions BoltLean/Ltl/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,12 @@ namespace Formula
/-- Whether the formula is satisfied by the Trace.-/
def accepts (phi: Formula n) (t: Trace n): Prop :=
match t with
-- Special case of the empty Trace: it is only accepted by True and Globally,
-- or their boolean combinations.
| .nil => match phi with
| True | Globally _ => _root_.True
| False | Finally _ | Var _ _ | Next _ | WeakNext _ | Until _ _ => _root_.False
| Or psi1 psi2 => (accepts psi1 t) ∨ (accepts psi2 t)
| And psi1 psi2 => (accepts psi1 t) ∧ (accepts psi2 t)
| .nil => _root_.False
| head::tail => match phi with
| True => _root_.True
| False => _root_.False
| Var v neg => xor head[v] neg
| Next psi => accepts psi tail
| Next psi => tail ≠ List.nil ∧ accepts psi tail
| WeakNext psi => tail = List.nil ∨ accepts psi tail
| Globally psi => ∀ j, j < t.length → accepts psi (t.drop j)
| Finally psi => ∃ j, j < t.length ∧ accepts psi (t.drop j)
Expand Down
152 changes: 99 additions & 53 deletions BoltLean/Ltl/UpperBound.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,14 +16,15 @@ namespace Trace
let all_var := l.map (get_exact_var pos)
all_var.foldr Formula.And Formula.True

/-- Return a formula that accepts `t` and rejects all other traces.-/
/-- Return a formula that accepts `t` and rejects all other traces, when `t` is non-empty. -/
def exact (t: Trace n) : Formula n :=
match t with
| .nil => Formula.False.Globally
| .nil => Formula.False
| head :: .nil => (exact_at_pos head (List.finRange n)).And (Formula.WeakNext Formula.False)
| head :: tail => (exact_at_pos head (List.finRange n)).And (exact tail).Next

-- We now prove that the `exact` construction works:
-- - it is true on `t`
-- - it is true on non-empty `t`
-- - it is only true on `t`

/-- Helper Lemma for correctness -/
Expand All @@ -37,16 +38,22 @@ namespace Trace
| nil => simp [Formula.accepts]
| cons v vs ih => simp [Formula.accepts, ih, get_exact_var]

/-- Correctness: `t.exact` evaluates to true on `t` -/
theorem exact_accepts (t: Trace n):
/-- Correctness: `t.exact` evaluates to true on non-empty `t`. -/
theorem exact_accepts (t: Trace n) (ht: t ≠ []):
(t.exact).accepts t := by
induction t with
| nil => simp [exact, Formula.accepts]
| nil => contradiction
| cons hd tl ih =>
simp [Formula.accepts, exact]
constructor
. exact exact_at_pos_accepts hd tl
. exact ih
cases tl with
| nil =>
simp [Formula.accepts, exact]
exact exact_at_pos_accepts hd []
| cons hd' tl' =>
simp [Formula.accepts, exact]
constructor
. exact exact_at_pos_accepts hd (hd'::tl')
. apply ih
simp

-- Soundness
/-- Lemma: Taking the `And` of a list of formulas and evaluating is the same as
Expand All @@ -62,12 +69,20 @@ namespace Trace
. unfold List.foldr at he
unfold Formula.accepts at he
simp [*] at he
cases t <;> simp at he <;> exact he.left
cases t with
| nil => cases he
| cons head tail =>
simp at he
exact he.left
. next h_in =>
unfold List.foldr at he
unfold Formula.accepts at he
simp [*] at he
cases t <;> simp at he <;> apply ih he.right f h_in
cases t with
| nil => cases he
| cons head tail =>
simp at he
apply ih he.right f h_in

/-- Lemma: If `exact_at_pos pos l` accepts, then `get_exact_var pos v` also accepts for all `v ∈ l`-/
theorem exact_at_pos_accepts_all (pos pos': Vector Bool n) (t: Trace n) (l: List (Fin n)) :
Expand All @@ -94,36 +109,36 @@ namespace Trace
/-- Lemma: If `exact t` accepts `t'`, then `t` and `t'` have the same head.-/
theorem exact_accepts_head (h h': Vector Bool n) (t t': Trace n):
(exact (h::t)).accepts (h'::t') → h = h' := by
simp [exact, Formula.accepts]
intro h_accepts h2
intro hyp
have h_accepts: (exact_at_pos h (List.finRange n)).accepts (h' :: t') := by
cases t with
| nil =>
simp [exact, Formula.accepts] at hyp
exact hyp.left
| cons head tail =>
simp [exact, Formula.accepts] at hyp
exact hyp.left
ext i hi
have h1 := exact_at_pos_accepts_all h h' t' (List.finRange n) h_accepts ⟨i, hi⟩ (List.mem_finRange ⟨i, hi⟩)
unfold Formula.accepts at h1
simp [get_exact_var] at h1
rw [h1]

/-- Lemma: If `exact t` accepts `t'`, then `t` and `t'` have the same tail.-/
theorem exact_accepts_cons (h h': Vector Bool n) (t t': Trace n):
theorem exact_accepts_cons (h h': Vector Bool n) (t t': Trace n) (ht: t ≠ []):
(exact (h::t)).accepts (h'::t') → (exact t).accepts t' := by
intro hyp
unfold exact at hyp
unfold Formula.accepts at hyp
simp at hyp
have h2 := hyp.right
unfold Formula.accepts at h2
simp at h2
exact h2
cases t with
| nil => contradiction
| cons head tail =>
simp [exact, Formula.accepts] at hyp
exact hyp.right.right

/-- Lemma: `exact` of the empty trace does not accept non-empty traces.-/
theorem exact_nil_not_accepts_cons (h: Vector Bool n) (t: Trace n):
¬ (exact []).accepts (h :: t) := by
intro h1
unfold exact at h1
unfold Formula.accepts at h1
simp at h1
have h2 := h1 0
simp [List.drop] at h2
simp [Formula.accepts] at h2
simp [exact, Formula.accepts] at h1

open Classical
/-- Soundness: `t.exact` only accepts `t`-/
Expand All @@ -140,31 +155,39 @@ namespace Trace
exact h
| cons hd tl ih =>
induction t' with
| nil => simp [exact, Formula.accepts] at h
| nil => simp [Formula.accepts] at h
| cons hd' tl' ih' =>
simp
constructor
. exact exact_accepts_head hd hd' tl tl' h
. apply ih
apply exact_accepts_cons hd hd'
assumption
. cases tl with
| nil =>
cases tl' with
| nil => rfl
| cons hd_tl' tl_tl' =>
simp [exact, Formula.accepts] at h
| cons hd_tl tl_tl =>
apply ih
apply exact_accepts_cons hd hd' (hd_tl::tl_tl) tl'
. simp
. assumption


/-- Correctness and soundness of `t.exact` -/
theorem exact_correct (t t': Trace n):
theorem exact_correct (t t': Trace n) (ht: t ≠ []):
t.exact.accepts t' ↔ t = t' := by
constructor
. exact exact_accepts_only t t'
. intro h
rw [h]
exact exact_accepts t'
rw [h] at ht ⊢
exact exact_accepts t' ht

theorem exists_accept_only (t: Trace n) :
theorem exists_accept_only (t: Trace n) (ht: t ≠ []) :
exists (phi: Formula n), phi.accepts t ∧
forall (t': Trace n), t ≠ t' → ¬phi.accepts t' := by
exists t.exact
constructor
. exact t.exact_accepts
. exact t.exact_accepts ht
. intro t'
intro hne
intro he
Expand All @@ -173,8 +196,8 @@ namespace Trace

end Trace

/-- Given a list of traces, construct a formula that accepts
exactly these traces, and no other. -/
/-- Given a list of non-empty traces, construct a formula that accepts
exactly those traces, and no other non-empty trace. -/
def UpperBoundFormula (ts: List (Trace n)) : Formula n :=
let fs := ts.map Trace.exact
fs.foldr Formula.Or Formula.False
Expand All @@ -191,12 +214,24 @@ theorem foldr_or_aux (l: List (Formula n)) (t: Trace n):
. unfold List.foldr
unfold Formula.accepts
simp
cases t <;> simp <;> left <;> exact he
cases t with
| nil =>
simp [Formula.accepts] at he
| cons head tail =>
simp
left
exact he
. next h_in =>
unfold List.foldr
unfold Formula.accepts
simp
cases t <;> simp <;> right <;> apply ih f h_in he
cases t with
| nil =>
simp [Formula.accepts] at he
| cons head tail =>
simp
right
apply ih f h_in he



Expand All @@ -213,12 +248,22 @@ theorem foldr_or_aux_rev (l: List (Formula n)) (t: Trace n):
unfold List.foldr at h
unfold Formula.accepts at h
simp at h
cases t
<;> simp at h
<;> simp
<;> match h with
| .inl h1 => left; exact h1
| .inr h1 => right; apply ih; exact h1
cases t with
| nil =>
simp at h
| cons head tail =>
simp at h
match h with
| .inl h1 =>
exists hd
simp
exact h1
| .inr h1 =>
have ⟨f, hf⟩ := ih h1
exists f
constructor
. exact List.mem_cons_of_mem hd hf.left
. exact hf.right

theorem list_map_contains (l: List α) (f: α → β):
(∀b, b ∈ l.map f → ∃ a ∈ l, b = f a) := by
Expand All @@ -238,10 +283,12 @@ theorem list_map_contains (l: List α) (f: α → β):


/-- Theorem:
For any disjoint set of positive and negative examples,
there exists a formula that accepts all the positive and rejects the negatives.
For any disjoint lists of non-empty positive and negative examples,
there exists a formula that accepts all positive examples and rejects all negative examples.
-/
theorem UpperBound (pos: List (Trace n)) (neg: List (Trace n)) (h: ∀ t ∈ pos, ∀ t'∈ neg, t ≠ t') :
theorem UpperBound (pos: List (Trace n)) (neg: List (Trace n))
(h: ∀ t ∈ pos, ∀ t'∈ neg, t ≠ t')
(h_nonempty: ∀ t, t ∈ pos ∨ t ∈ neg → t ≠ []) :
exists (phi: Formula n), (∀ t ∈ pos, phi.accepts t) ∧ (∀t ∈ neg, ¬ phi.accepts t):= by
exists UpperBoundFormula pos
constructor
Expand All @@ -261,7 +308,7 @@ theorem UpperBound (pos: List (Trace n)) (neg: List (Trace n)) (h: ∀ t ∈ pos
have hr := h.right
have h2 := ih hr
exists t
. exact t.exact_accepts
. exact t.exact_accepts (h_nonempty t (.inl ht))
. intro t ht he
unfold UpperBoundFormula at he
simp at he
Expand All @@ -271,6 +318,5 @@ theorem UpperBound (pos: List (Trace n)) (neg: List (Trace n)) (h: ∀ t ∈ pos
exact hf.left
have hf3 := hf.right
rw [ht'.right] at hf3
rw [Trace.exact_correct] at hf3
apply h t' ht'.left t ht
exact hf3
exact Trace.exact_accepts_only t' t hf3