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

[David Banas]

>
> 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...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200930/1e9fa290/attachment.html>