The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

In general, this happens with dependent types when you are dealing with some kind of equivalence. If two types are equivalent, you can find functions that get you back and forth that are mutual inverses, so:

f : A -> B

g : B -> A

where two properties called section and retraction hold:

section: forall a, g (f a) = a

retraction: forall b, f (g b) = b

But note that these properties don't hold definitionally. You must prove section and retraction hold, and then you rewrite by it in order to get the type you actually want. So the Coq specification is correct.

This problem of dealing with equivalent types is called "transport," and it's hard. It is easier in homotopy type theory, or in my tool DEVOID for some types like lists and vectors (paper: http://tlringer.github.io/pdf/ornpaper.pdf, tool: https://github.com/uwplse/ornamental-search), or in the univalent parametricity framework (https://arxiv.org/pdf/1909.05027.pdf).

If you want to do these conversions yourself, without using any external tools at all, your best bet is to prove section and retraction, and then rewrite by those. But it will suck. I really recommend using a tool for this kind of thing.

Talia

On Thu, May 21, 2020 at 6:05 AM Fritjof Bornebusch <fritjof AT uni-bremen.de> wrote:

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?