The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Wed, Nov 07, 2007 at 10:33:11AM +0100, 
frederic.blanqui AT loria.fr
 wrote:
> On Wed, 7 Nov 2007, Edsko de Vries wrote:
> 
> >Is there an implementation of multisets in Coq which has the property
> >that for two multisets M1 and M2, union M1 M2 = union M2 M1 (as in the
> >Multiset implementation in the standard library), but is "concrete" in
> >the sense that it supports an operation elems :: Multiset A -> List A?
> 
> see for instance the multiset modules of the CoLoR library on 
> http://color.loria.fr/.

Thanks for the suggestion. However, the only theorem I can regarding
equality is that union M1 M2 "meq" union M2 M1, rather than "=", and I'm
not sure that's what I need. Here's a simple example of what I'm trying
to do:

  Add Rec LoadPath "CoLoR" as Rewriting.
  
  Require Import Arith.
  Require Import Setoid.
  Require Import Rewriting.Util.Relation.RelExtras.
  Require Import Rewriting.Util.Multiset.MultisetList.
  Require Import Rewriting.Util.Multiset.MultisetTheory.
  
  Module Nat <: Eqset.
  
  Definition A := nat.
  Definition eqA := (@eq A).
  
  Definition sid_theoryA : Setoid_Theory A eqA.
  split ; unfold eqA ; intros ; auto.
  subst y ; auto.
  Defined.
  
  End Nat.
  
  Module NatList := FiniteMultisetList Nat.
  
  Module NatListTheory := FiniteMultiset NatList.
  
  Section test.
  
    Variables (M1 M2: NatList.Multiset).
  
    Variable P : NatList.Multiset -> Prop.
  
    Hypothesis p : P (NatList.union M1 M2).
  
    Lemma p' : P (NatList.union M2 M1).

At this point I'd like to do

    rewrite NatListTheory.union_comm ; assumption.

to finish the proof, but that tells me

  User error: Either the term NatList.union M2 M1 that must be rewritten
  occurs in a covariant position or the goal is not made of morphism
  applications only. You can replace only occurrences that are in a
  contravariant position and such that the context obtained by
  abstracting them is made of morphism applications only.

and I have absolutely no idea what that means. Any pointers?

Thanks!

Edsko