The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Yes. Rewrite doesn't do anything smart with matching (as it happens pattern-matching up to conversion is really hard). AACTactics would be one approach to your issue (though I'm not sure it features rewriting up to just associativity).

Otherwise, a trick I use for associativity when I don't have the appropriate tactics is to prove contextual versions of my lemma. Say have have a lemma stating  a++b = c  I would prove an alternative version   forall d, a++b++d = c++d. Then I would eagerly simplify my goals up to associativity, and rewrite with both the standard and contextual version of the lemma. It's hacky, full of boilerplate, and not extremely efficient. But it works.

On 26 April 2014 05:24, Jonathan <jonikelee AT gmail.com> wrote:

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