The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 25 Apr 2014 23:24:02 -0400,
Jonathan 
<jonikelee AT gmail.com>
 a écrit :

> Arnaud,
> 
> I somewhat expected to get associative rewriting of ILists as well -
> but that isn't working:
> 
>     Remark assoc_rw : forall A (p q r s:IList A), q++r = s ->
> (p++q)++r = p++s.
>     Proof.
>        intros A p q r s H.
>        rewrite H.(*fails*)
> 
> 
> I guess the thing to do is to use the AACTactics library with ILists.
> 
> -- Jonathan
> 

If that really is your code, it seems normal, as "rewrite H." where
H:q++r=s replace all occurences of q++r with s, and there is no
occurence of q++r.

If you want to rewrite the otherway (ie. s into q++r), you can try:
* subst H. (* This tactic rewrite equalities of the form var=exp or
  exp=var in the right direction *)
* destruct H. (* see the documentation, and see also "case H." *)
* rewrite <- H.

There is also a pattern I use a lot, but that I do not advise to use as
it looks completely cryptic:

"intros A p q r _ []."
It is equivalent to "intros A p q r s H; case H as []; clear s."


Furthermore, why not simply prove that:

Remark assoc_rw : forall A (p q r:IList A),
 (p++q)++r = p++(q++r).

?