From d63be9758d9d83bc9320bed4ab73a81c92c815e4 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Sat, 20 Jun 2026 15:57:49 +0200
Subject: start formalizing alternation depth

---
 SymbolicModalLogic/MuCalculus.lean | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'SymbolicModalLogic/MuCalculus.lean')

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
-- 
cgit v1.3.1