The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

OK, sorry, the way you asked it was a bit confusing.

Take a look at the substitution API I sent in the same email though. You don't have to use definitional equality. There is one for types too. It also handles state so in theory can support evars. Type checking in Coq under the hood actually always asks the question "is there a state (universe constraints and evar assignments and so on) under which this has a given type?" But you'll have to figure out how to use the updated state you get back. That will be painful. Then you can just tweak Abstract one you have that, though, to take care of the final step: Instead of having it stop when it finds anything of the goal type, have it stop when it has done all of the appropriate substitutions.

If you don't care about the particular lemma used and just want it to try to abstract your function in any way it can, you can just tweak Abstract to return all possible candidates that are well-typed instead of only one that has a specific type. This is a ~5 LOC change probably, and it would give you the term you mention, though also a whole bunch of other terms you might not want.

On Tue, Nov 12, 2019 at 1:59 PM Dan Christensen <jdc AT uwo.ca> wrote:

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