1 files changed, 58 insertions, 0 deletions
diff --git a/CoalgebraicMuCalculus/Instances/Relational.lean b/CoalgebraicMuCalculus/Instances/Relational.lean
new file mode 100644
index 0000000..0b0f7fc
--- /dev/null
+++ b/CoalgebraicMuCalculus/Instances/Relational.lean
@@ -0,0 +1,58 @@
+import Mathlib
+import CoalgebraicMuCalculus.MuCalculus
+
+inductive Relational where
+  | box
+  | diamond
+  deriving Repr
+
+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 | B ∩ A () ≠ ∅ }
+
+@[simp]
+lemma lift_box_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.box Set A ↔ ∀ x ∈ B, x ∈ A () := by
+  show B ∈ { B | B ⊆ A () } ↔ ∀ x ∈ B, x ∈ A ()
+  exact Set.mem_setOf
+
+@[simp]
+lemma lift_diamond_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.diamond Set A ↔ ∃ x ∈ B, x ∈ A () := by
+  show B ∈ { B | B ∩ A () ≠ ∅ } ↔ ∃ x ∈ B, x ∈ A ()
+  rw [Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty]
+  rfl
+
+instance : LawfulModel Relational Set where
+  lifting_natural {X Y} f l := by
+    cases l
+    all_goals intro A; ext B; simp
+  lifting_monotone {X} l := by
+    cases l with
+    | box =>
+        intro A A' h B hB
+        rw [lift_box_iff]; intro x hx
+        rw [lift_box_iff] at hB
+        exact h () (hB x hx)
+    | diamond =>
+        intro A A' h B hB
+        rw [lift_diamond_iff] at hB
+        obtain ⟨x, hx⟩ := hB
+        rw [lift_diamond_iff]; use x
+        exact ⟨hx.left, h () hx.right⟩
+  lifting_dual {X} l := by
+    cases l
+    all_goals intro A; ext B; simp [Modalities.dual, Modalities.dualSignature]
+
+end Relational