Add more properties for xor

CHANGELOG.md

@@ -1985,10 +1985,18 @@ Other minor changes
   <-wellFounded : WellFounded _<_
   ∨-conicalˡ : LeftConical false _∨_
   ∨-conicalʳ : RightConical false _∨_
-  ∨-conical : Conical false _∨_
+  ∨-conical  : Conical false _∨_
   ∧-conicalˡ : LeftConical true _∧_
   ∧-conicalʳ : RightConical true _∧_
-  ∧-conical : Conical true _∧_
+  ∧-conical  : Conical true _∧_
+  xor-same-false    : ∀ x → x xor x ≡ false
+  xor-false-neutral : ∀ x → false xor x ≡ x
+  xor-true-not      : ∀ x → true xor x ≡ not x
+  xor-not-true      : ∀ x → x xor (not x) ≡ true
+  not-xor           : ∀ x y → not (x xor y) ≡ (not x) xor y
+  not-xor-cancel    : ∀ x y → (not x) xor (not y) ≡ x xor y
+  xor-commutative   : ∀ x y → x xor y ≡ y xor x
+  xor-associative   : ∀ x y z → x xor (y xor z) ≡ (x xor y) xor z
   ```
 
 * Added new functions in `Data.Fin.Base`:

src/Data/Bool/Properties.agda

@@ -627,20 +627,7 @@ true  <? _     = no  (λ())
   }
 
 ------------------------------------------------------------------------
--- Properties of _xor_
-
-xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
-xor-is-ok true  y = refl
-xor-is-ok false y = sym (∧-identityʳ _)
-
-xor-∧-commutativeRing : CommutativeRing 0ℓ 0ℓ
-xor-∧-commutativeRing = ⊕-∧-commutativeRing
-  where
-  open BooleanAlgebraProperties ∨-∧-booleanAlgebra
-  open XorRing _xor_ xor-is-ok
-
-------------------------------------------------------------------------
--- Miscellaneous other properties
+-- Properties of not
 
 not-involutive : Involutive not
 not-involutive true  = refl
@@ -660,6 +647,64 @@ not-¬ {false} refl ()
 ¬-not {false} {true}  _   = refl
 ¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)
 
+------------------------------------------------------------------------
+-- Properties of _xor_
+
+xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
+xor-is-ok true  y = refl
+xor-is-ok false y = sym (∧-identityʳ _)
+
+not-xor : ∀ x y → not (x xor y) ≡ (not x) xor y
+not-xor false y = refl
+not-xor true  y = not-involutive _
+
+not-xor-cancel : ∀ x y → (not x) xor (not y) ≡ x xor y
+not-xor-cancel false y = not-involutive _
+not-xor-cancel true  y = refl
+
+xor-true : ∀ x → true xor x ≡ not x
+xor-true false = refl
+xor-true true  = refl
+
+xor-assoc : Associative _xor_
+xor-assoc true  y z = sym (not-xor y z)
+xor-assoc false y z = refl
+
+xor-comm : Commutative _xor_
+xor-comm false false = refl
+xor-comm false true  = refl
+xor-comm true  false = refl
+xor-comm true  true  = refl
+
+xor-identityˡ : LeftIdentity false _xor_
+xor-identityˡ _ = refl
+
+xor-identityʳ : RightIdentity false _xor_
+xor-identityʳ false = refl
+xor-identityʳ true  = refl
+
+xor-identity : Identity false _xor_
+xor-identity = xor-identityˡ , xor-identityʳ
+
+xor-inverseˡ : LeftInverse true not _xor_
+xor-inverseˡ false = refl
+xor-inverseˡ true = refl
+
+xor-inverseʳ : RightInverse true not _xor_
+xor-inverseʳ x = xor-comm x (not x) ⟨ trans ⟩ xor-inverseˡ x
+
+xor-inverse : Inverse true not _xor_
+xor-inverse = xor-inverseˡ , xor-inverseʳ
+
+xor-∧-commutativeRing : CommutativeRing 0ℓ 0ℓ
+xor-∧-commutativeRing = ⊕-∧-commutativeRing
+  where
+  open BooleanAlgebraProperties ∨-∧-booleanAlgebra
+  open XorRing _xor_ xor-is-ok
+
+------------------------------------------------------------------------
+-- Miscellaneous other properties
+
 ⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
 ⇔→≡ {true } {true }         hyp = refl
 ⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp ⟨$⟩ refl)