The Coq mailing list

[Bruno Barras <Bruno.Barras AT inria.fr>]

Hello,

> I'm working with the "Naive Set Theory in Coq". Naively, I think that
> two
> partial orders with the same carrier and the same order are equals. But
> It
> isn't (doesn't seem to be) provable in Coq. Shouldn't you add the
> following
> axiom to the "Naive Set Theory in Coq" ?
> 
> Axiom Extensionality_PO: (U:Type)(E,F:(PO U))
>   (Carrier_of U E)==(Carrier_of U F)->
>   (Rel_of U E)==(Rel_of U F)->
>   E==F.

In Sophia-Antipolis/Cours-de-Coq/podefs, PO is defined as a record
with 4 fields:
 - a carrier C
 - a relation R
 - a proof that C is non-empty
 - a proof that R is an order

Your statement says that if the first two components of E and F are
equal, then E and F are equal. This is consistent if you can't
discriminate between proofs of Non_empty and Order.

If you assume proof irrelevence (two proofs of a same statement are equal),
you can prove your statement:

Axiom proof_irrelevence: (A:Prop)(p1,p2:A)p1==p2.
Lemma Extensionality_PO: (U:Type)(E,F:(PO U))
  (Carrier_of U E)==(Carrier_of U F)->
  (Rel_of U E)==(Rel_of U F)->
  E==F.
Intro U.
Destruct E; Intros CE RE NE OE.
Destruct F; Intros CF RF NF OF.
Simpl; Intros eqC eqR.
Generalize NF OF; Clear NF OF.
Elim eqC; Elim eqR; Intros NF OF.
Elim proof_irrelevence with (Non_empty U CE) NE NF.
Elim proof_irrelevence with (Order U RE) OE OF.
Reflexivity.
Save.

The proof irrelevence above has been shown consistent, but not
provable. If you could prove it, you would be able to prove its
version stated in Set (all you can prove in Prop can be proved in
Set), which is inconsistent:

Axiom proof_irrelevence_set: (A:Set)(p1,p2:A)p1==p2.

implies that true==false. But we can prove ~true==false, thanks to the
strong elimination principle. Fortunately, strong elimination is not
allowed for inductive objects living in Prop, such as Non_empty and
Order.

So, you can safely add the axiom Extensionality_PO, if you need
it. Since it's an axiom, you should add it only when needed. It
appeared that the authors of the contribution didn't need it...

Regards,

Bruno Barras.

-- 
  Projet Coq - INRIA Rocquencourt
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://pauillac.inria.fr/~barras