start formalizing alternation depth

3 files changed, 215 insertions, 2 deletions

diff --git a/SymbolicModalLogic/AlternationDepth.lean b/SymbolicModalLogic/AlternationDepth.lean
new file mode 100644
index 0000000..b3b0a8e
--- /dev/null
+++ b/SymbolicModalLogic/AlternationDepth.lean
@@ -0,0 +1,194 @@
+import SymbolicModalLogic.MuCalculus
+import Mathlib
+
+inductive FixedPointOp where
+  | μ
+  | ν
+  deriving DecidableEq
+
+variable {Λ : Type} [Modalities Λ]
+open Formula
+
+inductive IsAlternationDepthBound : FixedPointOp → ℕ → Formula Λ → Prop where
+  | top {η : FixedPointOp} : IsAlternationDepthBound η 0 .top
+  | bot {η : FixedPointOp} : IsAlternationDepthBound η 0 .bot
+  | var {η : FixedPointOp} (x : ℕ) : IsAlternationDepthBound η 0 (.var x)
+  | or {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} :
+      IsAlternationDepthBound η n φ →
+      IsAlternationDepthBound η n ψ →
+      IsAlternationDepthBound η n (.or φ ψ)
+  | and {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} :
+      IsAlternationDepthBound η n φ →
+      IsAlternationDepthBound η n ψ →
+      IsAlternationDepthBound η n (.and φ ψ)
+  | modality {η : FixedPointOp} {n : ℕ} {l : Λ} {args : Modalities.signature l → Formula Λ} :
+      (∀ l, IsAlternationDepthBound η n (args l)) →
+      IsAlternationDepthBound η n (.modality l args)
+  | lfp {n : ℕ} {φ : Formula Λ} :
+      IsAlternationDepthBound .ν n φ →
+      IsAlternationDepthBound .ν n (μ, φ)
+  | gfp {n : ℕ} {φ : Formula Λ} :
+      IsAlternationDepthBound .μ n φ →
+      IsAlternationDepthBound .μ n (ν, φ)
+  | subst {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} {x : ℕ} :
+      IsAlternationDepthBound η n φ →
+      IsAlternationDepthBound η n ψ →
+      IsAlternationDepthBound η n (φ.subst (x, ψ))
+  | up {η₁ η₂ : FixedPointOp} {n : ℕ} {φ : Formula Λ} :
+      IsAlternationDepthBound η₁ n φ →
+      IsAlternationDepthBound η₂ (n + 1) φ
+
+def IsAlternationDepth (n : ℕ) (φ : Formula Λ) : Prop :=
+  IsAlternationDepthBound .μ n φ ∧ IsAlternationDepthBound .ν n φ
+
+example : IsAlternationDepth 2 ((μ, ν, ^0 ∧ μ, ^2 ∨ ^0) : Formula Λ) := by
+  suffices IsAlternationDepthBound .ν 1 ((ν, ^0 ∧ μ, ^2 ∨ ^0) : Formula Λ) by
+    constructor
+    · apply IsAlternationDepthBound.up
+      apply IsAlternationDepthBound.lfp
+      exact this
+    · apply IsAlternationDepthBound.up
+      apply IsAlternationDepthBound.lfp
+      exact this
+  rw [show ((ν, ^0 ∧ μ, ^2 ∨ ^0) : Formula Λ) = (ν, ^0 ∧ ^1).subst (0, (μ, ^1 ∨ ^0)) from rfl]
+  apply IsAlternationDepthBound.subst
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.or
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+
+example : IsAlternationDepth 1 ((ν, ^0) : Formula Λ) := by
+  constructor
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.var
+
+example : IsAlternationDepth 1 ((μ, ^0) : Formula Λ) := by
+  constructor
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.var
+
+example : IsAlternationDepth 1 ((ν, ν, ^0 ∧ ^1) : Formula Λ) := by
+  constructor
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+
+example : IsAlternationDepth 2 ((μ, ν, ^0 ∧ ^1) : Formula Λ) := by
+  constructor
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+
+example : IsAlternationDepth 2 ((ν, μ, ^0 ∧ ^1) : Formula Λ) := by
+  constructor
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+  · apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.gfp
+    apply IsAlternationDepthBound.up
+    apply IsAlternationDepthBound.lfp
+    apply IsAlternationDepthBound.and
+    · apply IsAlternationDepthBound.var
+    · apply IsAlternationDepthBound.var
+
+noncomputable def alternationDepth (φ : Formula Λ) : ℕ :=
+  sInf { n : ℕ | IsAlternationDepth n φ }
+
+private def collectOps : Formula Λ → List FixedPointOp
+  | .top => []
+  | .bot => []
+  | .or φ ψ => collectOps φ ++ collectOps ψ
+  | .and φ ψ => collectOps φ ++ collectOps ψ
+  | .modality l args =>
+      have : FinEnum (Modalities.signature l) := Modalities.signature_finenum l
+      FinEnum.toList (Modalities.signature l)
+        |>.flatMap fun a ↦ (collectOps (args a))
+  | .var _ => []
+  | .lfp φ => FixedPointOp.μ :: collectOps φ
+  | .gfp φ => FixedPointOp.ν :: collectOps φ
+
+def ad (φ : Formula Λ) : ℕ :=
+  let rec count (curr : FixedPointOp) (val : ℕ) : List FixedPointOp → ℕ
+    | .nil        => val
+    | .cons .μ xs => let val' := if _ : curr = .μ then val else val + 1
+                     count .μ val' xs
+    | .cons .ν xs => let val' := if _ : curr = .ν then val else val + 1
+                     count .ν val' xs
+  count .ν 0 (collectOps φ).reverse
+
+private lemma ad_count_add {curr : FixedPointOp} {val n : ℕ} {xs : List FixedPointOp} :
+    ad.count curr (val + n) xs = (ad.count curr val xs) + n := by
+  induction xs generalizing val curr with
+  | nil => simp [ad.count]
+  | cons x xs ih =>
+      cases x <;> cases curr
+      · simp [ad.count, ih]
+      · simp only [ad.count, reduceCtorEq, ↓reduceDIte]
+        rw [show val + n + 1 = (val + 1) + n by ring]
+        apply ih
+      · simp only [ad.count, reduceCtorEq, ↓reduceDIte]
+        rw [show val + n + 1 = (val + 1) + n by ring]
+        apply ih
+      · simp [ad.count, ih]
+
+lemma ad_isAlternationDepth (φ : Formula Λ) : IsAlternationDepth (ad φ) φ := by
+  sorry
+--   induction φ with
+--   | top =>
+--       simp only [ad, collectOps, List.reverse_nil, ad.count]
+--       constructor <;> apply IsAlternationDepthBound.top
+--   | bot =>
+--       simp only [ad, collectOps, List.reverse_nil, ad.count]
+--       constructor <;> apply IsAlternationDepthBound.bot
+--   | or ψ₁ ψ₂ ih₁ ih₂ =>
+--       simp [ad, collectOps]
+--   | and ψ₁ ψ₂ => sorry
+--   | modality l args => sorry
+--   | var x => sorry
+--   | lfp ψ => sorry
+--   | gfp ψ => sorry
+
+lemma alternationDepth_isAlternationDepth (φ : Formula Λ) : IsAlternationDepth (alternationDepth φ) φ := by
+  show sInf { n : ℕ | IsAlternationDepth n φ } ∈ { n : ℕ | IsAlternationDepth n φ }
+  apply Nat.sInf_mem
+  use ad φ
+  apply ad_isAlternationDepth
diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean
index 4c9155b..81d428d 100644
--- a/SymbolicModalLogic/Instances/Relational.lean
+++ b/SymbolicModalLogic/Instances/Relational.lean
@@ -4,6 +4,7 @@ import SymbolicModalLogic.MuCalculus
 inductive Relational where
   | box
   | diamond
+  deriving Repr
 
 namespace Relational
 
diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean
index 73d04f4..ca5b447 100644
--- a/SymbolicModalLogic/MuCalculus.lean
+++ b/SymbolicModalLogic/MuCalculus.lean
@@ -3,7 +3,7 @@ import SymbolicModalLogic.FixedPoints
 
 class Modalities (Λ : Type) where
   signature : Λ → Type
-  signature_fintype : ∀ l, Fintype (signature l) := by intro; infer_instance
+  [signature_finenum : ∀ l, FinEnum (signature l)]
   dual : Λ → Λ
   dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α)
   dual_involution : ∀ l, dual (dual l) = l
@@ -30,6 +30,24 @@ scoped notation "ν, " φ => Formula.gfp φ
 
 variable {Λ : Type} [Modalities Λ]
 
+instance [Repr Λ] : ToString (Formula Λ) where
+  toString :=
+    let rec impl : Formula Λ → String
+      | .top => "⊤"
+      | .bot => "⊥"
+      | .or φ ψ => s!"({impl φ}) ∨ ({impl ψ})"
+      | .and φ ψ => s!"({impl φ}) ∧ ({impl ψ})"
+      | .var x => s!"^{x}"
+      | .modality l args =>
+          have : FinEnum (Modalities.signature l) := Modalities.signature_finenum l
+          let argsStr := FinEnum.toList (Modalities.signature l)
+            |>.map (fun a ↦ impl (args a))
+            |> String.intercalate ", "
+          s!"{reprStr l}({argsStr})"
+      | .lfp φ => s!"μ, {impl φ}"
+      | .gfp φ => s!"ν, {impl φ}"
+    impl
+
 def not : Formula Λ → Formula Λ
   | .top             => ⊥
   | .bot             => ⊤
@@ -43,7 +61,7 @@ def not : Formula Λ → Formula Λ
 scoped notation "¬" φ:60 => Formula.not φ
 scoped infixl:25 " ⇒ " => fun φ ψ ↦ ¬φ ∨ ψ
 
-def up : Formula Λ → (start : ℕ := 1) → Formula Λ
+def up : Formula Λ → (start : ℕ := 0) → Formula Λ
   | .top,             _     => ⊤
   | .bot,             _     => ⊥
   | .or φ ψ,          start => up φ start ∨ up ψ start