Stream: Coq users

Topic: ✔ Problem reasoning with the return type of a vector func...


view this post on Zulip Pablo (Apr 22 2024 at 15:30):

I am using vector because this function is part of a larger project that relies on a set of definitions that use vectors. However, I will definitely talk to my supervisor to see whether the tuples type that is suggested in the comment you have sent me are more suitable to our project.
Nevertheless, I would like to know if there is a fix, since changing the definitions of vector to tuple is might be a change that I am not allowed to get done. Thank you for your comment.

view this post on Zulip Pierre Roux (Apr 22 2024 at 15:37):

You have to understand what is the structure of (2 * n_var) and mimick it in you function (for instance replacing [] with [] ++ []), but that's very painful. Another alternative is to use something else than (2 * _) but that's probably equally painful. Otherwise you need some explicit casts with proof terms, painful too.

view this post on Zulip Gaëtan Gilbert (Apr 22 2024 at 15:39):

you may find it easier to define by going through proof mode:

Fixpoint add_zeros {n_var} : t Z n_var -> t Z (2*n_var).
Proof.
destruct n_var as [|n_var'].
- intros _; exact nil.
- ...
Defined.

you will likely need to rewrite 2 * (S n) into S (2 * n + 1), do Print add_zeros after the Defined to see what got generated if you want to know how to do it by hand.

although tbh I wouldn't write that fixpoint, instead I would concatenate the input vector and the constant vector of the right length (cf About Vector.const)

view this post on Zulip Pablo (Apr 22 2024 at 15:56):

Thank you both for your answers. I realized that the function I was trying to define is excessively complex, given that I can do what @Gaëtan Gilbert suggested. Anyway, thank you for your thoughts. :)

view this post on Zulip Notification Bot (Apr 22 2024 at 15:56):

Pablo has marked this topic as resolved.

view this post on Zulip Josh K (Apr 23 2024 at 20:38):

ex_03_spinlock.v
Can anyone give code for lemma parallel_incr_locked_spec from above file


Last updated: Jun 23 2024 at 05:02 UTC