PDL Tableau with an idea how to represent repeats in inductive types

Pdl.lean

@@ -1,6 +1,7 @@
 -- This module serves as the root of the `Pdl` library.
 -- Import modules here that should be built as part of the library.
 import «Pdl».Syntax
+import «Pdl».Measures
 import «Pdl».Vocab
 import «Pdl».Semantics
 import «Pdl».Star

Pdl/Measures.lean

@@ -0,0 +1,68 @@
+-- MEASURES
+
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Data.Finset.Basic
+
+import Pdl.Syntax
+
+-- COMPLEXITY
+
+mutual
+  def lengthOfProgram : Program → Nat
+    | ·_ => 1
+    | α;β => 1 + lengthOfProgram α + lengthOfProgram β
+    | α⋓β => 1 + lengthOfProgram α + lengthOfProgram β
+    | ∗α => 1 + lengthOfProgram α
+    | ✓φ => 1 + lengthOfFormula φ
+  def lengthOfFormula : Formula → Nat
+    | Formula.bottom => 1
+    | ·_ => 1
+    | ~φ => 1 + lengthOfFormula φ
+    | φ⋀ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ
+    | ⌈α⌉φ => 1 + lengthOfProgram α + lengthOfFormula φ
+end
+termination_by -- silly but needed?!
+  lengthOfProgram p => sizeOf p
+  lengthOfFormula f => sizeOf f
+
+-- mwah
+@[simp]
+def lengthOfEither : PSum Program Formula → Nat
+  | PSum.inl p => lengthOfProgram p
+  | PSum.inr f => lengthOfFormula f
+
+class HasLength (α : Type) where
+  lengthOf : α → ℕ
+
+open HasLength
+@[simp]
+instance formulaHasLength : HasLength Formula := ⟨lengthOfFormula⟩
+@[simp]
+instance setFormulaHasLength : HasLength (Finset Formula) := ⟨fun X => X.sum lengthOfFormula⟩
+
+-- MEASURE
+mutual
+  @[simp]
+  def mOfProgram : Program → Nat
+    | ·_ => 0
+    | ✓ φ => 1 + mOfFormula φ
+    | α;β => 1 + mOfProgram α + mOfProgram β + 1 -- TODO: max (mOfFormula φ) (mOfFormula (~φ))
+    | α⋓β => 1 + mOfProgram α + mOfProgram β + 1
+    | ∗α => 1 + mOfProgram α
+  @[simp]
+  def mOfFormula : Formula → Nat
+    | ⊥ => 0
+    | ~⊥ => 0
+    |-- missing in borze?
+      ·_ =>
+      0
+    | ~·_ => 0
+    | ~~φ => 1 + mOfFormula φ
+    | φ⋀ψ => 1 + mOfFormula φ + mOfFormula ψ
+    | ~φ⋀ψ => 1 + mOfFormula (~φ) + mOfFormula (~ψ)
+    | ⌈α⌉ φ => mOfProgram α + mOfFormula φ
+    | ~⌈α⌉ φ => mOfProgram α + mOfFormula (~φ)
+end
+termination_by -- silly but needed?!
+  mOfProgram p => sizeOf p
+  mOfFormula f => sizeOf f

Pdl/Semantics.lean

@@ -5,6 +5,7 @@ import Mathlib.Order.CompleteLattice
 import Mathlib.Order.FixedPoints
 
 import Pdl.Syntax
+import Pdl.Measures
 
 -- Kripke Models aka Labelled Transition Systems
 structure KripkeModel (W : Type) : Type where

Pdl/Syntax.lean

@@ -14,7 +14,7 @@ mutual
     | union : Program → Program → Program
     | star : Program → Program
     | test : Formula → Program
-    deriving Repr, DecidableEq -- is not derivable here?
+    deriving Repr, DecidableEq
 end
 
 -- Notation and abbreviations
@@ -53,59 +53,6 @@ infixl:33 "⋓" => Program.union
 prefix:33 "∗" => Program.star
 prefix:33 "✓" => Program.test -- avoiding "?" which has a meaning in Lean 4
 
-
--- COMPLEXITY
-mutual
-  def lengthOfProgram : Program → Nat
-    | ·_ => 1
-    | α;β => 1 + lengthOfProgram α + lengthOfProgram β
-    | α⋓β => 1 + lengthOfProgram α + lengthOfProgram β
-    | ∗α => 1 + lengthOfProgram α
-    | ✓φ => 1 + lengthOfFormula φ
-  def lengthOfFormula : Formula → Nat
-    | Formula.bottom => 1
-    | ·_ => 1
-    | ~φ => 1 + lengthOfFormula φ
-    | φ⋀ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ
-    | ⌈α⌉φ => 1 + lengthOfProgram α + lengthOfFormula φ
-end
-termination_by -- silly but needed?!
-  lengthOfProgram p => sizeOf p
-  lengthOfFormula f => sizeOf f
-
--- mwah
-@[simp]
-def lengthOfEither : PSum Program Formula → Nat
-  | PSum.inl p => lengthOfProgram p
-  | PSum.inr f => lengthOfFormula f
-
--- MEASURE
-mutual
-  @[simp]
-  def mOfProgram : Program → Nat
-    | ·_ => 0
-    | ✓ φ => 1 + mOfFormula φ
-    | α;β => 1 + mOfProgram α + mOfProgram β + 1 -- TODO: max (mOfFormula φ) (mOfFormula (~φ))
-    | α⋓β => 1 + mOfProgram α + mOfProgram β + 1
-    | ∗α => 1 + mOfProgram α
-  @[simp]
-  def mOfFormula : Formula → Nat
-    | ⊥ => 0
-    | ~⊥ => 0
-    |-- missing in borze?
-      ·_ =>
-      0
-    | ~·_ => 0
-    | ~~φ => 1 + mOfFormula φ
-    | φ⋀ψ => 1 + mOfFormula φ + mOfFormula ψ
-    | ~φ⋀ψ => 1 + mOfFormula (~φ) + mOfFormula (~ψ)
-    | ⌈α⌉ φ => mOfProgram α + mOfFormula φ
-    | ~⌈α⌉ φ => mOfProgram α + mOfFormula (~φ)
-end
-termination_by -- silly but needed?!
-  mOfProgram p => sizeOf p
-  mOfFormula f => sizeOf f
-
 theorem boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
   by
   induction as

Pdl/Tableau.lean

@@ -1,21 +1,26 @@
+-- TABLEAU
+
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Option
+
 import Pdl.Syntax
+import Pdl.Measures
 import Pdl.Semantics
 import Pdl.Discon
 import Pdl.Unravel
 
--- NOTE: Much here should be replaced with extended versions of
--- https://github.com/m4lvin/tablean/blob/main/src/tableau.lean
--- but maybe we should mathport that project to Lean 4 first?
-
--- LOCAL TABLEAU
-
--- TODO: Can we use variables below without making them arguments of localRule?
--- variable (X : Finset Formula) (f g : Formula) (a b : Program)
+-- HELPER FUNCTIONS
 
 @[simp]
 def listsToSets : List (List Formula) → Finset (Finset Formula)
 | LS => (LS.map List.toFinset).toFinset
 
+-- LOCAL TABLEAU
+
+-- Definition 9, page 15
+-- A set X is closed  iff  0 ∈ X or X contains a formula and its negation.
+def Closed : Finset Formula → Prop := fun X => ⊥ ∈ X ∨ ∃ f ∈ X, (~f) ∈ X
+
 -- Local rules: given this set, we get these sets as child nodes
 inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   -- PROP LOGIC
@@ -314,19 +319,90 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
       -- split TODO
       sorry
 
+-- A set X is simple  iff  all P ∈ X are (negated) atoms or [A]_ or ¬[A]_.
+@[simp]
+def SimpleForm : Formula → Bool
+  | ⊥ => True
+  | ~⊥ => True
+  | ·_ => True
+  | ~·_ => True
+  | ⌈·_⌉_ => True
+  | ~⌈·_⌉_ => True
+  | _ => False
 
--- TODO inductive LocalTableau
+def Simple : Finset Formula → Bool
+  | X => ∀ P ∈ X, SimpleForm P
 
+-- Definition 8, page 14
+-- mixed with Definition 11 (with all PDL stuff missing for now)
+-- a local tableau for X, must be maximal
+inductive LocalTableau : Finset Formula → Type
+  | byLocalRule {X B} (_ : localRule X B) (next : ∀ Y ∈ B, LocalTableau Y) : LocalTableau X
+  | sim {X} : Simple X → LocalTableau X
 
--- TABLEAUX
+open LocalTableau
+
+open HasLength
+
+-- needed for endNodesOf
+instance localTableauHasSizeof : SizeOf (Σ X, LocalTableau X) :=
+  ⟨fun ⟨X, _⟩ => lengthOf X⟩
+
+-- open end nodes of a given localTableau
+@[simp]
+def endNodesOf : (Σ X, LocalTableau X) → Finset (Finset Formula)
+  | ⟨X, @byLocalRule _ B lr next⟩ =>
+    B.attach.biUnion fun ⟨Y, h⟩ =>
+      have : lengthOf Y < lengthOf X := sorry -- localRulesDecreaseLength lr Y h
+      endNodesOf ⟨Y, next Y h⟩
+  | ⟨X, sim _⟩ => {X}
 
-inductive Tableau -- to be rewritten as in tablean?
-  | leaf : Set Formula → Tableau
-  | Rule : Rule → List (Set Formula) → Tableau
+-- PROJECTIONS
 
-def projection : Char → Formula → Option Formula
-  | a, ⌈·b⌉ f => if a = b then some f else none
+@[simp]
+def formProjection : Char → Formula → Option Formula
+  | A, ⌈·B⌉φ => if A == B then some φ else none
   | _, _ => none
 
--- TODO inductive globalRule : ...
---  | nSt {a f} (h : (~⌈·a⌉f) ∈ X) : localRule X { X \ {~⌈·a⌉f} ∪ {~f} } -- TODO projection!!
+def projection : Char → Finset Formula → Finset Formula
+  | A, X => X.biUnion fun x => (formProjection A x).toFinset
+
+@[simp]
+theorem proj : g ∈ projection A X ↔ (⌈·A⌉g) ∈ X :=
+  by
+  rw [projection]
+  simp
+  constructor
+  · intro lhs
+    rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩
+    cases boxg
+    repeat' aesop
+  · intro rhs
+    use ⌈·A⌉g
+    simp
+    exact rhs
+
+theorem projSet : projection A X = {ϕ | (⌈·A⌉ϕ) ∈ X} :=
+  by
+  ext1
+  simp
+
+-- TABLEAUX
+
+-- Definition 16, page 29
+-- TODO: do we want a ClosedTableau or more general Tableau type?
+-- If more general, do we want an "open" constructor with(out) arguments/proofs?
+inductive ClosedTableau : List (Finset Formula) → Finset Formula → Type
+  | loc {X} (lt : LocalTableau X) : (∀ Y ∈ endNodesOf ⟨X, lt⟩, ClosedTableau Hist Y) → ClosedTableau Hist X
+  | atm {A X ϕ} : (~⌈·A⌉ϕ) ∈ X → Simple X → ClosedTableau (X :: Hist) (projection A X ∪ {~ϕ}) → ClosedTableau Hist X
+  | repeat {X} : X ∈ Hist → ClosedTableau Hist X
+
+inductive Provable : Formula → Prop
+  | byTableau {φ : Formula} : ClosedTableau _ {~φ} → Provable φ
+
+-- Definition 17, page 30
+def Inconsistent : Finset Formula → Prop
+  | X => Nonempty (ClosedTableau [] X)
+
+def Consistent : Finset Formula → Prop
+  | X => ¬Inconsistent X