restructureHEADmain

1 files changed, 0 insertions, 58 deletions

diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean
deleted file mode 100644
index 81d428d..0000000
--- a/SymbolicModalLogic/Instances/Relational.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-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