1 files changed, 33 insertions, 52 deletions
diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean
index 840a6b5..4c9155b 100644
--- a/SymbolicModalLogic/Instances/Relational.lean
+++ b/SymbolicModalLogic/Instances/Relational.lean
@@ -20,57 +20,38 @@ instance : Modalities Relational where
 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
+    | .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