Stream: Coq users

Topic: implicit arguments


view this post on Zulip Jeremy Dawson (Dec 26 2020 at 12:16):

Hi,

I have tried to find out when implicit arguments are inserted. Is this
in the documentation anywhere?

With a function

lja_dd_ord < About no_rpt_same.
no_rpt_same :
forall U : Type,
relationT U ->
forall (rules : list U -> U -> Type) (prems : U -> Type) (c0 : U),
derrec rules prems c0 -> Type

Arguments U, rules, prems, c0 are implicit

I find

lja_dd_ord < Check no_rpt_same seq_ord.
no_rpt_same seq_ord
: forall (rules : list (srseq (PropF ?V)) -> srseq (PropF ?V)
-> Type)
(prems0 : srseq (PropF ?V) -> Type) (c0 : srseq (PropF ?V)),
derrec rules prems0 c0 -> Type

which is as I expected (as a matter of fact, I can't find this
documented either, but I've discovered from experience that implicit
arguments (non-maximal) are inserted up to the last explicit argument)

but

lja_dd_ord < Check no_rpt_same seq_ord (prems:=prems).
no_rpt_same seq_ord (prems:=prems)
: forall c0 : srseq (PropF V), derrec ?rules prems c0 -> Type

ie it seems to have inserted the implicit argument rules also.

What are the rules about this?

And if there are any tips for finding things like this in the
documentation, I'd appreciate it.

Thanks

Jeremy

view this post on Zulip Théo Zimmermann (Dec 26 2020 at 13:32):

Hi Jeremy, I would be happy to determine with you where the documentation could be improved if it doesn't contain sufficient or sufficiently clear information.

view this post on Zulip Théo Zimmermann (Dec 26 2020 at 13:34):

Note that in Coq 8.12, the implicit status (maximal vs non-maximal) of arguments is made even clearer by reusing the { ... } / [ ... ] syntax in the output of About.

view this post on Zulip Théo Zimmermann (Dec 26 2020 at 13:35):

What do you think of the explanation in the first paragraph here: https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments ?

view this post on Zulip Théo Zimmermann (Dec 26 2020 at 13:36):

You think it should say more explicitly that non-maximal implicit arguments are inserted up to the last argument provided (whatever the status of this argument is)?

view this post on Zulip Théo Zimmermann (Dec 26 2020 at 13:40):

In any case, it seems that this rule (that may need to be made more explicit in the doc) explains both your first and your second example.

view this post on Zulip Jeremy Dawson (Dec 27 2020 at 14:11):

Hi Theo,

Yes the first para at :
https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments
seems clear (though this is something I already understood, so I guess I'm not
the best judge), though perhaps it should be noted that "partial application"
includes the situation where no arguments at all are provided. I guess the
reason I didn't find this originally was because it appears in the middle of a
document about how Coq or the user determines which arguments are implicit and
which aren't. I think this is important, because a user needs to know how
implicit arguments are used, he/she doesn't need to know how Coq decides to
make arguments implicit or not.

But do you mean also to suggest that that paragraph is meant to apply also to
the situation where an argument is given in the form (a := x)? If so, that is
not at all clear.

And if it does mean that, then wouldn't that mean that if f is defined as
f a b = ..., with both a and b being non-maximal implicit arguments,
then writing f (b := x) causes a to be inferred and inserted?

And if that is the case, then where it says in the following paragraph
"An implicit argument is considered trailing when all following arguments are
implicit. Trailing implicit arguments must be declared as maximally inserted;
otherwise they would never be inserted.", then that wouldn't be correct.

Cheers,

Jeremy

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:00):

@Jeremy Dawson

"partial application" includes the situation where no arguments at all are provided

Indeed, you're right that this is non-obvious.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:00):

it appears in the middle of a document about how Coq or the user determines which arguments are implicit and which aren't. I think this is important, because a user needs to know how implicit arguments are used, he/she doesn't need to know how Coq decides to make arguments implicit or not.

The section itself is not about that and the page as a whole is all (or most of) the documentation there is on implicit arguments, but you are probably right that the two types of implicit arguments is probably the first thing that should be presented.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:00):

he/she doesn't need to know how Coq decides to make arguments implicit or not.

This seems relatively important that this is predictable for a user wanting to Set Implicit Arguments but probably most of the users today prefer to set implicit arguments manually anyway.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:00):

But do you mean also to suggest that that paragraph is meant to apply also to the situation where an argument is given in the form (a := x)? If so, that is not at all clear.

Yes, and OK, this should be clarified.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:00):

And if it does mean that, then wouldn't that mean that if f is defined as f a b = ..., with both a and b being non-maximal implicit arguments, then writing f (b := x) causes a to be inferred and inserted?

Yes.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:07):

And if that is the case, then where it says in the following paragraph "An implicit argument is considered trailing when all following arguments are
implicit. Trailing implicit arguments must be declared as maximally inserted; otherwise they would never be inserted.", then that wouldn't be correct.

I guess you are right, although this is not the way implicit arguments are meant to be used most of the time. By the way, this also raises the question of what it means to have a maximal implicit argument follow a non-maximal one...

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:09):

Well, to answer my own question, a maximal implicit argument following a non-maximal one will behave as a non-maximal implicit argument, except when the previous argument is provided using the named argument syntax.

view this post on Zulip Théo Zimmermann (Dec 27 2020 at 22:11):

Thus, it seems that we could be consistent and not allow this case or be more lax and allow trailing implicit arguments to be non-maximal (except for the very last one).

view this post on Zulip Paolo Giarrusso (Dec 28 2020 at 20:30):

"Set Implicit Arguments" is still somewhat common (e.g. in math-comp), but the point stands: its behavior should come after the actual semantics of implicit arguments, as a more advanced topic.


Last updated: Feb 04 2023 at 21:02 UTC