10

背景：我正在做软件基础的练习。

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，除非我做错了）。

4

1 回答 1

10

正如 danportin 提到的，Coq 告诉你它不知道如何实例化y. 确实，当您这样做时rewrite -> neg_move，您要求它用 . 替换negb x一些y。现在，yCoq 应该在这里使用什么？它想不通。

一种选择是y在重写时显式实例化：

rewrite -> neg_move with (y:=some_term)

这将执行重写并要求您证明前提，这里它将添加表单的子目标x = negb some_term。

另一种选择是专注neg_move于重写：

rewrite -> (neg_move _ _ H)

这里H必须是一个类型的术语some_x = negb some_y。x我为 the和 的y参数添加了两个通配符，neg_move因为 Coq 能够分别从Hassome_x和推断它们some_y。然后 Coq 将尝试negb some_x用some_y. 但是你首先需要H在你的假设中得到这个术语，这可能是一些额外的负担......

（请注意，我给您的第一个选项应该等同于rewrite -> (neg_move _ some_term)）

另一个选项是erewrite -> negb_move，它将添加看起来像?x和的未实例化变量?y，并尝试进行重写。然后你必须证明这个前提，(evenb (S (S n'))) = negb ?y看起来?y像没有弄清楚?y必须是什么的目标）。

但是，对于您的特定问题，它更容易：

==========
evenb (S n') = negb (evenb (S (S n')))

symmetry.

==========
negb (evenb (S (S n'))) = evenb (S n')

apply neg_move.

==========
evenb (S (S n')) = negb (evenb (S n'))

symmetry.这就是你想要的（向后，如果你在乎，再做一个）。

于 2012-01-16T09:16:50.380 回答