The Coq mailing list

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

On 2019-11-12 16:58, Dan Christensen wrote:
> I would like Coq to figure out that by passing the arguments m and
> (3 * n) to add_comm you get an equality whose left-hand-side matches
> a sub-term of the given term, and have it generate the function
> 
>   fun k => (4 * k) * 2
> 
> that you get by abstracting the sub-term.

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.

  m, n : nat
  f := fun n m : nat => n + m : nat -> nat -> nat
  arg1 := m : nat
  arg2 := 3 * n : nat
  ============================
  (fun n0 : nat => 4 * n0 * 2 = 1) (f arg1 arg2)