From 0c9abfa845a1939f940b915d45d21518bc202595 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Mon, 16 Oct 2023 17:40:41 +0200
Subject: [PATCH] =?UTF-8?q?use=20w=20=E2=89=A0=20v=20in=20likeLemmaFour?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Pdl/Tableau.lean | 88 ++++++++++++++++++++++++++++++------------------
 Pdl/Unravel.lean | 38 +++++++++++----------
 2 files changed, 76 insertions(+), 50 deletions(-)

diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index d6172ad..8649a20 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -61,39 +61,63 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       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_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_v v_nF
-      · rw [conEval]
-        intro g g_in
-        simp at g_in
-        apply Mw_X
-        cases g_in
-        case inl => assumption
-        case inr h =>
-          convert aSf_in_X
-          cases h
+      -- NOTE: Borze also makes a distinction whether a is atomic. Not needed?
+      -- We still distinguish cases whether v = w
+      have : w = v ∨ w ≠ v := by tauto
+      cases this
+      case inl w_is_v =>
+        -- Same world, we can use the left branch.
+        subst w_is_v
+        use (X \ {~⌈∗a⌉f} ∪ {~f})
+        constructor
+        · apply union_elem_uplus
+          simp
+          unfold unravel
+          simp
+          use {~f}
+          constructor
+          · left
+            exact List.mem_of_mem_head? rfl
           · rfl
-          · exfalso
-            tauto
-      rcases lemFour with ⟨Z, Z_in, Mw_ZX, ⟨as, nBasf_in, w_as_v⟩⟩
-      use (X \ {~⌈∗a⌉f}) ∪ Z.toFinset -- hmmm, good guess?
-      constructor
-      · apply union_elem_uplus
-        · simp
-        · simp
-          use Z
-      · rw [conEval] at Mw_ZX
-        intro g g_in
-        apply Mw_ZX
-        simp
-        simp at g_in
-        tauto
+        · intro g g_in
+          simp at g_in
+          cases g_in
+          · tauto
+          case h.right.inr hyp =>
+            subst hyp
+            unfold evaluate
+            assumption
+      case inr w_neq_v =>
+        -- Different world, we use the right branch and Lemma 4 here:
+        specialize lemFour w v X.toList (X.toList ++ {~⌈∗a⌉f}) f w_neq_v rfl
+        unfold vDash.SemImplies modelCanSemImplyForm at lemFour -- mwah, why simp not do this?
+        simp at lemFour
+        specialize lemFour _ w_aS_v v_nF
+        · rw [conEval]
+          intro g g_in
+          simp at g_in
+          apply Mw_X
+          cases g_in
+          case a.inl => assumption
+          case a.inr h =>
+            convert aSf_in_X
+            cases h
+            · rfl
+            · exfalso
+              tauto
+        rcases lemFour with ⟨Z, Z_in, Mw_ZX, ⟨as, nBasf_in, w_as_v⟩⟩
+        use (X \ {~⌈∗a⌉f}) ∪ Z.toFinset -- hmmm, good guess?
+        constructor
+        · apply union_elem_uplus
+          · simp
+          · simp
+            use Z
+        · rw [conEval] at Mw_ZX
+          intro g g_in
+          apply Mw_ZX
+          simp
+          simp at g_in
+          tauto
   -- TODO
   all_goals { sorry }
 
diff --git a/Pdl/Unravel.lean b/Pdl/Unravel.lean
index 66ec767..4aa3ccb 100644
--- a/Pdl/Unravel.lean
+++ b/Pdl/Unravel.lean
@@ -93,7 +93,8 @@ theorem likeLemmaFourWithoutX :
   sorry
 
 theorem likeLemmaFour :
-    ∀ M (a : Program) (w v : W) (X' X : List Formula) (P : Formula),
+  ∀ M (a : Program) (w v : W) (X' X : List Formula) (P : Formula),
+    w ≠ v →
       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
@@ -104,7 +105,7 @@ theorem likeLemmaFour :
   -- no 'induction', but using recursive calls instead
   cases a
   case atom_prog A =>
-    intro w v X' X P X_def w_sat_X w_a_v v_sat_nP
+    intro w v X' X P w_neq_v X_def w_sat_X w_a_v v_sat_nP
     use X -- "The claim holds with Y = X" says MB.
     unfold unravel
     simp
@@ -121,12 +122,13 @@ theorem likeLemmaFour :
         exact List.mem_of_mem_head? rfl
       · exact w_a_v
   case sequence b c =>
-    intro w v X' X P X_def w_sat_X w_bc_v v_sat_nP
+    intro w v X' X P w_neq_v X_def w_sat_X w_bc_v v_sat_nP
     unfold relate at w_bc_v
     rcases w_bc_v with ⟨u, w_b_u, u_c_v⟩
     subst X_def
     have IHb := likeLemmaFour M b w u X' -- get IH using a recursive call
-    specialize IHb (X' ++ {~⌈b⌉ (⌈c⌉ P)}) (⌈c⌉ P) (by rfl) _ w_b_u _
+    specialize IHb (X' ++ {~⌈b⌉ (⌈c⌉ P)}) (⌈c⌉ P) _ (by rfl) _ w_b_u _
+    · sorry -- need w ≠ u here?
     · convert_to (evaluate M w (Con (X' ++ {~⌈b⌉⌈c⌉P})))
       rw [conEval]
       unfold vDash.SemImplies at w_sat_X
@@ -180,13 +182,14 @@ theorem likeLemmaFour :
           · rw [rel_steps_last]
             use u
   case union a b =>
-    intro w v X' X P X_def w_sat_X w_aub_v v_sat_nP
+    intro w v X' X P w_neq_v X_def w_sat_X w_aub_v v_sat_nP
     unfold relate at w_aub_v
     subst X_def
     cases w_aub_v
     case inl w_a_v =>
-      have IH := likeLemmaFour M a w v X' (X' ++ {~⌈a⌉ P}) (P) (by rfl)
-      specialize IH _ w_a_v _
+      have IH := likeLemmaFour M a w v X' (X' ++ {~⌈a⌉ P})
+      specialize IH  (P) _ (by rfl) _ w_a_v _
+      · sorry
       · unfold vDash.SemImplies at *
         unfold modelCanSemImplyForm at *
         simp at *
@@ -218,8 +221,9 @@ theorem likeLemmaFour :
         · exact w_conY
         · use as
     case inr w_b_v =>
-      have IH := likeLemmaFour M b w v X' (X' ++ {~⌈b⌉ P}) (P) (by rfl)
-      specialize IH _ w_b_v _
+      have IH := likeLemmaFour M b w v X' (X' ++ {~⌈b⌉ P}) (P)
+      specialize IH _  (by rfl) _ w_b_v _
+      · sorry
       · unfold vDash.SemImplies at *
         unfold modelCanSemImplyForm at *
         simp at *
@@ -251,9 +255,10 @@ theorem likeLemmaFour :
         · exact w_conY
         · use as
   case star a =>
-    intro w v X' X P X_def w_sat_X w_aS_v v_sat_nP
+    intro w v X' X P w_neq_v X_def w_sat_X w_aS_v v_sat_nP
     unfold relate at w_aS_v
     subst X_def
+    -- TODO get rid of the below, we now have w_neq_v
     have : v = w ∨ v ≠ w := by tauto
     cases this
     case inl v_is_w => -- MB: "If S = T, then ..."
@@ -290,7 +295,8 @@ theorem likeLemmaFour :
         rfl
       case step u w_a_u u_aS_v =>
         have IHa := likeLemmaFour M a w u X'
-        specialize IHa (X' ++ {~⌈a⌉⌈∗a⌉P}) (⌈∗a⌉P) (by rfl) _ w_a_u _
+        specialize IHa (X' ++ {~⌈a⌉⌈∗a⌉P}) (⌈∗a⌉P) _ (by rfl) _ w_a_u _
+        · sorry
         · sorry
         · sorry
         rcases IHa with ⟨Y, Y_in, w_conY, as, nBasaSP_in_Y, w_as_u⟩
@@ -313,13 +319,9 @@ theorem likeLemmaFour :
               · simp
                 assumption
   case test f =>
-    intro w v X' X P X_def w_sat_X w_tf_v v_sat_nP
+    intro w v X' X P w_neq_v X_def w_sat_X w_tf_v v_sat_nP
     unfold relate at w_tf_v
-    subst X_def
     rcases w_tf_v with ⟨w_is_v, w_f⟩
     subst w_is_v
-    -- Here MB uses ~(theF(P)) and things seem fishy ...
-    use X' ++ {f, ~P}
-    simp [unravel]
-    -- TODO next!
-    sorry
+    absurd w_neq_v
+    rfl