[Agda] libraries for Bin

[Sergei Meshveliani]

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