Hello,

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:

- 0.03 secs with both options off
- 0.09 secs with
`Implicit Arguments`

on - 0.03 secs with
`Contextual Arguments`

on - 8.9 secs with both options on

The options do some work as I end up with the following signature`equ_clos_sT_proper {E}%function_scope {R}%type_scope [RR]%function_scope [f x y] _ [x y] _`

but that still seems crazy to me. Is it to be expected?

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.

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.
*)
```

maybe a variant of https://github.com/coq/coq/issues/13435

Last updated: Jun 14 2024 at 18:01 UTC