From 1e50eac61fbd02211edd5f2e8cc72879b8de6f34 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Sun, 8 Oct 2023 19:46:50 +0200
Subject: [PATCH] work on Lemma 5 *-case

---
 Pdl/Discon.lean  | 21 +++++++++++++++++++++
 Pdl/Tableau.lean | 45 +++++++++++++++++++++++++++++++++++++++------
 2 files changed, 60 insertions(+), 6 deletions(-)

diff --git a/Pdl/Discon.lean b/Pdl/Discon.lean
index 4e91b0c..c16e547 100644
--- a/Pdl/Discon.lean
+++ b/Pdl/Discon.lean
@@ -165,3 +165,24 @@ theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS :=
     cases' f_in with f_in_X f_in_Y -- TODO: nicer match syntax?
     · apply satX f f_in_X
     · apply satY f f_in_Y
+
+theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} :
+  X ∈ XS → Y ∈ YS → ((X ∪ Y) ∈ (XS ⊎ YS)) :=
+  by
+  intro X_in Y_in
+  simp
+  ext1 -- this seems to go wrong?
+  constructor
+  · intro f_in
+    simp at f_in
+    simp
+    use X
+    constructor
+    · exact X_in
+    · use Y
+  · intro f_in
+    simp
+    simp at f_in
+    rcases f_in with ⟨X', X'_in, Y', Y'_in, f_in⟩
+    -- But now X' Y' are unrelated to X and Y :-(
+    sorry
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index b1a3761..e82fb7a 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -46,18 +46,51 @@ inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   -- TODO which rules need and modify markings?
   -- TODO only apply * if there is a marking.
 
-
--- TODO: rephrase this like Lemma 5 of MB with both directions / invertible?
+-- Like Lemma 5 of MB
 lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
   localRule X B → ((∃ Y ∈ B, (M,w) ⊨ Y) ↔ (M,w) ⊨ X) :=
   by
   intro locR
   cases locR
   case nSt a f aSf_in_X =>
-    have := likeLemmaFour M (∗ a)
-    simp at *
-    -- TODO
-    sorry
+    have lemFour := likeLemmaFour M (∗ a)
+    constructor
+    · intro lhs
+      sorry
+    · intro Mw_X
+      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⟩
+      -- 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
+      · 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
+          · 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 }