The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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.

Pierre

> and I have absolutely no idea what that means. Any pointers?
>
> Thanks!
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>