move and prove Formula.voc_boxes

Pdl/PartInterpolation.lean

@@ -1,3 +1,5 @@
+-- Interpolants for Partitions (big part of Section 7)
+
 import Mathlib.Data.Finset.Basic
 
 import Pdl.Completeness
@@ -24,10 +26,6 @@ def isPartInterpolant (X : TNode) (θ : Formula) :=
 
 def PartInterpolant (N : TNode) := Subtype <| isPartInterpolant N
 
--- TODO move elsewhere
-theorem Formula.voc_boxes : (⌈⌈δ⌉⌉φ).voc = δ.pvoc ∪ φ.voc := by
-  sorry
-
 -- move to UnfoldBox.lean ?
 theorem unfoldBox_voc {x α φ} {L} (L_in : L ∈ unfoldBox α φ) {ψ} (ψ_in : ψ ∈ L)
     (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
@@ -129,7 +127,7 @@ theorem localRuleApp_does_not_increase_jvoc (ruleA : LocalRuleApp X C) :
     sorry
 
 /-- Maehara's method for local rule applications.
-This is `easyItp` for singleton clusters in the notes, but not only. -/
+This is `itpLeaves` for singleton clusters in the notes, but not only. -/
 def localInterpolantStep (L R : List Formula) (o) (ruleA : LocalRuleApp (L,R,o) C)
     (subθs : Π c ∈ C, PartInterpolant c)
     : PartInterpolant (L,R,o) := by

Pdl/Vocab.lean

@@ -70,6 +70,14 @@ theorem Vocab.fromListProgram_map_iff n (L : List Program) :
     simp only [fromList, Finset.mem_union, List.mem_cons, exists_eq_or_imp]
     rw [← IH]
 
+theorem Formula.voc_boxes : (⌈⌈δ⌉⌉φ).voc = δ.pvoc ∪ φ.voc := by
+  induction δ
+  · simp
+  case cons α δ IH =>
+    simp only [List.pvoc, voc, Vocab.fromList, Finset.union_assoc] at *
+    rw [← IH]
+    rfl
+
 @[simp]
 def LoadFormula.voc (lf : LoadFormula) : Vocab := (unload lf).voc