coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove (a,b:Z) a=b == b=a ?

From: "Carlos.SIMPSON" <carlos AT math.unice.fr>
To: Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>
Cc: coq-club AT pauillac.inria.fr, Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>
Subject: Re: [Coq-Club] How to prove (a,b:Z) a=b == b=a ?
Date: Tue, 02 Sep 2003 11:16:14 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

Re: [Coq-Club] How to prove (a,b:Z) a=b == b=a ?, Carlos.SIMPSON