无法找到变量的实例
背景：我正在软件基础中进行练习。
Theorem neg_move : forall x y : bool,
x = negb y -> negb x = y.
Proof. Admitted.
Theorem evenb_n__oddb_Sn : forall n : nat,
evenb n = negb (evenb (S n)).
Proof.
intros n. induction n as [| n'].
Case "n = 0".
simpl. reflexivity.
Case "n = S n'".
rewrite -> neg_move.
在最后一行之前，我的子目标是这样的：
evenb (S n') = negb (evenb (S (S n')))
我想将其转换为：
negb (evenb (S n')) = evenb (S (S n'))
当我尝试单步执行 rewrite ->然而，neg_move 会产生以下错误：
错误：无法找到变量 y 的实例。
我确信这真的很简单，但是我做错了什么？ （请不要为了解决evenb_n__oddb_Sn而放弃任何东西，除非我做得完全错误）。
Context: I'm working on exercises in Software Foundations.
Theorem neg_move : forall x y : bool,
x = negb y -> negb x = y.
Proof. Admitted.
Theorem evenb_n__oddb_Sn : forall n : nat,
evenb n = negb (evenb (S n)).
Proof.
intros n. induction n as [| n'].
Case "n = 0".
simpl. reflexivity.
Case "n = S n'".
rewrite -> neg_move.
Before the last line, my subgoal is this:
evenb (S n') = negb (evenb (S (S n')))
And I want to transform it into this:
negb (evenb (S n')) = evenb (S (S n'))
When I try to step through rewrite -> neg_move, however, it produces this error:
Error: Unable to find an instance for the variable y.
I'm sure this is really simple, but what am I doing wrong? (Please don't give anything away for solving evenb_n__oddb_Sn, unless I'm doing it completely wrong).
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
正如 danportin 提到的，Coq 告诉您它不知道如何实例化
y。事实上，当你重写时 -> neg_move，你要求它用y替换一些negb x。现在，Coq 应该在这里使用什么y？它无法弄清楚。一种选择是在重写时显式实例化
y：rewrite -> neg_move with (y:=some_term)这将执行重写并要求您证明前提，这里它将添加一个
x = negb some_term形式的子目标。另一种选择是在重写时专门化
neg_move：rewrite -> (neg_move _ _ H)这里
H必须是some_x = negb some_y类型的项。我为neg_move的x和y参数放置了两个通配符，因为 Coq 能够从H推断出它们分别为some_x和some_y。然后，Coq 将尝试用some_y重写目标中出现的negb some_x。但你首先需要在你的假设中得到这个
H项，这可能会带来一些额外的负担......（请注意，我给你的第一个选项应该相当于
rewrite -> ( neg_move _ some_term))另一种选择是
erewrite -> negb_move，它将添加类似于?x和?y的未实例化变量，并尝试进行重写。然后你必须证明这个前提，它看起来像(evenb (S (S n'))) = negb ?y，希望在解决这个子目标的过程中，Coq 会发现?y从一开始就应该是什么（尽管有一些限制，并且可能会出现一些问题，因为 Coq 在没有弄清楚?y必须是什么的情况下解决了目标）。但是，对于您的特定问题，它相当容易：
对称。应用 neg_move。这就是您想要的（向后，做另一个
对称。如果你关心的话）。As danportin mentioned, Coq is telling you that it does not know how to instantiate
y. Indeed, when you dorewrite -> neg_move, you ask it to replace somenegb xby ay. Now, whatyis Coq supposed to use here? It cannot figure it out.One option is to instantiate
yexplicitly upon rewriting:rewrite -> neg_move with (y:=some_term)This will perform the rewrite and ask you to prove the premises, here it will add a subgoal of the form
x = negb some_term.Another option is to specialize
neg_moveupon rewriting:rewrite -> (neg_move _ _ H)Here
Hmust be a term of typesome_x = negb some_y. I put two wildcards for thexand theyparameters ofneg_movesince Coq is able to infer them fromHas beingsome_xandsome_yrespectively. Coq will then try to rewrite an occurence ofnegb some_xin your goal withsome_y.But you first need to get this
Hterm in your hypotheses, which might be some additional burden...(Note that the first option I gave you should be equivalent to
rewrite -> (neg_move _ some_term))Another option is
erewrite -> negb_move, which will add uninstantiated variables that will look like?xand?y, and try to do the rewrite. You will then have to prove the premise, which will look like(evenb (S (S n'))) = negb ?y, and hopefully in the process of solving this subgoal, Coq will find out what?yshould have been from the start (there are some restrictions though, and some problems may arise is Coq solves the goal without figuring out what?ymust be).However, for your particular problem, it is quite easier:
symmetry.apply neg_move.And that's what you wanted (backwards, do another
symmetry.if you care).