The Coq mailing list

[Frederic Peschanski <Frederic.Peschanski AT lip6.fr>]

Dear all,

I am relatively new to the coq assistant so please forgive my probably 
naive questions.
They relate to simple investigations about partial orders I am doing 
(mainly to learn coq).

In a first attempt, I use very simple definitions for POs, similar to 
the ones in Relations_1
Now, I see in the coq libraries that there is a Partial_order module.
It defines a record type integrating the carrier set,
the relation and two POSet conditions PO_cond1 and PO_cond2.
The first condition deals with Ensembles and I do not really see how
I may, for example, prove that nat is Inhabited ...  (I use (nat,le) as 
a prototype PO)
In fact, I do not really understand what Inhabited means.
So my first question is: how would I prove that (nat,le) is a partial 
order in this
setting ?

More generally, is there a place where I could learn about the
Ensembles part of the standard library ?  The library itself has few 
comments
to help me, and so is the Coq'Art.

The second question is more practical, I define bottom and top, e.g.:

Variable A : Type.
Variable R : Relation.
Definition porder_bottom : Prop :=
exists bottom : A, forall x : A, (R bottom x).
Definition porder_top : Prop :=
exists top : A, forall x : A, (R x top).

I can prove easily that (nat,le) as O as bottom, but I cannot prove
that it has no top (i.e ~(porder_top nat le) )
In classical reasoning, I would prove that forall y:nat, exists x:nat, 
~(le x y)
and use this to contradict the existence of a top.
But even with Classical imported, I cannot do the proof.

I wonder if there is some paper/document/tutorial on the use of classical
reasoning in Coq ?

Thanks in advance,
Frédéric Peschanski.