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.
By transparent, I mean I just want to have access to the term I construct mid proof.
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.
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.
Though there are probably better ways to achieve this nowadays. This tactic is basically doing the following:
refine (let myHyp : myType := _ in _).
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.
Awsome, Thank you so much!
Raymond Baker has marked this topic as resolved.
Last updated: Jan 29 2023 at 01:02 UTC