coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Maximilian Wuttke <mwuttke97 AT posteo.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] conversion from vector to list and back
Date: Thu, 21 May 2020 14:34:31 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mwuttke97 AT posteo.de; spf=Pass smtp.mailfrom=mwuttke97 AT posteo.de; spf=None smtp.helo=postmaster AT mout01.posteo.de
Ironport-phdr: 9a23:9dVFVBBqiz6vis6jcrPzUyQJP3N1i/DPJgcQr6AfoPdwSPT6rsbcNUDSrc9gkEXOFd2Cra4d1qyP6vmrBDRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+roQnMq8UajotvJroswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VoA+vqQJxw4DXbo+aOvVxcaHBct0VXmdBQsRcWjZdDo+gYYYCDewMNvtYoYnnoFsOqAOzCw62C+Lgyz9Ig3723ak70+s7FwHNwQwvH88SsHTIr9X6KroZXOewzKjG0DXDc+9W2TTj54XMcB0suumMXbVrccrN10YvEBnJgUiOpoH8OT6ey+sCvXSB4eV6SeKvl3Aoqxt3ojW3wsoglInEip4Rx17K+yh3wIY7KMG8RUN/fdOpEpteuiWEOoZ5TM4sQ2Vltig7x7AJt5O2fCYExpo6yxLCaPGKcI6F6Q/gWuaJOTp0mXFodbKlixuz80Ws0OPxW8iu3FtLridJitrBu3QX2xDO5cWKS+Fx8lm/1TqTzQzf9+9JLVwymKHGMZAu2KQwmYAWsUnbHi/5hkH2jKiOe0Uh/eio9vjnbqn7qpOGL490jRr+Mrgwlcy4G+g3LxYBU3Ca+eS6yrLj4VX0TKhJg/A2iKXUsZLXKd4Vq6O4GQNY04Yu5w66Dzi80dQYmXcHLEhCeBKCl4XpPl/PIO3kDfejgFSjjjNmyvLdM735BZXNNWTDn6nmfbpn9kFT1hI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1/IIAWYPvw4/Reqit0CeTT1eLyK3QL8g+jI2Wd2OFYDYWo2qxrCMinToVqZKb3xLXwjfWUzjcJ+JDq9VNHCiZ/R5mzlBboCPDpc73Ej35hf90KZqKazY939A7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzHsPXCM72+ZzrB4kkwrR4e1Dm/VdUOdrybZJXwM9bM6OyutnF4irHBrGZcuETxCqT4f+DA==

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.

[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