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