From 97e50580f9ff2235c48c74ea29b5a45dffa557b5 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Tue, 5 Dec 2023 22:59:53 +0100
Subject: [PATCH] WIP ReflTrans DagTab closure + loading type idea

---
 Pdl/Closure.lean    | 85 +++++++++++++++++++++++++++++++++++++++++++++
 Pdl/DagTableau.lean | 39 ++++++++++++++++-----
 Pdl/Loading.lean    |  7 ++++
 Pdl/Tableau.lean    |  4 +--
 4 files changed, 125 insertions(+), 10 deletions(-)
 create mode 100644 Pdl/Closure.lean
 create mode 100644 Pdl/Loading.lean

diff --git a/Pdl/Closure.lean b/Pdl/Closure.lean
new file mode 100644
index 0000000..0ebf609
--- /dev/null
+++ b/Pdl/Closure.lean
@@ -0,0 +1,85 @@
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Image
+import Mathlib.Logic.Function.Iterate
+
+-- reflexive transitive closure of a function on finsets
+
+def fTransRefl {α : Type} (f : Finset α → Finset α ) (h : DecidableEq α)
+    (m : Finset α → ℕ) (isDec : ∀ X, m (f X) < m X) :
+    Finset α → Finset α
+  | S => S ∪ (fTransRefl f h m isDec (f S))
+termination_by
+  fTransRefl f h m isDec S => m S
+decreasing_by simp_wf; apply isDec
+
+theorem ftr.toNth {α : Type}
+    {f : Finset α → Finset α}
+    {m : Finset α → ℕ}
+    (isDec : ∀ X, m (f X) < m X)
+    (h : DecidableEq α)
+    {k : ℕ}
+    :
+    ∀ (X : Finset α)
+    (_ : k = m X)
+    (x : α),
+    x ∈ fTransRefl f h m isDec X ↔ ∃ i, x ∈ (f^[i]) X := by
+  induction k using Nat.strong_induction_on
+  case h k IH =>
+    intro X k_is x
+    constructor
+    · intro x_in
+      rw [fTransRefl] at x_in
+      simp at x_in
+      cases x_in
+      case inl x_in_X =>
+        use 0
+        simp
+        assumption
+      case inr x_in =>
+        subst k_is
+        have := (IH (m (f X)) (isDec X) (f X) rfl x).1 x_in
+        rcases this with ⟨j,foo⟩
+        use j + 1
+        simp
+        exact foo
+    · rintro ⟨i, x_in_fiX⟩
+      cases i
+      case zero =>
+        simp at x_in_fiX
+        rw [fTransRefl]
+        simp
+        left
+        assumption
+      case succ i =>
+        rw [fTransRefl]
+        simp
+        right
+        subst k_is
+        specialize IH (m (f X)) (isDec X) (f X) rfl x
+        rw [IH]
+        simp at x_in_fiX
+        use i
+
+theorem ftr.Trans (S T U : Finset α) (s t u : α)
+    (f : Finset α → Finset α) (h : DecidableEq α)
+    (m : Finset α → ℕ) (isDec : ∀ X, m (f X) < m X)
+    (s_in_T : s ∈ fTransRefl f h m isDec {t})
+    (t_in_U : t ∈ fTransRefl f h m isDec U)
+    : s ∈ fTransRefl f h m isDec U
+  := by
+  rw [ftr.toNth isDec h U rfl s]
+  let T' : Finset α := {t}
+  rw [ftr.toNth isDec h T' rfl s] at s_in_T
+  rw [ftr.toNth isDec h U rfl t] at t_in_U
+  rcases s_in_T with ⟨sj, s_in⟩
+  rcases t_in_U with ⟨st, t_in⟩
+  simp at *
+  use sj + st
+  rw [Function.iterate_add]
+  simp at *
+  convert s_in -- WRONG, but to make inclusion enough here we need monotonicity!?
+  sorry
+
+-- U          T           S
+-- {...} -f-> {t,..} -f-> {s,..}
+--               s!
diff --git a/Pdl/DagTableau.lean b/Pdl/DagTableau.lean
index 4b47927..fb7f9b3 100644
--- a/Pdl/DagTableau.lean
+++ b/Pdl/DagTableau.lean
@@ -5,8 +5,6 @@ import Pdl.Discon
 import Pdl.Semantics
 import Pdl.Star
 
--- IDEA: adjust the type to forbid atomic program on (neg)top level?
-
 inductive DagFormula : Type
   | bottom : DagFormula
   | atom_prop : Char → DagFormula
@@ -240,6 +238,8 @@ theorem notStarSoundness M (a : Program) (v w : W) (Δ : DagTabNode)
   case test ψ =>
     sorry
 
+-- TODO: for boxes, use List DagFormula instead of Option DagFormula
+
 @[simp]
 def dagNext : (Finset Formula × Option DagFormula) → Finset (Finset Formula × Option DagFormula)
   | (fs, some (~⌈·A⌉φ)) => { (fs ∪ {undag (~⌈·A⌉φ)}, none) }
@@ -254,9 +254,24 @@ def dagNext : (Finset Formula × Option DagFormula) → Finset (Finset Formula 
   | (_, none) => { }  -- maybe wrong?
 
 def dagNextTransRefl : (Finset Formula × Option DagFormula) → Finset (Finset Formula × Option DagFormula)
-  | (fs, mdf) => {(fs,mdf)} ∪ ((dagNext (fs,mdf)).biUnion dagNextTransRefl)
+  | S => {S} ∪ ((dagNext S).biUnion dagNextTransRefl)
 decreasing_by sorry
 
+theorem dagNextTransRefl.Trans S T U
+    (S_in_T : S ∈ dagNextTransRefl T)
+    (T_in_U : T ∈ dagNextTransRefl U)
+    : S ∈ dagNextTransRefl U := by
+  rw [dagNextTransRefl] at *
+  simp only [Finset.mem_union, Finset.mem_singleton, Finset.mem_biUnion, Prod.exists] at *
+  cases S_in_T
+  all_goals (cases T_in_U)
+  · left; aesop
+  · aesop
+  · aesop
+  · right
+
+    all_goals sorry
+
 inductive DagTabNext : (Finset Formula × Option DagFormula) → Type
   | step fs f (next : ∀ Y ∈ dagNext (fs, some f), DagTabNext Y) : DagTabNext (fs, some f)
   | stop fs : DagTabNext (fs, none)
@@ -271,7 +286,7 @@ def successorsNext : (t : DagTabNext N) → Finset (Finset Formula × Option Dag
   | DagTabNext.step fs f next => {N} ∪ (dagNext (fs, some f)).attach.biUnion (fun ⟨Y, h⟩ => successorsNext (next Y h))
   | DagTabNext.stop _ => {N}
 
-
+-- rename to notStarSoundnessAux
 theorem notStarSoundnessNext (a : Program) M (v w : W) (fs)
     (φ : DagFormula)
     -- TODO: containsDag φ -- needed?
@@ -380,19 +395,27 @@ theorem notStarSoundnessNext (a : Program) M (v w : W) (fs)
               aesop
     · -- TODO "If (2) ..."
       -- subst v_is_u
-      have := notStarSoundnessNext γ M u w fs φ
+      have := notStarSoundnessNext γ M u w S.1 φ -- not use "fs" here!
       specialize this _ u_γ_w w_nP
       · intro f
         sorry -- should be easy
       rcases this with ⟨Γ, Γ_in, v_Γ, split⟩
-      -- rcases split with (⟨a,as,aasG_in_Γ, u_aas_w⟩ | ⟨ngPhi_in_Γ, u_is_w⟩)
+      -- need transitivity here
+      have also_in_prev : Γ ∈ dagNextTransRefl (fs, some (~⌈β;'γ⌉φ)) := by
+        apply dagNextTransRefl.Trans Γ S (fs, some (~⌈β;'γ⌉φ))
+        constructor
+        · convert Γ_in
+        · rw [dagNextTransRefl]
+          simp
+          right
+          exact S_in
       use Γ
       subst v_is_u
       constructor
-      · sorry -- exact Γ_in -- PROBLEM?!
+      · exact also_in_prev
       · constructor
         · exact v_Γ
-        · exact split
+        · tauto --
 
   case union α β =>
     simp at v_a_w
diff --git a/Pdl/Loading.lean b/Pdl/Loading.lean
new file mode 100644
index 0000000..a3f5e74
--- /dev/null
+++ b/Pdl/Loading.lean
@@ -0,0 +1,7 @@
+import Pdl.Syntax
+
+-- ft may be Formula or DagFormula
+inductive Loaded (ft : Type) : Type
+  | free : Formula → Loaded ft
+  | loadnbox : List Program → Formula → Loaded ft
+  deriving Repr
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index 9159cbb..d50d94e 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -295,8 +295,8 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       simp
       specialize w_X (⌈∗a⌉f) aSf_in_X
       simp at w_X
-      simp
-      use (X \ {⌈∗a⌉f} ∪ (List.toFinset {f} ∪ List.toFinset a_1))
+      -- simp
+      -- use (X \ {⌈∗a⌉f} ∪ (List.toFinset {f} ∪ List.toFinset a_1))
       sorry
 
   -- OTHER PDL RULES