Stream: Coq users

Topic: Displaying implicit arguments in a goal during a proof


view this post on Zulip Thomas Lamiaux (Apr 29 2024 at 18:29):

Hi, I am trying to prove a goal in which some arguments are implicit.
At a point in my proof, I would like to check them and hence to display them in my goal.
Is there a command or a tactic to do that ?

view this post on Zulip Thomas Lamiaux (Apr 29 2024 at 18:33):

Ideally, I would like to only display the implicit argument of my specific function, not of all terms involved in my goal

view this post on Zulip Théo Winterhalter (Apr 29 2024 at 18:37):

You can always print all implicit arguments with Set Printing Implicit (see https://coq.inria.fr/doc/V8.19.0/refman/language/extensions/implicit-arguments.html#coq:flag.Printing-Implicit).

view this post on Zulip Théo Winterhalter (Apr 29 2024 at 18:38):

If you want to print only the implicit argument for a specific function, then you could have an alternate notation or maybe even just set it?

view this post on Zulip Théo Winterhalter (Apr 29 2024 at 18:39):

Like so:

Definition f {A : Type} (x : A) := x.

Goal  A x, @f A x = x.
Proof.
  intros A x. (* f x = x *)
  set (g := @f). (* g A x = x *)

view this post on Zulip Thomas Lamiaux (Apr 29 2024 at 18:53):

Hum, I guess I would like to be able to write Set Implicit (f _ _ _)

view this post on Zulip Thomas Lamiaux (Apr 29 2024 at 18:55):

Using set is a good idea. It has the disadvantage to change the name of the function, but it enables me to partially control which arguments I want to be made explicit

view this post on Zulip Théo Winterhalter (Apr 29 2024 at 19:58):

I mean, you can use set (f_ := @f) or something.
There is also a command to change implicit arguments of a specific function:

Arguments f _ _ _ : clear implicits.

Last updated: Jun 23 2024 at 05:02 UTC