The Coq mailing list

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

Oh, sorry for the double emails in a row, but I guess right now it doesn't handle arguments nicely. So you can look for subterms convertible with the lemma itself, but you can't look for subterms convertible with the lemma applied to some particular arguments when those arguments are not already in your context. Extending it to handle that case would in theory be easy if I knew a good interface for using it, but I don't! This is the same reason why "Abstract" is a pain to use.

Some functions in my plugin library, if you do go the OCaml route, for substitution: https://github.com/uwplse/coq-plugin-lib/blob/master/src/coq/logicutils/hofs/substitution.ml

I think the Coq internal APIs have their own substitution functions, too. I don't know what they are. Again, the ones that I use here don't produce proofs yet.

Happy to guide you through plugin development if you choose to do it that way. Also happy to provide better command interfaces. I'm working on this for a user right now so I'd really like something useful.

On Tue, Nov 12, 2019 at 1:39 PM 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 can also do that over a whole module. I added a command interface to it yesterday. it doesn't generate equality proofs yet though. I'm working on that today. I'm happy to extend it more. You can also use the OCaml APIs as you'd like. I don't really know what people want for this sort of thing yet, but I'm playing around with it.

Single file version: https://github.com/uwplse/PUMPKIN-PATCH/commit/3e288f81969c7d404fc4e1c26e53a4cb9a6242b2

Whole module (still a bit wonky): https://github.com/uwplse/PUMPKIN-PATCH/commit/92721a345d7d9a76f980546d0bc512944a714601

I also have some abstraction functionality (the "Abstract" command) in that repository, but it is hard to use right now.

Talia

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

> Not sure if relevant, but I recently wrote my own rewrite tactic:
> https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/rewr.v
> It's more cumbersome to use (you have to spell out the left-hand side), but I
> find it easier to control it and to understand what's going on.

Thanks for the response.  I took a look at your rewrite tactic.  It's
clever, and it could probably handle the things I'm considering, but
for each lemma, I'd have to write a version of getEq that figures out
the arguments to use for the lemma.  Coq's built-in rewrite is able
to figure that out with no work on my part, and that's what I'd like
to figure out.

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?

If it's not currently possible, could a tactic be added to Coq that
gives access to what rewrite does?

Or can I call rewrite, examine the proof term it generates, undo the
rewrite, and use that info myself (all in Ltac)?

> And one more thing: Did you consider using multimatch instead of
> match? I had to do so at one point and maybe that's just what you're
> missing?

I also tried multimatch, and it didn't help, since my errors seem fatal,
not causing backtracking.

My original message follows, for reference.

Dan

On Mon, 2019-11-11 at 19:02 -0500, Dan Christensen wrote:

> The tactic
>
>   rewrite lem
>
> does two clever things.  It figures out arguments to pass to the
> function lem so that it produces an equality whose left-hand-side
> matches a sub-term of the goal, and it abstracts away that sub-term
> to make the goal into a type family.
>
> However, in the case where the goal is an equality, it produces proof
> terms that are more complicated than necessary.  (I'm working within
> the HoTT library, where I need to manipulate the proof terms later in
> the development.)
>
> Below I give a simplified example of two proofs of the same theorem,
> one using rewrite (which generates a proof term using eq_ind_r) and
> one using f_equal and eq_trans.  (In HoTT lingo, those would be
> internal_paths_rew_r, and ap and concat, respectively.)
>
> I would like a tactic that is as easy to use as rewrite but which
> produces proofs like the second method below.
>
> I came up with a crude tactic rewrite_in_lhs that often works, also
> shown below.  In this example, it works perfectly.  However, in more
> complicated examples, the line
>
>   let f := constr:(fun w : T => ltac:(let t := context F [w] in exact t))
> in
>
> generates an Ltac error when the lambda _expression_ is not well-typed,
> and Coq doesn't backtrack and try a different match.  (The same problem
> happens if I try using "eval pattern src in lhs".)
>
> So my question is whether there is a more robust way to match a lemma
> to a sub-term and then abstract the context of the sub-term to a
> function, which I can then manipulate further.
>
> If an Ltac error can be caught and converted into a tactic failure,
> that would work.  But even if that is possible, my method is much
> slower than rewrite, so I hope that there is a more direct solution.
>
> Thanks for any help!
>
> Dan
>
>
> Parameter A C : Type.
> Parameter g : A -> C.
> Parameter c : C.
>
> Axiom lem : forall a : A, g a = c.
>
> Theorem example {B : Type} (f : C -> B) (a : A) (b : B) (q : f c = b)
>   : f (g a) = b.
> Proof.
>   rewrite lem.  (* [lem a] gives [g a = c] *)
>   exact q.
> Qed.
>
> Print example.
> (* fun (B : Type) (f : C -> B) (a : A) (b : B) (q : f c = b) =>
>    eq_ind_r (fun c : C => f c = b) q (lem a) *)
>
> Theorem example' {B : Type} (f : C -> B) (a : A) (b : B) (q : f c = b)
>   : f (g a) = b.
> Proof.
>   exact (eq_trans (f_equal f (lem a)) q).
> Qed.
>
> Print example'.
> (* fun (B : Type) (f : C -> B) (a : A) (b : B) (q : f c = b) =>
>    eq_trans (f_equal f (lem a)) q  *)
>
> (* Try *every* subterm [t] of lhs to see if [lem] can give a path [p]
> starting at [t].
>    If so, do [refine (eq_trans (f_equal f p) _)] for suitable [f]. *)
> Tactic Notation "rewrite_in_lhs" uconstr(lem) :=
>   lazymatch goal with
>   | |- ?lhs = ?rhs
>     => match lhs with
>       | context F [?src]
>         => let T := type of src in
>           let f := constr:(fun w : T => ltac:(let t := context F [w] in
> exact t)) in
>           refine (eq_trans (f_equal f _) _); [eapply lem | idtac]
>       end
>   end.
>
> Lemma example'' {B : Type} (f : C -> B) (a : A) (b : B) (q : f c = b)
>   : f (g a) = b.
> Proof.
>   rewrite_in_lhs lem.
>   exact q.
> Qed.
>
> Print example''.
> (* fun (B : Type) (f : C -> B) (a : A) (b : B) (q : f c = b) =>
>    eq_trans (f_equal (fun w : C => f w) (lem a)) q *)