coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofs preserved by a certain equivalence relation

From: Adam Chlipala <adamc AT hcoop.net>
To: Eugene Kirpichov <ekirpichov AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Proofs preserved by a certain equivalence relation
Date: Sat, 16 May 2009 11:09:59 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Eugene Kirpichov wrote:

I'm doing some proofs with FSet and FMap, and I run a lot into the
problem that I can't use the 'rewrite' tactic or alike, because some
sets are related only by FSetInterface.eq, not by the global eq.

The setoid facility sounds very similar to what you're suggesting, and it's been included with Coq for a while.
http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual030.html

[Coq-Club] Proofs preserved by a certain equivalence relation, Eugene Kirpichov
- Re: [Coq-Club] Proofs preserved by a certain equivalence relation, Adam Chlipala
  - Re: [Coq-Club] Proofs preserved by a certain equivalence relation, Eugene Kirpichov