The Coq mailing list

[Eugene Kirpichov <ekirpichov AT gmail.com>]

Hello.

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.

I thought that it would be cool to use a meta-technique that allows to
judge about properties preserved by an equivalence relation.

Suppose that R is an equivalence relation on type T.

Then let's say that the algebra ALG of proofs of certain properties
about objects of type T, defined as

Inductive ALG : T->Prop := ...

 is preserved by R if

 forall (theorem:ALG) (a b:T), R a b -> theorem a -> theorem b.

Then, for FSet, I could define an algebra that would describe proofs
that only use the abstract properties of FSetInterface and are
preserved by FSetInterface.eq, I'd prove that this algebra is indeed
preserved by it, and probably I could create something like my own
rewrite tactic for FSetInterface.eq afterwards.

However, although it sounds cool, I am afraid that this would be a
huge lot of work, and I don't even know where to start.

Are there any similar formalizations at which I could have a look for
inspiration? Is this sort of thing actually tractable and practical
enough?

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