The Coq mailing list

[Fritjof Bornebusch <fritjof AT uni-bremen.de>]

On Thu, May 21, 2020 at 08:27:05PM -0700, Talia Ringer wrote:
>    I guess they also give the functions for the equivalence in a  really
>    awkward form in the standard library. The equivalence between { l :
>    list T & length l = n } to vector T n will move this problem to a place
>    where it actually makes sense for it to show up.
> 
>    On Thu, May 21, 2020, 8:12 PM Talia Ringer
>    <[1]tringer AT cs.washington.edu> wrote:
> 
>    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:
>    [2]http://tlringer.github.io/pdf/ornpaper.pdf, tool:
>    [3]https://github.com/uwplse/ornamental-search), or in the univalent
>    parametricity framework ([4]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
>

Thank you for the explanation and the hint. I will take a look
at your tool.
 

--f.
>    On Thu, May 21, 2020 at 6:05 AM Fritjof Bornebusch
>    <[5]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?
> 
> References
> 
>    1. mailto:tringer AT cs.washington.edu
>    2. http://tlringer.github.io/pdf/ornpaper.pdf
>    3. https://github.com/uwplse/ornamental-search
>    4. https://arxiv.org/pdf/1909.05027.pdf
>    5. mailto:fritjof AT uni-bremen.de