Skip to content
Switch branches/tags
Go to file
Cannot retrieve contributors at this time
{- Binary natural numbers (Anders Mörtberg, Jan. 2019)
This file defines two representations of binary numbers. We prove that
they are equivalent to unary numbers and univalence is then used to
transport both programs and properties between the representations.
This is an example of how having computational univalence can be
useful for practical programming.
The first definition is [Binℕ] and the numbers are essentially lists
of 0/1 with no trailing zeroes (in little-endian format). The main
definitions and examples are:
- Equivalence between Binℕ and ℕ ([Binℕ≃ℕ]) with an equality obtained
using univalence ([Binℕ≡ℕ]).
- Addition on Binℕ defined by transporting addition on ℕ to Binℕ
([_+Binℕ_]) along Binℕ≡ℕ together with a proof that addition on Binℕ
is associative obtained by transporting the proof for ℕ ([+Binℕ-assoc]).
- Functions testing whether a binary number is odd or even in O(1)
([oddBinℕ], [evenBinℕ]) and the corresponding functions for ℕ
obtained by transport. Proof that odd numbers are not even
transported from Binℕ to ℕ ([oddℕnotEvenℕ]).
- An example of the structure identity principle for natural number
structures ([NatImpl]). We first prove that Binℕ≡ℕ lifts to natural
number structures ([NatImplℕ≡Binℕ]) and we then use this to
transport "+-suc : m + suc n ≡ suc (m + n)" from ℕ to Binℕ ([+Binℕ-suc]).
- An example of program/data refinement using the structure identity
principle where we transport a property that is infeasible to prove
by computation for ℕ ([propDoubleℕ]):
2^20 · 2^10 = 2^5 · (2^15 · 2^10)
from the corresponding result on Binℕ which is proved instantly by
refl ([propDoubleBinℕ]).
These examples are inspired from an old cubicaltt formalization:
which itself is based on an even older cubical formalization (from 2014):
The second representation is more non-standard and inspired by:
Only some of the experiments have been done for this representation,
but it has the virtue of being a bit simpler to prove equivalent to
ℕ. The same representation can be found in:
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Data.BinNat.BinNat where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Empty
open import Cubical.Relation.Nullary
data Binℕ : Type₀
data Pos : Type₀
-- Binary natural numbers
data Binℕ where
binℕ0 : Binℕ
binℕpos : Pos Binℕ
-- Positive binary numbers
data Pos where
x0 : Pos Pos
x1 : Binℕ Pos
pattern pos1 = x1 binℕ0
pattern x1-pos n = x1 (binℕpos n)
-- Note on notation:
-- We use "⇒" for functions that are equivalences (and therefore
-- they don't preserve the numerical value where the ranges don't
-- match, as with Binℕ⇒Pos).
-- We use "→" for the opposite situation (numerical value is preserved,
-- but the function is not necessarily an equivalence)
Binℕ⇒Pos : Binℕ Pos
sucPos : Pos Pos
Binℕ⇒Pos binℕ0 = pos1
Binℕ⇒Pos (binℕpos n) = sucPos n
sucPos (x0 ps) = x1-pos ps
sucPos (x1 ps) = x0 (Binℕ⇒Pos ps)
Binℕ→ℕ : Binℕ
Pos⇒ℕ : Pos
Pos→ℕ : Pos
Binℕ→ℕ binℕ0 = zero
Binℕ→ℕ (binℕpos x) = Pos→ℕ x
Pos→ℕ ps = suc (Pos⇒ℕ ps)
Pos⇒ℕ (x0 ps) = suc (doubleℕ (Pos⇒ℕ ps))
Pos⇒ℕ (x1 ps) = doubleℕ (Binℕ→ℕ ps)
posInd : {P : Pos Type₀} P pos1 ((p : Pos) P p P (sucPos p)) (p : Pos) P p
posInd {P} h1 hs ps = f ps
H : (p : Pos) P (x0 p) P (x0 (sucPos p))
H p hx0p = hs (x1-pos p) (hs (x0 p) hx0p)
f : (ps : Pos) P ps
f pos1 = h1
f (x0 ps) = posInd (hs pos1 h1) H ps
f (x1-pos ps) = hs (x0 ps) (posInd (hs pos1 h1) H ps)
Binℕ⇒Pos⇒ℕ : (p : Binℕ) Pos⇒ℕ (Binℕ⇒Pos p) ≡ Binℕ→ℕ p
Binℕ⇒Pos⇒ℕ binℕ0 = refl
Binℕ⇒Pos⇒ℕ (binℕpos (x0 p)) = refl
Binℕ⇒Pos⇒ℕ (binℕpos (x1 x)) = λ i suc (doubleℕ (Binℕ⇒Pos⇒ℕ x i))
Pos⇒ℕsucPos : (p : Pos) Pos⇒ℕ (sucPos p) ≡ suc (Pos⇒ℕ p)
Pos⇒ℕsucPos p = Binℕ⇒Pos⇒ℕ (binℕpos p)
Pos→ℕsucPos : (p : Pos) Pos→ℕ (sucPos p) ≡ suc (Pos→ℕ p)
Pos→ℕsucPos p = cong suc (Binℕ⇒Pos⇒ℕ (binℕpos p))
ℕ⇒Pos : Pos
ℕ⇒Pos zero = pos1
ℕ⇒Pos (suc n) = sucPos (ℕ⇒Pos n)
ℕ→Pos : Pos
ℕ→Pos zero = pos1
ℕ→Pos (suc n) = ℕ⇒Pos n
Pos⇒ℕ⇒Pos : (p : Pos) ℕ⇒Pos (Pos⇒ℕ p) ≡ p
Pos⇒ℕ⇒Pos p = posInd refl hs p
hs : (p : Pos) ℕ⇒Pos (Pos⇒ℕ p) ≡ p ℕ⇒Pos (Pos⇒ℕ (sucPos p)) ≡ sucPos p
hs p hp =
ℕ⇒Pos (Pos⇒ℕ (sucPos p)) ≡⟨ cong ℕ⇒Pos (Pos⇒ℕsucPos p) ⟩
sucPos (ℕ⇒Pos (Pos⇒ℕ p)) ≡⟨ cong sucPos hp ⟩
sucPos p ∎
ℕ⇒Pos⇒ℕ : (n : ℕ) Pos⇒ℕ (ℕ⇒Pos n) ≡ n
ℕ⇒Pos⇒ℕ zero = refl
ℕ⇒Pos⇒ℕ (suc n) =
Pos⇒ℕ (ℕ⇒Pos (suc n)) ≡⟨ Pos⇒ℕsucPos (ℕ⇒Pos n) ⟩
suc (Pos⇒ℕ (ℕ⇒Pos n)) ≡⟨ cong suc (ℕ⇒Pos⇒ℕ n) ⟩
suc n ∎
ℕ→Binℕ : Binℕ
ℕ→Binℕ zero = binℕ0
ℕ→Binℕ (suc n) = binℕpos (ℕ⇒Pos n)
ℕ→Binℕ→ℕ : (n : ℕ) Binℕ→ℕ (ℕ→Binℕ n) ≡ n
ℕ→Binℕ→ℕ zero = refl
ℕ→Binℕ→ℕ (suc n) = cong suc (ℕ⇒Pos⇒ℕ n)
Binℕ→ℕ→Binℕ : (n : Binℕ) ℕ→Binℕ (Binℕ→ℕ n) ≡ n
Binℕ→ℕ→Binℕ binℕ0 = refl
Binℕ→ℕ→Binℕ (binℕpos p) = cong binℕpos (Pos⇒ℕ⇒Pos p)
Binℕ≃ℕ : Binℕ ≃ ℕ
Binℕ≃ℕ = isoToEquiv (iso Binℕ→ℕ ℕ→Binℕ ℕ→Binℕ→ℕ Binℕ→ℕ→Binℕ)
-- Use univalence (in fact only "ua") to get an equality from the
-- above equivalence
Binℕ≡ℕ : Binℕ ≡ ℕ
Binℕ≡ℕ = ua Binℕ≃ℕ
sucBinℕ : Binℕ Binℕ
sucBinℕ x = binℕpos (Binℕ⇒Pos x)
Binℕ→ℕsuc : (x : Binℕ) suc (Binℕ→ℕ x) ≡ Binℕ→ℕ (sucBinℕ x)
Binℕ→ℕsuc binℕ0 = refl
Binℕ→ℕsuc (binℕpos x) = sym (Pos→ℕsucPos x)
-- We can transport addition on ℕ to Binℕ
_+Binℕ_ : Binℕ Binℕ Binℕ
_+Binℕ_ = transport (λ i Binℕ≡ℕ (~ i) Binℕ≡ℕ (~ i) Binℕ≡ℕ (~ i)) _+_
-- Test: 4 + 1 = 5
_ : binℕpos (x0 (x0 pos1)) +Binℕ binℕpos pos1 ≡ binℕpos (x1-pos (x0 pos1))
_ = refl
-- It is easy to test if binary numbers are odd
oddBinℕ : Binℕ Bool
oddBinℕ binℕ0 = false
oddBinℕ (binℕpos (x0 _)) = false
oddBinℕ (binℕpos (x1 _)) = true
evenBinℕ : Binℕ Bool
evenBinℕ n = oddBinℕ (sucBinℕ n)
-- And prove the following property (without induction)
oddBinℕnotEvenBinℕ : (n : Binℕ) oddBinℕ n ≡ not (evenBinℕ n)
oddBinℕnotEvenBinℕ binℕ0 = refl
oddBinℕnotEvenBinℕ (binℕpos (x0 x)) = refl
oddBinℕnotEvenBinℕ (binℕpos (x1 x)) = refl
-- It is also easy to define and prove the property for unary numbers,
-- however the definition uses recursion and the proof induction
oddn : Bool
oddn zero = true
oddn (suc x) = not (oddn x)
evenn : Bool
evenn n = not (oddn n)
oddnSuc : (n : ℕ) oddn n ≡ not (evenn n)
oddnSuc zero = refl
oddnSuc (suc n) = cong not (oddnSuc n)
-- So what we can do instead is to transport the odd test from Binℕ to
-- ℕ along the equality
oddℕ : Bool
oddℕ = transport (λ i Binℕ≡ℕ i Bool) oddBinℕ
evenℕ : Bool
evenℕ = transport (λ i Binℕ≡ℕ i Bool) evenBinℕ
-- We can then also transport the property
oddℕnotEvenℕ : (n : ℕ) oddℕ n ≡ not (evenℕ n)
oddℕnotEvenℕ =
let -- We first build a path from oddBinℕ to oddℕ. When i=1 this is
-- "transp (λ j → Binℕ≡ℕ j → Bool) i0 oddBinℕ" (i.e. oddℕ)
oddp : PathP (λ i Binℕ≡ℕ i Bool) oddBinℕ oddℕ
oddp i = transp (λ j Binℕ≡ℕ (i ∧ j) Bool) (~ i) oddBinℕ
-- We then build a path from evenBinℕ to evenℕ
evenp : PathP (λ i Binℕ≡ℕ i Bool) evenBinℕ evenℕ
evenp i = transp (λ j Binℕ≡ℕ (i ∧ j) Bool) (~ i) evenBinℕ
in -- Then transport oddBinℕnotEvenBinℕ in a suitable equality type
-- When i=0 this is "(n : Binℕ) → oddBinℕ n ≡ not (evenBinℕ n)"
-- When i=1 this is "(n : ℕ) → oddℕ n ≡ not (evenℕ n)"
transport (λ i (n : Binℕ≡ℕ i) oddp i n ≡ not (evenp i n)) oddBinℕnotEvenBinℕ
-- We can do the same for natural numbers:
-- First construct the path
addp : PathP (λ i Binℕ≡ℕ (~ i) Binℕ≡ℕ (~ i) Binℕ≡ℕ (~ i)) _+_ _+Binℕ_
addp i = transp (λ j Binℕ≡ℕ (~ i ∨ ~ j) Binℕ≡ℕ (~ i ∨ ~ j) Binℕ≡ℕ (~ i ∨ ~ j)) (~ i) _+_
-- Then transport associativity:
+Binℕ-assoc : m n o m +Binℕ (n +Binℕ o) ≡ (m +Binℕ n) +Binℕ o
+Binℕ-assoc =
transport (λ i (m n o : Binℕ≡ℕ (~ i))
addp i m (addp i n o) ≡ addp i (addp i m n) o) +-assoc
-- We can also define what it means to be an implementation of natural
-- numbers and use this to transport properties between different
-- implementation of natural numbers. This can be seen as a special
-- case of the structure identity principle: any property that holds
-- for one structure also holds for an equivalent one.
-- An implementation of natural numbers (i.e. a "natural number
-- structure") has a zero and successor.
record NatImpl (A : Type₀) : Type₀ where
z : A
s : A A
open NatImpl
NatImplℕ : NatImpl ℕ
z NatImplℕ = zero
s NatImplℕ = suc
NatImplBinℕ : NatImpl Binℕ
z NatImplBinℕ = binℕ0
s NatImplBinℕ = sucBinℕ
-- Using the equality between binary and unary numbers we can get an
-- equality between the two implementations of the NatImpl interface
NatImplℕ≡Binℕ : PathP (λ i NatImpl (Binℕ≡ℕ (~ i))) NatImplℕ NatImplBinℕ
z (NatImplℕ≡Binℕ i) = transp (λ j Binℕ≡ℕ (~ i ∨ ~ j)) (~ i) zero
s (NatImplℕ≡Binℕ i) =
λ x glue (λ { (i = i0) suc x
; (i = i1) sucBinℕ x })
-- We need to do use and hcomp to do and endpoint
-- correction as "suc (unglue x)" connects "suc x"
-- with "suc (Binℕ→ℕ x)" along i (which makes sense as
-- x varies from ℕ to Binℕ along i), but we need
-- something from "suc x" to "Binℕ→ℕ (sucBinℕ x)" for
-- the glue to be well-formed
(hcomp (λ j λ { (i = i0) suc x
; (i = i1) Binℕ→ℕsuc x j })
(suc (unglue (i ∨ ~ i) x)))
-- We then use this to transport +-suc from unary to binary numbers
+Binℕ-suc : m n m +Binℕ sucBinℕ n ≡ sucBinℕ (m +Binℕ n)
+Binℕ-suc =
transport (λ i (m n : Binℕ≡ℕ (~ i))
addp i m (NatImplℕ≡Binℕ i .s n) ≡ NatImplℕ≡Binℕ i .s (addp i m n)) +-suc
-- Doubling experiment: we define a notion of "doubling structure" and
-- transport a proof that is proved directly using refl for binary
-- numbers to unary numbers. This is an example of program/data
-- refinement: we can use univalence to prove properties about
-- inefficient data-structures using efficient ones.
-- Doubling structures
record Double {ℓ} (A : Type ℓ) : Type (ℓ-suc ℓ) where
-- doubling function computing 2 · x
double : A A
-- element to double
elt : A
open Double
-- Compute: 2^n · x
doubles : {ℓ} {A : Type ℓ} (D : Double A) A A
doubles D n x = iter n (double D) x
Doubleℕ : Double ℕ
double Doubleℕ = doubleℕ
elt Doubleℕ = n1024
-- 1024 = 2^8 · 2^2 = 2^10
n1024 :
n1024 = doublesℕ 8 4
-- The doubling operation on binary numbers is O(1), while for unary
-- numbers it is O(n). What is of course even more problematic is that
-- we cannot handle very big unary natural numbers, but with binary
-- there is no problem to represent very big numbers
doubleBinℕ : Binℕ Binℕ
doubleBinℕ binℕ0 = binℕ0
doubleBinℕ (binℕpos x) = binℕpos (x0 x)
DoubleBinℕ : Double Binℕ
double DoubleBinℕ = doubleBinℕ
elt DoubleBinℕ = bin1024
-- 1024 = 2^10 = 10000000000₂
bin1024 : Binℕ
bin1024 = binℕpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))
-- As these function don't commute strictly we have to prove it
-- separately and insert it in the proof of DoubleBinℕ≡Doubleℕ below
-- (just like we had to in NatImplℕ≡NatImplBinℕ
Binℕ→ℕdouble : (x : Binℕ) doubleℕ (Binℕ→ℕ x) ≡ Binℕ→ℕ (doubleBinℕ x)
Binℕ→ℕdouble binℕ0 = refl
Binℕ→ℕdouble (binℕpos x) = refl
-- We use the equality between Binℕ and ℕ to get an equality of
-- doubling structures
DoubleBinℕ≡Doubleℕ : PathP (λ i Double (Binℕ≡ℕ i)) DoubleBinℕ Doubleℕ
double (DoubleBinℕ≡Doubleℕ i) =
λ x glue (λ { (i = i0) doubleBinℕ x
; (i = i1) doubleℕ x })
(hcomp (λ j λ { (i = i0) Binℕ→ℕdouble x j
; (i = i1) doubleℕ x })
(doubleℕ (unglue (i ∨ ~ i) x)))
elt (DoubleBinℕ≡Doubleℕ i) = transp (λ j Binℕ≡ℕ (i ∨ ~ j)) i (Doubleℕ .elt)
-- We can now use transport to prove a property that is too slow to
-- check with unary numbers. We define the property we want to check
-- as a record so that Agda does not try to unfold it eagerly.
record propDouble {ℓ} {A : Type ℓ} (D : Double A) : Type ℓ where
-- 2^20 · e = 2^5 · (2^15 · e)
proof : doubles D 20 (elt D) ≡ doubles D 5 (doubles D 15 (elt D))
open propDouble
-- The property we want to prove takes too long to typecheck for ℕ:
-- propDoubleℕ : propDouble Doubleℕ
-- propDoubleℕ = refl
-- With binary numbers it is instant
propDoubleBinℕ : propDouble DoubleBinℕ
proof propDoubleBinℕ = refl
-- By transporting the proof along the equality we then get it for
-- unary numbers
propDoubleℕ : propDouble Doubleℕ
propDoubleℕ = transport (λ i propDouble (DoubleBinℕ≡Doubleℕ i)) propDoubleBinℕ
-- Alternative encoding of binary natural numbers inspired by:
-- This representation makes the equivalence with ℕ a bit easier to
-- prove, but the doubling example wouldn't work as nicely as we
-- cannot define it as an O(1) operation
data binnat : Type₀ where
zero : binnat -- 0
consOdd : binnat binnat -- 2·n + 1
consEven : binnat binnat -- 2·{n+1}
binnat→ℕ : binnat
binnat→ℕ zero = 0
binnat→ℕ (consOdd n) = suc (doubleℕ (binnat→ℕ n))
binnat→ℕ (consEven n) = suc (suc (doubleℕ (binnat→ℕ n)))
suc-binnat : binnat binnat
suc-binnat zero = consOdd zero
suc-binnat (consOdd n) = consEven n
suc-binnat (consEven n) = consOdd (suc-binnat n)
ℕ→binnat : binnat
ℕ→binnat zero = zero
ℕ→binnat (suc n) = suc-binnat (ℕ→binnat n)
binnat→ℕ-suc : (n : binnat) binnat→ℕ (suc-binnat n) ≡ suc (binnat→ℕ n)
binnat→ℕ-suc zero = refl
binnat→ℕ-suc (consOdd n) = refl
binnat→ℕ-suc (consEven n) = λ i suc (doubleℕ (binnat→ℕ-suc n i))
ℕ→binnat→ℕ : (n : ℕ) binnat→ℕ (ℕ→binnat n) ≡ n
ℕ→binnat→ℕ zero = refl
ℕ→binnat→ℕ (suc n) = (binnat→ℕ-suc (ℕ→binnat n)) ∙ (cong suc (ℕ→binnat→ℕ n))
suc-ℕ→binnat-double : (n : ℕ) suc-binnat (ℕ→binnat (doubleℕ n)) ≡ consOdd (ℕ→binnat n)
suc-ℕ→binnat-double zero = refl
suc-ℕ→binnat-double (suc n) = λ i suc-binnat (suc-binnat (suc-ℕ→binnat-double n i))
binnat→ℕ→binnat : (n : binnat) ℕ→binnat (binnat→ℕ n) ≡ n
binnat→ℕ→binnat zero = refl
binnat→ℕ→binnat (consOdd n) =
(suc-ℕ→binnat-double (binnat→ℕ n)) ∙ (cong consOdd (binnat→ℕ→binnat n))
binnat→ℕ→binnat (consEven n) =
(λ i suc-binnat (suc-ℕ→binnat-double (binnat→ℕ n) i)) ∙ (cong consEven (binnat→ℕ→binnat n))
ℕ≃binnat : ℕ ≃ binnat
ℕ≃binnat = isoToEquiv (iso ℕ→binnat binnat→ℕ binnat→ℕ→binnat ℕ→binnat→ℕ)
ℕ≡binnat : ℕ ≡ binnat
ℕ≡binnat = ua ℕ≃binnat
-- We can transport addition on ℕ to binnat
_+binnat_ : binnat binnat binnat
_+binnat_ = transport (λ i ℕ≡binnat i ℕ≡binnat i ℕ≡binnat i) _+_
-- Test: 4 + 1 = 5
_ : consEven (consOdd zero) +binnat consOdd zero ≡ consOdd (consEven zero)
_ = refl
oddbinnat : binnat Bool
oddbinnat zero = false
oddbinnat (consOdd _) = true
oddbinnat (consEven _) = false
oddℕ' : Bool
oddℕ' = transport (λ i ℕ≡binnat (~ i) Bool) oddbinnat
-- The NatImpl example for this representation of binary numbers
NatImplbinnat : NatImpl binnat
z NatImplbinnat = zero
s NatImplbinnat = suc-binnat
-- Note that the s case is a bit simpler as no end-point correction
-- is necessary (things commute strictly)
NatImplℕ≡NatImplbinnat : PathP (λ i NatImpl (ℕ≡binnat i)) NatImplℕ NatImplbinnat
z (NatImplℕ≡NatImplbinnat i) = transp (λ j ℕ≡binnat (i ∨ ~ j)) i zero
s (NatImplℕ≡NatImplbinnat i) =
λ x glue (λ { (i = i0) suc x
; (i = i1) suc-binnat x })
(suc-binnat (unglue (i ∨ ~ i) x))
oddSuc : (n : binnat) oddbinnat n ≡ not (oddbinnat (suc-binnat n))
oddSuc zero = refl
oddSuc (consOdd _) = refl
oddSuc (consEven _) = refl
oddℕSuc' : (n : ℕ) oddℕ' n ≡ not (oddℕ' (suc n))
oddℕSuc' =
let eq : (i : I) ℕ≡binnat (~ i) Bool
eq i = transp (λ j ℕ≡binnat (~ i ∨ ~ j) Bool) (~ i) oddbinnat
in transport
(λ i (n : ℕ≡binnat (~ i)) eq i n ≡ not (eq i (NatImplℕ≡NatImplbinnat (~ i) .NatImpl.s n)))