6

我是 Coq 的新手，有一个关于破坏策略的快速问题。假设我有一个count函数可以计算给定自然数在自然数列表中出现的次数：

Fixpoint count (v : nat) (xs : natlist) : nat :=
  match xs with
    | nil => 0
    | h :: t =>
      match beq_nat h v with
        | true => 1 + count v xs
        | false => count v xs
      end
  end.

我想证明以下定理：

Theorem count_cons : forall (n y : nat) (xs : natlist),
  count n (y :: xs) = count n xs + count n [y].

如果我要证明 n = 0 的类似定理，我可以简单地将 y 破坏为 0 或 S y'。对于一般情况，我想做的是 destruct (beq_nat ny) 为真或假，但我似乎无法让它工作——我错过了一些 Coq 语法。

有任何想法吗？

4

1 回答 1

5

你的代码坏了

Fixpoint count (v : nat) (xs : natlist) : nat :=
 match xs with
  | nil => 0
  | h :: t =>
  match beq_nat h v with
    | true => 1 + count v xs (*will not compile since "count v xs" is not simply recursive*)
    | false => count v xs
  end
end.

你可能是说

Fixpoint count (v : nat) (xs : natlist) : nat :=
 match xs with
  | nil => 0
  | h :: t =>
  match beq_nat h v with
    | true => 1 + count v t
    | false => count v t
  end
end.

使用destruct是获得解决方案的绝佳方式。但是，你需要记住一些事情

  • destruct是句法，即它替换了在您的目标/假设中表达的术语。因此，您通常需要simpl（在此处工作）或unfold首先需要类似的东西。
  • 术语的顺序很重要。 destruct (beq_nat n y)不是一回事destruct (beq_nat y n)。在这种情况下，您需要其中的第二个

一般来说，问题是destruct愚蠢的，所以你必须自己做聪明的事。

无论如何，开始你的证明

intros n y xs. simpl. destruct (beq_nat y n).

一切都会好的。

于 2011-12-27T03:58:37.723 回答