Stream: Coq users

Topic: ✔ Rewriting by an equality within a dependent term


view this post on Zulip Paolo Giarrusso (Aug 21 2023 at 21:17):

the context you give is ill-typed (unless a1 and a2 are definitionally equal), and the right answer might depend on how you fix it...
but regardless — you can't convince Coq that H is definitionally equal to eq_refl — OTOH, if H appears in the goal then rewrite H2; simpl could help

view this post on Zulip Christopher Lam (Aug 21 2023 at 21:20):

a1 and a2 are definitionally equal - I'm effectively trying to rewrite by something like "2 = 1 + 1"

view this post on Zulip Paolo Giarrusso (Aug 21 2023 at 21:21):

can't you use change to replace a1 with a2 then? if H/H2 don't appear in the goal, just clear H H2

view this post on Zulip Paolo Giarrusso (Aug 21 2023 at 21:22):

the syntax is change a1 with a2 https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.change

view this post on Zulip Christopher Lam (Aug 21 2023 at 21:25):

Cool, yeah that worked! Didn't realize it would be that easy. Thanks!

view this post on Zulip Notification Bot (Aug 21 2023 at 21:44):

Christopher Lam has marked this topic as resolved.


Last updated: Jun 18 2024 at 20:02 UTC