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.

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.

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`

)

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. :)

Pablo has marked this topic as resolved.

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