Beta expansion in coq: can I make a term into a function, abstracting over another given term?

Question

I want to rewrite a term, as a function in a sort of beta expansion (inverse of beta reduction).

So, for example in the term a + 1 = RHS I would like to replace it as (fun x => x + 1) a = RHS. Obviously, the two terms are equal by betta reduction, but I can't figure out how to automate it.

The tactic pattern comes very close to what I want, except it only applies to a full goal, and I can't see how I would use it in a term inside an equality.

Similarly, I thought I could use the context holes. Here is my best attempt

Ltac betaExpansion term a:=
  let T:= type of a in
  match term with
    context hole [a] =>
      idtac hole;
      let f:= fun x => context hole [x] in
      remember ( fun x:T => f x ) as f'
  end.

Goal forall a: nat, a + 1 = 0.
intros a.
  
  match goal with
    |- ?LHS = _ =>
      betaExpansion LHS a (*Error: Variable f should be bound to a term but is bound to a tacvalue.*)
  end.

This obviously fails, because f is a tacvalue when I really need a normal value. Can I somehow evaluate the expression to make it a value?

Answer 1

You should have a look at the pattern tactic. pattern t replaced all occurrences of t in the goal by a beta expanded variable.

Answer 2

You may also use the change ... with ... at tactic.

Goal forall (a:nat) , a+1 = 2* (a+1) - (a+1).
intro x; change (x+1) with ((fun z => z) (x+1)) at 1 3.
(*
 x : nat
  ============================
  (fun z : nat => z) (x + 1) = 2 * (x + 1) - (fun z : nat => z) (x + 1)
*)

Or, more automatically

Ltac betaexp term i :=
  let x := fresh "x" in
  let T := type of term in 
   change term with ((fun x : T => x) term) at i.

Goal forall (a:nat) , a+1 = a+1 .
intro x; betaexp (x+1) ltac:(1).