Stream: Coq users

Topic: apply with Error: no such bound variable

view this post on Zulip Audrey Seo (Mar 20 2023 at 17:49):

I'm trying to update coq from 8.14.0 to 8.15.2 or 8.16.1. On both 8.15.2 and 8.16.1, however, I get error messages when i try to use apply <some hypothesis> with (<argument name> := ...). For example, when I have

H : forall (frame : nat) (x0 : list nat) (stk' : stack)
        (v : nat) (stk2 : list nat),
      aexp_frame_rule aexp fenv frame ->
      (stk1 ++ x, c) = (stk', v) ->
      stk1 ++ x = stk2 ++ x0 ->
      stk' = stk2 ++ x0 ->
      Datatypes.length stk2 = frame ->
      forall x' : list nat,
      aexp_stack_sem aexp fenv (stk2 ++ x') (stk2 ++ x', v)

in my context, and I try

eapply H with (stk2 := stk1) (x0 := x) (v := c) (stk' := stk1 ++ x) (x' := x') in H12.

I get the error

Error: No such bound variable stk2 (possible names are: frame, x, stk', v, stk1 and x').

(Also, x, stk', stk1, and x' are all bound in the context. v however is not, and only shows up as a quantified variable in H.)

I've been able to use workarounds like apply (<hypothesis name> <arguments>), but there are still approximately 190 places where I would have to make changes, and I wouldn't be able to just use a find and replace to fix them because the arguments aren't always in order.

Is there a better way of doing this? I've been unable to find any information about this elsewhere. Additionally, I was TA-ing a class that used Coq, and multiple students had issues with this same problem as well.

view this post on Zulip Gaëtan Gilbert (Mar 20 2023 at 17:54):

stk2 is the renamed printing name of stk1 (you can tell from the "possible names are ..."
its real name is stk1
apply stopped using the renamed names and uses the real names instead
this can be confusing but the previous behaviour was also a problem in other cases

view this post on Zulip Audrey Seo (Mar 20 2023 at 18:51):

Oh, thanks for letting me know! is there any way to see what the real names are/turn off the renaming of printing names?

view this post on Zulip Gaëtan Gilbert (Mar 20 2023 at 19:03):

for hypotheses it seems impossible other than relying on what the error tells you
otherwise About H would work saying Arguments H frame x stk' ... (ie if H is a definition or a section variable)

Last updated: Apr 19 2024 at 07:02 UTC