The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Jesper,

23.11.2011, 23:03, "Jesper Louis Andersen" 
<jesper.louis.andersen AT gmail.com>:
> On Wed, Nov 23, 2011 at 19:56, Victor Porton
>
>> šTheorem t: True.
>
> This is much easier to solve than you think:

You've misunderstood my question. My question is not how to prove [True], but 
how in a proof context to take an arbitrary proof of some proposition known 
to be true.

I used [Theorem True.] just as an example to set a proof context.

> Print I.
>
> Theorem t : True.
> ššexact I.
> Qed.
>
> True is constructed as an inductive type with only one inhabitant, I.
> Thus, if we want to prove True, we can just provide I since it is a
> construction of the sole True value.
>
> Note that in Coq, unlike mathematics, there are several ways to
> express something being "True". This is, among other things, to avoid
> hitting into Goedel, halting theorems, computability limitations and
> so on. Others can describe this way better than I.
>
> --
> J.

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