The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 23/11/2011 20:12, Victor Porton a écrit :
> 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.

What do you mean by "known to be true" ? If you have a proof p of P, 
then you can use p wherever you want.

Parameter P: Prop.


(* I assume P *)
Hypothesis p: P.

(* P's still "true" *)

Theorem t: P.
Proof p.

Theorem t' : P /\ P.
Proof (conj p p).




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