The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Dear David,

Thanks for your answer, but your answer is not a solution of my problem but a 
sly trick: instead of solving my problem you use an already stated fact 
P_true.

In order to get a proper solution I reformulate the problem in such a way 
that this trick becomes impossible (I hope).

[[[[
Parameter P: Prop.

Theorem t: P -> True.
proof.
  assume P.
  let X be such that (X : P).
end proof. Qed.
]]]]

The "let" statement does not work with the error message:

Error: In environment
_hyp : P
X : P
The term "X:P" has type "P" which should be Set, Prop or Type.

How to circumvent this problem? I need an arbitrary proof [X] of an assumed 
true proposition.

24.11.2011, 03:02, "David Pichardie" 
<david.pichardie AT inria.fr>:
> Hi Victor,
>
> Here the proof term of the statement "P" is "P_true" itself. Curry Howard 
> is behind the curtain.
>
> If this is really your question then I think it is time to read the Coq Art 
> book.
>
> Regards,
>
> David.
>
> Le 23 nov. 2011 à 13:56, Victor Porton a écrit :
>
>>  We should be able to take a proof of a true proposition. Is it 
>> implemented in Coq 8.3.pl2? My native attempt to do this steps on an error.
>>
>>  [[[[
>>  Parameter P: Prop.
>>
>>  Axiom P_true: P.
>>
>>  Theorem t: True.
>>  proof.
>>   let X be such that (X : P).
>>  end proof. Qed.
>>  ]]]]
>>
>>  Error: In environment
>>  X : P
>>  The term "X:P" has type "P" which should be Set, Prop or Type.
>>
>>  I hope Coq allows to get around this, but I'm not sure.
>>
>>  --
>>  Victor Porton - http://portonvictor.org

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