The Coq mailing list

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

On Wed, Nov 07, 2007 at 12:40:11PM +0100, Pierre Casteran wrote:
> Edsko de Vries a e'crit :
> >
> >  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.
> >  
> 
> 
> Hi,
> If you could have proved p', after closing the section test, you would get
> 
> p' : forall M1 M2, forall P, P (Natlist.union M1 M2) -> P (Natlist.union 
> M2 M1),
> 
> which is equivalent to Leibniz equality of the two unions.
> In order to do your rewrite, Coq needs that the enclosing P is a 
> morphism wrt
> Meq, which is not in your hypotheses.

But that means that I have to prove something for every property P I
need to prove stuff about (that P is a "morphism", whatever I that is)
-- which I don't want to have to do :) I am looking for an
implementation of multisets which has the property that (union M1 M2)
really *equals* union M2 M1, so that I can prove this property without
any further hypotheses about P (this would be possible if the multiset
uses some sort of ordering on the elements, for example).

Edsko