[destruct H] in a section can fail to clear [H] · Issue #2901 · rocq-prover/rocq · GitHub

Contributor Author

coqbot commented Sep 11, 2012 •

edited by Zimmi48

Loading

Comment author: @ntc2

Created attachment 356
Coq file with simple examples illustrating the bug (examples same in the description).

Using [destruct H] in a [Section] can fail to clear [H]. Outside of a section [H] is always cleared.

This bug is the real cause of the tactic loop in the
[firstorder'] example in CPDT (Ch 14.2 in the current draft).

Here is a simplified example of the problem (also included as attached .v file), tested in Coq 8.3pl4 on GNU/Linux:

(* Outside of a [Section] there is no problem *)
Theorem p :
forall (P Q : Prop), P /\ Q -> P.
   intros P Q H.
   destruct H. (* clears [H] as expected *)
   Abort.

(* But inside a [Section] there is a problem *)
Section section1.
   Variables P Q : Prop.
   Hypothesis H : P /\ Q.
   Theorem p : P.
     destruct H. (* does *not* clear [H] !!! ??? *)
     Abort.
End section1.

(* The problem goes away if rename [H] to [H'] *)
Section section2.
   Variables P Q : Prop.
   Hypothesis H : P /\ Q.
   Theorem p : P.
     rename H into H'.
     destruct H'. (* clears [H'] as expected *)
     Abort.
End section2.

(* But remains if we rename [H] identically *)
Section section3.
   Variables P Q : Prop.
   Hypothesis H : P /\ Q.
   Theorem p : P.
     rename H into H.
     destruct H. (* does *not* clear [H] !!! ??? *)
     Abort.
End section3.

Bug BZ#2243 may be related.

Attached file: destruct_in_section_bug_simplified.v (application/octet-stream, 1153 bytes)
Description: Coq file with simple examples illustrating the bug (examples same in the description).