From 0820eb9fbc18bc8b88d15ac5c6611450264c7127 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Tue, 17 Sep 2024 16:00:09 +0200
Subject: [PATCH] correction to Qtests, proof pieces for cp3a

---
 Pdl/Modelgraphs.lean | 63 ++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 58 insertions(+), 5 deletions(-)

diff --git a/Pdl/Modelgraphs.lean b/Pdl/Modelgraphs.lean
index 1db36c6..0e31f4c 100644
--- a/Pdl/Modelgraphs.lean
+++ b/Pdl/Modelgraphs.lean
@@ -422,12 +422,12 @@ theorem truthLemma {Worlds} (MG : ModelGraph Worlds) :
 
 /-- Q_F - for a list `F` of tests (instead of a set in the notes). -/
 def Qtests {W : Finset (Finset Formula)} (R : Nat → W → W → Prop) (F : List Formula) : W → W → Prop
-| v, w => ∀ τ ∈ F, Q R (?' τ) v w
+| v, w => v == w ∧ ∀ τ ∈ F, Q R (?' τ) v w
 
 /-- Q_δ for a list `δ` of programs. -/
-def Qsteps {W : Finset (Finset Formula)} (R : Nat → W → W → Prop) : (δ : List Program) → W → W → Prop
+def Qsteps {W : Finset (Finset Formula)} (R : Nat → W → W → Prop) : List Program → W → W → Prop
 | [], v, w => v == w
-| (α :: rest), v, w => Relation.Comp (Q R α) (Qsteps R rest) v w
+| (α :: δ), v, w => Relation.Comp (Q R α) (Qsteps R δ) v w
 
 /-- Q_{F, δ} for a list of tests and a list or programs. -/
 def Qcombo {W : Finset (Finset Formula)} (R : Nat → W → W → Prop)
@@ -436,5 +436,58 @@ def Qcombo {W : Finset (Finset Formula)} (R : Nat → W → W → Prop)
 
 theorem cp3a {W : Finset (Finset Formula)} (R : Nat → W → W → Prop) (α : Program) :
     ∀ Fδ ∈ H α, ∀ v w, Qcombo R Fδ.1 Fδ.2 v w → Q R α v w := by
-  -- proof should be similar to that of `existsBoxFP`
-  sorry
+  rintro ⟨F,δ⟩ in_H v w
+  cases α <;>
+    simp_all [Q, Qtests, Qsteps, Qcombo, Relation.Comp, H]
+  case union α β =>
+    have IHα := cp3a R α
+    have IHβ := cp3a R β
+    simp only [Qcombo, Relation.Comp, Qtests, beq_iff_eq, Q, Subtype.exists, forall_exists_index,
+      and_imp, Subtype.forall, Subtype.mk.injEq, Prod.forall] at *
+    -- aesop:
+    intro x x_1 a a_1 a_2
+    subst a
+    simp_all only [true_and]
+    obtain ⟨val, property⟩ := w
+    cases in_H with
+    | inl h =>
+      apply Or.inl
+      apply IHα
+      · exact h
+      on_goal 2 => {rfl
+      }
+      · simp_all only
+      · intro τ a
+        simp_all only
+      · exact a_2
+    | inr h_1 =>
+      apply Or.inr
+      apply IHβ
+      · exact h_1
+      on_goal 2 => {rfl
+      }
+      · simp_all only
+      · intro τ a
+        simp_all only
+      · exact a_2
+  case sequence α β =>
+    have IHα := cp3a R α
+    have IHβ := cp3a R β
+    simp only [Qcombo, Relation.Comp, Qtests, beq_iff_eq, Q, Subtype.exists, forall_exists_index,
+      and_imp, Subtype.forall, Subtype.mk.injEq, Prod.forall] at *
+
+    intro v_val v_in v_def F_sub_v v_δ_w
+
+    rcases in_H with ⟨L, ⟨F, δ, _in_H, def_L⟩, _in_L⟩
+    subst def_L
+
+    by_cases δ = []
+    · subst_eqs
+      sorry
+    · simp [*] at _in_L
+      sorry
+  case star β =>
+    have IHβ := cp3a R β
+    simp only [Qcombo, Relation.Comp, Qtests, beq_iff_eq, Q, Subtype.exists, forall_exists_index,
+      and_imp, Subtype.forall, Subtype.mk.injEq, Prod.forall] at *
+    sorry