Stream: Coq users

Topic: Coercion syntax

view this post on Zulip Enzo Crance (Nov 23 2022 at 15:48):

I have a hierarchy of records R0R_0 ... RnR_n. These records are all quantified over 2 arguments (i.e. Rk x yR_k\ x\ y is the record). I declared weakening functions Rk+1RkR_{k+1} \rightarrow R_k for every kk. How can I declare that these functions are coercions, i.e. for any mnm \geq n, if Coq expects an Rn x yR_n\ x\ y I can give a Rm x yR_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 xx and yy, and how does Coq behave regarding their compositions?

view this post on Zulip 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 for details. It may be more covenenient to do this in a Section with Variables x y.

view this post on Zulip Enzo Crance (Nov 23 2022 at 16:16):

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

view this post on Zulip 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 :)

view this post on Zulip 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