coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Eugene Kirpichov <ekirpichov AT gmail.com>
To: Adam Chlipala <adamc AT hcoop.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Proofs preserved by a certain equivalence relation
Date: Sat, 16 May 2009 19:13:26 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=rR4wuYc229m3FRqbxQKLyMFtCzWosraDW8NovFYFsumzG4tiwWcwPk4/L04fcjD0PU rHUhsaM0wOrpqaUzMPQRzw8yUgHmPAJSScZhQw9ep9LJsKn6DF5xBjPUsQNUeyejyvMw zLZhzkcm8rOsA2QtnJn/py7Wt6aFOtzZwu4WY=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks!
I must say it is rather pleasant to have "discovered" setoids :)

2009/5/16 Adam Chlipala
<adamc AT hcoop.net>:
> 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
>

--
Eugene Kirpichov
Web IR developer, market.yandex.ru

[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