redefine LoadFormula with mutual AnyFormula

Pdl/LocalTableau.lean

@@ -5,7 +5,7 @@ import Pdl.MultisetOrder
 
 open HasLength
 
--- TABLEAU NODES
+/-! ## Tableau Nodes -/
 
 -- A tableau node has two lists of formulas and one or no negated loaded formula.
 -- TODO: rename `TNode` to `Sequent`
@@ -49,6 +49,8 @@ theorem setEqTo_isLoaded_iff {X Y : TNode} (h : X.setEqTo Y) : X.isLoaded = Y.is
   all_goals
     exfalso; rcases h with ⟨_,_,impossible⟩ ; exact (Bool.eq_not_self _).mp impossible
 
+/-! ## Semantics of a TNode -/
+
 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)
 
@@ -69,6 +71,24 @@ theorem tautImp_iff_TNodeUnsat {φ ψ} {X : TNode} :
   subst defX
   simp [satisfiable,evaluate,modelCanSemImplyTNode,formCanSemImplyForm,semImpliesLists] at *
 
+/-! ## Different kinds of formulas as elements of TNode -/
+
+@[simp]
+instance : Membership Formula TNode := ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩
+
+def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop :=
+  X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf)
+
+@[simp]
+instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩
+
+def AnyNegFormula_in_TNode : (anf : AnyNegFormula) → (X : TNode) → Prop
+| ⟨.normal φ⟩, X => (~φ) ∈ X
+| ⟨.loaded χ⟩, X => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here
+
+@[simp]
+instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩
+
 /-! ## Local Tableaux -/
 
 /-- A set is closed iff it contains `⊥` or contains a formula and its negation. -/

Pdl/Modelgraphs.lean

@@ -56,7 +56,7 @@ theorem loadClaimHelper {Worlds : Finset (Finset Formula)}
     {X Y : { x // x ∈ Worlds }}
     {δ : List Program}
     {φ : Formula}
-    {l: List { x // x ∈ Worlds }}
+    {l : List { x // x ∈ Worlds }}
     (length_def: l.length + 1 = δ.length)
     (δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ X.val)
     (lchain : List.Chain' (pairRel MG.1) (List.zip ((?'⊤) :: δ) (X :: l ++ [Y])))

Pdl/Semantics.lean

@@ -108,6 +108,10 @@ instance modelCanSemImplyForm {W : Type} : vDash (KripkeModel W × W) Formula :=
 instance modelCanSemImplySet {W : Type} : vDash (KripkeModel W × W) (List Formula) := vDash.mk (λ ⟨M,w⟩ fs => ∀ f ∈ fs, @evaluate W M w f)
 @[simp]
 instance modelCanSemImplyList {W : Type} : vDash (KripkeModel W × W) (List Formula) := vDash.mk (λ ⟨M,w⟩ fs => ∀ f ∈ fs, @evaluate W M w f)
+instance modelCanSemImplyAnyNegFormula {W : Type} : vDash (KripkeModel W × W) AnyNegFormula :=
+  vDash.mk (λ ⟨M,w⟩ af => match af with
+   | ⟨.normal f⟩ => evaluate M w f
+   | ⟨.loaded f⟩ => evaluate M w (unload f) )
 instance setCanSemImplySet : vDash (List Formula) (List Formula) := vDash.mk semImpliesLists
 instance setCanSemImplyForm : vDash (List Formula) Formula:= vDash.mk fun X ψ => semImpliesLists X [ψ]
 instance formCanSemImplySet : vDash Formula (List Formula) := vDash.mk fun φ X => semImpliesLists [φ] X

Pdl/Soundness.lean

@@ -14,149 +14,105 @@ open HasSat
 /-- The PDL rules are sound. -/
 theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := by
   rcases satX with ⟨W, M, w, w_⟩
-  -- 8 cases, quite some duplication here unfortunately.
+  -- 6 cases, quite some duplication here unfortunately.
   cases r
   -- the loading rules are easy, because loading never changes semantics
   case loadL =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
     intro φ φ_in
     rcases φ_in with ((in_L | in_R) | φ_def)
-    all_goals
-      apply w_
-      subst_eqs
-      try tauto
-    · left
-      exact List.mem_of_mem_erase in_L
-    · left
-      simp [toNegLoad, unload]
-      sorry
+    all_goals (apply w_;  subst_eqs; try tauto)
+    left; exact List.mem_of_mem_erase in_L
   case loadR =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
+    intro φ φ_in
+    rcases φ_in with ((in_L | in_R) | φ_def)
+    all_goals (apply w_;  subst_eqs; try tauto)
+    right; exact List.mem_of_mem_erase in_R
   case freeL =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
+    intro φ φ_in
+    rcases φ_in with (φ_def | (in_L | in_R))
+    all_goals (apply w_;  subst_eqs; try tauto)
   case freeR =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
-  case atmL L R a χ X_def x_basic =>
-    subst X_def
-    use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋χ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
     intro φ φ_in
-    simp at φ_in
-    rcases φ_in with ((in_L | in_R) | φ_def)
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-  case atmR L R a χ X_def x_basic =>
+    rcases φ_in with (φ_def | (in_L | in_R))
+    all_goals (apply w_;  subst_eqs; try tauto)
+  case modL L R a χ X_def x_basic =>
     subst X_def
     use W, M -- but not the same world!
     have := w_ (negUnload (~'⌊·a⌋χ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with ((in_L | in_R) | φ_def)
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-  case atmL' L R a φ X_def x_basic =>
-    subst X_def
-    use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋φ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with (φ_def | (in_L | in_R))
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-  case atmR' L R a φ X_def x_basic =>
+    cases χ
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ( φ_def | (in_L | in_R))
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ((in_L | in_R) | φ_def)
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+  case modR L R a χ X_def x_basic =>
     subst X_def
     use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋φ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with (in_L | (φ_def | in_R))
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-
-/-- ## Tools for saying that different kinds of formulas are in a TNode -/
-
-@[simp]
-instance : Membership Formula TNode :=
-  ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩
-
-def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop :=
-  X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf)
-
-@[simp]
-instance NegLoadFormula.HasMem_TNode : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩
-
-def AnyFormula := Sum Formula LoadFormula
-
-inductive AnyNegFormula
-| neg : AnyFormula → AnyNegFormula
-
-local notation "~''" φ:arg => AnyNegFormula.neg φ
-
-instance modelCanSemImplyAnyNegFormula {W : Type} : vDash (KripkeModel W × W) AnyNegFormula :=
-  vDash.mk (λ ⟨M,w⟩ af => match af with
-   | ⟨Sum.inl f⟩ => evaluate M w f
-   | ⟨Sum.inr f⟩ => evaluate M w (unload f)
-   )
-
-def anyNegLoad : Program → AnyFormula → NegLoadFormula
-| α, Sum.inl φ => ~'⌊α⌋φ
-| α, Sum.inr χ => ~'⌊α⌋χ
-
-local notation "~'⌊" α "⌋" χ => anyNegLoad α χ
-
-def AnyNegFormula_in_TNode := fun (anf : AnyNegFormula) (X : TNode) => match anf with
-| ⟨Sum.inl φ⟩ => (~φ) ∈ X
-| ⟨Sum.inr χ⟩ => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here
-
-@[simp]
-instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩
+    have := w_ (negUnload (~'⌊·a⌋χ))
+    cases χ
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with (in_L | (φ_def | in_R))
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ((in_L | in_R) | φ_def)
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
 
 /-- ## Navigating through tableaux with PathIn -/
 
@@ -315,12 +271,9 @@ match t with
 def PathIn.isCritical (t : PathIn tab) : Prop :=
 match t with
   | .nil => False
-  | .pdl r _ => match r with
-     | .atmL _ _ => True
-     | .atmR _ _ => True
-     | .atmL' _ _ => True
-     | .atmR' _ _ => True
-     | _ => False
+  | .pdl (.modL _ _) _ => True
+  | .pdl (.modR _ _) _ => True
+  | .pdl _ tail => tail.isCritical
   | .loc _ tail => tail.isCritical
 
 /-- Prefix of a path, taking only the first `k` steps. -/
@@ -635,9 +588,21 @@ theorem tableauThenNotSat (tab : ClosedTableau .nil Root) (t : PathIn tab) :
       apply eProp2.c t _ t_is_free t_s
     case pdl Y r ctY =>
       simp [nodeAt]
-      -- use soundness of pdl rules here?!
-      sorry
-
+      intro hyp
+      have := pdlRuleSat r hyp -- using soundness of pdl rules here!
+      absurd this
+      -- As in `loc` case, it now remains to define a path leading to `Y`.
+      let t_to_s : PathIn _ := (@PathIn.pdl _ _ _ ctY r .nil)
+      let s : PathIn tab := t.append (t_def ▸ t_to_s)
+      have t_s : t ◃ s := by
+        unfold_let s
+        sorry
+      have : Y = nodeAt s := by
+        unfold_let s
+        sorry
+      rw [this]
+      apply IH
+      apply eProp2.c t _ t_is_free t_s
 
   case inr not_free =>
     simp [TNode.isFree] at not_free