coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 axiomSince this axiom is still inconsistent with Coq, it may be a good idea to avoid it ;).
Extensionality_Ensembles, you have A = B as soon as you have Same_set A B.
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.
- [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Amin Timany, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Guillaume Melquiond, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Robbert Krebbers, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/10/2014
Archive powered by MHonArc 2.6.18.