Stream: Coq users

Topic: ✔ Tactic Like assert but Transparent

Raymond Baker (Feb 12 2022 at 20:14):

Hey, I am looking for a coq tactic like assert but transparent. I essentially want to be able to make a definition mid proof. But, I don't want something like the pose tactic where I have to be ready to explicitly right out the term. I've looked at the Coq manual and the only thing that seems like this is the pose proof tactic. But even this behaves like assert.

Raymond Baker (Feb 12 2022 at 20:14):

By transparent, I mean I just want to have access to the term I construct mid proof.

Raymond Baker (Feb 12 2022 at 20:16):

I'm thinking that I could use a tactic to generate a new subgoal which helps with the construction of the term I want. But once I do construct the term and fulfill the sub-goal, I still want to have access to that specific term.

Ali Caglayan (Feb 12 2022 at 20:18):

In the HoTT library we use "transparent assert":

(** [transparent assert (H : T)] is like [assert (H : T)], but leaves the body transparent. *)
(** Since binders don't respect [fresh], we use a name unlikely to be reused. *)
Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
  simple refine (let __transparent_assert_hypothesis := (_ : type) in _);
  [
  | ((* We cannot use the name [__transparent_assert_hypothesis], due to some infelicities in the naming of bound variables.  So instead we pull the bottommost hypothesis. *)
    let H := match goal with H := _ |- _ => constr:(H) end in
    rename H into name) ].

However often you might have to write transparent assert (H : (my stuff)) instead of transparent assert (H : my stuff) since the parsing is a bit weird.

Ali Caglayan (Feb 12 2022 at 20:20):

Though there are probably better ways to achieve this nowadays. This tactic is basically doing the following:

refine (let myHyp : myType := _ in _).

Ali Caglayan (Feb 12 2022 at 20:21):

And because refine is "lazy"/"clever", it will try to infer the first hole from the second, so your best bet is to use simple refine which won't shelve anything.

Raymond Baker (Feb 12 2022 at 20:22):

Awsome, Thank you so much!

Notification Bot (Feb 12 2022 at 20:25):

Raymond Baker has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC