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.
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
Oh, thanks for letting me know! is there any way to see what the real names are/turn off the renaming of printing names?
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: Oct 13 2024 at 01:02 UTC