Replace boolean evaluation with Prop instead

Author: GBathie

BoltLean/Ltl.lean

@@ -18,37 +18,27 @@ inductive Formula n_pred
 
 namespace Formula
 
-  def fin_range (s e: Fin n) : List (Fin n) :=
-    if h : s < e then
-      s :: fin_range ⟨s.val + 1, by omega⟩ e
-    else
-      List.nil
-    termination_by n - s
-
-  def eval_aux (t: Trace) (phi: Formula t.n_pred) (i: Fin t.length): Bool :=
+  def eval_aux (t: Trace) (phi: Formula t.n_pred) (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
+        False
     | WeakNext psi => if h: i < t.length - 1 then
         eval_aux t psi ⟨i.val + 1, by omega⟩
       else
-        true
-    | Globally psi => (List.finRange t.length).all (fun j => j < i  || eval_aux t psi j)
-    | Finally psi => (List.finRange t.length).any (fun 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)
-    | Until psi1 psi2 => (List.finRange t.length).any (
-        fun j =>
-          j >= i
-          && ((List.finRange t.length).all (fun k => k < i || k >= j || eval_aux t psi1 k))
-          && (eval_aux t psi2 j)
-       )
-
-  -- def eval (t: Trace) (phi: Formula t.n_pred): Bool :=
-  --   eval_aux t phi ⟨0, by rfl⟩
+        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)
+    | Until psi1 psi2 => ∃ j, j ≥ i ∧
+                              (eval_aux t psi2 j) ∧
+                              (∀ k, i ≤ k → k < j → eval_aux t psi1 k)
+
+  -- def eval (t: Trace) (phi: Formula t.n_pred) (h: t.length > 0): Bool :=
+  --   eval_aux t phi ⟨0, h⟩
 
 
 end Formula