[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?
> 
> 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