The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

On Nov 12, 2019, Talia Ringer 
<tringer AT cs.washington.edu>
 wrote:

>     Does anyone know if it's possible to access the power of
>     rewriting, without doing a rewrite? That is, to find a sub-term of
>     a given term that unifies with the lhs of a lemma (with arguments)
>     and so that the sub-term can be abstracted away from the term?
>
> AFAIK you need access to the internal API for this.
>
> I have a simple OCaml function that does this. Right now it just
> replaces all subterms of a term "bar" convertible with "foo" with
> "foo" itself, and returns a new definition "baz."

It doesn't look to me like this is related to what I asked since it
deals with convertible terms (definitional equality).  Can you explain
further?

Here's a simple example of what I want.  Given the term

  (4 * (m + (3 * n))) * 2

and a Lemma

  add_comm : forall a b : nat, a + b = b + a

I would like Coq to figure out that by passing the arguments m and
(3 * n) to add_comm you get an equality whose left-hand-side matches
a sub-term of the given term, and have it generate the function

  fun k => (4 * k) * 2

that you get by abstracting the sub-term.

Note that some sub-terms can't be abstracted (at least not in a
trivial way) due to dependencies, and I would want the tactic to
ignore such failures and continue looking for other matches.

Dan