破坏应用谓词功能的结果

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'。对于一般情况，我想做的是将（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).

一切都会很好。