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