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


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

\end{code}

Definition (Minimum of binary numbers):

\begin{code}

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

\end{code}

Addition modulo 2:

\begin{code}

₁- :   
₁-  = 
₁-  = 

infixr 30 _⊕_

_⊕_ :     
  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}