The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

> 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 *)