<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">But we're talking about xor for the Word64 type, so it is slightly more<br>complicated to prove that it has a unit.</blockquote><div><br></div><div>Here's a proof in Agda:</div><div><br></div><div><font face="monospace">-- Agda proof that zero is the unit (i.e. - left and right identity)<br>-- for the XOR operation.<br><br>import Relation.Binary.PropositionalEquality as Eq<br>open        Eq       using (_≡_; refl; cong; sym)<br>open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)<br><br>-- Binary data.<br><br>data Bin : Set where<br>  ⟨⟩ : Bin<br>  _O : Bin → Bin<br>  _I : Bin → Bin<br><br>_xor_ : Bin → Bin → Bin<br>⟨⟩    xor y      =  y<br>(x O) xor ⟨⟩     =  x O<br>(x O) xor (y O)  = (x xor y) O<br>(x O) xor (y I)  = (x xor y) I<br>(x I) xor ⟨⟩     =  x I<br>(x I) xor (y O)  = (x xor y) I<br>(x I) xor (y I)  = (x xor y) O<br><br>lemma : ∀ (b : Bin)<br>    ------------<br>  → b xor ⟨⟩ ≡ b<br>lemma ⟨⟩    = refl<br>lemma (b O) = refl<br>lemma (b I) = refl<br>  <br>_ : ( ⟨⟩ I O O I O I I O )  xor<br>    ( ⟨⟩ O I I I O O O O )<br>    ----------------------<br>  ≡ ( ⟨⟩ I I I O O I I O )<br>_ = refl<br><br>-- Left & right identity proofs.<br>postulate<br>  binO : (⟨⟩ O) ≡ ⟨⟩  -- Just accomodating a syntactical nuisance.<br><br>xor-idₗ : ∀ (b : Bin)<br>    ----------------<br>  → (⟨⟩ O) xor b ≡ b<br>xor-idₗ ⟨⟩ rewrite binO  =  refl<br>xor-idₗ (b O)            =  refl<br>xor-idₗ (b I)            =  refl<br><br>xor-idᵣ : ∀ (b : Bin)<br>    ----------------<br>  → b xor (⟨⟩ O) ≡ b<br>xor-idᵣ ⟨⟩    rewrite binO     =  refl<br>xor-idᵣ (b O) rewrite lemma b  =  refl<br>xor-idᵣ (b I) rewrite lemma b  =  refl<br></font></div><div><br></div><div>-db</div><div><br></div></div>