The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Tue, Aug 16, 2016 at 3:20 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

[setoid_rewrite <-compose_assoc at 2] works in Vadim's example.  The way that setoid_rewrite matches patterns is different from the way that rewrite matches patterns.  I think that setoid_rewrite's method is more intuitive.

That's very interesting. Thanks! I think it would good to mention this in the documentation. Confusingly it mentions that 'rewrite ... at ..." uses Setoid equality, but apparently that does not mean that it matches patterns in the same way as 'setoid_rewrite'.

My remaining problem is that I am working in environment where I am already using setoid equality and thus my 'default_relation' is re-defined ('equiv' not 'eq'), while `comp_assoc` is defined for 'eq'. So I need to find a way to use `setoid_rewrite` tactics but with 'eq' relation. You can specify one for 'setoid_replace' tactic ('using relation' argument), but unfortunately not for `setoid_rewrite`!

Vadim

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060