[Agda] libraries for Bin

[Anton Trunov]

The file you linked uses `N` type from https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html as
the underlying implementation.
I think that the comments explaining the representation are quite clear but let me retell the story a bit.

Inductive positive : Set :=
  | xI : positive -> positive
  | xO : positive -> positive
  | xH : positive.

defines essentially a list of bits (in reverse order): a_0 a_1 … a_n 1
which can be interpreted as a positive natural number.

To introduce the non-negative numbers the library uses yet another datatype:

Inductive N : Set :=
  | N0 : N
  | Npos : positive -> N.

This ensures that each natural number has unique representation.
It looks like the Coq devs did it this way to reuse `positive` type for binary integers.

The `succ_double` and `double` definitions you mentioned are functions on N type.

I hope it helps. You can get more insights about Coq asking on
Coq Club mailing list, Reddit (/r/Coq), Stackoverflow (`coq` tag), IRC (freenode, #coq), functionalprogramming.slack.com (#coq), the Telegram Dependent Types group,
or feel free to drop me a personal email (I don’t want to keep spamming the Agda list with Coq).

Best,
Anton

> On 5 Jul 2018, at 13:25, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 
> On Tue, 2018-07-03 at 22:18 +0200, Anton Trunov wrote:
>> Hi Sergei,
>> 
>> What part of the Coq Standard library have you looked into?
>> 
>> This representation seems to be admitting only unique representations:
>> https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
>> 
> 
> 
> I was looking at 
> https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNatDef.html
> 
> There it is written
>  Operation x -> 2*x+1
> 
>  Definition succ_double x :=
>   match x with
>   | 0 => 1
>   | pos p => pos p~1
>   end.
> 
>  Operation x -> 2*x
> 
>  Definition double n :=
>   match n with
>   | 0 => 0
>   | pos p => pos p~0
>   end.
>  ...
> 
> I do not know Coq, nor its language Gallina.
> I thought that  double and suc_double  are constructors for a data type
> of Bin(ary natural).
> But probably they are not (?).
> 
> And where I have seen  0#  -- I do not recall, probably I have
> `invented' it.
> 
> Generally: looking at this www page, and in other Coq pages, I cannot
> guess how natural numbers are represented in Coq Standard library in the
> binary system.
> 
> Can anybody, please, explain shortly ? 
> 
> ------
> Sergei
> 
> 
> 
>>> On 3 Jul 2018, at 22:06, Sergei Meshveliani <mechvel at botik.ru> wrote:
>>> 
>>> 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.
>>>>> 
>>>>> `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    : 𝔹 → 𝔹
>>>> [..]
>>> 
>>> 
>>> For me, it is easier to understand what is written at the referred page:
>>> 
>>> The isomorphic copy is formally constructed from 0 iterating the
>>> functions L(n)=2n+1 and R(n)=2n+2.
>>> 
>>> So: instead of       0#, double, suc-double     of Coq  
>>> (not unique for 0)
>>> there are suggested  0#, 2n+1, 2n+2
>>> 
>>> -- zero, arbitrary odd, arbitrary non-zero even. 
>>> This represents Bin uniquely.
>>> 
>>> Looks nicer!
>>> Thank you.
>>> 
>>> ------
>>> Sergei
>>> 
>>> 
>>> 
>>> 
>>>> 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
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>> 
>>> 
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda