delete HasVocabulary, use .voc, stronger unfoldBoxContent (subprograms)

Pdl/Discon.lean

@@ -223,26 +223,24 @@ theorem mapCon_mapForall (M : KripkeModel W) w φ
     · use a, b
     · rw [conEval]; intro f; tauto
 
-open HasVocabulary
-
 theorem in_voc_dis n (L : List Formula) :
-    n ∈ voc (dis L) ↔ ∃ φ ∈ L, n ∈ voc φ := by
+    n ∈ (dis L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc := by
   induction L
-  · simp [voc, dis, vocabOfFormula]
+  · simp [dis, Formula.voc]
   case cons h t IH =>
     induction t -- needed to select case in `dis`
-    · simp [voc, dis, vocabOfFormula]
+    · simp [dis, Formula.voc]
     case cons h t IH =>
-      simp [voc, dis, vocabOfFormula] at *
+      simp [dis, Formula.voc] at *
       rw [← IH]
 
 theorem in_voc_con n (L : List Formula) :
-    n ∈ voc (Con L) ↔ ∃ φ ∈ L, n ∈ voc φ := by
+    n ∈ (Con L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc := by
   induction L
-  · simp [voc, Con, vocabOfFormula]
+  · simp [Con, Formula.voc]
   case cons h t IH =>
     induction t -- needed to select case in `Con`
-    · simp [voc, Con, vocabOfFormula]
+    · simp [Con, Formula.voc]
     case cons h t IH =>
-      simp [voc, Con, vocabOfFormula] at *
+      simp [Con, Formula.voc] at *
       rw [← IH]

Pdl/Fresh.lean

@@ -18,12 +18,10 @@ mutual
     | ?'φ  => freshVarForm φ
 end
 
-open HasVocabulary
-
 mutual
-theorem freshVarForm_is_larger (φ) : ∀ n ∈ (vocabOfFormula φ).atomProps, n < freshVarForm φ := by
+theorem freshVarForm_is_larger (φ) : ∀ n ∈ φ.voc.atomProps, n < freshVarForm φ := by
   cases φ
-  all_goals simp [freshVarForm, voc, vocabOfFormula, not_or, Vocab.atomProps]
+  all_goals simp [freshVarForm, Formula.voc, not_or, Vocab.atomProps]
   case neg φ =>
     have IH := freshVarForm_is_larger φ
     simp [Vocab.atomProps] at *
@@ -39,9 +37,9 @@ theorem freshVarForm_is_larger (φ) : ∀ n ∈ (vocabOfFormula φ).atomProps, n
     simp [Vocab.atomProps] at *
     aesop
 
-theorem freshVarProg_is_larger (α) : ∀ n ∈ (vocabOfProgram α).atomProps, n < freshVarProg α := by
+theorem freshVarProg_is_larger (α) : ∀ n ∈ α.voc.atomProps, n < freshVarProg α := by
   cases α
-  all_goals simp [freshVarProg, voc, vocabOfProgram, Vocab.atomProps]
+  all_goals simp [freshVarProg, Program.voc, Vocab.atomProps]
   case union α β =>
     have IHα := freshVarProg_is_larger α
     have IHβ := freshVarProg_is_larger β
@@ -62,17 +60,17 @@ theorem freshVarProg_is_larger (α) : ∀ n ∈ (vocabOfProgram α).atomProps, n
     aesop
 end
 
-theorem freshVarForm_is_fresh (φ) : Sum.inl (freshVarForm φ) ∉ voc φ := by
+theorem freshVarForm_is_fresh (φ) : Sum.inl (freshVarForm φ) ∉ φ.voc := by
   have := freshVarForm_is_larger φ
-  simp [freshVarForm, voc, vocabOfFormula, Vocab.atomProps] at *
+  simp [freshVarForm, Formula.voc, Vocab.atomProps] at *
   by_contra hyp
   specialize this (freshVarForm φ)
   have := Nat.lt_irrefl (freshVarForm φ)
   tauto
 
-theorem freshVarProg_is_fresh (α) : Sum.inl (freshVarProg α) ∉ vocabOfProgram α := by
+theorem freshVarProg_is_fresh (α) : Sum.inl (freshVarProg α) ∉ α.voc := by
   have := freshVarProg_is_larger α
-  simp [freshVarProg, voc, vocabOfFormula, Vocab.atomProps] at *
+  simp [freshVarProg, Formula.voc, Vocab.atomProps] at *
   by_contra hyp
   specialize this (freshVarProg α)
   have := Nat.lt_irrefl (freshVarProg α)

Pdl/Interpolation.lean

@@ -2,10 +2,10 @@ import Mathlib.Data.Finset.Basic
 
 import Pdl.PartInterpolation
 
-open HasVocabulary vDash HasSat
+open vDash HasSat
 
 def Interpolant (φ : Formula) (ψ : Formula) (θ : Formula) :=
-  voc θ ⊆ voc φ ∩ voc ψ  ∧  φ ⊨ θ  ∧  θ ⊨ ψ
+  θ.voc ⊆ φ.voc ∩ ψ.voc  ∧  φ ⊨ θ  ∧  θ ⊨ ψ
 
 theorem interpolation : ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ : Formula, Interpolant φ ψ θ :=
   by
@@ -23,8 +23,8 @@ theorem interpolation : ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ : Formula, Int
   use θ
   constructor
   · intro f f_in
-    simp [voc, jvoc, vocabOfFormula, Vocab.fromList] at pI_prop f_in
-    simp only [voc, Finset.mem_inter]
+    simp [jvoc, Formula.voc, Vocab.fromList] at pI_prop f_in
+    simp only [Finset.mem_inter]
     have := pI_prop.1 f_in
     aesop
   constructor

Pdl/LocalTableau.lean

@@ -13,16 +13,11 @@ open HasLength
 /-- In nodes we optionally have a negated loaded formula on the left or right. -/
 abbrev Olf := Option (NegLoadFormula ⊕ NegLoadFormula)
 
-open HasVocabulary
-
 @[simp]
-def vocabOfOlf : Olf → Vocab
+def Olf.voc : Olf → Vocab
 | none => {}
-| some (Sum.inl nlf) => voc nlf
-| some (Sum.inr nlf) => voc nlf
-
-@[simp]
-instance : HasVocabulary Olf := ⟨ vocabOfOlf ⟩
+| some (Sum.inl nlf) => nlf.voc
+| some (Sum.inr nlf) => nlf.voc
 
 /-- A tableau node has two lists of formulas and an `Olf`. -/
 -- TODO: rename `TNode` to `Sequent`
@@ -788,7 +783,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
@@ -803,7 +798,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
@@ -817,7 +812,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
@@ -831,7 +826,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

Pdl/PartInterpolation.lean

@@ -3,7 +3,7 @@ import Mathlib.Data.Finset.Basic
 import Pdl.Completeness
 import Pdl.Distance
 
-open HasVocabulary HasSat
+open HasSat
 
 def Olf.toForms : Olf → List Formula
 | none => []
@@ -17,24 +17,24 @@ def TNode.right (X : TNode) : List Formula := X.R ++ X.O.toForms
 
 /-- Joint vocabulary of all parts of a TNode. -/
 @[simp]
-def jvoc (X : TNode) : Vocab := voc (X.left) ∩ voc (X.right)
+def jvoc (X : TNode) : Vocab := (X.left).fvoc ∩ (X.right).fvoc
 
 def isPartInterpolant (X : TNode) (θ : Formula) :=
-  voc θ ⊆ jvoc X ∧ (¬ satisfiable ((~θ) :: X.left) ∧ ¬ satisfiable (θ :: X.right))
+  θ.voc ⊆ jvoc X ∧ (¬ satisfiable ((~θ) :: X.left) ∧ ¬ satisfiable (θ :: X.right))
 
 def PartInterpolant (N : TNode) := Subtype <| isPartInterpolant N
 
 -- TODO move elsewhere
-theorem Formula.voc_boxes : vocabOfFormula (⌈⌈δ⌉⌉φ) =
-    Vocab.fromList (δ.map vocabOfProgram) ∪ vocabOfFormula φ := by sorry
+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 ∈ vocabOfFormula ψ) : x ∈ vocabOfProgram α ∨ x ∈ vocabOfFormula φ := by
-  rcases unfoldBoxContent _ _ _ L_in _ ψ_in with ψ_def | ⟨τ, τ_in, ψ_def⟩ | ⟨a, δ, ψ_def⟩
+    (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
+  rcases unfoldBoxContent _ _ _ L_in _ ψ_in with ψ_def | ⟨τ, τ_in, ψ_def⟩ | ⟨a, δ, ψ_def, _⟩
   all_goals subst ψ_def
   · right; exact x_in_voc_ψ
-  · simp only [vocabOfFormula] at x_in_voc_ψ
+  · simp only [Formula.voc] at x_in_voc_ψ
     left
     -- PROBLEM: here and in next case we need the stronger version of `unfoldBoxContent`.
     sorry
@@ -44,7 +44,7 @@ theorem unfoldBox_voc {x α φ} {L} (L_in : L ∈ unfoldBox α φ) {ψ} (ψ_in :
 
 -- move to UnfoldDia.lean ?
 theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ} (ψ_in : ψ ∈ L)
-    (x_in_voc_ψ : x ∈ vocabOfFormula ψ) : x ∈ vocabOfProgram α ∨ x ∈ vocabOfFormula φ := by
+    (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
   simp [unfoldDiamond, Yset] at L_in
   -- TODO use unfoldDiamondContent here instead?
   rcases L_in with ⟨Fs, δ, in_H, def_L⟩
@@ -56,12 +56,11 @@ theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ}
     have := H_mem_test α ψ in_H hyp
     rcases this with ⟨τ, τ_in, ψ_def⟩
     subst ψ_def
-    -- need lemma that voc-of-testsOfProgram is subset of voc
-    sorry
+    exact testsOfProgram.voc α τ_in x_in_voc_ψ
   case inr ψ_def =>
     have := H_mem_sequence
     subst ψ_def
-    simp only [vocabOfFormula, Formula.voc_boxes, Finset.mem_union] at x_in_voc_ψ
+    simp only [Formula.voc, Formula.voc_boxes, Finset.mem_union] at x_in_voc_ψ
     cases x_in_voc_ψ
     case inl hyp =>
       left
@@ -73,7 +72,7 @@ theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ}
       assumption
 
 theorem localRule_does_not_increase_vocab_L (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.1 ⊆ voc Lcond := by
+    ∀ res ∈ ress, res.1.fvoc ⊆ Lcond.fvoc := by
   intro res ress_in_ress x x_in_res
   cases rule
   case oneSidedL ress orule =>
@@ -110,12 +109,12 @@ theorem localRule_does_not_increase_vocab_L (rule : LocalRule (Lcond, Rcond, Oco
   · aesop
 
 theorem localRule_does_not_increase_vocab_R (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.2.1 ⊆ voc Rcond := by
+    ∀ res ∈ ress, res.2.1.fvoc ⊆ Rcond.fvoc := by
   -- should be dual to _L version
   sorry
 
 theorem localRule_does_not_increase_vocab_O (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.2.2 ⊆ voc Ocond := by
+    ∀ res ∈ ress, res.2.2.voc ⊆ Ocond.voc := by
   sorry
 
 theorem localRuleApp_does_not_increase_jvoc (ruleA : LocalRuleApp X C) :

Pdl/Substitution.lean

@@ -48,33 +48,32 @@ theorem repl_in_dis : repl_in_F x ψ (dis l) = dis (l.map (repl_in_F x ψ)) := b
       simp [dis]
       apply repl_in_dis
 
-open HasVocabulary
-
 mutual
 theorem repl_in_F_non_occ_eq {x φ ρ} :
-    (Sum.inl x) ∉ voc φ → repl_in_F x ρ φ = φ := by
+    (Sum.inl x) ∉ φ.voc → repl_in_F x ρ φ = φ := by
   intro x_notin_phi
   cases φ
   case bottom => simp
   case atom_prop c =>
     simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
-    intro c_is_x; simp [voc,vocabOfFormula] at *; subst_eqs; tauto
+    intro c_is_x; simp [Formula.voc] at *; subst_eqs; tauto
   case neg φ0 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     apply repl_in_F_non_occ_eq; tauto
   case and φ1 φ2 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
   case box α φ0 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     constructor
     · apply repl_in_P_non_occ_eq; tauto
     · apply repl_in_F_non_occ_eq; tauto
+
 theorem repl_in_P_non_occ_eq {x α ρ} :
-    (Sum.inl x) ∉ voc α → repl_in_P x ρ α = α := by
+    (Sum.inl x) ∉ α.voc → repl_in_P x ρ α = α := by
   intro x_notin_alpha
   cases α
-  all_goals simp [voc,vocabOfProgram] at *
+  all_goals simp [Program.voc] at *
   case sequence β γ =>
     constructor <;> (apply repl_in_P_non_occ_eq; tauto)
   case union β γ =>
@@ -86,47 +85,47 @@ theorem repl_in_P_non_occ_eq {x α ρ} :
 end
 
 theorem repl_in_boxes_non_occ_eq_neg (δ : List Program) :
-    (Sum.inl x) ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ := by
+    (Sum.inl x) ∉ Vocab.fromList (δ.map Program.voc) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ := by
   intro nonOcc
   induction δ
   · simp
   case cons α δ IH =>
     simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 theorem repl_in_boxes_non_occ_eq_pos (δ : List Program) :
-    (Sum.inl x) ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉·x) = ⌈⌈δ⌉⌉ψ := by
+    (Sum.inl x) ∉ Vocab.fromList (δ.map Program.voc) → repl_in_F x ψ (⌈⌈δ⌉⌉·x) = ⌈⌈δ⌉⌉ψ := by
   intro nonOcc
   induction δ
   · simp
   case cons α δ IH =>
     simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 theorem repl_in_list_non_occ_eq (F : List Formula) :
-     (Sum.inl x) ∉ voc F → F.map (repl_in_F x ρ) = F := by
+     (Sum.inl x) ∉ Vocab.fromList (F.map Formula.voc) → F.map (repl_in_F x ρ) = F := by
   intro nonOcc
   induction F
   · simp
   case cons φ F IH =>
     simp only [List.map_cons, List.cons.injEq]
     constructor
     · apply repl_in_F_non_occ_eq
-      simp [voc, vocabOfProgram, Vocab.fromList] at *
+      simp [Program.voc, Vocab.fromList] at *
       exact nonOcc.left
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 /-- Overwrite the valuation of `x` with the current value of `ψ` in a model. -/
 def repl_in_model (x : Nat) (ψ : Formula) : KripkeModel W → KripkeModel W