While trying to work on ticket 928, I'm getting stuck on something I encounter on a regular basis: I define some kind of function where I expect `f a b c`

to make sense, and indeed `Check f`

seems to confirm it, but when I `Check f _`

or try a partial evaluation `f a`

, it doesn't typecheck.

There's certainly something I miss in there...

Maybe implicit arguments, have you tried `Check @f`

?

```
telescope_sumr_eq
: forall f : nat -> ?V,
(forall k : nat, (?a <= k < ?b)%N -> ?u k = f k.+1 - f k) ->
\sum_(?a <= k < ?b) ?u k = f ?b - f ?a
```

vs

```
@telescope_sumr_eq
: forall a b : nat,
(a <= b)%N ->
forall (V : zmodType) (u f : nat -> V),
(forall k : nat, (a <= k < b)%N -> u k = f k.+1 - f k) -> \sum_(a <= k < b) u k = f b - f a
```

Looks like the explanation indeed

The `forall k...`

always comes after f, so I don't understand what happens

You can use `About`

to see the implicit arguments and `Arguments`

to change them for a specific lemma.

Otherwise just copy paste your code here (can't help without being able to reproduce the issue).

I pasted my code in the ticket ; do you need it here too?

Paste the output of `About telescope_sumr_eq.`

Long story short, don't use `Check`

to figure out what has to be passed

```
telescope_sumr_eq :
forall {a b : nat},
(a <= b)%N ->
forall (V : zmodType) (u f : nat -> V),
(forall k : nat, (a <= k < b)%N -> u k = f k.+1 - f k) -> \sum_(a <= k < b) u k = f b - f a
telescope_sumr_eq is not universe polymorphic
Arguments telescope_sumr_eq {a b}%nat_scope {aleqb V} {u}%function_scope [f]%function_scope
_%function_scope
telescope_sumr_eq is opaque
Expands to: Constant bug_mathcomp_928.telescope_sumr_eq
```

I must admit I'm a bit confused about About/Check.

So, `f`

is implicit, you can't pass it unless you use its name or disable implicits with `@`

Ok, I read the ticket, don't use `apply`

, use `rewrite`

If you expect to need to pass it all the times, put that argument early, and make it explicit via `Arguments`

.

(and in any case prefer `apply:`

to `apply`

in ssreflect scripts)

I don't think `f`

is implicit ; and rewrite didn't seem to work better when I tried.

It is `[f]`

in the ouput of `About`

mean implicit.

You have two problems here I guess. One is the implicit (so you are not passing f) and the other one is that you don't want to apply, IMO.

I thought { } was the implicit?

(and `{x}`

means that `x`

is implicit and maximally inserted (i.e. `f`

actually means `f _`

if `x`

is the first argument of `f`

))

They both are

oh, dear

I'm not a big fan of `[ ]`

implicits, but they have a reason to exist. The manual of Coq explains them.

In your case Coq decided f was implicit because it "thought" you would apply, and not rewrite with it.

Or maybe not, just be cause it is followed by another argument which mentions it.

In any case the guessing does not match your use case, so override it with Arguments.

I'm reading the Coq manual on implicit arguments... it will take some time, and seems to be more about making implicit than forcing explicit.

The refman page about implicit is quite terrible (it goes in great length in how Coq decides what is implicit automatically more than explaining what implicit arguments are), probably just have a look to the `Arguments`

command for now.

Amusing: `About telescope_sumr_eq.`

just after my call to `Arguments`

shows:

```
Arguments telescope_sumr_eq [a b]%nat_scope [V] [u]%function_scope f%function_scope _
```

but just before I try to apply it:

```
Arguments telescope_sumr_eq {a b}%nat_scope {V} {u}%function_scope [f]%function_scope _
```

```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
```

I think you are asking Coq to compute them automatically, at section closing time as well.

It's indeed getting out of the `Missing`

section which triggers the change.

I think it is a bug to recompute them all, but well, a Coq bug

So I should try to write a minimal example and report?

Yes, put your `Arguments`

calls outside sections, otherwise effects might only be local to the section.

Last updated: Jan 29 2023 at 16:02 UTC