diff options
Diffstat (limited to 'SymbolicModalLogic')
| -rw-r--r-- | SymbolicModalLogic/AlternationDepth.lean | 194 | ||||
| -rw-r--r-- | SymbolicModalLogic/Instances/Relational.lean | 1 | ||||
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 22 |
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 |