star case likeLemmaFour only has a dagger-or-not problem left

m4lvin · Oct 23, 2023 · 7fd343f · 7fd343f
1 parent a80f0d5
commit 7fd343f
Show file tree

Hide file tree

Showing 3 changed files with 57 additions and 9 deletions.
diff --git a/Pdl/Semantics.lean b/Pdl/Semantics.lean
@@ -103,3 +103,27 @@ theorem forms_to_sets {φ ψ : Formula} : φ⊨ψ → ({φ} : Finset Formula)⊨
   -- needed even though no ψ_1 in goal here?!
   apply impTaut
   exact lhs
+
+lemma relate_steps : ∀ x z, relate M (Program.steps (as ++ bs)) x z  ↔
+  ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z :=
+  by
+  induction as
+  · simp
+  case cons a as IH =>
+    intro x z
+    constructor
+    · intro lhs
+      simp at *
+      rcases lhs with ⟨y, x_a_y, y_asbs_z⟩
+      rw [IH] at y_asbs_z
+      rcases y_asbs_z with ⟨y', y_as_ys', ys'_bs_z⟩
+      use y'
+      constructor
+      · use y
+      · exact ys'_bs_z
+    · intro rhs
+      simp at *
+      rcases rhs with ⟨y, ⟨y', x_a_y', y'_as_y⟩, bla⟩
+      use y'
+      rw [IH y' z]
+      tauto
diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean
@@ -160,9 +160,15 @@ instance formulaHasVocabulary : HasVocabulary Formula := ⟨vocabOfFormula⟩
 instance programHasVocabulary : HasVocabulary Program := ⟨vocabOfProgram⟩
 instance finsetFormulaHasVocabulary : HasVocabulary (Finset Formula) := ⟨vocabOfSetFormula⟩
 
-lemma boxes_last : ∀ {a as P} , (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
+lemma boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
+  by
+  induction as
+  · simp
+  · simp at *
+    assumption
+
+lemma boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.boxes bs P) :=
   by
-  intro a as P
   induction as
   · simp
   · simp at *

diff --git a/Pdl/Unravel.lean b/Pdl/Unravel.lean
@@ -229,32 +229,50 @@ theorem likeLemmaFour :
       assumption
     case inr hyp =>
       rcases hyp with ⟨w_neq_v, ⟨y, w_neq_y, w_a_y, y_aS_v⟩⟩
-      have IHa := likeLemmaFour M a w y X' (†⌈∗a⌉P) w_neq_y
+      have IHa := likeLemmaFour M a w y X' (†⌈∗a⌉P) w_neq_y -- dagger here or not?
       specialize IHa _ w_a_y _
       · intro f
         simp
         intro f_in
         cases f_in
-        · apply w_sat_X
+        case inl f_in_X' =>
+          apply w_sat_X
           simp
           left
-          assumption
+          exact f_in_X'
         case inr f_def =>
           subst f_def
           simp
           use y
           constructor
-          · assumption
+          · exact w_a_y
           · use v
       · unfold vDash.SemImplies
         unfold modelCanSemImplyForm
         simp
         use v
-      rcases IHa with ⟨Y, Y_in, w_conY, as, nBasaSP_in_Y, w_as_u⟩
+      rcases IHa with ⟨Y, Y_in, w_conY, as, nBasaSP_in_Y, w_as_y⟩
       use Y
       constructor
-      · sorry -- mismatch:  unravel (~⌈a⌉†⌈∗a⌉P)  vs.  unravel (~⌈∗a⌉P)  :-(
-      · sorry
+      · simp
+        simp at Y_in
+        rcases Y_in with ⟨L, L_in_unrav, defY⟩
+        use L
+        constructor
+        · right
+          exact L_in_unrav -- wants dagger
+        · exact defY
+      · constructor
+        · assumption
+        · use (as ++ [∗ a])
+          rw [boxes_append]
+          simp
+          constructor
+          · sorry -- exact nBasaSP_in_Y -- wants no dagger
+          · rw [relate_steps]
+            use y
+            simp
+            exact ⟨w_as_y, y_aS_v⟩
   case test f =>
     intro w v X' P w_neq_v w_sat_X w_tf_v v_sat_nP
     unfold relate at w_tf_v