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}

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