The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

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

> Something along these lines? You'd have to generalize it to cover more 
> arguments, of course.
>
> Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
>   intros.
>   match type of Nat.add_comm with
>   | forall a b, @?f a b = _ =>
>     let fn := fresh "f" in
>     set f as fn;
>       match goal with
>       | [  |- context[fn ?x ?y] ] =>
>         pattern (fn x y);
>           set x as arg1; set y as arg2
>       end
>   end.

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.

but the match on the goal fails.

Also, it would be nice to not have to repeat the (f x y) pattern,
especially if I want to handle lemmas with between 0 and 10 arguments.
I tried the following:

Definition path_source {A : Type} {x y : A} (p : x = y) := x : A.

Goal forall m n, (4 * (m + (3 * n)) * 2) = 1.
  intros.
  let x := fresh "x" in
  evar (x : nat);
    let x' := eval unfold x in x in
        let y := fresh "y" in
        evar (y : nat);
          let y' := eval unfold y in y in
              let source := eval unfold path_source in (path_source (add_comm 
x' y')) in
              match goal with
              | [  |- context[source] ] =>
                pattern (source);
                  set x' as arg1; set y' as arg2
              | _ => idtac source "unmatched"
              end.

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?

If this could work, then one could use a tactic like Chlipala's insterU
to insert the required existential variables.

Thanks again for the help!

Dan