Skip to content

Commit 0056b0b

Browse files
author
GBathie
committed
Upper bound formally proven!
1 parent 16a3442 commit 0056b0b

4 files changed

Lines changed: 401 additions & 368 deletions

File tree

‎BoltLean/Ltl-alt.lean‎

Lines changed: 0 additions & 163 deletions
This file was deleted.

‎BoltLean/Ltl-old.lean‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
import BoltLean.Helpers
2+
3+
structure Trace (n_pred: Nat) where
4+
length: Nat
5+
pos_length : length > 0
6+
pos_n_pred: n_pred > 0
7+
predicates : Vector (Vector Bool length) n_pred
8+
deriving Repr
9+
10+
/-- LTL Formulas in NNF -/
11+
inductive Formula n_pred
12+
| True : Formula n_pred
13+
| False : Formula n_pred
14+
| Var : Fin n_pred -> (neg: Bool) -> Formula n_pred -- neg: Whether the variable is negated
15+
| Next : Formula n_pred -> Formula n_pred
16+
| WeakNext : Formula n_pred -> Formula n_pred
17+
| Globally : Formula n_pred -> Formula n_pred
18+
| Finally : Formula n_pred -> Formula n_pred
19+
| Or : Formula n_pred -> Formula n_pred -> Formula n_pred
20+
| And : Formula n_pred -> Formula n_pred -> Formula n_pred
21+
| Until : Formula n_pred -> Formula n_pred -> Formula n_pred
22+
deriving DecidableEq
23+
24+
namespace Formula
25+
26+
def eval_aux (phi: Formula n) (t: Trace n) (i: Fin t.length): Prop :=
27+
match phi with
28+
| True => _root_.True
29+
| False => _root_.False
30+
| Var v neg => xor t.predicates[v][i] neg
31+
| Next psi => if h: i < t.length - 1 then eval_aux psi t ⟨i.val + 1, by omega⟩ else _root_.False
32+
| WeakNext psi => (h: i < t.length - 1) → eval_aux psi t ⟨i.val + 1, by omega⟩
33+
| Globally psi => ∀ j, j ≥ i → eval_aux psi t j
34+
| Finally psi => ∃ j, j ≥ i ∧ eval_aux psi t j
35+
| Or psi1 psi2 => (eval_aux psi1 t i) ∨ (eval_aux psi2 t i)
36+
| And psi1 psi2 => (eval_aux psi1 t i) ∧ (eval_aux psi2 t i)
37+
| Until psi1 psi2 => ∃ j, j ≥ i ∧
38+
(eval_aux psi2 t j) ∧
39+
(∀ k, i ≤ k → k < j → eval_aux psi1 t k)
40+
41+
def eval (phi : Formula n) (t : Trace n) : Prop :=
42+
eval_aux phi t ⟨0, t.pos_length⟩
43+
44+
45+
-- theorem or_eval (phi psi: Formula n) (t: Trace n):
46+
-- (phi.Or psi).eval t ↔ phi.eval t ∨ psi.eval t := by
47+
-- constructor
48+
-- . intro h
49+
-- simp [eval, eval_aux] at h
50+
-- by_cases htl: 0 < t.length
51+
-- . simp [htl] at h
52+
-- unfold eval
53+
-- simp [htl]
54+
-- exact h
55+
-- . simp [htl] at h
56+
-- assumption
57+
-- . intro h
58+
-- rw [eval]
59+
-- by_cases htl: 0 < t.length
60+
-- all_goals simp [htl]
61+
-- . unfold eval at h
62+
-- simp [htl] at h
63+
-- rw [eval_aux]
64+
-- assumption
65+
-- . exact h
66+
67+
68+
-- theorem and_eval (phi psi: Formula n) (t: Trace n):
69+
-- (phi.And psi).eval t ↔ phi.eval t ∧ psi.eval t := by
70+
-- constructor
71+
-- . intro h
72+
-- simp [eval, eval_aux] at h
73+
-- by_cases htl: 0 < t.length
74+
-- . simp [htl] at h
75+
-- unfold eval
76+
-- simp [htl]
77+
-- exact h
78+
-- . simp [htl] at h
79+
-- assumption
80+
-- . intro h
81+
-- rw [eval]
82+
-- by_cases htl: 0 < t.length
83+
-- all_goals simp [htl]
84+
-- . unfold eval at h
85+
-- simp [htl] at h
86+
-- rw [eval_aux]
87+
-- assumption
88+
-- . exact h
89+
90+
91+
end Formula

‎BoltLean/Ltl.lean‎

Lines changed: 68 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,6 @@
11
import BoltLean.Helpers
22

3-
structure Trace (n_pred: Nat) where
4-
length: Nat
5-
pos_length : length > 0
6-
pos_n_pred: n_pred > 0
7-
predicates : Vector (Vector Bool length) n_pred
8-
deriving Repr
3+
abbrev Trace (n_pred: Nat): Type := List (Vector Bool n_pred)
94

105
/-- LTL Formulas in NNF -/
116
inductive Formula n_pred
@@ -23,23 +18,73 @@ deriving DecidableEq
2318

2419
namespace Formula
2520

26-
def eval_aux (phi: Formula n) (t: Trace n) (i: Fin t.length): Prop :=
27-
match phi with
28-
| True => _root_.True
29-
| False => _root_.False
30-
| Var v neg => xor t.predicates[v][i] neg
31-
| Next psi => if h: i < t.length - 1 then eval_aux psi t ⟨i.val + 1, by omega⟩ else _root_.False
32-
| WeakNext psi => (h: i < t.length - 1) → eval_aux psi t ⟨i.val + 1, by omega⟩
33-
| Globally psi => ∀ j, j ≥ i → eval_aux psi t j
34-
| Finally psi => ∃ j, j ≥ i ∧ eval_aux psi t j
35-
| Or psi1 psi2 => (eval_aux psi1 t i) ∨ (eval_aux psi2 t i)
36-
| And psi1 psi2 => (eval_aux psi1 t i) ∧ (eval_aux psi2 t i)
37-
| Until psi1 psi2 => ∃ j, j ≥ i ∧
38-
(eval_aux psi2 t j) ∧
39-
(∀ k, i ≤ k → k < j → eval_aux psi1 t k)
40-
41-
def eval (phi : Formula n) (t : Trace n) : Prop :=
42-
eval_aux phi t ⟨0, t.pos_length⟩
21+
def eval (phi: Formula n) (t: Trace n): Prop :=
22+
match t with
23+
| .nil => match phi with
24+
| True | WeakNext _ | Globally _ => _root_.True
25+
| False | Finally _ | Var _ _ | Next _ | Until _ _ => _root_.False
26+
| Or psi1 psi2 => (eval psi1 t) ∨ (eval psi2 t)
27+
| And psi1 psi2 => (eval psi1 t) ∧ (eval psi2 t)
28+
| head::tail => match phi with
29+
| True => _root_.True
30+
| False => _root_.False
31+
| Var v neg => xor head[v] neg
32+
| Next psi => eval psi tail
33+
| WeakNext psi => tail = List.nil ∨ eval psi tail
34+
| Globally psi => ∀ j, j < t.length → eval psi (t.drop j)
35+
| Finally psi => ∃ j, j < t.length ∧ eval psi (t.drop j)
36+
| Or psi1 psi2 => (eval psi1 t) ∨ (eval psi2 t)
37+
| And psi1 psi2 => (eval psi1 t) ∧ (eval psi2 t)
38+
| Until psi1 psi2 => ∃ j, j < t.length ∧
39+
(eval psi2 (t.drop j)) ∧
40+
(∀ k, k < j → eval psi1 (t.drop k))
41+
42+
def equivalence (phi psi : Formula n) : Prop := ∀ (t : Trace n), eval phi t ↔ eval psi t
43+
44+
theorem congruence_finally (phi1 phi2 : Formula n) :
45+
(equivalence phi1 phi2) → equivalence (Finally phi1) (Finally phi2) := by
46+
intro h1 h2
47+
unfold eval
48+
simp
49+
match h2 with
50+
| List.nil => simp
51+
| head::tail => simp
52+
constructor
53+
<;> intro h
54+
<;> have ⟨j, hj⟩ := h
55+
<;> exists j
56+
<;> first | rw [h1] | rw [←h1]
57+
<;> exact hj
58+
exact hj
59+
60+
61+
theorem congruence_globally (phi1 phi2 : Formula n) :
62+
(equivalence phi1 phi2) → equivalence (Globally phi1) (Globally phi2) := by
63+
intro h1 h2
64+
unfold eval
65+
simp
66+
match h2 with
67+
| List.nil => simp
68+
| head::tail => simp
69+
constructor
70+
<;> (
71+
intro h j
72+
first | rw [h1] | rw [←h1]
73+
apply h
74+
)
75+
76+
77+
78+
79+
theorem congruence (phi1 psi1 phi2 psi2 : Formula n) :
80+
(equivalence phi1 phi2) → (equivalence psi1 psi2) → equivalence (Until phi1 psi1) (Until phi2 psi2) := by
81+
unfold equivalence
82+
intro h1 h2
83+
sorry
84+
85+
86+
87+
theorem simplification_rule (phi : Formula n) : equivalence (Finally (Finally phi)) (Finally phi) := by sorry
4388

4489

4590
-- theorem or_eval (phi psi: Formula n) (t: Trace n):

0 commit comments

Comments
 (0)