Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why do section variables behave differently in a definition than its arguments with respect to tactics?

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:

https://coq.inria.fr/bugs/show_bug.cgi?id=2243

It was about destruct and not clear.


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\...



Archive powered by MHonArc 2.6.18.

Top of Page