import Mathlib
import SymbolicModalLogic.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