From 27632fe05c93b0400af8e80d339f204bfe8a5578 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Mon, 9 Oct 2023 15:26:37 +0200
Subject: [PATCH] meeting notes and TODOs

---
 Pdl/Discon.lean  |  4 ++++
 Pdl/Tableau.lean | 11 +++++++----
 Pdl/Unravel.lean | 40 ++++++++++++++++++++++++++++++----------
 3 files changed, 41 insertions(+), 14 deletions(-)

diff --git a/Pdl/Discon.lean b/Pdl/Discon.lean
index c16e547..413e9d3 100644
--- a/Pdl/Discon.lean
+++ b/Pdl/Discon.lean
@@ -166,6 +166,10 @@ theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS :=
     · apply satX f f_in_X
     · apply satY f f_in_Y
 
+theorem disconOr {XS YS} : discon (XS ∪ YS) ≡ discon XS ⋁ discon YS :=
+  by
+  sorry
+
 theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} :
   X ∈ XS → Y ∈ YS → ((X ∪ Y) ∈ (XS ⊎ YS)) :=
   by
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index e82fb7a..f01addc 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -55,17 +55,20 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
   case nSt a f aSf_in_X =>
     have lemFour := likeLemmaFour M (∗ a)
     constructor
-    · intro lhs
+    · intro lhs -- invertibility
       sorry
-    · intro Mw_X
+    · intro Mw_X -- soundness
       have w_adiamond_f := Mw_X (~⌈∗a⌉f) aSf_in_X
       simp at w_adiamond_f lemFour
-      rcases w_adiamond_f with ⟨v, w_aS_x, v_nF⟩
+      rcases w_adiamond_f with ⟨v, w_aS_v, v_nF⟩
+      -- TODO: update the below when Lemma 4 is updated to demand v ≠ w.
+      -- a atomic, then done?
+      -- a not atomic, disitnguish cases if v = w
       -- Now we use Lemma 4 here:
       specialize lemFour w v X.toList (X.toList ++ {~⌈∗a⌉f}) f rfl
       unfold vDash.SemImplies modelCanSemImplyForm at lemFour -- mwah, why simp not do this?
       simp at lemFour
-      specialize lemFour _ w_aS_x v_nF
+      specialize lemFour _ w_aS_v v_nF
       · rw [conEval]
         intro g g_in
         simp at g_in
diff --git a/Pdl/Unravel.lean b/Pdl/Unravel.lean
index 27f1e93..b6450ae 100644
--- a/Pdl/Unravel.lean
+++ b/Pdl/Unravel.lean
@@ -9,19 +9,19 @@ import Pdl.Semantics
 @[simp]
 def unravel : Formula → List (List Formula)
   -- diamonds:
-  | ~⌈·a⌉ P => [[~⌈·a⌉ P]]
-  | ~⌈Program.union p1 p2⌉ P => unravel (~⌈p1⌉ P) ∪ unravel (~⌈p2⌉ P) -- no theF here. fishy?
-  | ~⌈✓ Q⌉ P => [[Q]]⊎unravel (~P)
-  | ~⌈a;b⌉ P => unravel (~⌈a⌉ (⌈b⌉ P))
+  | ~⌈·a⌉P => [[~⌈·a⌉P]]
+  | ~⌈Program.union p1 p2⌉P => unravel (~⌈p1⌉P) ∪ unravel (~⌈p2⌉P) -- no theF here. fishy?
+  | ~⌈✓ Q⌉P => [[Q]] ⊎ unravel (~P)
+  | ~⌈a;b⌉P => unravel (~⌈a⌉(⌈b⌉P))
   | ~†_ => ∅
-  | ~⌈∗a⌉ P => unravel (~P) ∪ unravel (~⌈a⌉ (†⌈∗a⌉ P))
+  | ~⌈∗a⌉P => unravel (~P) ∪ unravel (~⌈a⌉(†⌈∗a⌉P))
   -- boxes:
   | ⌈·a⌉P => [[⌈·a⌉ P]]
-  | ⌈Program.union a b⌉ P => unravel (⌈a⌉ P)⊎unravel (⌈b⌉ P)
-  | ⌈✓ Q⌉ P => [[~Q]] ∪ unravel P
-  | ⌈a;b⌉ P => unravel (⌈a⌉ (⌈b⌉ P))
+  | ⌈Program.union a b⌉ P => unravel (⌈a⌉P) ⊎ unravel (⌈b⌉P)
+  | ⌈✓ Q⌉P => [[~Q]] ∪ unravel P
+  | ⌈a;b⌉P => unravel (⌈a⌉(⌈b⌉P))
   | †P => {∅}
-  | ⌈∗a⌉ P => unravel P⊎unravel (⌈a⌉ (†⌈∗a⌉ P))
+  | ⌈∗a⌉P => unravel P ⊎ unravel (⌈a⌉(†⌈∗a⌉P))
   -- all other formulas we do nothing, but let's pattern match them all.
   | ·c => [[·c]]
   | ~·c => [[~·c]]
@@ -75,11 +75,28 @@ theorem rel_steps_last {as} : ∀ v w,
 -- see https://malv.in/2020/borzechowski-pdl/Borzechowski1988-PDL-translation-Gattinger2020.pdf#lemma.4
 -- TODO: maybe simplify by not having a context X' here / still as useful for showing soundness of ~* rule?
 -- TODO: analogous lemma for the box case? and * rule?
+-- TODO: rename to:
+-- - diamondStarSound <<<
+-- - diamondStarInvert
+-- - boxStarSound
+-- - boxStarInvert
+-- and more?
+
+theorem likeLemmaFourWithoutX :
+    ∀ M (a : Program) (w v : W) (P : Formula),
+      -- (M, w) ⊨ (~⌈a⌉P) →
+        relate M a w v → (M, v)⊨(~P) →
+          ∃ Y ∈ unravel (~⌈a⌉P), (M, w)⊨Con Y
+          ∧ ∃ as : List Program, (~ Formula.boxes as P) ∈ Y
+            ∧ relate M (Program.steps as) w v :=
+  by
+  sorry
+
 theorem likeLemmaFour :
     ∀ M (a : Program) (w v : W) (X' X : List Formula) (P : Formula),
       X = X' ++ {~⌈a⌉ P} →
         (M, w)⊨Con X → relate M a w v → (M, v)⊨(~P) →
-          ∃ Y ∈ {X'}⊎unravel (~⌈a⌉ P), (M, w)⊨Con Y
+          ∃ Y ∈ {X'} ⊎ unravel (~⌈a⌉P), (M, w)⊨Con Y
           ∧ ∃ as : List Program, (~ Formula.boxes as P) ∈ Y
             ∧ relate M (Program.steps as) w v :=
   by
@@ -235,7 +252,10 @@ theorem likeLemmaFour :
         · use as
   case star =>
     intro w v X' X P X_def w_sat_X w_a_v v_sat_nP; subst X_def
+    -- TODO next next.
+
     sorry
   case test =>
     intro w v X' X P X_def w_sat_X w_a_v v_sat_nP; subst X_def
+    -- TODO next!
     sorry