I have a hierarchy of records ... . These records are all quantified over 2 arguments (i.e. is the record). I declared weakening functions for every . How can I declare that these functions are coercions, i.e. for any , if Coq expects an I can give a 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 and , 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: Oct 13 2024 at 01:02 UTC