make our own union notation with ⋓ instead of ∪

(because we cannot pattern match overloaded/typeclass operators)

Pdl/Semantics.lean

@@ -43,7 +43,7 @@ mutual
   def relate {W : Type} : KripkeModel W → Program → W → W → Prop
     | M, ·c, w, v => M.Rel c w v
     | M, α;β, w, v => ∃ y, relate M α w y ∧ relate M β y v
-    | M, Program.union α β, w, v => relate M α w v ∨ relate M β w v
+    | M, α⋓β, w, v => relate M α w v ∨ relate M β w v
     | M, ∗α, w, v => StarCat (relate M α) w v
     | M, ✓φ, w, v => w = v ∧ evaluate M w φ
 end

Pdl/Syntax.lean

@@ -55,11 +55,11 @@ infixr:66 "⋀" => Formula.and
 infixr:60 "⋁" => Formula.or
 notation:55 φ:56 " ↣ " ψ:55 => ~φ ⋀ (~ψ)
 notation:55 φ:56 " ⟷ " ψ:55 => (φ↣ψ) ⋀ (φ↣φ)
-notation "⌈" α "⌉" P => Formula.box α P -- TOOD: adjust precedence to make ⌈α⌉⌈β⌉P work, or is it fine already?
+notation "⌈" α "⌉" P => Formula.box α P
 prefix:33 "†" => Formula.nstar
 
 infixl:33 ";" => Program.sequence -- TODO avoid ; which has a meaning in Lean 4
-instance : Union Program := ⟨Program.union⟩
+infixl:33 "⋓" => Program.union
 prefix:33 "∗" => Program.star
 prefix:33 "✓" => Program.test -- avoiding "?" which has a meaning in Lean 4
 
@@ -78,7 +78,7 @@ mutual
   def lengthOfProgram : Program → Nat
     | ·_ => 1
     | α;β => 1 + lengthOfProgram α + lengthOfProgram β
-    | Program.union α β => 1 + lengthOfProgram α + lengthOfProgram β
+    | α⋓β => 1 + lengthOfProgram α + lengthOfProgram β
     | ∗α => 1 + lengthOfProgram α
     | ✓φ => 1 + lengthOfFormula φ
   def lengthOfFormula : Formula → Nat
@@ -106,7 +106,7 @@ mutual
     | ·_ => 0
     | ✓ φ => 1 + mOfFormula φ
     | α;β => 1 + mOfProgram α + mOfProgram β + 1 -- TODO: max (mOfFormula φ) (mOfFormula (~φ))
-    | Program.union α β => 1 + mOfProgram α + mOfProgram β + 1
+    | α⋓β => 1 + mOfProgram α + mOfProgram β + 1
     | ∗α => 1 + mOfProgram α
   @[simp]
   def mOfFormula : Formula → Nat

Pdl/Tableau.lean

@@ -32,13 +32,13 @@ inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   -- Single-branch rules:
   | nTe {X φ ψ} (h : (~⌈✓φ⌉ψ) ∈ X) : localRule X { X \ {~⌈✓φ⌉ψ} ∪ {φ, ~ψ}} -- TODO should remove marking ?
   | nSe {X a b f} (h : (~⌈a;b⌉f) ∈ X) : localRule X { X \ {~⌈a;b⌉f} ∪ {~⌈a⌉⌈b⌉f}}
-  | uni {X a b f} (h : (⌈a∪b⌉f) ∈ X) : localRule X { X \ {⌈a∪b⌉f} ∪ {⌈a⌉ f, ⌈b⌉ f}}
+  | uni {X a b f} (h : (⌈a⋓b⌉f) ∈ X) : localRule X { X \ {⌈a⋓b⌉f} ∪ {⌈a⌉ f, ⌈b⌉ f}}
   | seq {X a b f} (h : (⌈a;b⌉f) ∈ X) : localRule X { X \ {⌈a⌉⌈b⌉f}}
   -- Splitting rules:
   | tes {X f g} (h : (⌈✓f⌉g) ∈ X) : localRule X { X \ {⌈✓f⌉g} ∪ {~f}
                                                  , X \ {⌈✓f⌉g} ∪ {g} }
-  | nUn {a b f} (h : (~⌈a ∪ b⌉f) ∈ X) : localRule X { X \ {~⌈a ∪ b⌉f} ∪ {~⌈a⌉f}
-                                                    , X \ {~⌈a ∪ b⌉f} ∪ {~⌈b⌉f} }
+  | nUn {a b f} (h : (~⌈a ⋓ b⌉f) ∈ X) : localRule X { X \ {~⌈a ⋓ b⌉f} ∪ {~⌈a⌉f}
+                                                    , X \ {~⌈a ⋓ b⌉f} ∪ {~⌈b⌉f} }
   -- STAR
   | sta {X a f} (h : (⌈∗a⌉f) ∈ X) : localRule X ({ X \ {⌈∗a⌉f} } ⊎ (listsToSets (unravel (⌈∗a⌉f))))
   | nSt {a f} (h : (~⌈∗a⌉f) ∈ X) : localRule X ({ X \ {~⌈∗a⌉f} } ⊎ (listsToSets (unravel (~⌈∗a⌉f))))

Pdl/Unravel.lean

@@ -8,20 +8,20 @@ import Pdl.Semantics
 -- | New Definition 10
 @[simp]
 def unravel : Formula → List (List Formula)
-  -- diamonds:
+  -- diamonds: ⋓
   | ~⌈·a⌉P => [[~⌈·a⌉P]]
-  | ~⌈Program.union p1 p2⌉P => unravel (~⌈p1⌉P) ∪ unravel (~⌈p2⌉P) -- no theF here. fishy?
+  | ~⌈a ⋓ b⌉P => unravel (~⌈a⌉P) ∪ unravel (~⌈b⌉P)
   | ~⌈✓ Q⌉P => [[Q]] ⊎ unravel (~P)
-  | ~⌈a;b⌉P => unravel (~⌈a⌉(⌈b⌉P))
+  | ~⌈a;b⌉P => unravel (~⌈a⌉⌈b⌉P)
   | ~†_ => ∅
-  | ~⌈∗a⌉P => {{~P}} ∪ unravel (~⌈a⌉(†⌈∗a⌉P)) -- {{~P}} was "unravel P"
+  | ~⌈∗a⌉P => {{~P}} ∪ unravel (~⌈a⌉(†⌈∗a⌉P)) -- TODO omit {{~P}} if P contains dagger
   -- boxes:
   | ⌈·a⌉P => [[⌈·a⌉ P]]
-  | ⌈Program.union a b⌉ P => unravel (⌈a⌉P) ⊎ unravel (⌈b⌉P)
+  | ⌈a ⋓ b⌉ P => unravel (⌈a⌉P) ⊎ unravel (⌈b⌉P)
   | ⌈✓ Q⌉P => [[~Q]] ∪ unravel P
-  | ⌈a;b⌉P => unravel (⌈a⌉(⌈b⌉P))
+  | ⌈a;b⌉P => unravel (⌈a⌉⌈b⌉P)
   | †P => {∅}
-  | ⌈∗a⌉P => {{P}} ⊎ unravel (⌈a⌉(†⌈∗a⌉P)) -- {{P}} was "unravel P"
+  | ⌈∗a⌉P => {{P}} ⊎ unravel (⌈a⌉(†⌈∗a⌉P)) -- TODO omit {{P}} when P contains dagger
   -- all other formulas we do nothing, but let's pattern match them all.
   | ·c => [[·c]]
   | ~·c => [[~·c]]