coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] conversion from vector to list and back

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] conversion from vector to list and back
Date: Thu, 21 May 2020 15:05:09 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT gabriel-vm-2.zfn.uni-bremen.de
Ironport-phdr: 9a23:HcAvhx0DjiwcqHitsmDT+DRfVm0co7zxezQtwd8ZseIQKvad9pjvdHbS+e9qxAeQG9mCtrQd0rOd7v+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTqwbalvIBmrsAnduckbjIl/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+gqJVrgy8qRJ8zY7bb52aO+d8ca7GYdMWWXBMUtpNWyBdAI6xaZYEAeobPeZfqonwv1sArQG/BQmwBuPvzTFIjWLr0K09yeQhFx/J0xc9H9IVrHvUrMj+OaAcUeCvzanI0TfDb/RY2Trm9YjIdBEhreiXUrJqb8XRzFcgFwXfglqNt4PoJjWY3fkCvGaH9eRvT/6vi3I5pAFrpDii3sMhh4fVi48W11zJ+zh1zog0KNO3VkN1bsKpHYZNuy2HN4Z7QMwsTm50tSg0y7ALupG1cDUXxJknyRDSafyJfpSO7xn+V+iROS91iG9rdb+wnRq+7FSsxvPmWsS0zFpGtDdJn9vUun0OyRDf8NaLRud/80u7xzqDyR3f5vtELE00k6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk9fKn5P/9YrXnuJCcM5Z4ih/7Mqg3hMCzG+U5MgYIX2SB5OS80rzj8VTiT7VQkPI2l7fWsJbAKcsGuKG1Gw5V0oA95BajFzqqzdoVkHYdIF5YZB6LkZLlNlHSLPziEPuygUygkDJxyPDHOr3hDI/NLn/GkLr5c7Z98U9cyBYxzdBY6ZJZEawBIPTyWkPor9PYFAE2MwmqzObhEtlyy50RVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4rqaAwCW8ENV8YXpAB1qRCnzoP9GKQfYQaiWcCtJnk3kOT7WkRoln2Rz451yy8KZuMueBon5QjpnkztUgv7SOxyF3ziR9CoGm60/IT2xwmThSFTA/1rp+rEg41FLGi+5qjfoeCNpSovlTXwI3M9jQwr4iUoGgakf6Zt6MDW2ebJCjCDA1QMg2xoZTMVt7GpColB3G0izsD7JHzuXXVqxxybrV2j3KH+g402zPjfRzkl8nB8FVOGirgOhz+lqLCg==

On Thu, May 21, 2020 at 02:34:31PM +0200, Maximilian Wuttke wrote:
> On 21/05/2020 14:18, Fritjof Bornebusch wrote:
> >
> > => In environment
> > bv : BitVector_10
> > The term "Vector.of_list (Vector.to_list bv)" has type
> > "Vector.t bool (length (Vector.to_list bv))"
> > while it is expected to have type "BitVector_10".
>
> You might have to 'cast' `length (Vector.to_list bv)` to `10`. (The are
> equal, but not simply by conversion). You can try to use the function
> `cast: forall {A m} (v: t A m) {n}, m = n -> t A n`.
>
> Heads up: Some functions (including `cast` and `to_list`) in the vector
> library don't have the expected `cbn` simplification behaviour. Also,
> many obvious lemmas are missing. There are some libraries that extend
> (among others) this part of the standard library.
>
>

Thanks for the hint. Do you have a link to these libraries?

[Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/21/2020
- Re: [Coq-Club] conversion from vector to list and back, Siegfried, 05/21/2020
- Re: [Coq-Club] conversion from vector to list and back, Maximilian Wuttke, 05/21/2020
  - Re: [Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/21/2020
    - Re: [Coq-Club] conversion from vector to list and back, Talia Ringer, 05/22/2020
      - Re: [Coq-Club] conversion from vector to list and back, Talia Ringer, 05/22/2020
        
        Re: [Coq-Club] conversion from vector to list and back, Fritjof Bornebusch, 05/22/2020