Stream: Coq devs & plugin devs

Topic: When does `destruct H` not clear `H`?


view this post on Zulip Janno (Mar 28 2024 at 17:24):

I've been debugging a loop in repeat match goal with | H : _ /\ _ |- _ => destruct H end for a while. I already know I can work around it with repeat match goal with | H : _ /\ _ |- _ => revert H; case; intros end but I would like to understand under which circumstances destruct behaves this way. Does anybody happen to know?

view this post on Zulip Guillaume Melquiond (Mar 28 2024 at 18:12):

If H is a section variable, it will not be cleared. I do not know if there are other cases.

view this post on Zulip Janno (Mar 28 2024 at 18:17):

H is not a section variable but there might have been a section variable called H that got renamed to make room for the new H.

view this post on Zulip Janno (Mar 28 2024 at 18:17):

I wonder if the logic to detect if something is a section variable knows that section variables can be renamed

view this post on Zulip Janno (Mar 28 2024 at 18:20):

It does not..

Section Test.
 Context (H : True).
 Goal True /\ True -> True.
 Proof.
   intros H'. rename H into H0. rename H' into H.
   Fail Timeout 1 repeat match goal with [ H : _ /\ _ |- _ ] => destruct H end.

view this post on Zulip Janno (Mar 28 2024 at 18:20):

@Guillaume Melquiond thank you. You solved the mystery!

view this post on Zulip Janno (Mar 28 2024 at 18:27):

Reported in https://github.com/coq/coq/issues/18858


Last updated: Oct 13 2024 at 01:02 UTC