I have such error message: The term "imap fEmbedding l" has type "ilist domain' (relation_arities L R)" while it is expected to have type "ilist domain' (relation_arities L' (fRelations H R))"
I have proof that relation_arities L R = relation_arities L' (fRelations H R)
. How can I use it to get rid of the error message?
Temporary (?) thing I did was to define function "aux" that transforms "ilist domain' (relation_arities L R)" to "ilist domain' (relation_arities L' (fRelations H R))" and use "imap fEmbedding (aux l)" instead of "imap fEmbedding l".
I looked what's inside the "aux" function and learned, hopefully, how to use eq_rect.
That's the right way to do it, and it does make reasoning harder, it's a known big drawback of dependent types.
The parameters to eq_rect
can be difficult to remember; there's a notation rew H in x
(in analogy to rewriting) from the standard library which makes eq_rect
easier to write and read. See https://github.com/tchajed/coq-tricks/blob/master/src/RewNotation.v for a working example.
Last updated: Oct 13 2024 at 01:02 UTC