coq - 破坏应用谓词函数的结果

Question

我是 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) 设为 true 或 false，但我似乎无法让它发挥作用——我错过了一些 Coq 语法。

有任何想法吗？

Answer 1

你的代码坏了

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).

一切都会好起来的。