From e130400f267f8e2bd95157c7a2f49f1bea8c75a1 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Tue, 24 Oct 2023 14:42:44 +0200
Subject: [PATCH] =?UTF-8?q?add=20placeholder=20for=20Lemma=204=C2=BE?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Pdl/Tableau.lean |  5 ++++-
 Pdl/Unravel.lean | 20 +++++++++++++++-----
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index 3330df1..022b7a9 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -110,7 +110,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
           case a.inr h =>
             convert aSf_in_X
         rcases lemFour with ⟨Z, Z_in, Mw_ZX, ⟨as, nBasf_in, w_as_v⟩⟩
-        use (X \ {~⌈∗a⌉f}) ∪ Z.toFinset -- hmmm, good guess?
+        use (X \ {~⌈∗a⌉f}) ∪ Z.toFinset
         constructor
         · apply union_elem_uplus
           · simp
@@ -121,6 +121,9 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
           simp at g_in
           tauto
   -- TODO
+  case sta =>
+    have := lemmaFourAndThreeQuarters M -- use here
+    sorry
   all_goals { sorry }
 
 
diff --git a/Pdl/Unravel.lean b/Pdl/Unravel.lean
index 48f5897..01579ad 100644
--- a/Pdl/Unravel.lean
+++ b/Pdl/Unravel.lean
@@ -142,16 +142,13 @@ termination_by
   unravel f => mOfDagFormula f
 
 -- Like Lemma 4 from Borzechowski, but using "unravel" instead of a local tableau with n-nodes.
--- 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?
+-- This is used in the proof that the (¬∗) rule is sound.
+-- See https://is.gd/borzepdl#lemma.4 for the original.
 -- TODO: rename to:
 -- - diamondStarSound <<<
 -- - diamondStarInvert
 -- - boxStarSound
 -- - boxStarInvert
--- and more?
-
 theorem likeLemmaFour :
   ∀ M (a : Program) (w v : W) (X' : List Formula) (P : DagFormula),
     w ≠ v →
@@ -375,3 +372,16 @@ theorem likeLemmaFour :
     subst w_is_v
     absurd w_neq_v
     rfl
+
+-- 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.
+theorem lemmaFourAndThreeQuarters :
+  ∀ M (a : Program) (w v : W) (X' : List Formula) (P : DagFormula),
+    w ≠ v → -- change this?
+      (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 :=
+  by
+  sorry