The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

I think the intended behavior of rewrite is to always create a proof term that uses eq_rect.

If you don't want an eq_rect, I would, given a definitional rewrite that replaces lhs with rhs in H, just do "change lhs with rhs in H".

Or if you insist that you want to use the rewrite tactic to determine the new type T of H, you could do the rewrite in a throw-away subgoal and pass T back to the original goal using an evar, and then do "change T in H" in the original goal. Demo based on your gist:

https://gist.github.com/samuelgruetter/d50c05b46e58412948eca13e6f67cc63

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <aa755 AT pm.me>
Sent: Monday, October 10, 2022 11:03 PM
To: coq-club
Subject: [Coq-Club] rewrite clears hypotheses in evar's context

 

As shown in the lemma test1 here (https://gist.github.com/aa755/1ebc84dc22108fecccfe1ceedb33066e),

rewriting in a hypothesis that existed when an evar was created results in the deletion of that hypothesis from the context of that evar. 

More surprisingly, this happens even when the rewrite uses a definitional equation, as shown in the lemma test2 in the page linked above.

In this case, it seems trivial for Coq to not clear the hypothesis.

Even when the rewrite is with a non-definitional equality, can Coq not insert eq_rect​ at appropriate places to avoid dropping the hypothesis from the context of the evar?

--

Abhishek Anand