add placeholder for Lemma 4¾

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 }
 
 

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