define alternation depth

2 files changed, 125 insertions, 146 deletions

diff --git a/SymbolicModalLogic/AlternationDepth.lean b/SymbolicModalLogic/AlternationDepth.lean
index b3b0a8e..717c928 100644
--- a/SymbolicModalLogic/AlternationDepth.lean
+++ b/SymbolicModalLogic/AlternationDepth.lean
@@ -38,157 +38,128 @@ inductive IsAlternationDepthBound : FixedPointOp → ℕ → Formula Λ → Prop
       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
+noncomputable def alternationDepth (φ : Formula Λ) : ℕ :=
+  sInf { n : ℕ | IsAlternationDepthBound .μ n φ ∧ IsAlternationDepthBound .ν n φ }
 
-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
+def Formula.closure : Formula Λ → List (ℕ × Formula Λ)
+  | .top => [(0, ⊤)]
+  | .bot => [(0, ⊥)]
+  | .or φ ψ => [(0, φ ∨ ψ)] ++ closure φ ++ closure ψ
+  | .and φ ψ => [(0, φ ∧ ψ)] ++ closure φ ++ closure ψ
+  | .modality l args =>
+      [(0, .modality l args)] ++ (Modalities.args l |>.flatMap fun a ↦ closure (args a))
+  | .var x => [(0, ^x)]
+  | .lfp φ => [(0, μ, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ))
+  | .gfp φ => [(0, ν, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ))
 
-noncomputable def alternationDepth (φ : Formula Λ) : ℕ :=
-  sInf { n : ℕ | IsAlternationDepth n φ }
+def mentionsVar (n : ℕ) : Formula Λ → Bool
+  | .top => false
+  | .bot => false
+  | .or φ ψ => mentionsVar n φ || mentionsVar n ψ
+  | .and φ ψ => mentionsVar n φ || mentionsVar n ψ
+  | .modality l args =>
+      Modalities.args l |>.any fun a ↦ mentionsVar n (args a)
+  | .var x => x == n
+  | .lfp φ => mentionsVar (n + 1) φ
+  | .gfp φ => mentionsVar (n + 1) φ
 
-private def collectOps : Formula Λ → List FixedPointOp
-  | .top => []
-  | .bot => []
-  | .or φ ψ => collectOps φ ++ collectOps ψ
-  | .and φ ψ => collectOps φ ++ collectOps ψ
+def size : Formula Λ → ℕ
+  | .top => 1
+  | .bot => 1
+  | .or φ ψ => 1 + size φ + size ψ
+  | .and φ ψ => 1 + size φ + size ψ
   | .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 φ
+      1 + (Modalities.args l |>.map (fun a ↦ size (args a)) |>.sum)
+  | .var _ => 1
+  | .lfp φ => 1 + size φ
+  | .gfp φ => 1 + size φ
 
-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
+lemma closure_mem_size (φ : Formula Λ) : ∀ {n ψ}, (n, ψ) ∈ φ.closure → size ψ ≤ size φ := by
+  intro n χ
+  induction φ generalizing n χ with
+  | top => grind [Formula.closure]
+  | bot => grind [Formula.closure]
+  | or φ ψ hφ hψ =>
+      intro h
+      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h
+      cases h with
+      | inl eq => rw [eq.right]
+      | inr h => cases h <;> grind [size]
+  | and φ ψ hφ hψ =>
+      intro h
+      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h
+      cases h with
+      | inl eq => rw [eq.right]
+      | inr h => cases h <;> grind [size]
+  | modality l args hargs =>
+      intro h
+      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_flatMap] at h
+      cases h with
+      | inl eq => rw [eq.right]
+      | inr h =>
+          obtain ⟨a, _, ha⟩ := h
+          simp only [size]
+          grw [hargs _ ha]
+          apply Nat.le_add_left_of_le
+          apply List.le_sum_of_mem
+          apply List.mem_map_of_mem
+          apply Modalities.args_mem
+  | var x => grind [Formula.closure]
+  | lfp φ hφ =>
+      intro h
+      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h
+      cases h with
+      | inl eq => rw [eq.right]
+      | inr h => obtain ⟨_, h, _⟩ := h; grind [size]
+  | gfp φ hφ =>
+      intro h
+      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h
+      cases h with
+      | inl eq => rw [eq.right]
+      | inr h => obtain ⟨_, h, _⟩ := h; grind [size]
 
-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]
+def ad : Formula Λ → ℕ
+  | .top => 0
+  | .bot => 0
+  | .or φ ψ => Nat.max (ad φ) (ad ψ)
+  | .and φ ψ => Nat.max (ad φ) (ad ψ)
+  | .modality l args =>
+      Modalities.args l
+        |>.map (fun a ↦ ad (args a))
+        |> List.foldr Nat.max 0
+  | .var _ => 0
+  | .lfp φ => Id.run do
+      let mut n := Nat.max 1 (ad φ)
+      for h : (offset, ψ) in closure φ do
+        if h' : mentionsVar offset ψ then
+          if let Formula.gfp χ := ψ then
+            n := Nat.max n (ad (ν, χ) + 1)
+      return n
+  | .gfp φ => Id.run do
+      let mut n := Nat.max 1 (ad φ)
+      for h : (offset, ψ) in closure φ do
+        if h' : mentionsVar offset ψ then
+          if let Formula.lfp χ := ψ then
+            n := Nat.max n (ad (μ, χ) + 1)
+      return n
+  termination_by φ => size φ
+  decreasing_by
+    · grind [size]
+    · grind [size]
+    · grind [size]
+    · grind [size]
+    · rw [size, Nat.lt_one_add_iff]
+      apply List.le_sum_of_mem
+      apply List.mem_map_of_mem
+      apply Modalities.args_mem
+    · grind [size]
+    · rw [show size (μ, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff]
+      apply closure_mem_size
+      exact h
+    · grind [size]
+    · rw [show size (ν, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff]
+      apply closure_mem_size
+      exact h
 
-lemma ad_isAlternationDepth (φ : Formula Λ) : IsAlternationDepth (ad φ) φ := by
+lemma ad_eq_alternationDepth (φ : Formula Λ) : ad φ = alternationDepth φ := 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/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean
index ca5b447..4722928 100644
--- a/SymbolicModalLogic/MuCalculus.lean
+++ b/SymbolicModalLogic/MuCalculus.lean
@@ -8,6 +8,14 @@ class Modalities (Λ : Type) where
   dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α)
   dual_involution : ∀ l, dual (dual l) = l
 
+def Modalities.args {Λ : Type} [Modalities Λ] (l : Λ) : List (Modalities.signature l) :=
+  have : FinEnum (signature l) := Modalities.signature_finenum l
+  FinEnum.toList (signature l)
+
+def Modalities.args_mem {Λ : Type} [Modalities Λ] (l : Λ) (a : Modalities.signature l) : a ∈ args l := by
+  rw [args]
+  apply @FinEnum.mem_toList _ (Modalities.signature_finenum l)
+
 inductive Formula (Λ : Type) [Modalities Λ] where
   | top : Formula Λ
   | bot : Formula Λ