WIP on domination

Author: GBathie

BoltLean/Domination.lean

@@ -0,0 +1,24 @@
+import BoltLean.Ltl
+
+namespace Formula
+def dominates (phi psi: Formula n): Prop :=
+  ∀ (t: Trace n), psi.eval t → phi.eval t
+
+
+theorem or_dominates (phi psi: Formula n) (f: Formula n):
+  phi.dominates psi → (f.Or phi).dominates (f.Or psi) := by
+    rw [dominates, dominates]
+    apply forall_imp
+    intro t h1 h2
+    simp [eval, eval_aux] at h2
+    simp [eval, eval_aux]
+    match h2 with
+    | ⟨hi, h_or⟩ => exists hi
+                    match h_or with
+                    | .inl hf => apply Or.inl; assumption
+                    | .inr h_psi => apply Or.inr
+                                    simp [eval, hi] at h1;
+                                    apply h1; assumption
+
+
+end Formula

BoltLean/Ltl.lean

@@ -1,10 +1,8 @@
-structure Trace where
-  n_pred: Nat
+structure Trace (n_pred: Nat) where
   length: Nat
   predicates : Vector (Vector Bool length) n_pred
 deriving Repr
 
-
 /-- LTL Formulas in NNF -/
 inductive Formula n_pred
   | Var : Fin n_pred -> (neg: Bool) -> Formula n_pred -- neg: Whether the variable is negated
@@ -15,30 +13,80 @@ inductive Formula n_pred
   | Or : Formula n_pred -> Formula n_pred -> Formula n_pred
   | And : Formula n_pred -> Formula n_pred -> Formula n_pred
   | Until : Formula n_pred -> Formula n_pred -> Formula n_pred
+deriving DecidableEq
 
 namespace Formula
 
-  def eval_aux (t: Trace) (phi: Formula t.n_pred) (i: Fin t.length): Prop :=
+  def eval_aux (phi: Formula n) (t: Trace n) (i: Fin t.length): Prop :=
     match phi with
     | Var v neg => xor t.predicates[v][i] neg
-    | Next psi => if h: i < t.length - 1 then
-        eval_aux t psi ⟨i.val + 1, by omega⟩
-      else
-        False
-    | WeakNext psi => if h: i < t.length - 1 then
-        eval_aux t psi ⟨i.val + 1, by omega⟩
-      else
-        True
-    | Globally psi => ∀ j, j ≥ i  → eval_aux t psi j
-    | Finally psi => ∃ j, j ≥ i ∧ eval_aux t psi j
-    | Or psi1 psi2 => (eval_aux t psi1 i) ∨ (eval_aux t psi2 i)
-    | And psi1 psi2 => (eval_aux t psi1 i) ∧ (eval_aux t psi2 i)
+    | Next psi => if h: i < t.length - 1 then eval_aux psi t ⟨i.val + 1, by omega⟩ else False
+    | WeakNext psi => (h: i < t.length - 1) → eval_aux psi t ⟨i.val + 1, by omega⟩
+    | Globally psi => ∀ j, j ≥ i  → eval_aux psi t j
+    | Finally psi => ∃ j, j ≥ i ∧ eval_aux psi t j
+    | Or psi1 psi2 => (eval_aux psi1 t i) ∨ (eval_aux psi2 t i)
+    | And psi1 psi2 => (eval_aux psi1 t i) ∧ (eval_aux psi2 t i)
     | Until psi1 psi2 => ∃ j, j ≥ i ∧
-                              (eval_aux t psi2 j) ∧
-                              (∀ k, i ≤ k → k < j → eval_aux t psi1 k)
+                              (eval_aux psi2 t j) ∧
+                              (∀ k, i ≤ k → k < j → eval_aux psi1 t k)
+
+  def eval (phi : Formula n) (t : Trace n) : Prop :=
+    if h : t.length > 0 then
+      eval_aux phi t ⟨0, h⟩
+    else
+      match phi with
+      -- I guess technically, WeakNext and Globally
+      -- are both true on empty traces, and are the only ones.
+      | WeakNext _ | Globally _ => True
+      | Or psi1 psi2 => eval psi1 t ∨ eval psi2 t
+      | And psi1 psi2 => eval psi1 t ∧ eval psi2 t
+      | _ => False
+
+
+  theorem or_eval (phi psi: Formula n) (t: Trace n):
+    (phi.Or psi).eval t ↔ phi.eval t ∨ psi.eval t  := by
+      constructor
+      . intro h
+        simp [eval, eval_aux] at h
+        by_cases htl: 0 < t.length
+        . simp [htl] at h
+          unfold eval
+          simp [htl]
+          exact h
+        . simp [htl] at h
+          assumption
+      . intro h
+        rw [eval]
+        by_cases htl: 0 < t.length
+        all_goals simp [htl]
+        . unfold eval at h
+          simp [htl] at h
+          rw [eval_aux]
+          assumption
+        . exact h
+
 
-  -- def eval (t: Trace) (phi: Formula t.n_pred) (h: t.length > 0): Bool :=
-  --   eval_aux t phi ⟨0, h⟩
+  theorem and_eval (phi psi: Formula n) (t: Trace n):
+    (phi.And psi).eval t ↔ phi.eval t ∧ psi.eval t  := by
+      constructor
+      . intro h
+        simp [eval, eval_aux] at h
+        by_cases htl: 0 < t.length
+        . simp [htl] at h
+          unfold eval
+          simp [htl]
+          exact h
+        . simp [htl] at h
+          assumption
+      . intro h
+        rw [eval]
+        by_cases htl: 0 < t.length
+        all_goals simp [htl]
+        . unfold eval at h
+          simp [htl] at h
+          rw [eval_aux]
+          assumption
+        . exact h
 
 
 end Formula