Feature request: accept patterns in argument of replace

[cpitclaudel]

Description of the problem

Currently the change tactic accepts patterns, but replace does not: one can write change (?x + ?x) with (2 * x), but not replace (?x + 1) with (1 + x) by lia.

This feature is really convenient when change-ing large terms; it would be nice to have it for replace, too.

The current alternative of course is to use match goal with context instead, like match goal with [ |- context[f ?x + ?y] => replace (f x + y) with (x + g y), but it's syntactically heavy.

[herbelin]

This is a long-standing wish (at least of mine). Initially, I intended to implement it following the way change is implemented.

However, replace is defined as a TACTIC EXTEND which is not able to interpret left-hand side patterns the way change is doing it, so either replace had to be turned into a tactic interpreted natively (but defeating the idea of a flexible architecture for defining new tactics), or some refinement of the TACTIC EXTEND had to be done.

As of now, there is some confusion about the future of tactics which somehow inhibates evolutions.

For instance, the status of TACTIC EXTEND is unknown. @ppedrot is often blaming it which makes me hesitant to recommend extending it further (if @ppedrot knows how to do better, let's not waste time at maintaining an infrastructure that some other architecture can eventually provide in a more general, more flexible, more efficient way...).

Still, something has to be done, so I'd be tempted to ask @ppedrot about how he would recommend your wish to be efficiently implemented, whatever way it is. Maybe it is more direct that I'd think.

[ppedrot]

We can discuss this at the next weekly call. Technically you can perfectly implement the wish with TACTIC EXTEND using specific genargs defined for that (and you could even port change to this). But in terms of functionality, I am kind of wary of the issues with change used with patterns, it also has quite a few drawbacks regarding type inference and pattern substitution. I'd rather have two different tactics, one with patterns and the other with terms (and fix change accordingly).

[Zimmi48]

@ppedrot echange and ereplace then?

@cpitclaudel Note that you can work around this limitation of replace by relying on eassert instead:

Require Import Lia.
Goal forall P x, P (x + 1).
intros.
eassert (?[x] + 1 = 1 + ?x) as -> by lia.

The nice thing about the as -> clause is that it makes the side goal concrete (instead of still containing existential variables as if this clause had not been used).