Stream: Coq users

Topic: Determine correct name of argument


view this post on Zulip Ralf Jung (Sep 20 2021 at 22:03):

I want to use a lemma that About prints as follows:

wptp_recv_strong_adequacy :
 (Λ : language) (Σ : gFunctors) (irisGS0 : irisGS Λ Σ) (CS : crash_semantics Λ)
  (Φ : val Λ  iProp Σ) (Φinv Φinv' : generationGS Λ Σ  iProp Σ) (Φr :
                                                                   generationGS Λ Σ
                                                                    val Λ  iProp Σ)
  (κs' : list (observation Λ)) (s : stuckness) (k : nat) (HG : generationGS Λ Σ)
  (ns : list nat) (mj : fracR) (D : coPset) (n : nat) (r1 e1 : expr Λ) (t1 : list (expr Λ))
  (κs : list (observation Λ)) (t2 : list (expr Λ)) (σ1 : state Λ) (g1 : global_state Λ)
  (ncurr : nat) (σ2 : state Λ) (g2 : global_state Λ) (stat : status),
[...]
Arguments wptp_recv_strong_adequacy {Λ Σ irisGS0 CS} {Φ Φinv Φinv' Φr}%function_scope
  {κs'}%list_scope {s} {k}%nat_scope {HG} _%list_scope _ _ _%nat_scope (_ _)%expr_scope (_ _
  _)%list_scope _ _ _%nat_scope _ _ _ _

so I write

wptp_recv_strong_adequacy
                (Φinv' := λ HG,  σ nt, state_interp σ nt - |NC={, }=>  φinv σ )%I
                (κs' := [])

but Coq complains:

Error: Wrong argument name: κs'.

I assume some kind of implicit rename is happening due to sections or so, Coq sometimes likes to do that... but is there any way to figure out the name it picked? I tried κs'0 and similar variations, but none of them is accepted. Rght now it seems impossible to apply this lemma using named argument syntax, which is quite a bummer...

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:49):

You can have coq to account all parameters as explicit, like this Check @wptp_recv_strong_adequacy.
and this @wptp_recv_strong_adequacy lang gfs iris....

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 10:11):

@Ralf Jung can you rename the argument explicitly at definition site? I've also ran into this recently without recourse.

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 10:12):

(because I'm seldom willing to use @, especially with so many arguments around)

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 10:21):

@Ralf Jung as a potential workaround, maybe you can apply @wptp_recv_strong_adequacy with (Φinv' := ...) (κs' := ...), since apply foo with args lets you use names for explicit arguments. Might fail the same way.

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:03):

Andrey Klaus said:

You can have coq to account all parameters as explicit, like this Check @wptp_recv_strong_adequacy.
and this @wptp_recv_strong_adequacy lang gfs iris....

yeah I can write

@wptp_recv_strong_adequacy _ _ _ _ _ _
                ((*Φinv' := *) λ HG,  σ nt, state_interp σ nt - |@NC={iris_crashGS, , }=>  φinv σ )%I
                _ ((*κs' := *) [])

but Id really prefer to use the named argument syntax... if it wasnt so horribly broken...

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:04):

@Paolo Giarrusso this is with iApply, so with is not an option unfortunately

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:05):

hmmmm, does iApply (ltac:(apply …)) work here?

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:06):

I think it did, and I’m at least sure I used iApply (!!(lemma )) with @Enrico Tassi ‘s math-comp !!, which produces something similar

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:06):

Paolo Giarrusso said:

Ralf Jung can you rename the argument explicitly at definition site? I've also ran into this recently without recourse.

that does not help,

Arguments wptp_recv_strong_adequacy {Λ Σ irisGS0} {CS Φ Φinv Φinv' Φr κs' s k HG}.

does not change anything

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:07):

oh, do you need Arguments … : rename?

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:07):

it would tell me if it would be needed...

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:08):

(except in case of bugs?)

view this post on Zulip Théo Winterhalter (Sep 21 2021 at 19:08):

If it's a bug of Arguments maybe having a new Definition as alias.

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:10):

oh interesting, wptp_recv_strong_adequacy (κs' := []) works

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:10):

only if I supply both Φinv' and κs' it fails

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:11):

oh even better, this works

wptp_recv_strong_adequacy
(Φinv' :=   HG,  σ nt, state_interp σ nt - |@NC={iris_crashGS, , }=>  φinv σ )%I)
 (κs' :=  []).

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:11):

but the %I on the outside seems to confuse it

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:12):

oh ugh right, %I is a syntax error!

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:12):

and of course, “wrong name” is _not_ only used for wrong names

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:13):

I forget the rules but I’m pretty confident I’ve seen this error masking other things

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:14):

well this is the worst Coq has lead me astray in quite a while^^

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:15):

okay Check 1 (a := 2). gives “wrong argument name”

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:15):

well yeah S O does not have an argument of name a... that makes sense, in a way?

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:16):

I mean, that makes exactly as much sense as in your case I’d say

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:16):

yes, it’s impossible to interpret a := 2 as a named argument of name ”a” :-)

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:17):

Paolo Giarrusso said:

I mean, that makes exactly as much sense as in your case I’d say

looks very different to me

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:17):

FWIW this works fine

Arguments S {n} : rename.
Check S (n:=0)%nat.

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:18):

do you consider Check 0 (a := 2). different?

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:18):

because the error’s the same

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:18):

I think that “wrong argument name” should be reserved to positions where at least one named argument would be valid, so the error is likely to be a typo.

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:19):

I mean sure for non-functions a more specific error would be better

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:19):

but my issue is something else entirely

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:19):

Definition foo {n m : nat} := 0.
Fail Check foo (n:=0)%nat (m:=0)%nat.
Check foo (n:=0) (m:=0)%nat.

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:19):

only the last one can have a scope... or so...

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:20):

(for better results, it wouldn’t be horrible if Coq showed what is accepted)

view this post on Zulip Gaëtan Gilbert (Sep 21 2021 at 19:21):

foo (n:=0) (m:=0)%nat is (foo (n:=0) (m:=0))%nat btw

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:21):

wat

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:22):

padme: that’s a priority bug?

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:23):

Paolo Giarrusso said:

wat

my thoughts exactly...

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:23):

@foo 0%nat is not the same as (@foo 0)%nat, right?

view this post on Zulip Gaëtan Gilbert (Sep 21 2021 at 19:24):

right, but (n:=0) is not a term so cannot have a scope

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:26):

thanks for root-tracing the behavior, but are you suggesting that it is reasonable?

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:27):

(no, I don’t know on the spot how to define a grammar that doesn’t violate expectations, or in general how to fix that “locally”)

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:27):

Gaëtan Gilbert said:

right, but (n:=0) is not a term so cannot have a scope

well %foo is accepted in many non-term positions.... at least I think I have seen that...
EDIT> hm cannot find any nice examples

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:28):

actually I was wondering whether to add %foo to the grammar for this non-terminal

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:28):

and anyway if it cant have a scope it should just error

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:28):

but accepting foo (name:=term)%scope and then interpreting it in this weird way is definitely a bug

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:28):

it should either be equivalent to foo (name:=(term)%scope) or rejected

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:29):

I guess the bug could be that the grammar is term%scope and term includes term (name := term) — that’d give this effect

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:31):

so it wouldn’t be a parse error, but errors in post-processing can be nicer anyway (parse error tend to trigger backtracking and produce bad messages)

view this post on Zulip Gaëtan Gilbert (Sep 21 2021 at 19:43):

https://github.com/coq/coq/issues/14914

view this post on Zulip Ralf Jung (Sep 21 2021 at 19:46):

Thanks for opening an issue!


Last updated: Feb 01 2023 at 13:03 UTC