Stream: Coq users

Topic: 8s to set implicit arguments?

view this post on Zulip Yannick Zakowski (Mar 26 2022 at 23:14):


I have a case of a lemma whose Qed was unexpectedly taking 8s. After a lot of head scratching, I eventually observed that I had activated Implicit Arguments and Contextual Implicit and that to my surprise, I observe that the Qed takes consistently of the order of:

view this post on Zulip Li-yao (Mar 27 2022 at 15:47):

If I understand the doc correctly, Implicit Arguments must be on for the other related flags to take effect. Then I wonder if determining whether to make an argument implicit may involve unfolding definitions.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 02:13):

Yes. For instance, constant functions don't really depend on their argument, and maybe "constant" is checked up to conversion. For instance, in the next example, it seems easier to infer the argument of bar than the argument of foo. But Coq seems to disagree.

Set Implicit Arguments.
Set Contextual Implicit.
Definition f (x : nat) := 0.
Lemma foo x : f x = 0. reflexivity. Qed.
About foo.
foo : forall {x : nat}, f x = 0
Definition g (x : nat) := x - x.
Lemma bar x : g x = 0. Admitted.
About bar.
bar : forall x : nat, g x = 0.

view this post on Zulip Pierre-Marie P├ędrot (Mar 28 2022 at 06:43):

maybe a variant of

Last updated: Jan 29 2023 at 05:03 UTC