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}

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