The Coq mailing list

[Vincent Cremet <vincent.cremet AT epfl.ch>]

On Mon, 7 Aug 2006, Frederic Peschanski wrote:

> Dear all,

Hi,

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

Actually, you can do a constructive proof for proving your second
property. For instance, as follows.

----------------------------------------------------------
Require Import Arith.

Section PO.

  Variable A : Type.
  Definition Relation := A -> A -> Prop.
  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).

End PO.

Lemma no_top_in_nat: ~(porder_top nat le).

Proof.
  unfold not.
  unfold porder_top.
  intros.
  induction H.
  absurd (S x <= x).
  apply le_Sn_n. trivial.
Qed.
------------------------------------------------------------

Vincent Cremet.