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