The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  Pierre-Marie is right, you need to inform the tactic at least how to build reflexivity proofs for eqLinProp (when a rewrite doesn't change some argument, a reflexivity is needed). Otherwise CoLoR contains a fairly rich library on multisets with a setoid rewriting setup.

Cheers,
-- Matthieu

Le lun. 11 mai 2015 à 07:04, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> a écrit :

On 11/05/2015 02:40, Katherine Ye wrote:
> Any help would be appreciated.

It seems that you're lacking the definition of eqLinProp as an
equivalence relation...

> Other suggestions about ways to represent the environment, which is a
> set that can contain the same element multiple times, are also
> welcome. (I considered Ensembles and ListSet, but they were missing
> things. Maybe lists with permutations?)

I made a proof of completeness of phase semantics once, using lists up
to permutations. It is here.

https://github.com/ppedrot/ll-coq

PMP