The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Are there any tricks for rewriting in the middle of a list?  For example, say I know x++y = z, and I have a++b++c++...++x++y++d++e++...++f, and I want to replace the x++y in the middle with z.  Is there a good way to do this (and, more generally, to do this for associative binary operations which aren't the constructor of an inductive type)?  The only way I know is a reflective solver.

-Jason

On Mon, Apr 28, 2014 at 4:08 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

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