Stream: math-comp devs

Topic: Ticket #928


view this post on Zulip 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...

view this post on Zulip Pierre Roux (Sep 27 2022 at 12:52):

Maybe implicit arguments, have you tried Check @f?

view this post on Zulip 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

view this post on Zulip Pierre Roux (Sep 27 2022 at 13:13):

Looks like the explanation indeed

view this post on Zulip Julien Puydt (Sep 27 2022 at 13:16):

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

view this post on Zulip 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).

view this post on Zulip Julien Puydt (Sep 27 2022 at 13:21):

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

view this post on Zulip Enrico Tassi (Sep 27 2022 at 13:23):

Paste the output of About telescope_sumr_eq.

view this post on Zulip Enrico Tassi (Sep 27 2022 at 13:24):

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

view this post on Zulip 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

view this post on Zulip Julien Puydt (Sep 27 2022 at 13:25):

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

view this post on Zulip 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 @

view this post on Zulip Pierre Roux (Sep 27 2022 at 13:26):

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

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Sep 27 2022 at 13:26):

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

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Sep 27 2022 at 13:27):

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

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Sep 27 2022 at 13:28):

I thought { } was the implicit?

view this post on Zulip 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))

view this post on Zulip Enrico Tassi (Sep 27 2022 at 13:28):

They both are

view this post on Zulip Julien Puydt (Sep 27 2022 at 13:28):

oh, dear

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 27 2022 at 13:32):

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

view this post on Zulip Enrico Tassi (Sep 27 2022 at 13:32):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 _

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Sep 27 2022 at 14:02):

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

view this post on Zulip Enrico Tassi (Sep 27 2022 at 14:02):

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

view this post on Zulip Julien Puydt (Sep 27 2022 at 14:02):

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

view this post on Zulip Pierre Roux (Sep 27 2022 at 14:02):

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