choukh (Aug 20 2021 at 08:42): 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
Kenji Maillard (Aug 20 2021 at 08:45):(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.
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 *)
@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: Sep 25 2023 at 12:01 UTC