Stream: Coq users

Topic: ✔ Is it possible to make assert transparent?

Daniel Hilst Selli (Jun 21 2022 at 00:22):

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

Gaëtan Gilbert (Jun 21 2022 at 07:25):

refine (let F := _ : T in _) instead of assert T as F

Gaëtan Gilbert (Jun 21 2022 at 07:26):

or for exists goals you can just unshelve eexists

Daniel Hilst Selli (Jun 21 2022 at 12:30):

Oh, I didn't know about unshelve eexists thanks, cool!

Notification Bot (Jun 21 2022 at 12:30):

Daniel Hilst Selli has marked this topic as resolved.

Daniel Hilst Selli (Jun 21 2022 at 13:34):

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