Paolo Giarrusso (Aug 21 2023 at 21:17): 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
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"
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
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
Christopher Lam (Aug 21 2023 at 21:25):Cool, yeah that worked! Didn't realize it would be that easy. Thanks!
Notification Bot (Aug 21 2023 at 21:44):Christopher Lam has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC