Stream: Coq users

Topic: How to use proof of equality?

view this post on Zulip Lessness (Oct 21 2020 at 23:42):

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?

view this post on Zulip Lessness (Oct 22 2020 at 00:05):

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".

view this post on Zulip Lessness (Oct 22 2020 at 00:12):

I looked what's inside the "aux" function and learned, hopefully, how to use eq_rect.

view this post on Zulip Li-yao (Oct 22 2020 at 00:20):

That's the right way to do it, and it does make reasoning harder, it's a known big drawback of dependent types.

view this post on Zulip Tej Chajed (Oct 22 2020 at 13:57):

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 for a working example.

Last updated: Jan 29 2023 at 05:03 UTC