relational mu calculus

3 files changed, 290 insertions, 0 deletions

diff --git a/SymbolicModalLogic.lean b/SymbolicModalLogic.lean
index e69de29..5fbdbe6 100644
--- a/SymbolicModalLogic.lean
+++ b/SymbolicModalLogic.lean
@@ -0,0 +1,2 @@
+import SymbolicModalLogic.MuCalculus
+import SymbolicModalLogic.Instances.Relational
diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean
new file mode 100644
index 0000000..840a6b5
--- /dev/null
+++ b/SymbolicModalLogic/Instances/Relational.lean
@@ -0,0 +1,76 @@
+import Mathlib
+import SymbolicModalLogic.MuCalculus
+
+inductive Relational where
+  | box
+  | diamond
+
+namespace Relational
+
+instance : Modalities Relational where
+  signature _ := Unit
+  dual
+    | .box     => .diamond
+    | .diamond => .box
+  dualSignature
+    | .box,     f => f
+    | .diamond, f => f
+  dual_involution := by intro l; cases l <;> simp
+
+instance : Model Relational Set where
+  lifting
+    | .box,     A => { B | B ⊆ A () }
+    | .diamond, A => { B | A () ∩ B ≠ ∅ }
+  lifting_natural {X Y} f
+    | .box => by simp
+    | .diamond => by
+        intro A; ext B
+        simp only [Set.mem_setOf_eq, Set.preimage_setOf_eq, Set.fmap_eq_image]
+        rw [← Set.nonempty_iff_ne_empty, ← Set.nonempty_iff_ne_empty]
+        show (∃ x, x ∈ f ⁻¹' A () ∧ x ∈ B) ↔ (∃ x, x ∈ A () ∧ x ∈ f '' B)
+        constructor
+        · intro ⟨x, h₁, h₂⟩
+          use f x; exact ⟨Set.mem_preimage.mpr h₁, Set.mem_image_of_mem f h₂⟩
+        · intro ⟨fx, h₁, h₂⟩
+          rw [Set.mem_image] at h₂
+          obtain ⟨x, hx₁, hx₂⟩ := h₂
+          use x; rw [Set.mem_preimage, hx₂]; exact ⟨h₁, hx₁⟩
+  lifting_monotone {X}
+    | .box => by
+        intro A A' h
+        simp only [Set.setOf_subset_setOf]
+        intro B hB; trans
+        · exact hB
+        · exact h ()
+    | .diamond => by
+        intro A A' h
+        simp only [Set.setOf_subset_setOf, ← Set.nonempty_iff_ne_empty]
+        intro B ⟨x, hx₁, hx₂⟩; use x
+        exact ⟨h () hx₁, hx₂⟩
+  lifting_dual {X}
+    | .box => by
+        intro A; ext B
+        simp only [Set.mem_setOf_eq, Modalities.dualSignature, ← Set.nonempty_iff_ne_empty]
+        constructor
+        · intro ⟨x, hx₁, hx₂⟩ hcontra
+          exact hcontra hx₂ hx₁
+        · show (¬(∀ x ∈ B, x ∈ (A ()).compl)) → (A () ∩ B).Nonempty
+          simp only [not_forall]
+          intro ⟨x, hx₁, hx₂⟩
+          use x
+          exact ⟨Set.not_notMem.mp hx₂, hx₁⟩
+    | .diamond => by
+        intro A; ext B
+        simp only [Modalities.dualSignature, Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty]
+        show (∀ x ∈ B, x ∈ A ()) ↔ ¬(∃ x, x ∈ (A ()).compl ∩ B)
+        rw [not_exists]
+        constructor
+        · intro h; by_contra
+          simp only [Set.mem_inter_iff, not_and, not_forall, not_not] at this
+          obtain ⟨x, hx₁, hx₂⟩ := this
+          exact hx₁ (h x hx₂)
+        · intro h x hx; by_contra
+          simp only [Set.mem_inter_iff, not_and] at h
+          exact h x this hx
+
+end Relational
diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean
new file mode 100644
index 0000000..a2e322e
--- /dev/null
+++ b/SymbolicModalLogic/MuCalculus.lean
@@ -0,0 +1,212 @@
+import Mathlib
+
+class Modalities (Λ : Type) where
+  signature : Λ → Type
+  signature_fintype : ∀ l, Fintype (signature l) := by intro; infer_instance
+  dual : Λ → Λ
+  dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α)
+  dual_involution : ∀ l, dual (dual l) = l
+
+inductive Formula (Λ : Type) [Modalities Λ] where
+  | top : Formula Λ
+  | bot : Formula Λ
+  | or : Formula Λ → Formula Λ → Formula Λ
+  | and : Formula Λ → Formula Λ → Formula Λ
+  | modality : (l : Λ) → (args : Modalities.signature l → Formula Λ) → Formula Λ
+  | var : ℕ → Formula Λ
+  | lfp : Formula Λ → Formula Λ
+  | gfp : Formula Λ → Formula Λ
+
+namespace Formula
+
+scoped notation "⊤" => Formula.top
+scoped notation "⊥" => Formula.bot
+scoped infixl:30 " ∨ " => Formula.or
+scoped infixl:35 " ∧ " => Formula.and
+scoped notation "^" n:max => Formula.var n
+scoped notation "μ, " φ => Formula.lfp φ
+scoped notation "ν, " φ => Formula.gfp φ
+
+variable {Λ : Type} [Modalities Λ]
+
+def not : Formula Λ → Formula Λ
+  | .top             => ⊥
+  | .bot             => ⊤
+  | .or φ ψ          => (not φ) ∧ (not ψ)
+  | .and φ ψ         => (not φ) ∨ (not ψ)
+  | .modality l args => .modality (Modalities.dual l) (Modalities.dualSignature l fun a ↦ not (args a))
+  | .var x           => ^x
+  | .lfp φ           => ν, not φ
+  | .gfp φ           => μ, not φ
+
+scoped notation "¬" φ:60 => Formula.not φ
+scoped infixl:25 " ⇒ " => fun φ ψ ↦ ¬φ ∨ ψ
+
+def up : Formula Λ → (start : ℕ := 1) → Formula Λ
+  | .top,             _     => ⊤
+  | .bot,             _     => ⊥
+  | .or φ ψ,          start => up φ start ∨ up ψ start
+  | .and φ ψ,         start => up φ start ∧ up ψ start
+  | .modality l args, start => .modality l fun a ↦ up (args a) start
+  | .var x,           start => if x < start then ^x else ^(x + 1)
+  | .lfp φ,           start => μ, up φ (start + 1)
+  | .gfp φ,           start => ν, up φ (start + 1)
+
+scoped notation "⇑ " φ => Formula.up φ
+
+def subst : Formula Λ → (ℕ × Formula Λ) → Formula Λ
+  | .top,             _      => ⊤
+  | .bot,             _      => ⊥
+  | .or φ ψ,          σ      => subst φ σ ∨ subst ψ σ
+  | .and φ ψ,         σ      => subst φ σ ∧ subst ψ σ
+  | .modality l args, σ      => .modality l fun a ↦ subst (args a) σ
+  | .var x,           (y, ψ) => if x < y then ^x else
+                                if x > y then ^(x - 1) else
+                                ψ
+  | .lfp φ,           (y, ψ) => μ, subst φ (y + 1, ⇑ψ)
+  | .gfp φ,           (y, ψ) => ν, subst φ (y + 1, ⇑ψ)
+
+macro_rules
+  | `($φ[$ψ/^$n]) => `(Formula.subst $φ ($n, $ψ))
+
+end Formula
+
+section Semantics
+
+class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] where
+  lifting {X : Type} (l : Λ) : (args : Modalities.signature l → Set X) → Set (F X)
+  lifting_natural {X Y : Type} (f : X → Y) (l : Λ) (args : Modalities.signature l → Set Y) :
+      (lifting l fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (lifting l args))
+  lifting_monotone {X : Type} (l : Λ) (args args' : Modalities.signature l → Set X) :
+      (∀ a, args a ⊆ args' a) → lifting l args ⊆ lifting l args'
+  lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) :
+      lifting (Modalities.dual l) (Modalities.dualSignature l args) = Set.compl (lifting l fun a ↦ Set.compl (args a))
+
+variable {Λ : Type} [Modalities Λ]
+variable {F : Type → Type} [Functor F] [LawfulFunctor F] [Model Λ F]
+
+def Environment (X : Type) : Type := ℕ → Set X
+
+namespace Environment
+
+variable {X : Type}
+
+def empty : Environment X := λ _ ↦ ∅
+
+def up (xs : Environment X) : Environment X
+  | 0     => ∅
+  | n + 1 => xs n
+
+def subst (xs : Environment X) (n : ℕ) (x : Set X) : Environment X :=
+  λ m ↦ if m = n then x else xs m
+
+scoped notation "⇑ " φ => Environment.up φ
+
+def add (x : Set X) (xs : Environment X) : Environment X := subst (⇑ xs) 0 x
+
+infixr:67 " :: " => Environment.add
+
+variable {xs : Environment X} {x y : Set X} {n m : ℕ}
+
+@[simp]
+lemma subst_eq : subst xs n x n = x := by simp [subst]
+
+@[simp]
+lemma subst_neq : m ≠ n → subst xs n x m = xs m := by intro h; simp [subst, h]
+
+@[simp]
+lemma subst_subst_eq : subst (subst xs n x) n y = subst xs n y := by
+  apply funext
+  intro m
+  by_cases h : m = n <;> simp [h]
+
+lemma subst_subst_neq : m ≠ n → subst (subst xs n x) m y = subst (subst xs m y) n x := by
+  intro hneq
+  apply funext
+  intro k
+  by_cases h₁ : k = m <;> by_cases h₂ : k = n <;> simp [h₁, h₂, hneq, Ne.symm hneq]
+
+lemma subst_up : (⇑(subst xs n x)) = subst (⇑xs) (n + 1) x := by
+  apply funext
+  intro m
+  cases m with
+  | zero   => simp [up]
+  | succ m => by_cases h : m = n <;> simp [h, up]
+
+lemma subst_add : x :: subst xs n y = subst (x :: xs) (n + 1) y := by
+  rw [add, add, subst_subst_neq, subst_up]
+  simp
+
+end Environment
+
+def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X
+  | .top,             _  => Set.univ
+  | .bot,             _  => ∅
+  | .or φ ψ,          xs => (interp γ φ xs) ∪ (interp γ ψ xs)
+  | .and φ ψ,         xs => (interp γ φ xs) ∩ (interp γ ψ xs)
+  | .modality l args, xs => γ ⁻¹' Model.lifting l fun a ↦ interp γ (args a) xs
+  | .var x,           xs => xs x
+  | .lfp φ,           xs => ⋂₀ { S | interp γ φ (S :: xs) ⊆ S }
+  | .gfp φ,           xs => ⋃₀ { S | S ⊆ interp γ φ (S :: xs) }
+
+def interp_subst_monotone {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) :
+    Monotone fun x ↦ interp γ φ (xs.subst n x) := by
+  induction φ generalizing xs n with
+  | top =>
+      intro S S' hle
+      rfl
+  | bot =>
+      intro S S' hle
+      rfl
+  | or φ ψ ihφ ihψ =>
+      intro S S' hle
+      simp only [Set.le_eq_subset, Set.union_subset_iff, interp]
+      constructor
+      · apply Set.subset_union_of_subset_left
+        exact ihφ xs n hle
+      · apply Set.subset_union_of_subset_right
+        exact ihψ xs n hle
+  | and φ ψ ihφ ihψ =>
+      intro S S' hle
+      simp only [Set.le_eq_subset, Set.subset_inter_iff, interp]
+      constructor
+      · intro x ⟨hx, _⟩
+        exact ihφ xs n hle hx
+      · intro x ⟨_, hx⟩
+        exact ihψ xs n hle hx
+  | modality l args ih =>
+      intro S S' hle
+      simp only [Set.le_eq_subset]
+      apply Set.preimage_mono
+      apply Model.lifting_monotone
+      intro a
+      exact ih a xs n hle
+  | var x =>
+      intro S S' hle
+      by_cases h : x = n
+      · simp only [interp, h, Environment.subst_eq, Set.le_eq_subset]
+        exact hle
+      · simp [h, interp]
+  | lfp φ ihφ =>
+      intro S S' hle
+      simp only [interp, Set.le_eq_subset, Set.subset_sInter_iff, Set.mem_setOf_eq]
+      intro U hU x hx
+      apply hx
+      calc
+        interp γ φ (U :: xs.subst n S) = interp γ φ ((U :: xs).subst (n + 1) S)  := by rw [Environment.subst_add]
+        _                              ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle
+        _                              = interp γ φ (U :: xs.subst n S')         := by rw [Environment.subst_add]
+        _                              ⊆ U                                       := hU
+  | gfp φ ihφ =>
+      intro S S' hle
+      simp only [interp, Set.le_eq_subset, Set.sUnion_subset_iff, Set.mem_setOf_eq]
+      intro U hU x hx
+      use U; constructor
+      · calc
+          U ⊆ interp γ φ (U :: xs.subst n S)          := hU
+          _ = interp γ φ ((U :: xs).subst (n + 1) S)  := by rw [Environment.subst_add]
+          _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle
+          _ = interp γ φ (U :: xs.subst n S')         := by rw [Environment.subst_add]
+      · exact hx
+
+end Semantics