From 6e730be5a31a46515583c2569dacbb11e5f602f1 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Mon, 13 Nov 2023 21:28:57 +0000
Subject: [PATCH] wip

---
 Pdl/Tableau.lean |  1 +
 Pdl/Unravel.lean | 81 ++++++++++++++++++++++++++++++++++++++++++------
 2 files changed, 72 insertions(+), 10 deletions(-)

diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index c1af972..72a7b3f 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -223,6 +223,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
             exact List.mem_of_mem_head? rfl
         case inr FS_in_unrav =>
           simp [unravel] at FS_in_unrav
+          -- TODO: use another one of the four lemmas similar to Lemma 4 here?
           sorry
       case inr g_neq_nsSf =>
         apply MwY
diff --git a/Pdl/Unravel.lean b/Pdl/Unravel.lean
index a7b3832..b4c3187 100644
--- a/Pdl/Unravel.lean
+++ b/Pdl/Unravel.lean
@@ -151,11 +151,12 @@ termination_by
 -- - boxStarInvert
 theorem likeLemmaFour :
   ∀ M (a : Program) (w v : W) (X' : List Formula) (P : DagFormula),
-    w ≠ v →
+    w ≠ v → -- TODO: Borzechowski does not assume this, for good reasons?
       (M, w) ⊨ (X' ++ [~⌈a⌉(undag P)]) → relate M a w v → (M, v)⊨(~undag P) →
         ∃ Y ∈ {X'} ⊎ unravel (~⌈a⌉P), (M, w)⊨Y
-          ∧ ∃ (a : Char) (as : List Program), (~ ⌈·a⌉ (Formula.boxes as (undag P))) ∈ Y
-            ∧ relate M (Program.steps ([Program.atom_prog a] ++ as)) w v :=
+          -- TODO: Bozechowski allows n=0 here, i.e. not even having an atomic A.
+          ∧ ∃ (A : Char) (as : List Program), (~ ⌈·A⌉ (Formula.boxes as (undag P))) ∈ Y
+            ∧ relate M (Program.steps ([Program.atom_prog A] ++ as)) w v :=
   by
   intro M a
   -- no 'induction', but using recursive calls instead
@@ -225,8 +226,8 @@ theorem likeLemmaFour :
               exact ⟨w'_as_u,u_c_v⟩
     case inl w_is_u =>
       subst w_is_u -- now u is gone, just say w
-      have IHb := likeLemmaFour M c w v X' (P) w_neq_v
-      specialize IHb _ u_c_v _
+      have IHc := likeLemmaFour M c w v X' (P) w_neq_v
+      specialize IHc _ u_c_v _
       · intro f lhs
         simp at lhs
         cases' lhs with f_in_X f_def
@@ -238,9 +239,10 @@ theorem likeLemmaFour :
           use v
       · simp [vDash.SemImplies, modelCanSemImplyForm]
         exact v_sat_nP
-      rcases IHb with ⟨Y, Y_in, w_conY, a, as, nBascP_in_Y, w_as_u⟩
+      rcases IHc with ⟨Y, Y_in, w_conY, a, as, nBascP_in_Y, w_as_u⟩
       simp at Y_in
       rcases Y_in with ⟨L,⟨L_in_unrav,Ydef⟩⟩
+      let whatIwant := unravel (~⌈b⌉⌈c⌉P) -- but we have no idea if b goes away or not here !!
       use L
       constructor
       · sorry -- mismatch:  unravel (~⌈c⌉P) ≠ unravel (~⌈b⌉⌈c⌉P)  ???
@@ -322,15 +324,13 @@ theorem likeLemmaFour :
         · use a, as
   case star a =>
     intro w v X' P w_neq_v w_sat_X w_aS_v v_sat_nP
-    unfold vDash.SemImplies at v_sat_nP -- mwah
-    unfold modelCanSemImplyForm at v_sat_nP
-    simp at v_sat_nP
+    simp [vDash.SemImplies, modelCanSemImplyForm] at v_sat_nP
     unfold relate at w_aS_v
     have := starCases w_aS_v
     cases this
     case inl w_is_v =>
       absurd w_neq_v
-      assumption
+      exact w_is_v
     case inr hyp =>
       rcases hyp with ⟨w_neq_v, ⟨y, w_neq_y, w_a_y, y_aS_v⟩⟩
       -- w -a-> y -a*-> v
@@ -398,6 +398,7 @@ theorem likeLemmaFour :
               · simp
                 exact y_aS_v
   case test f =>
+    -- TODO: this will no longer be trivial!
     intro w v X' P w_neq_v w_sat_X w_tf_v v_sat_nP
     unfold relate at w_tf_v
     rcases w_tf_v with ⟨w_is_v, w_f⟩
@@ -405,6 +406,64 @@ theorem likeLemmaFour :
     absurd w_neq_v
     rfl
 
+-- rename to not be about star only?
+theorem diamondStarInvert : ∀ M a (w : W) (X' : List Formula) (FS : List Formula) (P : DagFormula) Y,
+    Y ∈ {X'} ⊎ unravel (~⌈a⌉P) →
+      ((M, w) ⊨ (Y ++ {~⌈a⌉(undag P)})) →
+        ∃ x, relate M a w x ∧ ¬evaluate M x (undag P) := by
+
+  intro M a w X' FS P Y Y_in MwY
+
+  cases a
+
+  case atom_prog A =>
+    specialize MwY (~⌈·A⌉(undag P)) (by simp; right; exact List.mem_of_mem_head? rfl)
+    simp at MwY
+    rcases MwY with ⟨v, w_A_v, v_P⟩
+    use v
+    constructor
+    · simp; exact w_A_v
+    · exact v_P
+
+  case star a =>
+    simp at *
+    cases em (containsDag P)
+    case inl noDag =>
+      rw [noDag] at Y_in
+      simp at Y_in
+      sorry
+    case inr withDag =>
+      rw [Bool.not_eq_true] at withDag
+      rw [withDag] at Y_in
+      simp at Y_in
+      rcases Y_in with ⟨fs, (fs_nP | fs_in_unrav), def_Y⟩
+      case inl =>
+        use w
+        constructor
+        · exact Relation.ReflTransGen.refl
+        · specialize MwY (~⌈∗a⌉(undag P))
+          simp  at MwY
+          sorry
+      case inr =>
+        have := diamondStarInvert M a w X' FS (⌈a†⌉P) Y
+        simp at this
+        specialize this fs fs_in_unrav def_Y _
+        · sorry -- STUCK - reflexive case of the star gets in the way here. Should we rephrase the lemma to distinguish v≠w vs v=w? What v?
+        rcases this with ⟨x, w_a_x, y, x_aS_y, y_nP⟩
+        use y
+        constructor
+        · exact Relation.ReflTransGen.head w_a_x x_aS_y
+        · assumption
+
+  case sequence a b =>
+    sorry
+
+  case union a b =>
+    sorry
+
+  case test f =>
+    sorry
+
 -- Analogous to Lemma 4 we need one for the box case.
 -- This is used in the proof that the (∗) rule is sound.
 -- TODO statement is probably still a messy mixture of box and diamond case.
@@ -417,3 +476,5 @@ theorem lemmaFourAndThreeQuarters :
             ∧ relate M (Program.steps ([Program.atom_prog a] ++ as)) w v :=
   by
   sorry
+
+-- TODO: fourth lemma for box invertability?