The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Hello,
 Sorry to bother everybody with an old answer, but I thought I could 
take the opportunity to point out that:
(1) the coq bugs site has been inaccessible for the past week. In 
particular, it is impossible to use the bug website to report that
bug!
(2) the bug I had reported just prior, and which I would be very 
interested to know the answer to, is: how to compile and
use files in a multi-file development, in the windows xp distribution? 
It was good to put in an installer, however, maybe there
is still some kind of path thing to do, but I didn't find a README file 
explaining what to do.
(3) by the way,  at least 2 weeks ago, the precompiled code for windows 
didn't work in the 8.1pl1 version. The previous version
8.1 did work, however I don't see how to do coqc.
Thanks for any help or suggestions!
---Carlos Simpson

Now to the question at hand:

Ethan Aubin wrote:
> Hi,  This might be an obvious question, but is 'forall (A:Set)(x y:A), 
> (x=y)=(y=x)' provable in Coq? - EA
(*** I spruced up the old script to work with the current version; see 
below for the historical context...***)
Require Ensembles.
Import Ensembles.
Inductive U : Type := pt : U.

Definition ensemble_of : Prop -> (Ensemble U) :=
fun (p:Prop) (u:U) => p.

Lemma iff_eq : forall (P Q:Prop), (P -> Q) -> (Q -> P) -> P = Q.
intros.
set (ensP := ensemble_of P).
set (ensQ := ensemble_of Q).
assert (ensP = ensQ).
apply Extensionality_Ensembles.
unfold Same_set.
unfold Included.
split; intros; unfold In.
exact (H H1). exact (H0 H1).
transitivity (ensP pt).
trivial.
transitivity (ensQ pt).
rewrite H1; trivial.
trivial.
Save.


Lemma symmetric_equality: forall (A:Set)(x y:A), (x=y)=(y=x).
intros.
apply iff_eq; intros; symmetry; assumption.
Save.

(*******************************************************************

Historical context:
Here was the original question:

[Coq-Club] How to prove (a,b:Z) a=b == b=a ? 
<http://pauillac.inria.fr/pipermail/coq-club/2003/000996.html>
/Wed, 27 Aug 2003 11:06:58 +0200/

Probably this is simple for many of you.

Unfortunately, as a beginner, I can't find a simple elegant solution 
(nor the uggly one, I must say...).

I wanted to use sym_eq , but I can't find out how to apply it to a 
subterm of the goal...

Many thanks in advance.
Jean-Yves

--
Jean-Yves Vion-Dury 

Here was my script at the time:
/Tue, 02 Sep 2003 11:16:14 +0200/

Here is a script. Of course,
Extensionality_Ensembles is an axiom but at least it is included in the
standard library
in the Ensembles section.
---Carlos Simpson

Require ZArith.
Require Ensembles.

Inductive U : Type := pt : U.

Definition ensemble_of : Prop -> (Ensemble U) :=
[p:Prop; u:U]p.

Lemma iff_eq : (P,Q:Prop)(P -> Q) -> (Q -> P) -> P == Q.
Intros.
LetTac ensP := (ensemble_of P).
LetTac ensQ := (ensemble_of Q).
Assert ensP == ensQ.
Apply Extensionality_Ensembles.
Unfold Same_set.
Unfold Included.
Split; Intros; Unfold In.
Exact (H H1). Exact (H0 H1).
Transitivity (ensP pt).
Trivial.
Transitivity (ensQ pt).
Rewrite H1; Trivial.
Trivial.
Save.

Lemma ans : (a,b:Z)(a=b) == (b=a).
Intros.
Apply iff_eq; Intros; Symmetry; Assumption.
Save.


***********************************************************)