From e9ef4cb62cda496667507d47686d7e167f83a126 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Mon, 15 Jun 2026 00:01:45 +0200
Subject: relational mu calculus

---
 SymbolicModalLogic/Instances/Relational.lean | 76 ++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 SymbolicModalLogic/Instances/Relational.lean

(limited to 'SymbolicModalLogic/Instances/Relational.lean')

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
-- 
cgit v1.3.1