coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?
Chronological Thread
- From: Cedric Auger <sedrikov AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?
- Date: Wed, 25 Jun 2014 09:46:48 +0200
I already reported a probably related bug in 2010:
2014-06-25 8:27 GMT+02:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:
On 24/06/2014 19:56, Jonathan wrote:
There are times when certain case analysis tactics can be used to
replace the hypothesis they are used on. For instance, something like
"induction H as [H ...]." This is convenient. However, I just noticed
that it matters as to whether H is a local hypothesis in the definition,
or if it is a section variable. As a section variable, this replacing
via intro pattern does not work - but it does still work to do this the
long way as "induction H as [H' ...]. clear H. rename H' into H."
Is this a bug or a feature? I only noticed it because it broke one of
my tactics - but I can of course just use the clear/rename workaround. I
am just curious why there might be any difference at all between the two
case.
The discrepancy between induction and clear is indeed a bug. Whether the bug is in induction or clear is not that obvious though. Not so long ago (I haven't tested if it is still true), it was possible to write ill-formed proofs by clearing section variables. Fortunately, Coq would catch the issue at Qed, but still this was hardly satisfactory. Worse, clearing section variables would also cause Coq to reject some well-formed proofs.
Best regards,
Guillaume
--
.../Sedrikov\...
- [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?, Jonathan, 06/24/2014
- Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?, Guillaume Melquiond, 06/25/2014
- Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?, Cedric Auger, 06/25/2014
- Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?, Guillaume Melquiond, 06/25/2014
Archive powered by MHonArc 2.6.18.