The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

2011/11/14 Victor Porton 
<porton AT narod.ru>:
> Yes, it is provable. But it isn't obvious for Coq prover. It is what I need 
> with the purpose of testing, to make some statement which is to be proved 
> explicitly.
>
> I don't think that it would prove "P x" for an arbitrary x. I am just 
> playing around with testing different features of Coq.
>
> Alexandre, thanks for your information, but you haven't answered my 
> question: How to prove [Instance C2]?

Ok, this is my last email to you, since you never read them, never try
to think that maybe you are wrong, and never even try to THINK.

Yes, it would prove P x for an arbitrary x, I showed you how, with a
proof of False. So I answered your question: you CANNOT prove Instance
C2, because it would mean that Coq is very trivially inconsistant, and
it's not.

Now, you said:

2011/11/8 Victor Porton 
<porton AT narod.ru>:
> This is my last message sent before I look into exercises.

but also
2011/11/11 Victor Porton 
<porton AT narod.ru>
> For now, I pause my using and learning of Coq until the next release, 
> because dealing with bugs is not what I want to do.


I really think you should stick with both.

Alexandre