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 #-}

module Two where

open import SetsAndFunctions
open import CurryHoward
open import Equality

data  : Set where
  : 
  : 

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

two-induction : {A :   Prp}  A   A   ∀(x : )  A x
two-induction r s  = r
two-induction r s  = s


two-cases : {A : Set}  A  A    A
two-cases = two-induction


two-equality-cases : {A : Prp}  ∀{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₁ : Prp}  ∀{b : }  (b    A₀)  (b    A₁)  A₀ + A₁
two-equality-cases' {A₀} {A₁} {} f₀ f₁ = in₀(f₀ refl)
two-equality-cases' {A₀} {A₁} {} f₀ f₁ = in₁(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 : )  Prp
a  b = a    b  

_≥_ : (a b : )  Prp
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 = r
Lemma[min₂ab≡₁→b≡₁] {a} {} 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 = in₁ r
max₂-lemma  b r = in₀ refl

max₂-lemma-converse : (a b : )  a   + b    max₂ a b   
max₂-lemma-converse  b (in₀ r) = unique-from-∅ (zero-is-not-one r)
max₂-lemma-converse  b (in₁ 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 (cong  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}