## Stream: Coq users

### Topic: match goal as lambda

#### choukh (Aug 20 2021 at 08:42):

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

#### choukh (Aug 20 2021 at 08:43):

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

(deleted)

#### choukh (Aug 20 2021 at 08:47):

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

#### choukh (Aug 20 2021 at 08:50):

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

#### choukh (Aug 20 2021 at 08:52):

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

#### Kenji Maillard (Aug 20 2021 at 08:52):

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.
``````

#### Kenji Maillard (Aug 20 2021 at 08:54):

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 ?

#### choukh (Aug 20 2021 at 09:03):

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

#### choukh (Aug 20 2021 at 09:04):

Oh I got some idea to try

#### Kenji Maillard (Aug 20 2021 at 09:08):

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 *)
``````

#### Olivier Laurent (Aug 20 2021 at 11:52):

@choukh is `pattern` what you are looking for?
with for example:

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

#### choukh (Aug 20 2021 at 12:34):

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

Last updated: Jan 31 2023 at 13:02 UTC