Stream: Coq users

Topic: Morphisms for identity and composition?


view this post on Zulip Shea Levy (Oct 31 2020 at 20:08):

There are straightforward instances of Proper (R ==> R) (λ x, x) and, assuming f and g are proper, Proper (R₁ ==> R₃) (λ x, g (f x)). Do I need to declare these or are the tactics smart enough to find them?

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:17):

no, but

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:18):

if you _name_ g (f x), yes. stdpp’s solve_proper finds those. the stdlib has a solve_proper, but I never tried it.

view this post on Zulip Paolo Giarrusso (Oct 31 2020 at 20:19):

but otherwise, rewrite will search separately for instances for f and g


Last updated: Jan 28 2023 at 05:02 UTC