------------------------------------------------------------------------
-- 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  _⊕_

    _⊕_ : 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  _⊕_

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

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