Created rewrite tactic

[patrick-nicodemus]

I have created a simple rewriting tactic that Enrico suggested on the Zulip would be a good fit for the eltac repo.

[patrick-nicodemus]

Some comments Enrico made on the Zulip:

• coq.typecheck works for any term, no need to check if Eq is a proof variable or a gref
• the copy clause needs to be quantified on J
• nested_forall must exist somewhere, I usually call it "saturate"
• you should be able to write _ istead of {{ _ }}, holes in Elpi are holes in Coq

I will address these.

[patrick-nicodemus]

Okay, comments fixed.
N. b. - I call coq.typecheck Eq' Ty' ok right after coq.saturate to get the type of the term Eq', but it seems like
it might be more efficient to have coq.saturate compute the type of Eq' as it's traversing the chain of nested products.

[gares]

Thanks for your contribution, please take a look at my comments

[gares]

The LHS of ; should suffice since Ctx is loaded hence you are really running Ctx => coq.typecheck ... and that knows the type of proof variables.

[gares]

This looks like a good introduction to the power of copy etc, thanks for providing it.

But this implementation of rewrite is known to be a "bad rewrite" since it is too smart, eg lets you rewrite with commutativity of addition on a goal like 2 * x = .. that has no addition in it. I recommend at least writing a comment about this, or write a more complex line that compares the key verbatim, see for
example

coq-elpi/elpi/elpi_elaborator.elpi

Lines 173 to 177 in c40e913

	bind-list [app [C| AS] |VS] T R :- key C, !,
	pi x\
	(pi L X\ bind (app[C|L]) X :- get-option "unif:greedy" tt, unify-list-eq L AS, X = x, !) =>
	(pi L X\ bind (app[C|L]) X :- not (get-option "unif:greedy" tt),unify-list-eq L AS, X = x) =>
	bind-list VS T (R x).

or the ssreflect section in the Coq manual for keyd matching.

[gares]

Suggested change

	(fun _ S (a\
	fun _ {{ @eq lp:S lp:P lp:Q }} (_\ A a )
	))
	{{ fun a (e : @eq lp:S lp:P lp:Q) => lp:(A a) }}

Also shouldn't Q be a ?