weaken unfoldBoxContent to what we actually use

m4lvin · Oct 8, 2024 · c7fada3 · c7fada3
1 parent dda2955
commit c7fada3
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 19 deletions.
diff --git a/Pdl/LocalTableau.lean b/Pdl/LocalTableau.lean
@@ -695,7 +695,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
   have ubc := unfoldBoxContent (α) φ X X_in ψ ψ_in_X
   cases α <;> simp [Program.isAtomic] at *
   case sequence α β =>
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (α;'β)).attach).sum.succ by
@@ -710,7 +710,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case union α β => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (α⋓β)).attach).sum.succ by
@@ -724,7 +724,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case star β => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (∗β)).attach).sum.succ by
@@ -738,7 +738,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case test τ0 => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (?'τ0)).attach).sum.succ by

diff --git a/Pdl/UnfoldBox.lean b/Pdl/UnfoldBox.lean
@@ -500,15 +500,17 @@ theorem boxHelperTermination α (ℓ : TP α) :
         simp_all
 
 /-- Where formulas in the unfolding can come from.
-NOTE: the paper version also says φ ∈ fischerLadner [⌈α⌉ψ], not done here. -/
+NOTE: the paper version says two things more which we omit here:
+ - `φ ∈ fischerLadner [⌈α⌉ψ]`
+ - `∀ γ ∈ δ, γ ∈ subprograms α` (in the last conjunct) -/
 theorem unfoldBoxContent α ψ :
     ∀ X ∈ (unfoldBox α ψ),
     ∀ φ ∈ X,
         -- φ ∈ fischerLadner [⌈α⌉ψ] -- not done for now.
         -- ∧
         (  (φ = ψ)
          ∨ (∃ τ ∈ testsOfProgram α, φ = (~τ))
-         ∨ (∃ (a : Nat), ∃ δ, φ = (⌈·a⌉⌈⌈δ⌉⌉ψ) ∧ ∀ γ ∈ δ, γ ∈ subprograms α))
+         ∨ (∃ (a : Nat), ∃ δ, φ = (⌈·a⌉⌈⌈δ⌉⌉ψ) /- ∧ ∀ γ ∈ δ, γ ∈ subprograms α -/))
     := by
   intro X X_in φ φ_in_X
   simp [unfoldBox, Xset] at X_in
@@ -524,16 +526,16 @@ theorem unfoldBoxContent α ψ :
       case union α β =>
         rw [F_mem_iff_neg, F_mem_iff_neg] at φ_in_F
         rcases φ_in_F with
-          (⟨τ, τ_in, φ_def, not_ℓ_τ⟩ | ⟨τ, τ_in, φ_def, not_ℓ_τ⟩)
+          (⟨τ, τ_in, φ_def, _⟩ | ⟨τ, τ_in, φ_def, _⟩)
           <;> simp_all
       case sequence α β =>
         rw [F_mem_iff_neg, F_mem_iff_neg] at φ_in_F
         rcases φ_in_F with
-          (⟨τ, τ_in, φ_def, not_ℓ_τ⟩ | ⟨τ, τ_in, φ_def, not_ℓ_τ⟩)
+          (⟨τ, τ_in, φ_def, _⟩ | ⟨τ, τ_in, φ_def, _⟩)
           <;> simp_all
       case star β =>
         rw [F_mem_iff_neg] at φ_in_F
-        rcases φ_in_F with (⟨τ, τ_in, φ_def, not_ℓ_τ⟩)
+        rcases φ_in_F with (⟨τ, τ_in, φ_def, _⟩)
         simp_all
       case test τ =>
         simp only [allTP, List.mem_map, List.mem_sublists] at *
@@ -545,25 +547,29 @@ theorem unfoldBoxContent α ψ :
       case atom_prog a =>
         clear bht
         right
-        use a, []
+        use []
         simp
       case sequence α β =>
-        -- cases δ_in -- ??
         rcases bht with _ | ⟨a, δ1n, δ_def⟩
         · subst_eqs; simp
         · subst δ_def
           simp_all
           right
-          use a, δ1n
-          simp
-          -- need some IH after all? Or improve `bht` to also give `∈ subprograms`?
-          have := unfoldBoxContent α ψ
-          have := unfoldBoxContent β ψ
-          sorry
+          use δ1n
       case union α β =>
-        sorry
+        rcases bht with _ | ⟨a, δ1n, δ_def⟩
+        · subst_eqs; simp
+        · subst δ_def
+          simp_all
+          right
+          use δ1n
       case star β =>
-        sorry
+        rcases bht with _ | ⟨a, δ1n, δ_def⟩
+        · subst_eqs; simp
+        · subst δ_def
+          simp_all
+          right
+          use δ1n ++ [∗β]
       case test τ =>
         simp only [allTP, List.mem_map, List.mem_sublists] at *
         by_cases ℓ ⟨τ, (by simp : τ ∈ [τ])⟩ <;> simp_all