Is there a way to match goal and turn the whole to a lambda expression.

Suppose I have a goal: n = n. I want to turn it to lambda n, n = n

(deleted)

I want it because I need the lambda expression to construct other term for proof

If the goal is not only about n, I should be able to specify which to bind to the lambda

I want to make it a Ltac so I dont need to copy and paste the goal every time

ok, my first try didn't work, here is something that may correspond to what you want using 2nd order patterns in match goal

```
Goal forall n m p : nat, n = n.
Proof.
intros n m p.
(* choose the variable to capture*)
revert n.
match goal with
| [ |- forall n, @?G n ] => pose (z := G)
end.
(* revert the goal to the original state *)
intro n.
```

My first tentative didn't introduce the variable in the goal, but 2nd order pattern matching does not seem to accept variables bound in the context (e.g a pattern `[n : _ |- @?G n]`

). Does anyone know why it is the case ?

Thank you. But what if n is already used in hypothesis?

Oh I got some idea to try

Something like this ?

```
Goal forall n m p : nat, n = n -> n = n.
Proof.
intros n m p H.
refine (let k := n in _).
revert k.
match goal with
| [ |- let k := _ in @?G k ] => pose (z := G)
end.
hnf. (* remove the let ; or intro k; unfold k; clear k. to be more precise *)
```

@choukh is `pattern`

what you are looking for?

with for example:

```
pattern n.
match goal with | |- ?t _ => pose (f := t) end.
```

Yes! It's exactly what I need. Thank you very much!

Last updated: Jun 18 2024 at 21:01 UTC