无法找到变量的实例

Question

上下文:我正在从事软件基础的练习.

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除非我完全错了,否则请不要给任何东西解决问题).

Answer 1

正如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和y参数neg_move,因为勒柯克能够从他们推断H为some_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,并且希望在解决这个子目标的过程中,Coq会发现?y从一开始应该有什么(虽然有一些限制,但可能会出现一些问题,Coq解决了没有弄清楚?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.如果你关心的话再做一次).