## Stream: Coq users

### Topic: Coercion syntax

#### Enzo Crance (Nov 23 2022 at 15:48):

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?

#### Pierre Roux (Nov 23 2022 at 16:07):

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.

#### Enzo Crance (Nov 23 2022 at 16:16):

Ok now I understand the syntax around >-> on the right hand side of the colon. Thanks!

#### Ana de Almeida Borges (Nov 23 2022 at 16:25):

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

#### Cyril Cohen (Nov 23 2022 at 17:08):

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

Last updated: Jan 27 2023 at 01:03 UTC