Martin Escardo 2011.

This module defines the set 𝟚 of binary numbers with elements ₀
and ₁, and a number of operations and relations on them.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Two where

open import SpartanMLTT

data 𝟚 : U where
  : 𝟚
  : 𝟚

zero-is-not-one :   
zero-is-not-one ()

𝟚-induction : {A : 𝟚  U}  A   A   (x : 𝟚)  A x
𝟚-induction r s  = r
𝟚-induction r s  = s


𝟚-cases : {A : U}  A  A  𝟚  A
𝟚-cases = 𝟚-induction


two-equality-cases : {A : U}  {b : 𝟚}  (b    A)  (b    A)  A
two-equality-cases {A} {} f₀ f₁ = f₀ refl
two-equality-cases {A} {} f₀ f₁ = f₁ refl

two-equality-cases' : {A₀ A₁ : U}  {b : 𝟚}  (b    A₀)  (b    A₁)  A₀ + A₁
two-equality-cases' {A₀} {A₁} {} f₀ f₁ = inl(f₀ refl)
two-equality-cases' {A₀} {A₁} {} f₀ f₁ = inr(f₁ refl)


Lemma[b≡₁→b≢₀] : {b : 𝟚}  b    b  
Lemma[b≡₁→b≢₀] r s = zero-is-not-one(Lemma[x≡y→y≡z→y≡z] s r)


Lemma[b≢₀→b≡₁] : {b : 𝟚}  b    b  
Lemma[b≢₀→b≡₁] f = two-equality-cases (∅-elim  f)  r  r) 

Lemma[b≢₁→b≡₀] : {b : 𝟚}  b    b  
Lemma[b≢₁→b≡₀] f = two-equality-cases  r  r) (∅-elim  f)

Lemma[b≡₀→b≢₁] : {b : 𝟚}  b    b  
Lemma[b≡₀→b≢₁] r s = zero-is-not-one(Lemma[x≡y→y≡z→y≡z] r s)


Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] : {a b : 𝟚}  (a    b  )  b    a  
Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] f = Lemma[b≢₁→b≡₀]  (contra-positive f)  Lemma[b≡₀→b≢₁]


Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] : {a b : 𝟚}  (a    b  )  b    a  
Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] f = Lemma[b≢₀→b≡₁]  (contra-positive f)  Lemma[b≡₁→b≢₀]

\end{code}

 Definition (Natural order of binary numbers):

\begin{code}

_≤_ : (a b : 𝟚)  U
a  b = a    b  

_≥_ : (a b : 𝟚)  U
a  b = b  a

min𝟚 : 𝟚  𝟚  𝟚
min𝟚  b = 
min𝟚  b = b

Lemma[minab≤a] : {a b : 𝟚}  min𝟚 a b   a
Lemma[minab≤a] {} {b} r = ∅-elim(Lemma[b≡₁→b≢₀] r refl)
Lemma[minab≤a] {} {b} r = refl

Lemma[min𝟚ab≡₁→b≡₁]  : {a b : 𝟚}  min𝟚 a b    b  
Lemma[min𝟚ab≡₁→b≡₁] {} {} r = r
Lemma[min𝟚ab≡₁→b≡₁] {} {} r = refl
Lemma[min𝟚ab≡₁→b≡₁] {} {} r = r
Lemma[min𝟚ab≡₁→b≡₁] {} {} r = refl

Lemma[min𝟚ab≡₁→a≡₁]  : {a b : 𝟚}  min𝟚 a b    a  
Lemma[min𝟚ab≡₁→a≡₁] {} r = r
Lemma[min𝟚ab≡₁→a≡₁] {} r = refl


max𝟚 : 𝟚  𝟚  𝟚
max𝟚  b = b
max𝟚  b = 

max𝟚-lemma : (a b : 𝟚)  max𝟚 a b    a   + b  
max𝟚-lemma  b r = inr r
max𝟚-lemma  b r = inl refl

max𝟚-lemma-converse : (a b : 𝟚)  a   + b    max𝟚 a b   
max𝟚-lemma-converse  b (inl r) = unique-from-∅ (zero-is-not-one r)
max𝟚-lemma-converse  b (inr r) = r
max𝟚-lemma-converse  b x = refl

\end{code}

Addition modulo 2:

\begin{code}

₁- : 𝟚  𝟚
₁-  = 
₁-  = 

infixr 31 _⊕_

_⊕_ : 𝟚  𝟚  𝟚
  x = x
  x = ₁- x

Lemma[b⊕b≡₀] : {b : 𝟚}  b  b  
Lemma[b⊕b≡₀] {} = refl
Lemma[b⊕b≡₀] {} = refl

Lemma[b≡c→b⊕c≡₀] : {b c : 𝟚}  b  c  b  c  
Lemma[b≡c→b⊕c≡₀] {b} {c} r = trans (ap  d  b  d) (sym r)) (Lemma[b⊕b≡₀] {b})

Lemma[b⊕c≡₀→b≡c] : {b c : 𝟚}  b  c    b  c
Lemma[b⊕c≡₀→b≡c] {} {} r = refl
Lemma[b⊕c≡₀→b≡c] {} {} ()
Lemma[b⊕c≡₀→b≡c] {} {} () 
Lemma[b⊕c≡₀→b≡c] {} {} r = refl

Lemma[b≢c→b⊕c≡₁] : {b c : 𝟚}  b  c  b  c  
Lemma[b≢c→b⊕c≡₁] = Lemma[b≢₀→b≡₁]  (contra-positive Lemma[b⊕c≡₀→b≡c])

Lemma[b⊕c≡₁→b≢c] : {b c : 𝟚}  b  c    b  c
Lemma[b⊕c≡₁→b≢c] =  (contra-positive Lemma[b≡c→b⊕c≡₀])  Lemma[b≡₁→b≢₀]  

\end{code}