[Agda] libraries for Bin

[Martin Escardo]

On 02/07/18 10:46, mechvel at botik.ru wrote:
> Also I look now into Coq Standard library, the part for binary natural.
> Generally, Coq shows the code, and it is difficult to find any reference
> to the related papers, docs. May be, this particular subject is too
> simple for a paper, but one page `readme' is desirable.
> 
> Looking at the code, I have an impression that the Bin data is defined
> there with the constructors
> 
>                              0#, double, suc-double.
> 
> `double' constructs any even number, suc-double any odd number.
> I suspect that this way binary arithmetic is expressed simpler.
> Only zero is not uniquely represented. But this can be fixed by
> introducing four constructors instead.

I have a very simple binary naturals library with *unique* 
representations, and which allows linear addition.


http://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html

data 𝔹 : Set where
  zero : 𝔹
  l    : 𝔹 → 𝔹
  r    : 𝔹 → 𝔹

The interpretation function is

unary : 𝔹 → ℕ
unary zero = zero
unary(l m) = L(unary m)
unary(r m) = R(unary m)

where

double : ℕ → ℕ
double zero    = zero
double(succ n) = succ(succ(double n))

L : ℕ → ℕ
L n = succ(double n)

R : ℕ → ℕ
R n = succ(L n)

This interpretation function is an equivalence in the sense of HoTT/UF. 
Its inverse is easy to define:

Succ : 𝔹 → 𝔹
Succ zero  = l zero
Succ(l m)  = r m
Succ(r m)  = l(Succ m)

binary : ℕ → 𝔹
binary zero    = zero
binary(succ n) = Succ(binary n)

I am sure people must have considered this isomorphic representation of 
the natural numbers, though, because it is very simple and natural.

Martin