[Agda] libraries for Bin

[Anton Trunov]

Sure, we can chat about Coq packages, but let’s do that off the Agda mailing list! :)

Best,
Anton

> On 4 Jul 2018, at 14:52, 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?
>> 
> 
> Somewhere there:    BinNatDef, ZArith, NArith.
> 
> I shall try to repeat the search when I get to appropriate machine. 
> 
> 
> By the way, can you inform me, please, what is a common way to find
> materials on the packages or methods in Coq ? 
> Typically, there is announced a package Foo in Coq, and it refers to the
> code (written, may be, in Gallina, I do not know), and I see this code.
> But where is a reference to the method explanation, to comments, to
> manual on the package, to papers, to books?
> A program package is somehow supposed to have a manual on this package.
> 
> I wonder of what I am missing.
> May be binary naturals are too simple to provide it with comments, but
> there are many other quite involved packages.
> 
> For example, when one programs factoring an integer, one is supposed to
> add a comment: the theory is described in this paper <reference>, and
> the algorithm is taken from <reference>, its evaluation cost is O(foo),
> and this estimation is proved in <reference>.
> 
> Can you, please, explain: how is this organized in Coq packages?
> 
> Regards,
> 
> ------
> Sergei
> 
> 
> 
>> This representation seems to be admitting only unique representations:
>> https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
>> 
>> Best regards,
>> Anton Trunov
>> 
>>> 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