relational mu calculus

1 files changed, 76 insertions, 0 deletions

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