more Lemma 4 problems, semicolon case stuck in four approaches

Pdl/Syntax.lean

@@ -67,7 +67,6 @@ theorem boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.bo
   · simp at *
     assumption
 
-@[simp]
 def isAtomic : Program → Bool
 | Program.atom_prog _  => True
 | _ => False

Pdl/Unravel.lean

@@ -143,6 +143,41 @@ def unravel : DagFormula → List (List Formula)
 termination_by
   unravel f => mOfDagFormula f
 
+theorem atNoDagHelper :
+  containsDag P = false →
+    (containsDag (if isAtomic b = true then inject (undag (⌈c⌉P)) else ⌈c⌉P) = false) :=
+  by
+  intro noDag
+  aesop
+
+@[simp]
+theorem dagSemIrrelevant :
+  evaluate M u (undag (if isAtomic b = true then ⌈c⌉inject (undag P) else ⌈c⌉P))
+    ↔ evaluate M u (undag (⌈c⌉P)) :=
+  by
+  sorry
+
+@[simp]
+theorem unravelAtomicIrrelevant b P :
+  unravel (~⌈b⌉if isAtomic b = true then inject (undag P) else P) = unravel (~⌈b⌉P) :=
+  by
+  cases b
+  all_goals (simp [isAtomic])
+
+@[simp]
+theorem undagOfIte b P :
+  undag (if isAtomic b = true then inject (undag P) else P) = undag P :=
+  by
+  cases b
+  all_goals (simp [isAtomic])
+
+theorem dagHelper :
+  containsDag P = true →
+    ∀ b c, ((containsDag (if isAtomic b = true then inject (undag (⌈c⌉P)) else ⌈c⌉P) = true) ↔ isAtomic b = false) :=
+  by
+  intro dag
+  aesop
+
 -- Like Lemma 4 from Borzechowski, but using "unravel" instead of a local tableau with n-nodes.
 -- This is used in the proof that the (¬∗) rule is sound.
 -- See https://is.gd/borzepdl#lemma.4 for the original.
@@ -155,7 +190,7 @@ 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) →
+    (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) →
@@ -171,20 +206,23 @@ theorem likeLemmaFour :
   -- no 'induction', but using recursive calls instead
   cases a
   case atom_prog A =>
-    intro w v X' P w_sat_X w_a_v v_sat_nP
+    intro w v X' P atNoDag w_sat_X w_a_v v_sat_nP
     simp
     constructor
     · assumption
     · use [·A]
-      simp [Formula.boxes] at *
+      simp [isAtomic,Formula.boxes] at *
       exact w_a_v
   case sequence b c =>
-    intro w v X' P w_sat_X w_bc_v v_sat_nP
+    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⟩
     simp [vDash.SemImplies, modelCanSemImplyForm] at *
-    have IHb := likeLemmaFour M b w u X' (⌈c⌉P)
-    specialize IHb _ w_b_u _
+    have IHb := likeLemmaFour M b w u X' (if isAtomic b then inject (undag (⌈c⌉P)) else ⌈c⌉P)
+    specialize IHb _ _ w_b_u _
+    · simp [isAtomic] at atNoDag
+      rw [dagHelper atNoDag b c]
+      simp
     · intro f lhs
       simp at lhs
       cases' lhs with f_in_X f_def
@@ -197,11 +235,16 @@ theorem likeLemmaFour :
         constructor
         · exact w_b_u
         · use v
-    · simp [vDash.SemImplies, modelCanSemImplyForm]
+    · 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
@@ -219,7 +262,8 @@ theorem likeLemmaFour :
           · rw [boxes_append]
             rw [← Ydef] at nBascP_in_Y
             simp at nBascP_in_Y
-            exact nBascP_in_Y
+            have := undagOfIte b (⌈c⌉P)
+            aesop
           · constructor
             · rw [relate_steps]
               use u
@@ -241,17 +285,15 @@ theorem likeLemmaFour :
       subst emp -- w = u
       subst as_is_emp
       simp at *
-      have IHc := likeLemmaFour M c w v (X' ++ L) (P) -- idea: context L, not all of Y
-      specialize IHc _ u_c_v _
-      · simp -- sorry
+      -- 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
       · intro f lhs
         simp at lhs
-        rcases lhs with f_in_X' | f_in_L | f_def
-        · apply w_conY f
-          rw [← Ydef]
-          simp
-          left
-          exact f_in_X'
+        rcases lhs with f_in_L | f_def
         · apply w_conY f
           rw [← Ydef]
           simp
@@ -260,69 +302,139 @@ theorem likeLemmaFour :
         · subst f_def
           simp
           use v
-      · simp [vDash.SemImplies, modelCanSemImplyForm]
+      · 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' -- Kaputt. -- What do I know about L' here?
-      rcases nBascP_in_Y' with in_X' | in_L | in_L'
-      · use L -- (L ++ L')
+      simp at nBascP_in_Y'
+      rcases nBascP_in_Y' with in_L | in_L'
+      · use L
         constructor
-        · assumption -- now matching
+        · exact L_in_unrav -- now matching
         · constructor
           · intro f lhs
             apply w_conY
             simp
             exact lhs
           · use as'
             constructor
-            · left
-              assumption
+            · right
+              exact in_L
             · constructor
-              · assumption
+              · exact w_as_v'
               · tauto
-      · use L -- (L ++ L')
+      -- four combinations at least:
+      -- (1) use L ... use as'
+      /-
+      · use L -- seems we need L' here ...
         constructor
-        · assumption -- now matching
+        · exact L_in_unrav -- needs "use L"
         · constructor
           · intro f lhs
-            apply w_conY
-            simp
-            exact lhs
+            cases lhs
+            · apply w_conY; simp; tauto
+            · apply w_conY'; simp; tauto
           · use as'
             constructor
-            · tauto
+            · right
+              sorry -- exact in_L' -- needs "use L'" when using as'
             · constructor
-              · assumption
+              · exact w_as_v'
               · tauto
-      · sorry -- no way this third case seems to work out ? use (L ++ L')
-        /-
+      -/
+      -- (2) use L ... use [c]
+      /-
+      · use L -- seems we need L here ...
         constructor
-        · assumption -- now matching
+        · exact L_in_unrav -- .needs "use L"
         · constructor
           · intro f lhs
-            apply w_conY
-            simp
-            exact lhs
+            cases lhs
+            · apply w_conY; simp; tauto
+            · apply w_conY'; simp; tauto
+          · use [c]
+            constructor
+            · simp at nBascP_in_Y
+              simp
+              exact nBascP_in_Y
+            · constructor
+              · simp; exact u_c_v
+              · simp
+                sorry -- needs that c is atomic?!?!
+      -/
+      -- (2') use L ... use [b] ++ as'
+      · use L -- seems we need L here ...
+        constructor
+        · exact L_in_unrav -- .needs "use L"
+        · constructor
+          · intro f lhs
+            cases lhs
+            · apply w_conY; simp; tauto
+            · apply w_conY'; simp; tauto
+          · use [b] ++ as'
+            constructor
+            · simp at nBascP_in_Y
+              simp
+              sorry -- exact nBascP_in_Y -- seems impossible to find [b][as']P in X' or L
+            · constructor
+              · simp; use w
+              · simp
+                sorry -- needs that b is atomic?!?!
+
+
+
+      -- (3) use L' ... use as'
+      /-
+      · use L' -- seems we need L here ...
+        constructor
+        · sorry -- exact L_in_unrav -- needs "use L"
+        · constructor
+          · intro f lhs
+            cases lhs
+            · apply w_conY; simp; tauto
+            · apply w_conY'; simp; tauto
           · use as'
             constructor
-            · left
-              assumption
+            · simp at nBascP_in_Y
+              right
+              exact in_L'
             · constructor
-              · assumption
+              · exact w_as_v'
+              · tauto
+      -/
+      -- (4) use L' ... use [c]  (TODO)
+      /-
+      · use L' -- seems we need L here ...
+        constructor
+        · sorry -- exact L_in_unrav -- needs "use L"
+        · constructor
+          · intro f lhs
+            cases lhs
+            · apply w_conY; simp; tauto
+            · apply w_conY'; simp; tauto
+          · use [c]
+            constructor
+            · simp at nBascP_in_Y
+              right
+              exact in_L'
+            · constructor
+              · exact w_as_v'
               · tauto
-              -/
+       -/
+
+
   case union a b =>
-    intro w v X' P w_sat_X w_aub_v v_sat_nP
+    intro w v X' P atNoDag w_sat_X w_aub_v v_sat_nP
     unfold relate at w_aub_v
     cases w_aub_v
     case inl w_a_v =>
       have IH := likeLemmaFour M a w v X'
-      specialize IH P _ w_a_v _
-      · simp at atNoDag
+      specialize IH P _ _ w_a_v _
+      · simp [isAtomic] at atNoDag
         sorry
       · unfold vDash.SemImplies at *
         unfold modelCanSemImplyList at *