Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Facts about Ensembles

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Facts about Ensembles


Chronological Thread 
  • From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Facts about Ensembles
  • Date: Wed, 09 Jul 2014 15:47:34 +0200

On 07/09/2014 03:37 PM, Guillaume Melquiond wrote:
This kind of transformation is pointless. Because of the axiom
Extensionality_Ensembles, you have A = B as soon as you have Same_set A B.
Since this axiom is still inconsistent with Coq, it may be a good idea to avoid it ;).

Anyway, making it work with setoids is easy: just declare Same_set as an equivalence relation, and prove that all operations on it respect it.

Require Import Ensembles Setoid Morphisms.

Instance: forall U, Equivalence (Same_set U).
Proof. firstorder. Qed.
Instance: forall U, Proper (Same_set U ==> eq ==> iff) (In U).
Proof. intros U A B ? x y ->; firstorder. Qed.

Goal forall U A B x, Same_set U A B -> In U A x -> In U B x.
Proof. intros U A B x H. rewrite H. easy. Qed.



Archive powered by MHonArc 2.6.18.

Top of Page