The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2019-11-12 20:24, Dan Christensen wrote:
> This looks very promising!  I had tried something similar which didn't
> work.  Can you explain why these two lines are needed:
> 
>     let fn := fresh "f" in
>     set f as fn;> 
> I had tried something like:
> 
> Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
>   intros.
>   match type of Nat.add_comm with
>   | forall a b, @?f a b = _ =>
>       match goal with
>       | [  |- context[f ?x ?y] ] =>
>         pattern (f x y);
>           set x as arg1; set y as arg2
>       end
>   end.

`set` is a bit more powerful that context[] pattern-matching.  Your `f` is 
eta-expanded here, so it's not a plain Nat.add, it's (fun a b => a + b).  
Here's an example:

Require Import Arith.
Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
  intros.

  Fail lazymatch goal with (* This is essentially what your tactic tries to 
do *)
       | [  |- context[(fun a b => a + b) ?x ?y] ] => idtac
       end. (* It fails because the goal doesn't have a literal eta-expanded 
(fun a b => a + b) in it *)

  change Nat.add with (fun a b => a + b).
  lazymatch goal with (* This one works *)
  | [  |- context[(fun a b => a + b) ?x ?y] ] => idtac
  end.

  cbv beta.
  set (fun a b => a + b). (* So does [set] *)

> This correctly gets source to be (?x + ?y), but the match of the goal
> against context[source] fails.  Maybe I'm just confused and these
> existential variables are different from the variables in match
> patterns?

Yup, the notation is the same, but these are quite different beasts.  Your 
pattern-matches looks for a subterm of the goal that contains references to 
the evars you just created, but your goal doesn't contain that.  What you 
need to make your example go through is 

              match goal with
              | [  |- context[?x] ] =>
                unify x source;
                …
              | _ => idtac source "unmatched"
              end.

… but in general, I'd stay away from evar-based strategies.  Consider this 
instead:

Require Import Arith.

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.

Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
  intros.
  let f := source @Nat.add_comm in
  let fn := fresh "f" in
  set f as fn.

Clément.