start formalizing alternation depth

1 files changed, 194 insertions, 0 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