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,56 @@ 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ʳ _)
+
+xor-same : ∀ x → x xor x ≡ false
+xor-same false = refl
+xor-same true  = refl
+
+xor-false : ∀ x → false xor x ≡ x
+xor-false false = refl
+xor-false true  = refl
+
+xor-true : ∀ x → true xor x ≡ not x
+xor-true false = refl
+xor-true true  = refl
+
+xor-not : ∀ x → x xor (not x) ≡ true
+xor-not false = refl
+xor-not true  = refl
+
+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-commutative : ∀ x y → x xor y ≡ y xor x
+xor-commutative false false = refl
+xor-commutative false true  = refl
+xor-commutative true  false = refl
+xor-commutative true  true  = refl
+
+xor-associative : ∀ x y z → x xor (y xor z) ≡ (x xor y) xor z
+xor-associative false y z = refl
+xor-associative true  y z = not-xor y z
+
+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)