I have a hierarchy of records $R_0$ ... $R_n$. These records are all quantified over 2 arguments (*i.e.* $R_k\ x\ y$ is the record). I declared weakening functions $R_{k+1} \rightarrow R_k$ for every $k$. How can I declare that these functions are coercions, *i.e.* for any $m \geq n$, if Coq expects an $R_n\ x\ y$ I can give a $R_m\ x\ y$ and it inserts the composition of weakening functions?

In the documentation and examples, I have found simple coercions such as `nat >-> bool`

, or getting a field by giving a record (projection as a coercion), but what about a family of coercions for any arguments $x$ and $y$, and how does Coq behave regarding their compositions?

Maybe `Coercion Rkp1_to_Rk : Rkp1 >-> Rk.`

if `Rkp1_to_Rk : forall x y, Rkp1 x y -> Rk x y`

is your weakening function. See https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html for details. It may be more covenenient to do this in a `Section`

with `Variables x y`

.

Ok now I understand the syntax around `>->`

on the right hand side of the colon. Thanks!

If perchance your weakening functions simply "forget" every part of R_{n+1} except an instance of R_n, then you can automatically insert the coercion as follows:

```
Record Rn1 x y := {Rn_of_Rn1 :> Rn; bla : foo;}
```

(note the `:>`

instead of a simple `:`

)

@Ana de Almeida Borges I believe it's not an option in Enzo's case

Last updated: Sep 23 2023 at 14:01 UTC