# [Haskell-cafe] I think I discovered my first Monoid instance

David Banas capn.freako at gmail.com
Wed Sep 30 18:52:56 UTC 2020

```>
> But we're talking about xor for the Word64 type, so it is slightly more
> complicated to prove that it has a unit.

Here's a proof in Agda:

-- Agda proof that zero is the unit (i.e. - left and right identity)
-- for the XOR operation.

import Relation.Binary.PropositionalEquality as Eq
open        Eq       using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

-- Binary data.

data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin

_xor_ : Bin → Bin → Bin
⟨⟩    xor y      =  y
(x O) xor ⟨⟩     =  x O
(x O) xor (y O)  = (x xor y) O
(x O) xor (y I)  = (x xor y) I
(x I) xor ⟨⟩     =  x I
(x I) xor (y O)  = (x xor y) I
(x I) xor (y I)  = (x xor y) O

lemma : ∀ (b : Bin)
------------
→ b xor ⟨⟩ ≡ b
lemma ⟨⟩    = refl
lemma (b O) = refl
lemma (b I) = refl

_ : ( ⟨⟩ I O O I O I I O )  xor
( ⟨⟩ O I I I O O O O )
----------------------
≡ ( ⟨⟩ I I I O O I I O )
_ = refl

-- Left & right identity proofs.
postulate
binO : (⟨⟩ O) ≡ ⟨⟩  -- Just accomodating a syntactical nuisance.

xor-idₗ : ∀ (b : Bin)
----------------
→ (⟨⟩ O) xor b ≡ b
xor-idₗ ⟨⟩ rewrite binO  =  refl
xor-idₗ (b O)            =  refl
xor-idₗ (b I)            =  refl

xor-idᵣ : ∀ (b : Bin)
----------------
→ b xor (⟨⟩ O) ≡ b
xor-idᵣ ⟨⟩    rewrite binO     =  refl
xor-idᵣ (b O) rewrite lemma b  =  refl
xor-idᵣ (b I) rewrite lemma b  =  refl

-db
-------------- next part --------------
An HTML attachment was scrubbed...