The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The most proper solution would be to introduce special mode such that when it 
turned on, every section variable would always generalize, even if it is not 
used.

I propose this syntax:

Set AllSectionVariables True.

(maybe not the best syntax, but you've got the idea).

Maybe it will be useful to turn it on by default in a future version of Coq?

We need also to put a comment with agreed solution to 
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2642

14.11.2011, 19:21, "Alexandre Pilkiewicz" 
<alexandre.pilkiewicz AT polytechnique.org>:
> 2011/11/14 Adam Chlipala 
> <adamc AT csail.mit.edu>:
>
>>  I'm surprised that [C2] has type [C], so I think Victor has a legitimate
>>  point here.  The usual section behavior rules imply to me that [C2] should
>>  be parametrized over [Other].
>
> No, definitions in section only generalize the Variables that are used
> in the body of the definition (or its type). When you admit the proof,
> you don't use Other, so it is not generalized. Changing this would
> break tons of codes!
>
> That being said, when defining a lemma, it would be nice to be able to
> specify which variable are "used" whether they are or not. This is
> useful when you want to accelerate compilation of your .v files by
> removing the body of all proofs and replacing them by Admitted. But
> the issue is known, and Arthur Charguéraud already proposed solution
> to it.
>
> Cheers,
> Alexandre
>
>>  On the other hand, the specific proposition used for [Other] is 
>> dangerously
>>  close to inconsistent (easily implies [False] for any interesting choice 
>> of
>>  [Q]), so there may be other serious issues in the code.
>>
>>  Victor Porton wrote:
>>>  See also this my bug report:
>>>
>>>  http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2642
>>>
>>>  14.11.2011, 18:58, "Thomas 
>>> Braibant"<thomas.braibant AT gmail.com>:
>>>>   - C2 has type "C"
>>>>   - whatever the type of ax2, you cannot apply C to it, because "C" is
>>>>   not a function type.
>>>>   - it happens that "ax2 C" as type "Q num", but since your whole script
>>>>   does not has much sense to me, I cannot assume that it was what you
>>>>   wanted to write.
>>>>
>>>>   Cheers,
>>>>   thomas
>>>>
>>>>   On Mon, Nov 14, 2011 at 3:41 PM, Victor 
>>>> Porton<porton AT narod.ru>
>>>>   wrote:
>>>>>    Hypothesis P: nat->Prop.
>>>>>    Hypothesis Q: nat->Prop.
>>>>>
>>>>>    Axiom Eq: forall x:nat, P(x)<->Q(x).
>>>>>
>>>>>    Class C := {
>>>>>     num: nat;
>>>>>     cond: P num
>>>>>    }.
>>>>>
>>>>>    Section sect.
>>>>>     Hypothesis Other: forall obj:C, Q num.
>>>>>
>>>>>     Instance C2: C := { num:=0 }.
>>>>>     Proof. Admitted.
>>>>>    End sect.
>>>>>
>>>>>    Axiom ax2: forall obj:C, Q num.
>>>>>
>>>>>    Definition C3 := C2(ax2).

-- 
Victor Porton - http://portonvictor.org