diff options
Diffstat (limited to 'SymbolicModalLogic/MuCalculus.lean')
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 22 |
1 files changed, 20 insertions, 2 deletions
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 |