imitating scratch Lemma 1: is ~[A]... unravel-unravel-transitive?

Pdl/Unravel.lean

@@ -120,7 +120,7 @@ def unravel : DagFormula → List (List Formula)
       -- omit {{~P}} if P contains dagger
       --if containsDag P then unravel (~⌈a⌉(⌈a†⌉P))
       --else
-      {{~(undag P)}} ∪ unravel (~⌈a⌉(⌈a†⌉P))
+      [[~(undag P)]] ∪ unravel (~⌈a⌉(⌈a†⌉P))
   -- boxes:
   | ⌈·a⌉P => [[⌈·a⌉ (undag P)]]
   | ⌈a ⋓ b⌉ P => unravel (⌈a⌉P) ⊎ unravel (⌈b⌉P)
@@ -131,7 +131,7 @@ def unravel : DagFormula → List (List Formula)
       -- omit {{P}} when P contains dagger
       --if containsDag P then unravel (⌈a⌉(⌈a†⌉P))
       -- else
-      { {undag P} } ⊎ unravel (⌈a⌉(⌈a†⌉P))
+      [[undag P]] ⊎ unravel (⌈a⌉(⌈a†⌉P))
   -- all other formulas we do nothing, but let's pattern match them all.
   | ·c => [[·c]]
   | ~·c => [[~·c]]
@@ -143,6 +143,38 @@ def unravel : DagFormula → List (List Formula)
 termination_by
   unravel f => mOfDagFormula f
 
+-- this monster would be useful
+theorem extracted_1 {W : Type} (M : KripkeModel W) (b c : Program) (v w : W) (X' : List Formula) (P : DagFormula)
+  (hasDag : containsDag P = true) (v_sat_X : ∀ (f : Formula), f ∈ X' ∨ f = (~⌈b;'c⌉undag P) → evaluate M v f)
+  (w_sat_nP : ¬evaluate M w (undag P)) (L : List Formula) (L_in_unrav : L ∈ unravel (~⌈b⌉⌈c⌉P))
+  (w_conY : (M, v)⊨X' ++ L) (nBPhi_in_X : (~undag (⌈c⌉P)) ∈ X' ++ L) (w_b_u : relate M b v v) (u_c_w : relate M c v w)
+  (A' : Char) (as' : List Program) (v_Aas_u' : relate M (Program.steps ((·A') :: as')) v w) (L' : List Formula)
+  (L_in_unrav' : L' ∈ unravel (~⌈c⌉P)) (w_conY' : (M, v)⊨X' ++ L') (in_L' : (~⌈·A'⌉Formula.boxes as' (undag P)) ∈ L') :
+  (~⌈·A'⌉Formula.boxes as' (undag P)) ∈ L := sorry
+
+/-
+theorem unravel_unravel {L : List Formula} {a : Program}:
+    L ∈ unravel P → (~(⌈a⌉Q : Formula)) ∈ L →
+      K ∈ unravel (~(⌈a⌉Q)) → f ∈ K →
+        R ∈ L
+    :=
+  by
+  intro L_in_uP Q_in_L K_in_uQ naR_inK
+  cases P
+  all_goals (try (simp at *; subst L_in_uP; simp at *; subst Q_in_L; simp at *; subst K_in_uQ); simp at *)
+  case neg f =>
+    sorry
+  case box a f =>
+    cases a
+    all_goals (simp at *)
+    all_goals sorry
+  case dag =>
+    simp at *
+    cases L_in_uP
+    cases Q_in_L
+    tauto
+-/
+
 theorem atNoDagHelper :
   containsDag P = false →
     (containsDag (if isAtomic b = true then inject (undag (⌈c⌉P)) else ⌈c⌉P) = false) :=
@@ -186,147 +218,138 @@ theorem dagHelper :
 -- - diamondStarInvert
 -- - boxStarSound
 -- - boxStarInvert
+
+-- PROBLEM: X' should be List DagFormula (for union case?)
 theorem likeLemmaFour :
-  ∀ M (a : Program) (w v : W) (X' : List Formula) (P : DagFormula),
-    -- add condition from MB here?
-    -- "P normal if a is atomic, otherwise??? P is n-formula"
-    (isAtomic a ↔ ¬ containsDag P) →
-    -- or with ↔ instead?
-    -- either way, showing that we can apply the IH then becomes impossible?!
-      (M, w) ⊨ (X' ++ [~⌈a⌉(undag P)]) → relate M a w v → (M, v)⊨(~undag P) →
-        ∃ Y ∈ {X'} ⊎ unravel (~⌈a⌉P), (M, w)⊨Y
-          ∧ ∃ (as : List Program), (~ (Formula.boxes as (undag P))) ∈ Y
-            ∧ relate M (Program.steps (as)) w v
-            -- what follows is a silly way to phrase Borzechowskis "If n > 0 ..."
-            -- TODO: rephrase with dite, but needs DecidableEq (List Program) or so?
-            ∧ (∀ h : as ≠ [], ∃ A, as.head h = (·A : Program))
-            ∧ (∀ h : as = [], w = v) :=
+  ∀ M (a : Program) (v w : W) (X' : List Formula) (P : DagFormula) (hasDag : containsDag P),
+    (M, v) ⊨ (X' ++ [~⌈a⌉(undag P)]) → relate M a v w → (M, w)⊨(~undag P) →
+      ∃ Y ∈ {X'} ⊎ unravel (~⌈a⌉P),
+          (M, v)⊨Y
+        ∧ ( (∃ (A : Char) (as : List Program),
+                 (~ (Formula.boxes ((·A)::as) (undag P))) ∈ Y
+               ∧ relate M (Program.steps ((·A)::as)) v w)
+            ∨ (((~undag P) ∈ Y) ∧ v=w)
+          ) :=
   by
   intro M a
   -- no 'induction', but using recursive calls instead
   cases a
   case atom_prog A =>
-    intro w v X' P atNoDag w_sat_X w_a_v v_sat_nP
+    intro v w X' P hasDag v_sat_X v_a_w w_sat_nP
     simp
     constructor
-    · assumption
-    · use [·A]
+    · exact v_sat_X
+    · left
+      use A, []
       simp [isAtomic,Formula.boxes] at *
-      exact w_a_v
+      exact v_a_w
   case sequence b c =>
-    intro w v X' P atNoDag 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⟩
+    intro v w X' P hasDag v_sat_X v_bc_w w_sat_nP
+    unfold relate at v_bc_w
+    rcases v_bc_w with ⟨u, w_b_u, u_c_w⟩
     simp [vDash.SemImplies, modelCanSemImplyForm] at *
-    have IHb := likeLemmaFour M b w u X' (if isAtomic b then inject (undag (⌈c⌉P)) else ⌈c⌉P)
+    have IHb := likeLemmaFour M b v u X' (⌈c⌉P)
     specialize IHb _ _ w_b_u _
-    · simp [isAtomic] at atNoDag
-      rw [dagHelper atNoDag b c]
-      simp
+    · simp
+      exact hasDag
     · intro f lhs
       simp at lhs
       cases' lhs with f_in_X f_def
-      · apply w_sat_X f
+      · apply v_sat_X f
         left
         exact f_in_X
       · subst f_def
         simp
         use u
         constructor
         · exact w_b_u
-        · use v
+        · use w
     · simp [vDash.SemImplies, modelCanSemImplyForm, dagSemIrrelevant]
-      use v
-    rcases IHb with ⟨Y, Y_in, w_conY, as, nBascP_in_Y, w_as_u, nonemp, emp⟩
-    rw [undagOfIte b (⌈c⌉P)] at nBascP_in_Y
-    simp at Y_in
-    rcases Y_in with ⟨L,⟨L_in_unrav,Ydef⟩⟩
-    have := unravelAtomicIrrelevant b (⌈c⌉P)
-    simp at this
-    rw [this] at L_in_unrav
-
-    cases em (as = [])
-    case inr as_not_emp => -- "If N > 0 then we are done"
-      specialize nonemp as_not_emp
-      use L
+      use w
+    rcases IHb with ⟨Y, Y_in, w_conY, ( ⟨A, as, nBascP_in_Y, v_Aas_u⟩ | ⟨nBPhi_in_X, v_is_u⟩ )⟩
+    all_goals (simp at Y_in; rcases Y_in with ⟨L,⟨L_in_unrav,Ydef⟩⟩; subst Ydef)
+    · use L
       constructor
       · exact L_in_unrav
       · constructor
         · intro f lhs
           apply w_conY
-          rw [← Ydef]
           simp
           exact lhs
-        · use (as ++ [c])
-          constructor
-          · rw [boxes_append]
-            rw [← Ydef] at nBascP_in_Y
-            simp at nBascP_in_Y
-            have := undagOfIte b (⌈c⌉P)
-            aesop
-          · constructor
-            · rw [relate_steps]
-              use u
+        · constructor
+          · use A, (as ++ [c])
+            constructor
+            · simp at nBascP_in_Y
+              rw [boxes_append]
+              exact nBascP_in_Y
+            · simp at v_Aas_u
+              rcases v_Aas_u with ⟨z, v_A_z, z_as_u⟩
+              use z
+              rw [relate_steps]
               simp
-              exact ⟨ w_as_u, u_c_v ⟩
-            · simp
-              intro h
-              rcases nonemp with ⟨A, A_claim⟩
-              use A
-              rw [← A_claim]
-              -- List.head (as ++ [c]) h = List.head as as_not_emp
-              cases as
-              case nil =>
-                simp at as_not_emp
-              case cons =>
-                simp
-    case inl as_is_emp => -- "otherwise we again apply the IH"
-      specialize emp as_is_emp
-      subst emp -- w = u
-      subst as_is_emp
-      simp at *
-      -- QUESTION: What should be the context here? Just L, or all of Y, or something else?
-      have IHc := likeLemmaFour M c w v (L) (if isAtomic c then inject (undag (P)) else P)
-      specialize IHc _ _ u_c_v _
-      · simp [isAtomic] at atNoDag
-        have := dagHelper atNoDag c
-        sorry
+              exact ⟨v_A_z, ⟨u, ⟨z_as_u, u_c_w⟩⟩⟩
+    · subst v_is_u
+      have IHc := likeLemmaFour M c v w X' P
+      specialize IHc _ _ u_c_w _
+      · exact hasDag
       · intro f lhs
         simp at lhs
-        rcases lhs with f_in_L | f_def
+        rcases lhs with f_in_X | f_def
         · apply w_conY f
-          rw [← Ydef]
           simp
-          right
-          exact f_in_L
+          left
+          exact f_in_X
         · subst f_def
           simp
-          use v
+          use w
       · simp [vDash.SemImplies, modelCanSemImplyForm, undagOfIte c P]
-        exact v_sat_nP
-      subst Ydef
-      rcases IHc with ⟨Y', Y_in', w_conY', as', nBascP_in_Y', w_as_v', nonemp', emp'⟩
-      simp at Y_in'
-      rcases Y_in' with ⟨L', ⟨L_in_unrav', Ydef'⟩⟩
-
-      subst Ydef'
-      simp at nBascP_in_Y'
-      rcases nBascP_in_Y' with in_L | in_L'
+        exact w_sat_nP
+      rcases IHc with ⟨Y', Y_in', w_conY', ( ⟨A', as', nBascP_in_Y', v_Aas_u'⟩ | ⟨nBPhi_in_X', v_is_w⟩ )⟩
+      all_goals (simp at Y_in'; rcases Y_in' with ⟨L', ⟨L_in_unrav', Ydef'⟩⟩; subst Ydef')
+
+      · simp at nBascP_in_Y';
+        rcases nBascP_in_Y' with in_X | in_L'
+        · use L
+          constructor
+          · exact L_in_unrav -- now matching
+          · constructor
+            · intro f lhs
+              apply w_conY
+              simp
+              exact lhs
+            · constructor
+              · use A', as'
+                constructor
+                · left
+                  exact in_X
+                · aesop
+        · use L
+          constructor
+          · exact L_in_unrav -- needs "use L"
+          · constructor
+            · intro f lhs
+              apply w_conY
+              simp
+              exact lhs
+            · constructor
+              · use A', as'
+                constructor
+                · right
+                  extract_goal
+                  sorry -- exact in_L' -- wants "use L'" above
+                · aesop
+
+
       · use L
         constructor
-        · exact L_in_unrav -- now matching
+        · assumption
         · constructor
           · intro f lhs
             apply w_conY
             simp
             exact lhs
-          · use as'
-            constructor
-            · right
-              exact in_L
-            · constructor
-              · exact w_as_v'
-              · tauto
+          · right
+            sorry -- aesop
       -- four combinations at least:
       -- (1) use L ... use as'
       /-
@@ -428,7 +451,7 @@ theorem likeLemmaFour :
 
 
   case union a b =>
-    intro w v X' P atNoDag w_sat_X w_aub_v v_sat_nP
+    intro v w X' P hasDag v_sat_X w_aub_v w_sat_nP
     unfold relate at w_aub_v
     cases w_aub_v
     case inl w_a_v =>
@@ -443,14 +466,14 @@ theorem likeLemmaFour :
         intro f f_in
         cases f_in
         case inl f_in_X' =>
-          apply w_sat_X f
+          apply v_sat_X f
           left
           exact f_in_X'
         case inr f_is_naP =>
           subst f_is_naP
           simp
           use v
-      · exact v_sat_nP
+      · exact w_sat_nP
       rcases IH with ⟨Y, Y_in, w_conY, as, nBasP_in_Y, w_as_v, emp, nonEmp⟩
       use Y
       constructor
@@ -471,14 +494,14 @@ theorem likeLemmaFour :
         intro f f_in
         cases f_in
         case inl f_in_X' =>
-          apply w_sat_X f
+          apply v_sat_X f
           left
           exact f_in_X'
         case inr f_is_nbP =>
           subst f_is_nbP
           simp
           use v
-      · exact v_sat_nP
+      · exact w_sat_nP
       rcases IH with ⟨Y, Y_in, w_conY, a, as, nBasP_in_Y, w_as_v⟩
       use Y
       constructor
@@ -490,8 +513,8 @@ theorem likeLemmaFour :
         · exact w_conY
         · use a, as
   case star a =>
-    intro w v X' P w_sat_X w_aS_v v_sat_nP
-    simp [vDash.SemImplies, modelCanSemImplyForm] at v_sat_nP
+    intro v w X' P hasDag w_aS_v w_sat_nP
+    simp [vDash.SemImplies, modelCanSemImplyForm] at w_sat_nP
     unfold relate at w_aS_v
     have := starCases w_aS_v
     cases this
@@ -510,7 +533,7 @@ theorem likeLemmaFour :
           simp at f_in
           cases f_in
           case inl f_in_X' =>
-            apply w_sat_X f
+            apply v_sat_X f
             simp
             left
             assumption
@@ -521,7 +544,7 @@ theorem likeLemmaFour :
               rfl
             subst f
             simp
-            exact v_sat_nP
+            exact w_sat_nP
         · use []
           constructor
           · simp
@@ -542,7 +565,7 @@ theorem likeLemmaFour :
         intro f_in
         cases f_in
         case inl f_in_X' =>
-          apply w_sat_X
+          apply v_sat_X
           simp
           left
           exact f_in_X'
@@ -592,7 +615,7 @@ theorem likeLemmaFour :
                 exact emp
   case test f =>
     -- TODO: this will no longer be trivial!
-    intro w v X' P w_sat_X w_tf_v v_sat_nP
+    intro v w X' P hasDag w_tf_v w_sat_nP
     unfold relate at w_tf_v
     rcases w_tf_v with ⟨w_is_v, w_f⟩
     subst w_is_v