The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

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