[Agda] libraries for Bin

[Sergei Meshveliani]

On Tue, 2018-07-03 at 11:29 +0100, Martin Escardo wrote:
> 
> 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.
                                                            (I)
> > 
> > `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
                                -- (II)
>   zero : 𝔹
>   l    : 𝔹 → 𝔹
>   r    : 𝔹 → 𝔹
> 
> [..] 


1) I have improved the representation  0#, double, suc-double
   to  
   0#, 
   2suc    -- (2(n+1)),
   suc2*   -- (1+2n)              (III),

and this has produced the library  
    https://github.com/mechvel/Binary-4

2) I have come to the representation III due to misunderstanding of a
certain part of the Coq documentation. In fact, Coq represents Bin very
differently. 

3) Now, returning to Martin's letter, I see that my III differs from II
only in constructor renaming.  

So that I apologize.
And I need to say that 

  my Binary-4 uses the Bin representation that have been used earlier 
  by Martin Escardo

(the algorithms implementation is done independently).
Due to not paying enough attention to Martin's letter, I used the
representation III without understanding that it repeats II.

Regards,

------
Sergei