I'm using this technique to look for functions :
Open Scope Z_scope.
Lemma foo : forall x,
exists function, 2 * x = function x.
Proof.
intros.
match goal with
| |- exists (_ : ?T), _ => assert T as F
end.
{ refine (fun x => x + x). }
exists F.
Fail unfold F.
Abort.
I pretty common to need to search for a function to convert one term to another, the idea is to state that such a function exists and use refine to search for its implementation. I use match goal
to capture the function type and make one assertion with it, then I prove the assertion by implementing the function with help of refine
. At this point copy and paste the function to another place, my question is: Is it possible to make the assertion transparent so that I can unfold the F and continue the proof from where I stopped (instead of copy/pasting)?
refine (let F := _ : T in _)
instead of assert T as F
or for exists goals you can just unshelve eexists
Oh, I didn't know about unshelve eexists
thanks, cool!
Daniel Hilst Selli has marked this topic as resolved.
Oh I can do unshelve eassert (2 * x = _ x)
and get a subgoal focused for this hole
Last updated: Oct 05 2023 at 02:01 UTC