Stream: Coq users

Topic: match goal as lambda


view this post on Zulip choukh (Aug 20 2021 at 08:42):

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

view this post on Zulip choukh (Aug 20 2021 at 08:43):

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

view this post on Zulip Kenji Maillard (Aug 20 2021 at 08:45):

(deleted)

view this post on Zulip choukh (Aug 20 2021 at 08:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip choukh (Aug 20 2021 at 09:03):

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

view this post on Zulip choukh (Aug 20 2021 at 09:04):

Oh I got some idea to try

view this post on Zulip 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 *)

view this post on Zulip 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.

view this post on Zulip 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