The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

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.

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?


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