The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Dear Frederic,

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

I'm not an intensive user of this Ensemble library. I frequently prefer 
to use my own definitions according to the problem I want to solve.
Remember that doing "set theoretical" proof in Coq is not always the 
easiest way.

However I have a script to solve your first question. (Inhabited A Car) 
is an inductive with only one constructor. It a synonym to (exists x:A, 
In x Car).

Require Export Partial_Order.
Require Export Arith.

Definition all_nat : Ensemble nat := fun _ => True.

Lemma all_nat_inhabited : Inhabited nat all_nat.
Proof.
  exists 0.
  unfold In, all_nat; trivial.
Qed.

Lemma nat_le_order : Order nat le.
Proof.
  split.
  exact le_refl.
  exact le_trans.
  exact le_antisym.
Qed.

Definition all_nat_le_PO : PO nat :=
  Definition_of_PO
    nat
    all_nat
    le
    all_nat_inhabited
    nat_le_order.



Frederic Peschanski wrote :

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

Concerning this second question, an induction is sufficient to prove 
what you want.

Require Export Relations_1.
Require Export Omega.

Section po.

Variable A : Type.
Variable R : Relation A.
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).

End po.

Lemma no_top_aux : forall n,
  ~ (forall x : nat, x <= n).
Proof.
  induction n; intro.
  generalize (H 1); omega.
  elim IHn; intros.
  generalize (H (S x)); omega.
Qed.

Theorem no_top :  ~(porder_top nat le).
Proof.
  intros (top,Htop).
  elim no_top_aux with top; assumption.
Qed.



Hope this helps,

David.