From 65d34b0aac81215cfbd573881a3bd7e287229404 Mon Sep 17 00:00:00 2001 From: Pierre Vandenhove Date: Wed, 17 Jun 2026 13:41:38 +0200 Subject: [PATCH] changing the semantics --- BoltLean.lean | 3 + BoltLean/Boolean/Basic.lean | 4 +- BoltLean/Boolean/UpperBound.lean | 4 + BoltLean/Ltl/Basic.lean | 10 +- BoltLean/Ltl/UpperBound.lean | 152 ++++++++++++++++++++----------- 5 files changed, 110 insertions(+), 63 deletions(-) diff --git a/BoltLean.lean b/BoltLean.lean index 2782ae9..9aa54a4 100644 --- a/BoltLean.lean +++ b/BoltLean.lean @@ -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 diff --git a/BoltLean/Boolean/Basic.lean b/BoltLean/Boolean/Basic.lean index 2105e98..dd98787 100644 --- a/BoltLean/Boolean/Basic.lean +++ b/BoltLean/Boolean/Basic.lean @@ -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 diff --git a/BoltLean/Boolean/UpperBound.lean b/BoltLean/Boolean/UpperBound.lean index 6849f29..09e0c5d 100644 --- a/BoltLean/Boolean/UpperBound.lean +++ b/BoltLean/Boolean/UpperBound.lean @@ -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 @@ -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 diff --git a/BoltLean/Ltl/Basic.lean b/BoltLean/Ltl/Basic.lean index e84ec3f..2496c3f 100644 --- a/BoltLean/Ltl/Basic.lean +++ b/BoltLean/Ltl/Basic.lean @@ -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) diff --git a/BoltLean/Ltl/UpperBound.lean b/BoltLean/Ltl/UpperBound.lean index 735326c..295b542 100644 --- a/BoltLean/Ltl/UpperBound.lean +++ b/BoltLean/Ltl/UpperBound.lean @@ -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 -/ @@ -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 @@ -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)) : @@ -94,8 +109,15 @@ 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 @@ -103,27 +125,20 @@ namespace Trace 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`-/ @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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