The Coq mailing list

[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).
>>>>
>
>