building the roof of the house first

Pdl/Interpolation.lean

@@ -7,21 +7,36 @@ open HasVocabulary vDash HasSat
 def Interpolant (φ : Formula) (ψ : Formula) (θ : Formula) :=
   voc θ ⊆ voc φ ∩ voc ψ  ∧  φ ⊨ θ  ∧  θ ⊨ ψ
 
-
-
-theorem interpolation : ∀ (φ : Formula) (ψ : Formula), φ⊨ψ → ∃ θ : Formula, Interpolant φ ψ θ :=
-  by sorry /-
+theorem interpolation : ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ : Formula, Interpolant φ ψ θ :=
+  by
   intro φ ψ hyp
-  let L : List Formula := {φ}
-  let R : List Formula := {~ψ}
-  have : ¬Satisfiable (L ∪ R) := by
-    rw [notSat_iff_semImplies]
-    exact forms_to_sets hyp
-  have haveInt := partInterpolation L R this
-  rcases haveInt with ⟨θ, ⟨vocSubs, φ_θ, θ_ψ⟩⟩
+  let X : TNode := ([φ], [~(ψ)], none)
+  have ctX : ClosedTableau _ X :=
+    by
+    rw [tautImp_iff_TNodeUnsat rfl] at hyp
+    rw [← completeness] at hyp -- using completeness
+    simp [Consistent,Inconsistent] at hyp
+    exact Classical.choice hyp
+  have partInt := tabToInt ctX -- using tableau interpolation
+  rcases partInt with ⟨θ, pI_prop⟩
+  unfold isPartInterpolant at pI_prop
   use θ
-  rw [notSat_iff_semImplies] at φ_θ
-  rw [notSat_iff_semImplies] at θ_ψ
-  unfold Interpolant
-  simp [voc, vocabOfFormula, vocabOfSetFormula] at vocSubs
-  tauto-/
+  constructor
+  · intro f f_in
+    simp [voc,jvoc,vocabOfListFormula,vocabOfFormula] at pI_prop
+    exact pI_prop.1 f_in
+  constructor
+  · have := pI_prop.2.1
+    clear pI_prop
+    rw [tautImp_iff_comboNotUnsat]
+    simp [Satisfiable] at *
+    intro W M w
+    specialize this W M w
+    tauto
+  · have := pI_prop.2.2
+    clear pI_prop
+    rw [tautImp_iff_comboNotUnsat]
+    simp [Satisfiable] at *
+    intro W M w
+    specialize this W M w
+    tauto

Pdl/LocalTableau.lean

@@ -3,7 +3,6 @@
 import Pdl.Setsimp
 import Pdl.Discon
 import Pdl.DagTableau
-import Pdl.Vocab
 import Pdl.MultisetOrder
 
 open Undag HasLength
@@ -41,10 +40,6 @@ def TNode.isLoaded : TNode → Bool
 | ⟨_, _, none  ⟩ => False
 | ⟨_, _, some _⟩ => True
 
-open HasVocabulary
-def sharedVoc : TNode → Finset Char := λN => voc N.L ∩ voc N.R
-instance tNodeHasVocabulary : HasVocabulary (TNode) := ⟨sharedVoc⟩
-
 instance modelCanSemImplyTNode : vDash (KripkeModel W × W) TNode :=
   vDash.mk (λ ⟨M,w⟩ ⟨L, R, o⟩ => ∀ f ∈ L ∪ R ∪ (o.map (Sum.elim negUnload negUnload)).toList, evaluate M w f)
 
@@ -55,6 +50,14 @@ instance modelCanSemImplyLLO : vDash (KripkeModel W × W) (List Formula × List
 instance tNodeHasSat : HasSat TNode :=
   HasSat.mk fun Δ => ∃ (W : Type) (M : KripkeModel W) (w : W), (M,w) ⊨ Δ
 
+theorem tautImp_iff_TNodeUnsat {φ ψ} {X : TNode} :
+    X = ([φ], [~ψ], none) →
+    (φ ⊨ ψ ↔ ¬HasSat.Satisfiable X) :=
+  by
+  intro defX
+  subst defX
+  simp [HasSat.Satisfiable,evaluate,modelCanSemImplyTNode,formCanSemImplyForm,semImpliesLists] at *
+
 -- LOCAL TABLEAU
 
 -- Definition 9, page 15

Pdl/PartInterpolation.lean

@@ -8,10 +8,25 @@ open HasVocabulary HasSat
 
 def canonProg : sorry := sorry
 
-def IsPartInterpolant (N : TNode) (θ : Formula) :=
-  voc θ ⊆ voc N ∧ (¬Satisfiable (N.L ∪ {~θ}) ∧ ¬Satisfiable (N.R ∪ {θ}))
+@[simp]
+def TNode.left : TNode → List Formula
+| ⟨L, _, none⟩ => L
+| ⟨L, _, some (Sum.inl ⟨f⟩)⟩ => unload f :: L
+| ⟨L, _, some (Sum.inr _  )⟩ => L
 
-def PartInterpolant (N : TNode) := Subtype <| IsPartInterpolant N
+@[simp]
+def TNode.right : TNode → List Formula
+| ⟨_, R, none⟩ => R
+| ⟨_, R, some (Sum.inl _  )⟩ => R
+| ⟨_, R, some (Sum.inr ⟨f⟩)⟩ => unload f :: R
+
+@[simp]
+def jvoc : (LR: TNode) → Finset Char := λ X => voc (X.left) ∩ voc (X.right)
+
+def isPartInterpolant (X : TNode) (θ : Formula) :=
+  voc θ ⊆ jvoc X ∧ (¬Satisfiable ((~θ) :: X.left) ∧ ¬Satisfiable (θ :: X.right))
+
+def PartInterpolant (N : TNode) := Subtype <| isPartInterpolant N
 
 theorem localInterpolantStep
   (C : List TNode)
@@ -39,7 +54,10 @@ theorem localInterpolantStep
   | loadedL χ lrule => sorry
   | loadedR χ lrule => sorry
 
-
 theorem partInterpolation :
     ∀ (L R : List Formula), ¬Satisfiable (L ∪ R) → PartInterpolant (L,R,none) := by
   sorry
+
+theorem tabToInt {X : TNode} (tab : ClosedTableau LoadHistory.nil X) :
+    PartInterpolant X := by
+  sorry

Pdl/Semantics.lean

@@ -147,7 +147,6 @@ theorem forms_to_lists {φ ψ : Formula} : φ⊨ψ → ([φ] : List Formula)⊨(
   · tauto
   · aesop
 
-
 theorem notSat_iff_semImplies (X : List Formula) (χ : Formula):
     ¬Satisfiable (X ∪ [~χ]) ↔ X ⊨ ([χ] : List Formula) := by
   simp only [Satisfiable, not_exists, not_forall, exists_prop, setCanSemImplySet, semImpliesSets, forall_eq]
@@ -168,10 +167,10 @@ theorem equivSat {M : KripkeModel W} {w : W} (φ ψ : Formula): φ ≡ ψ → (M
     rw [φ_eq_ψ] at this
     tauto
 
-theorem equiv_iff {M : KripkeModel W} {w : W} {φ ψ : Formula} (hyp : φ ≡ ψ) : (M, w) ⊨ φ ↔ (M, w) ⊨ ψ :=
+theorem tautImp_iff_comboNotUnsat {φ ψ : Formula} :
+    φ ⊨ ψ ↔ ¬Satisfiable ([φ, ~ψ]) :=
   by
-    simp only [semEquiv, modelCanSemImplyForm, evaluatePoint] at *
-    exact hyp W M w
+  simp [formCanSemImplyForm, semImpliesLists, Satisfiable, evaluate]
 
 theorem 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 :=

Pdl/Vocab.lean

@@ -22,7 +22,7 @@ def vocabOfSetFormula : Finset Formula → Finset Char
   | X => X.biUnion vocabOfFormula
 
 def vocabOfListFormula : List Formula → Finset Char := λX =>
-  X.foldl (λV φ => V ∪ vocabOfFormula φ ) ∅
+  X.foldl (λ V φ => V ∪ vocabOfFormula φ) ∅
 
 theorem inVocList : ℓ ∈ vocabOfListFormula L ↔ ∃φ ∈ L, ℓ ∈ vocabOfFormula φ := by sorry