Ralf Jung (Sep 20 2021 at 22:03): 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...
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....
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.
Paolo Giarrusso (Sep 21 2021 at 10:12):(because I'm seldom willing to use @, especially with so many arguments around)
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.
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...
Ralf Jung (Sep 21 2021 at 19:04):@Paolo Giarrusso this is with iApply, so with is not an option unfortunately
Paolo Giarrusso (Sep 21 2021 at 19:05):hmmmm, does iApply (ltac:(apply …)) work here?
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
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
Paolo Giarrusso (Sep 21 2021 at 19:07):oh, do you need Arguments … : rename?
Ralf Jung (Sep 21 2021 at 19:07):it would tell me if it would be needed...
Paolo Giarrusso (Sep 21 2021 at 19:08):(except in case of bugs?)
Théo Winterhalter (Sep 21 2021 at 19:08):If it's a bug of Arguments maybe having a new Definition as alias.
Ralf Jung (Sep 21 2021 at 19:10):oh interesting, wptp_recv_strong_adequacy (κs' := []) works
Ralf Jung (Sep 21 2021 at 19:10):only if I supply both Φinv' and κs' it fails
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' := []).
but the %I on the outside seems to confuse it
Paolo Giarrusso (Sep 21 2021 at 19:12):oh ugh right, %I is a syntax error!
Paolo Giarrusso (Sep 21 2021 at 19:12):and of course, “wrong name” is _not_ only used for wrong names
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
Ralf Jung (Sep 21 2021 at 19:14):well this is the worst Coq has lead me astray in quite a while^^
Paolo Giarrusso (Sep 21 2021 at 19:15):okay Check 1 (a := 2). gives “wrong argument name”
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?
Paolo Giarrusso (Sep 21 2021 at 19:16):I mean, that makes exactly as much sense as in your case I’d say
Paolo Giarrusso (Sep 21 2021 at 19:16):yes, it’s impossible to interpret a := 2 as a named argument of name ”a” :-)
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
Ralf Jung (Sep 21 2021 at 19:17):FWIW this works fine
Arguments S {n} : rename.
Check S (n:=0)%nat.
do you consider Check 0 (a := 2). different?
Paolo Giarrusso (Sep 21 2021 at 19:18):because the error’s the same
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.
Ralf Jung (Sep 21 2021 at 19:19):I mean sure for non-functions a more specific error would be better
Ralf Jung (Sep 21 2021 at 19:19):but my issue is something else entirely
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.
only the last one can have a scope... or so...
Paolo Giarrusso (Sep 21 2021 at 19:20):(for better results, it wouldn’t be horrible if Coq showed what is accepted)
Gaëtan Gilbert (Sep 21 2021 at 19:21):foo (n:=0) (m:=0)%nat is (foo (n:=0) (m:=0))%nat btw
Paolo Giarrusso (Sep 21 2021 at 19:21):wat
Paolo Giarrusso (Sep 21 2021 at 19:22):padme: that’s a priority bug?
Ralf Jung (Sep 21 2021 at 19:23):Paolo Giarrusso said:
wat
my thoughts exactly...
Ralf Jung (Sep 21 2021 at 19:23):@foo 0%nat is not the same as (@foo 0)%nat, right?
Gaëtan Gilbert (Sep 21 2021 at 19:24):right, but (n:=0) is not a term so cannot have a scope
Paolo Giarrusso (Sep 21 2021 at 19:26):thanks for root-tracing the behavior, but are you suggesting that it is reasonable?
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”)
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
Paolo Giarrusso (Sep 21 2021 at 19:28):actually I was wondering whether to add %foo to the grammar for this non-terminal
Ralf Jung (Sep 21 2021 at 19:28):and anyway if it cant have a scope it should just error
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
Ralf Jung (Sep 21 2021 at 19:28):it should either be equivalent to foo (name:=(term)%scope) or rejected
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
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)
Gaëtan Gilbert (Sep 21 2021 at 19:43):https://github.com/coq/coq/issues/14914
Ralf Jung (Sep 21 2021 at 19:46):Thanks for opening an issue!
Last updated: Oct 13 2024 at 01:02 UTC