Stream: math-comp devs

Topic: ✔ Ticket #928

Julien Puydt (Sep 27 2022 at 12:48):

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...

Pierre Roux (Sep 27 2022 at 12:52):

Maybe implicit arguments, have you tried Check @f?

Julien Puydt (Sep 27 2022 at 13:01):

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

Pierre Roux (Sep 27 2022 at 13:13):

Looks like the explanation indeed

Julien Puydt (Sep 27 2022 at 13:16):

The forall k... always comes after f, so I don't understand what happens

Pierre Roux (Sep 27 2022 at 13:20):

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

Julien Puydt (Sep 27 2022 at 13:21):

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

Enrico Tassi (Sep 27 2022 at 13:23):

Paste the output of About telescope_sumr_eq.

Enrico Tassi (Sep 27 2022 at 13:24):

Long story short, don't use Check to figure out what has to be passed

Julien Puydt (Sep 27 2022 at 13:24):

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

Julien Puydt (Sep 27 2022 at 13:25):

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

Enrico Tassi (Sep 27 2022 at 13:25):

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

Pierre Roux (Sep 27 2022 at 13:26):

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

Enrico Tassi (Sep 27 2022 at 13:26):

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

Pierre Roux (Sep 27 2022 at 13:26):

(and in any case prefer apply: to apply in ssreflect scripts)

Julien Puydt (Sep 27 2022 at 13:26):

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

Pierre Roux (Sep 27 2022 at 13:27):

It is [f] in the ouput of About mean implicit.

Enrico Tassi (Sep 27 2022 at 13:28):

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.

Julien Puydt (Sep 27 2022 at 13:28):

I thought { } was the implicit?

Pierre Roux (Sep 27 2022 at 13:28):

(and {x} means that x is implicit and maximally inserted (i.e. f actually means f _ if x is the first argument of f))

Enrico Tassi (Sep 27 2022 at 13:28):

They both are

Julien Puydt (Sep 27 2022 at 13:28):

oh, dear

Enrico Tassi (Sep 27 2022 at 13:30):

I'm not a big fan of [ ] implicits, but they have a reason to exist. The manual of Coq explains them.

Enrico Tassi (Sep 27 2022 at 13:31):

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

Enrico Tassi (Sep 27 2022 at 13:32):

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

Enrico Tassi (Sep 27 2022 at 13:32):

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

Julien Puydt (Sep 27 2022 at 13:33):

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.

Pierre Roux (Sep 27 2022 at 13:35):

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.

Julien Puydt (Sep 27 2022 at 13:58):

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 _

Enrico Tassi (Sep 27 2022 at 14:00):

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.

Julien Puydt (Sep 27 2022 at 14:02):

It's indeed getting out of the Missing section which triggers the change.

Enrico Tassi (Sep 27 2022 at 14:02):

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

Julien Puydt (Sep 27 2022 at 14:02):

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

Pierre Roux (Sep 27 2022 at 14:02):

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

Enrico Tassi (Sep 27 2022 at 14:03):

The behavior is expected.

Pierre Roux (Sep 27 2022 at 14:04):

(I'm not sure it's a bug, probably just the efect of Arguments that is local by default (maybe one can use the #[global] attribute but I got used to put all the arguments at the end of sections))

Enrico Tassi (Sep 27 2022 at 14:04):

Yes, I was wrong

Julien Puydt (Sep 27 2022 at 14:06):

@Enrico Tassi yes I should report because you were wrong to think it's an expected behaviour?

Enrico Tassi (Sep 27 2022 at 14:06):

It is not a bug, it is a surprising behavior. Please don't report it.

Enrico Tassi (Sep 27 2022 at 14:08):

I was surprised that implicits were recomputed even if no argument was added by section discharging. But this is not how the system works, it is really your directive which has a local scope. My bad.

Julien Puydt (Sep 27 2022 at 14:13):

Ok, let's go with it, but I hope that code will accept to work when put in ssralg, since that's the goal.

In any case, rewrite worked!

Thanks all!

Notification Bot (Sep 27 2022 at 14:13):

Julien Puydt has marked this topic as resolved.

Last updated: May 31 2023 at 04:01 UTC