From 9d6710fe2397182e92c5b7bad8facf1f80cf5686 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Mon, 22 Jul 2024 18:21:35 +0200
Subject: [PATCH] idea to define the semEquiv Quotient

---
 Pdl/SemQuot.lean   | 25 +++++++++++++++++++++++++
 Pdl/Semantics.lean | 20 +++++++++++++-------
 2 files changed, 38 insertions(+), 7 deletions(-)
 create mode 100644 Pdl/SemQuot.lean

diff --git a/Pdl/SemQuot.lean b/Pdl/SemQuot.lean
new file mode 100644
index 0000000..80c1aa4
--- /dev/null
+++ b/Pdl/SemQuot.lean
@@ -0,0 +1,25 @@
+
+import Pdl.Semantics
+
+/-! ## Semantic Quotients -/
+
+#print semEquiv
+
+def semEquiv.Equivalence : Equivalence semEquiv :=
+  ⟨ by convert semEquiv.refl
+  , by convert semEquiv.symm
+  , by convert semEquiv.trans ⟩
+  -- (why) are the "by convert" needed here?
+
+instance Formula.instSetoid : Setoid Formula := ⟨semEquiv, semEquiv.Equivalence⟩
+
+-- How should I name this?
+abbrev SemProp := Quotient Formula.instSetoid
+
+-- Now, can we lift connectives such as ~ and ⋀ to the quotient?
+
+def SemProp.neg : SemProp → SemProp :=
+  Quotient.map Formula.neg (by sorry)
+
+def SemProp.and : SemProp → SemProp → SemProp :=
+  Quotient.map₂ Formula.and (by sorry)
diff --git a/Pdl/Semantics.lean b/Pdl/Semantics.lean
index d51f59f..cd70830 100644
--- a/Pdl/Semantics.lean
+++ b/Pdl/Semantics.lean
@@ -90,13 +90,19 @@ theorem notsatisfnotThenTaut : ∀ φ, ¬ satisfiable (~φ) → tautology φ :=
 theorem subsetSat {M : KripkeModel W} {w : W} {X Y : List Formula} : (∀ φ ∈ X, evaluate M w φ) → Y ⊆ X → ∀ φ ∈ Y, evaluate M w φ :=
   by aesop
 
-theorem semEquiv.transitive : Transitive semEquiv :=
-  by
-  unfold Transitive
-  unfold semEquiv
-  intro f g h f_is_g g_is_h W M w
-  specialize f_is_g W M w
-  specialize g_is_h W M w
+theorem semEquiv.refl : Reflexive semEquiv := by
+  tauto
+
+theorem semEquiv.symm : Symmetric semEquiv := by
+  intro φ1 φ2 hyp
+  intro W M w
+  specialize hyp W M w
+  tauto
+
+theorem semEquiv.trans : Transitive semEquiv := by
+  intro _ _ _ hyp1 hyp2 W M w
+  specialize hyp1 W M w
+  specialize hyp2 W M w
   tauto
 
 class vDash (α : Type) (β : Type) where