The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

On Nov 12, 2019, Clément Pit-Claudel 
<cpitclaudel AT gmail.com>
 wrote:

> `set` is a bit more powerful that context[] pattern-matching.

Thanks for explaining!

> What you need to make your example go through is
>
>               match goal with
>               | [  |- context[?x] ] =>
>                 unify x source;
>                 …
>
> … but in general, I'd stay away from evar-based strategies.

Right, I tried unify after sending my last message, and it doesn't work
well.  For example, the term 4 * (m + (3 * n) *does* unify against
?x + ?y, since it expands to a sum.  But I don't want to rewrite
something that isn't explicitly written as a sum.  So unify is out.

> Consider this instead:
>
> Ltac source thm :=
>   let tau := type of thm in
>   lazymatch tau with
>   | forall x: ?t, _ =>
>     constr:(fun x: t =>
>               ltac:(let thm' := constr:(thm x) in
>                     let thm'' := (eval cbv beta in thm') in
>                     let src := source thm'' in
>                     exact src))
>   | ?src = _ => constr:(src)
>   end.

That's a nice way to avoid having to know the number of arguments that
the lemma takes.  There are still two other places where I need to list
the arguments, which I've pulled out into another helper function.

Ltac find_function fn term :=
  match term with
    | context[fn ?a1 ?a2 ?a3] => constr:(fn a1 a2 a3)
    | context[fn ?a1 ?a2    ] => constr:(fn a1 a2)
    | context[fn ?a1        ] => constr:(fn a1)
    | context[fn            ] => constr:(fn)
  end.

I was hoping to be able to use the "as ident" form to avoid repeating
myself, e.g.

  match term with
    | context[fn ?a1 ?a2 ?a3 as W],
      context[fn ?a1 ?a2     as W] => constr:(W)

(and more cases) but it doesn't work within a context search.  Any
ideas?

With those two helper functions, my tactic is now:

Tactic Notation "rewrite_in_lhs" uconstr(lem) :=
  let f := source lem in
  let fn := fresh "f" in
  set f as fn;
  lazymatch goal with
  | |- ?lhs = ?rhs =>
    let fnargs := find_function fn lhs in
    let P := eval pattern fnargs in lhs in
        match P with
        | ?F ?w =>
          refine (eq_trans (f_equal F _) _); [eapply lem | ]
        end
  end;
  subst fn.

And it works!

Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
  intros.
  rewrite_in_lhs' Nat.add_comm.
Abort.

There are still some issues, though:

1) I found an edge case where the set method doesn't work.  Sometimes
the type of the equality is forall a : A, a = foo a.  Then the source of
this is the identity function, and set does not insert the identity
function into the goal, so the match fails.  Here's an example:

Axiom Pt : Type.
Axiom c0 : Pt.
Axiom alleq : forall c : Pt, c = c0.
Goal forall c c' : Pt, c = c'.
  intros.
  Fail let f := source alleq in
  let fn := fresh "f" in
  set f as fn;
    match goal with [ |- context[fn ?x] ] => idtac end.
  rewrite alleq at 1.  (* Succeeds. *)
Abort.

Any ideas?

2) I want to work with one side of the equation at a time, but
the "set f as fn" applies to the whole goal.  Is there a way to
do that substitution just in the lhs?  Not only would it be more
efficient, it would avoid changing the rhs:

Goal forall m n, (4 * (m + (3 * n)) * 2) = m + n.
  intros.
  rewrite_in_lhs Nat.add_comm.
  (* RHS changes to (fun n0 m0 : nat => n0 + m0) m n  *)
Abort.

Thanks again!

Dan