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}

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