```------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Properties.BooleanAlgebra
{b₁ b₂} (B : BooleanAlgebra b₁ b₂)
where

open BooleanAlgebra B
import Algebra.Properties.DistributiveLattice
private
open module DL = Algebra.Properties.DistributiveLattice
distributiveLattice public
hiding (replace-equality)
open import Algebra.Structures
open import Algebra.FunctionProperties _≈_
open import Algebra.FunctionProperties.Consequences
record {isEquivalence = isEquivalence}
open import Relation.Binary.EqReasoning setoid
open import Relation.Binary
open import Function
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product

------------------------------------------------------------------------
-- Some simple generalisations

∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
∨-complementˡ = comm+invʳ⇒invˡ ∨-comm ∨-complementʳ

∨-complement : Inverse ⊤ ¬_ _∨_
∨-complement = ∨-complementˡ , ∨-complementʳ

∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
∧-complementˡ = comm+invʳ⇒invˡ ∧-comm ∧-complementʳ

∧-complement : Inverse ⊥ ¬_ _∧_
∧-complement = ∧-complementˡ , ∧-complementʳ

------------------------------------------------------------------------
-- The dual construction is also a boolean algebra

∧-∨-isBooleanAlgebra : IsBooleanAlgebra _≈_ _∧_ _∨_ ¬_ ⊥ ⊤
∧-∨-isBooleanAlgebra = record
{ isDistributiveLattice = ∧-∨-isDistributiveLattice
; ∨-complementʳ         = ∧-complementʳ
; ∧-complementʳ         = ∨-complementʳ
; ¬-cong                = ¬-cong
}

∧-∨-booleanAlgebra : BooleanAlgebra _ _
∧-∨-booleanAlgebra = record
{ _∧_              = _∨_
; _∨_              = _∧_
; ⊤                = ⊥
; ⊥                = ⊤
; isBooleanAlgebra = ∧-∨-isBooleanAlgebra
}

------------------------------------------------------------------------
-- (∨, ∧, ⊥, ⊤) and (∧, ∨, ⊤, ⊥) are commutative semirings

∧-identityʳ : RightIdentity ⊤ _∧_
∧-identityʳ x = begin
x ∧ ⊤          ≈⟨ refl ⟨ ∧-cong ⟩ sym (∨-complementʳ _) ⟩
x ∧ (x ∨ ¬ x)  ≈⟨ proj₂ absorptive _ _ ⟩
x              ∎

∧-identityˡ : LeftIdentity ⊤ _∧_
∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ

∧-identity : Identity ⊤ _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ

∨-identityʳ : RightIdentity ⊥ _∨_
∨-identityʳ x = begin
x ∨ ⊥          ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-complementʳ _) ⟩
x ∨ x ∧ ¬ x    ≈⟨ proj₁ absorptive _ _ ⟩
x              ∎

∨-identityˡ : LeftIdentity ⊥ _∨_
∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ

∨-identity : Identity ⊥ _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ

∧-zeroʳ : RightZero ⊥ _∧_
∧-zeroʳ x = begin
x ∧ ⊥          ≈⟨ refl ⟨ ∧-cong ⟩ sym (∧-complementʳ _) ⟩
x ∧  x  ∧ ¬ x  ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(x ∧ x) ∧ ¬ x  ≈⟨ ∧-idempotent _ ⟨ ∧-cong ⟩ refl ⟩
x       ∧ ¬ x  ≈⟨ ∧-complementʳ _ ⟩
⊥              ∎

∧-zeroˡ : LeftZero ⊥ _∧_
∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ

∧-zero : Zero ⊥ _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤
∨-zeroʳ x = begin
x ∨ ⊤          ≈⟨ refl ⟨ ∨-cong ⟩ sym (∨-complementʳ _) ⟩
x ∨  x  ∨ ¬ x  ≈⟨ sym \$ ∨-assoc _ _ _ ⟩
(x ∨ x) ∨ ¬ x  ≈⟨ ∨-idempotent _ ⟨ ∨-cong ⟩ refl ⟩
x       ∨ ¬ x  ≈⟨ ∨-complementʳ _ ⟩
⊤              ∎

∨-zeroˡ : LeftZero ⊤ _∨_
∨-zeroˡ _ = ∨-comm _ _ ⟨ trans ⟩ ∨-zeroʳ _

∨-zero : Zero ⊤ _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ

∨-isSemigroup : IsSemigroup _≈_ _∨_
∨-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc         = ∨-assoc
; ∙-cong        = ∨-cong
}

∧-isSemigroup : IsSemigroup _≈_ _∧_
∧-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc         = ∧-assoc
; ∙-cong        = ∧-cong
}

∨-⊥-isMonoid : IsMonoid _≈_ _∨_ ⊥
∨-⊥-isMonoid = record
{ isSemigroup = ∨-isSemigroup
; identity    = ∨-identity
}

∧-⊤-isMonoid : IsMonoid _≈_ _∧_ ⊤
∧-⊤-isMonoid = record
{ isSemigroup = ∧-isSemigroup
; identity    = ∧-identity
}

∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∨_ ⊥
∨-⊥-isCommutativeMonoid = record
{ isSemigroup = ∨-isSemigroup
; identityˡ = ∨-identityˡ
; comm      = ∨-comm
}

∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∧_ ⊤
∧-⊤-isCommutativeMonoid = record
{ isSemigroup = ∧-isSemigroup
; identityˡ = ∧-identityˡ
; comm      = ∧-comm
}

∨-∧-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∨_ _∧_ ⊥ ⊤
∨-∧-isCommutativeSemiring = record
{ +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
; *-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
; distribʳ = proj₂ ∧-∨-distrib
; zeroˡ    = ∧-zeroˡ
}

∨-∧-commutativeSemiring : CommutativeSemiring _ _
∨-∧-commutativeSemiring = record
{ _+_                   = _∨_
; _*_                   = _∧_
; 0#                    = ⊥
; 1#                    = ⊤
; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
}

∧-∨-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∧_ _∨_ ⊤ ⊥
∧-∨-isCommutativeSemiring = record
{ +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
; *-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
; distribʳ = proj₂ ∨-∧-distrib
; zeroˡ    = ∨-zeroˡ
}

∧-∨-commutativeSemiring : CommutativeSemiring _ _
∧-∨-commutativeSemiring = record
{ _+_                   = _∧_
; _*_                   = _∨_
; 0#                    = ⊤
; 1#                    = ⊥
; isCommutativeSemiring = ∧-∨-isCommutativeSemiring
}

------------------------------------------------------------------------
-- Some other properties

-- I took the statement of this lemma (called Uniqueness of
-- Complements) from some course notes, "Boolean Algebra", written
-- by Gert Smolka.

private
lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
lemma x y x∧y=⊥ x∨y=⊤ = begin
¬ x                ≈⟨ sym \$ ∧-identityʳ _ ⟩
¬ x ∧ ⊤            ≈⟨ refl ⟨ ∧-cong ⟩ sym x∨y=⊤ ⟩
¬ x ∧ (x ∨ y)      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨ ∧-complementˡ _ ⟨ ∨-cong ⟩ refl ⟩
⊥ ∨ ¬ x ∧ y        ≈⟨ sym x∧y=⊥ ⟨ ∨-cong ⟩ refl ⟩
x ∧ y ∨ ¬ x ∧ y    ≈⟨ sym \$ proj₂ ∧-∨-distrib _ _ _ ⟩
(x ∨ ¬ x) ∧ y      ≈⟨ ∨-complementʳ _ ⟨ ∧-cong ⟩ refl ⟩
⊤ ∧ y              ≈⟨ ∧-identityˡ _ ⟩
y                  ∎

¬⊥=⊤ : ¬ ⊥ ≈ ⊤
¬⊥=⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _)

¬⊤=⊥ : ¬ ⊤ ≈ ⊥
¬⊤=⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _)

¬-involutive : Involutive ¬_
¬-involutive x = lemma (¬ x) x (∧-complementˡ _) (∨-complementˡ _)

deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
where
lem₁ = begin
(x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
(x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ (∧-comm _ _ ⟨ ∧-cong ⟩ refl) ⟨ ∨-cong ⟩ refl ⟩
(y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (refl ⟨ ∧-cong ⟩ ∧-complementʳ _) ⟨ ∨-cong ⟩
(refl ⟨ ∧-cong ⟩ ∧-complementʳ _) ⟩
(y ∧ ⊥) ∨ (x ∧ ⊥)              ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩
⊥ ∨ ⊥                          ≈⟨ ∨-identityʳ _ ⟩
⊥                              ∎

lem₃ = begin
(x ∧ y) ∨ ¬ x          ≈⟨ proj₂ ∨-∧-distrib _ _ _ ⟩
(x ∨ ¬ x) ∧ (y ∨ ¬ x)  ≈⟨ ∨-complementʳ _ ⟨ ∧-cong ⟩ refl ⟩
⊤ ∧ (y ∨ ¬ x)          ≈⟨ ∧-identityˡ _ ⟩
y ∨ ¬ x                ≈⟨ ∨-comm _ _ ⟩
¬ x ∨ y                ∎

lem₂ = begin
(x ∧ y) ∨ (¬ x ∨ ¬ y)  ≈⟨ sym \$ ∨-assoc _ _ _ ⟩
((x ∧ y) ∨ ¬ x) ∨ ¬ y  ≈⟨ lem₃ ⟨ ∨-cong ⟩ refl ⟩
(¬ x ∨ y) ∨ ¬ y        ≈⟨ ∨-assoc _ _ _ ⟩
¬ x ∨ (y ∨ ¬ y)        ≈⟨ refl ⟨ ∨-cong ⟩ ∨-complementʳ _ ⟩
¬ x ∨ ⊤                ≈⟨ ∨-zeroʳ _ ⟩
⊤                      ∎

deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
deMorgan₂ x y = begin
¬ (x ∨ y)          ≈⟨ ¬-cong \$ sym (¬-involutive _) ⟨ ∨-cong ⟩
sym (¬-involutive _) ⟩
¬ (¬ ¬ x ∨ ¬ ¬ y)  ≈⟨ ¬-cong \$ sym \$ deMorgan₁ _ _ ⟩
¬ ¬ (¬ x ∧ ¬ y)    ≈⟨ ¬-involutive _ ⟩
¬ x ∧ ¬ y          ∎

-- One can replace the underlying equality with an equivalent one.

replace-equality :
{_≈′_ : Rel Carrier b₂} →
(∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → BooleanAlgebra _ _
replace-equality {_≈′_} ≈⇔≈′ = record
{ _≈_              = _≈′_
; _∨_              = _∨_
; _∧_              = _∧_
; ¬_               = ¬_
; ⊤                = ⊤
; ⊥                = ⊥
; isBooleanAlgebra =  record
{ isDistributiveLattice = DistributiveLattice.isDistributiveLattice
(DL.replace-equality ≈⇔≈′)
; ∨-complementʳ         = λ x → to ⟨\$⟩ ∨-complementʳ x
; ∧-complementʳ         = λ x → to ⟨\$⟩ ∧-complementʳ x
; ¬-cong                = λ i≈j → to ⟨\$⟩ ¬-cong (from ⟨\$⟩ i≈j)
}
} where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})

------------------------------------------------------------------------
-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring

-- This construction is parameterised over the definition of xor.

module XorRing
(xor : Op₂ Carrier)
(⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y))
where

private
infixl 6 _⊕_

_⊕_ : Op₂ Carrier
_⊕_ = xor

helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v
helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v

⊕-cong : Congruent₂ _⊕_
⊕-cong {x} {y} {u} {v} x≈y u≈v = begin
x ⊕ u                ≈⟨ ⊕-def _ _ ⟩
(x ∨ u) ∧ ¬ (x ∧ u)  ≈⟨ helper (x≈y ⟨ ∨-cong ⟩ u≈v)
(x≈y ⟨ ∧-cong ⟩ u≈v) ⟩
(y ∨ v) ∧ ¬ (y ∧ v)  ≈⟨ sym \$ ⊕-def _ _ ⟩
y ⊕ v                ∎

⊕-comm : Commutative _⊕_
⊕-comm x y = begin
x ⊕ y                ≈⟨ ⊕-def _ _ ⟩
(x ∨ y) ∧ ¬ (x ∧ y)  ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩
(y ∨ x) ∧ ¬ (y ∧ x)  ≈⟨ sym \$ ⊕-def _ _ ⟩
y ⊕ x                ∎

⊕-¬-distribˡ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
⊕-¬-distribˡ x y = begin
¬ (x ⊕ y)                              ≈⟨ ¬-cong \$ ⊕-def _ _ ⟩
¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (proj₂ ∧-∨-distrib _ _ _) ⟩
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-cong \$
refl ⟨ ∨-cong ⟩
(refl ⟨ ∧-cong ⟩
¬-cong (∧-comm _ _)) ⟩
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-cong \$ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)              ≈⟨ deMorgan₁ _ _ ⟨ ∧-cong ⟩ refl ⟩
(¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)          ≈⟨ helper (refl ⟨ ∨-cong ⟩ ¬-involutive _)
(∧-comm _ _) ⟩
(¬ x ∨ y) ∧ ¬ (¬ x ∧ y)                ≈⟨ sym \$ ⊕-def _ _ ⟩
¬ x ⊕ y                                ∎
where
lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
lem x y = begin
x ∧ ¬ (x ∧ y)          ≈⟨ refl ⟨ ∧-cong ⟩ deMorgan₁ _ _ ⟩
x ∧ (¬ x ∨ ¬ y)        ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
(x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ ∧-complementʳ _ ⟨ ∨-cong ⟩ refl ⟩
⊥ ∨ (x ∧ ¬ y)          ≈⟨ ∨-identityˡ _ ⟩
x ∧ ¬ y                ∎

⊕-¬-distribʳ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y
⊕-¬-distribʳ x y = begin
¬ (x ⊕ y)  ≈⟨ ¬-cong \$ ⊕-comm _ _ ⟩
¬ (y ⊕ x)  ≈⟨ ⊕-¬-distribˡ _ _ ⟩
¬ y ⊕ x    ≈⟨ ⊕-comm _ _ ⟩
x ⊕ ¬ y    ∎

⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y
⊕-annihilates-¬ x y = begin
x ⊕ y        ≈⟨ sym \$ ¬-involutive _ ⟩
¬ ¬ (x ⊕ y)  ≈⟨ ¬-cong \$ ⊕-¬-distribˡ _ _ ⟩
¬ (¬ x ⊕ y)  ≈⟨ ⊕-¬-distribʳ _ _ ⟩
¬ x ⊕ ¬ y    ∎

⊕-identityˡ : LeftIdentity ⊥ _⊕_
⊕-identityˡ x = begin
⊥ ⊕ x                ≈⟨ ⊕-def _ _ ⟩
(⊥ ∨ x) ∧ ¬ (⊥ ∧ x)  ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩
x ∧ ¬ ⊥              ≈⟨ refl ⟨ ∧-cong ⟩ ¬⊥=⊤ ⟩
x ∧ ⊤                ≈⟨ ∧-identityʳ _ ⟩
x                    ∎

⊕-identityʳ : RightIdentity ⊥ _⊕_
⊕-identityʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-identityˡ _

⊕-identity : Identity ⊥ _⊕_
⊕-identity = ⊕-identityˡ , ⊕-identityʳ

⊕-inverseˡ : LeftInverse ⊥ id _⊕_
⊕-inverseˡ x = begin
x ⊕ x               ≈⟨ ⊕-def _ _ ⟩
(x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idempotent _) (∧-idempotent _) ⟩
x ∧ ¬ x             ≈⟨ ∧-complementʳ _ ⟩
⊥                   ∎

⊕-inverseʳ : RightInverse ⊥ id _⊕_
⊕-inverseʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-inverseˡ _

⊕-inverse : Inverse ⊥ id _⊕_
⊕-inverse = ⊕-inverseˡ , ⊕-inverseʳ

∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_
∧-distribˡ-⊕ x y z = begin
x ∧ (y ⊕ z)                ≈⟨ refl ⟨ ∧-cong ⟩ ⊕-def _ _ ⟩
x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(x ∧ (y ∨ z)) ∧ ¬ (y ∧ z)  ≈⟨ refl ⟨ ∧-cong ⟩ deMorgan₁ _ _ ⟩
(x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z)                ≈⟨ sym \$ ∨-identityˡ _ ⟩
⊥ ∨
((x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z))               ≈⟨ lem₃ ⟨ ∨-cong ⟩ refl ⟩
((x ∧ (y ∨ z)) ∧ ¬ x) ∨
((x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z))               ≈⟨ sym \$ proj₁ ∧-∨-distrib _ _ _ ⟩
(x ∧ (y ∨ z)) ∧
(¬ x ∨ (¬ y ∨ ¬ z))        ≈⟨  refl ⟨ ∧-cong ⟩
(refl ⟨ ∨-cong ⟩ sym (deMorgan₁ _ _)) ⟩
(x ∧ (y ∨ z)) ∧
(¬ x ∨ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∧-cong ⟩ sym (deMorgan₁ _ _) ⟩
(x ∧ (y ∨ z)) ∧
¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
(x ∧ (y ∨ z)) ∧
¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟨ ∧-cong ⟩
refl ⟩
((x ∧ y) ∨ (x ∧ z)) ∧
¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ sym \$ ⊕-def _ _ ⟩
(x ∧ y) ⊕ (x ∧ z)          ∎
where
lem₂ = begin
x ∧ (y ∧ z)  ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(x ∧ y) ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩
(y ∧ x) ∧ z  ≈⟨ ∧-assoc _ _ _ ⟩
y ∧ (x ∧ z)  ∎

lem₁ = begin
x ∧ (y ∧ z)        ≈⟨ sym (∧-idempotent _) ⟨ ∧-cong ⟩ refl ⟩
(x ∧ x) ∧ (y ∧ z)  ≈⟨ ∧-assoc _ _ _ ⟩
x ∧ (x ∧ (y ∧ z))  ≈⟨ refl ⟨ ∧-cong ⟩ lem₂ ⟩
x ∧ (y ∧ (x ∧ z))  ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(x ∧ y) ∧ (x ∧ z)  ∎

lem₃ = begin
⊥                      ≈⟨ sym \$ ∧-zeroʳ _ ⟩
(y ∨ z) ∧ ⊥            ≈⟨ refl ⟨ ∧-cong ⟩ sym (∧-complementʳ _) ⟩
(y ∨ z) ∧ (x ∧ ¬ x)    ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
((y ∨ z) ∧ x) ∧ ¬ x    ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl  ⟩
(x ∧ (y ∨ z)) ∧ ¬ x    ∎

∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_
∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕

∧-distrib-⊕ : _∧_ DistributesOver _⊕_
∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕

private

lemma₂ : ∀ x y u v →
(x ∧ y) ∨ (u ∧ v) ≈
((x ∨ u) ∧ (y ∨ u)) ∧
((x ∨ v) ∧ (y ∨ v))
lemma₂ x y u v = begin
(x ∧ y) ∨ (u ∧ v)              ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v)  ≈⟨ proj₂ ∨-∧-distrib _ _ _
⟨ ∧-cong ⟩
proj₂ ∨-∧-distrib _ _ _ ⟩
((x ∨ u) ∧ (y ∨ u)) ∧
((x ∨ v) ∧ (y ∨ v))            ∎

⊕-assoc : Associative _⊕_
⊕-assoc x y z = sym \$ begin
x ⊕ (y ⊕ z)                                ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩
x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z))                  ≈⟨ ⊕-def _ _ ⟩
(x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧
¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))              ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩
(((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ ∧-assoc _ _ _ ⟩
((x ∨ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ refl ⟨ ∧-cong ⟩ lem₅ ⟩
((x ∨ y) ∨ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩
(((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧
¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)              ≈⟨ sym \$ ⊕-def _ _ ⟩
((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z                  ≈⟨ sym \$ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩
(x ⊕ y) ⊕ z                                ∎
where
lem₁ = begin
((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)  ≈⟨ sym \$ proj₂ ∨-∧-distrib _ _ _ ⟩
((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈⟨ (refl ⟨ ∧-cong ⟩ sym (deMorgan₁ _ _))
⟨ ∨-cong ⟩ refl ⟩
((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎

lem₂' = begin
(x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈⟨ sym \$ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
(⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈⟨ sym \$
(∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
⟨ ∧-cong ⟩
(refl ⟨ ∧-cong ⟩ ∨-complementˡ _) ⟩
((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
((¬ x ∨ y) ∧ (¬ y ∨ y))            ≈⟨ sym \$ lemma₂ _ _ _ _ ⟩
(¬ x ∧ ¬ y) ∨ (x ∧ y)              ≈⟨ sym \$ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y)            ≈⟨ sym (deMorgan₁ _ _) ⟩
¬ ((x ∨ y) ∧ ¬ (x ∧ y))            ∎

lem₂ = begin
((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈⟨ sym \$ proj₂ ∨-∧-distrib _ _ _ ⟩
((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ lem₂' ⟨ ∨-cong ⟩ refl ⟩
¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈⟨ sym \$ deMorgan₁ _ _ ⟩
¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎

lem₃ = begin
x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∨-cong ⟩
(refl ⟨ ∧-cong ⟩ deMorgan₁ _ _) ⟩
x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
(x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-cong ⟩
sym (∨-assoc _ _ _) ⟩
((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎

lem₄' = begin
¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
(¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
((¬ y ∨ z) ∧ (¬ z ∨ z))    ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
⟨ ∧-cong ⟩
(refl ⟨ ∧-cong ⟩ ∨-complementˡ _) ⟩
(⊤ ∧ (y ∨ ¬ z)) ∧
((¬ y ∨ z) ∧ ⊤)            ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
(y ∨ ¬ z) ∧ (¬ y ∨ z)      ∎

lem₄ = begin
¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ refl ⟨ ∨-cong ⟩ lem₄' ⟩
¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
(¬ x ∨ (y     ∨ ¬ z)) ∧
(¬ x ∨ (¬ y ∨ z))              ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-cong ⟩
sym (∨-assoc _ _ _) ⟩
((¬ x ∨ y)     ∨ ¬ z) ∧
((¬ x ∨ ¬ y) ∨ z)              ≈⟨ ∧-comm _ _ ⟩
((¬ x ∨ ¬ y) ∨ z) ∧
((¬ x ∨ y)     ∨ ¬ z)          ∎

lem₅ = begin
((x ∨ ¬ y) ∨ ¬ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ sym \$ ∧-assoc _ _ _ ⟩
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩
(((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-assoc _ _ _ ⟩
((¬ x ∨ ¬ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎

⊕-isSemigroup : IsSemigroup _≈_ _⊕_
⊕-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc         = ⊕-assoc
; ∙-cong        = ⊕-cong
}

⊕-⊥-isMonoid : IsMonoid _≈_ _⊕_ ⊥
⊕-⊥-isMonoid = record
{ isSemigroup = ⊕-isSemigroup
; identity    = ⊕-identity
}

⊕-⊥-isGroup : IsGroup _≈_ _⊕_ ⊥ id
⊕-⊥-isGroup = record
{ isMonoid = ⊕-⊥-isMonoid
; inverse  = ⊕-inverse
; ⁻¹-cong  = id
}

⊕-⊥-isAbelianGroup : IsAbelianGroup _≈_ _⊕_ ⊥ id
⊕-⊥-isAbelianGroup = record
{ isGroup = ⊕-⊥-isGroup
; comm    = ⊕-comm
}

⊕-∧-isRing : IsRing _≈_ _⊕_ _∧_ id ⊥ ⊤
⊕-∧-isRing = record
{ +-isAbelianGroup = ⊕-⊥-isAbelianGroup
; *-isMonoid = ∧-⊤-isMonoid
; distrib = ∧-distrib-⊕
}

isCommutativeRing : IsCommutativeRing _≈_ _⊕_ _∧_ id ⊥ ⊤
isCommutativeRing = record
{ isRing = ⊕-∧-isRing
; *-comm = ∧-comm
}

commutativeRing : CommutativeRing _ _
commutativeRing = record
{ _+_               = _⊕_
; _*_               = _∧_
; -_                = id
; 0#                = ⊥
; 1#                = ⊤
; isCommutativeRing = isCommutativeRing
}

infixl 6 _⊕_

_⊕_ : Op₂ Carrier
x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y)

module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl)
```