[Agda] Nat -iso- Bin

[Arseniy Alekseyev]

FWIW, there is my proof of bijection together with proofs of
equivalence for addition and multiplication:
https://github.com/Rotsor/BinDivMod
See modules Data.Bin.{Bijection, Addition, Multiplication}
Too bloated, I guess, but that's what I've got.

Cheers!

On 29 October 2013 20:00, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Tue, 2013-10-29 at 23:21 +0400, Sergei Meshveliani wrote:
>> Correction:  ``{m : ℕ} → ''
>> is not needed here.
>>
>> Also there is a question about availability of  fromℕ ∘ toℕ ≗ id,
>> fromDigits ∘ toDs ≗ id.
>>
>>
>> On Tue, 2013-10-29 at 22:51 +0400, Sergei Meshveliani wrote:
>> > Please, has  lib-0.7  something for the isomorphism  ℕ <-> Bin ?
>> >
>> > For example, I need
>> >
>> >   toDigits-suc-eq : {m : ℕ} →
>> >                     let toDs : ℕ → Bin⁺
>> >                         toDs = proj₁ ∘ toDigits 2
>> >                     in
>> >                     toDs ∘ suc ≗ (addCarryToBitList 1b ∘ toDs)
>> >
>> > Probably,      fromℕ ∘ suc ≗ Bin.suc ∘ fromℕ
>> > will also do.
>> >
>> > I think of proving  toDigits-suc-eq,  but this needs looking into a
>> > non-trivial definition of  toDigits.
>> >
>
> I hope now that
>
>   bs → fromDigits (addCarryToBitList 1b bs) \equiv (suc (fromDigits bs))
>
> is not difficult to prove -- because  fromDigits  is simpler than
> toDigits.
> I hope that then, the proof part  pr  in  toDigits m  will help with the
> proof for  toDigits-suc-eq.
>
> On the other hand, something needs to be in Standard library that easily
> gives the  suc (or _+_) isomorphism for  Nat <--> Bin, Bin⁺.
> Am I missing something?
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda