0

我已经开始学习 Coq，并试图证明一些看起来相当简单的事情：如果一个列表包含 x，那么该列表中 x 的实例数将 > 0。

我定义了 contains 和 count 函数如下：

Fixpoint contains (n: nat) (l: list nat) : Prop :=
  match l with
  | nil => False
  | h :: t => if beq_nat h n then True else contains n t
  end.

Fixpoint count (n acc: nat) (l: list nat) : nat :=
  match l with
  | nil => acc
  | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
  end.

我试图证明：

Lemma contains_count_ge1 : forall (n: nat) (l: list nat), contains n l -> (count n 0 l > 0).

我知道证明将涉及展开计数和包含的定义，但我想说“列表不能为零，因为包含是真的，所以必须有一个元素是x真的”，我'玩了一会儿，但不知道如何使用战术来做到这一点。任何指导将不胜感激。lbeq_nat h x

4

2 回答 2

6

ejgallego 已经在他的回答中为您的问题提供了很好的解决方案。我仍然想指出他遗漏的重要一点：在 Coq 中，你必须始终从第一原理开始争论，并且对你的证明非常迂腐和精确。

您认为证明应按以下步骤进行：

列表不可能是nil，因为contains是真的，所以其中必须有一个元素x是。lbeq_nat h xtrue

尽管这对人类来说具有直观意义，但对于 Coq 来说还不够精确。正如 ejgallego 的回答所示，问题在于您的非正式推理隐藏了归纳的使用。事实上，在将其转化为策略之前，尝试更详细地扩展您的论点是很有用的。我们可以这样进行，例如：

让我们证明，对于每个n : natand ns : list nat，都contains n ns蕴含count n 0 ns > 0。我们通过归纳对列表进行ns。如果ns = nil， 的定义contains意味着False成立；一个矛盾。因此，我们只剩下这种情况ns = n' :: ns'，我们可以使用以下归纳假设：contains n ns' -> count n 0 ns' > 0。有两个子情况需要考虑：beq_nat n n'是否true。

  • 如果beq_nat n n'是true，根据 的定义count，我们看到我们只需要证明count n (0 + 1) ns' > 0。请注意，这里没有直接的方法。count这是因为您使用累加器以递归方式编写了尾部。虽然这在函数式编程中是完全合理的，但它会使证明属性count变得更加困难。在这种情况下，我们需要以下辅助引理，也可以通过归纳证明：forall n acc ns, count n acc ns = acc + count n 0 ns. 我会让你弄清楚如何证明这一点。但是假设我们已经建立了它，那么目标将简化为显示1 + count n 0 ns' > 0. 这通过简单的算术是正确的。（有一种更简单的方法不需要辅助引理，但需要稍微概括您要证明的陈述。）

  • 如果beq_nat n n'是，根据andfalse的定义，我们需要证明这意味着。这正是归纳假设给我们的，我们已经完成了。containscountcontains n ns'count n 0 ns' > 0

这里有两个教训需要学习。第一个是做正式证明通常需要将你的直觉翻译成系统可以理解的正式术语。我们直观地知道让某些元素出现在列表中意味着什么。但是，如果我们要更正式地解释这意味着什么，我们将诉诸于列表的某种递归遍历，这很可能count就是您在 Coq 中编写的定义。为了推理递归，我们需要归纳。第二个教训是，你在 Coq 中定义事物的方式会对你编写的证明产生重要影响。ejgallego 的解决方案不需要任何超出标准库中的辅助引理，正是因为他的定义count不是尾递归的。

于 2017-04-17T16:15:11.563 回答
2

好吧，你提出了许多关于基本 Coq 的问题，超出了 IMO 可能在这里解决的问题。对于这个特定的问题，我会这样处理（实际上我会使用 MathComp 中已经提供的引理）：

From Coq Require Import PeanoNat Bool List.

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => if Nat.eqb h n then true else contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil => 0
  | h :: t => if Nat.eqb h n then S (count n t) else count n t
  end.

Lemma contains_count_ge1 n l : contains n l = true -> count n l > 0.
Proof.
induction l as [|x l IHl]; simpl; [now congruence|].
now destruct (Nat.eqb_spec x n); auto with arith.
Qed.

我的“标准”解决方案：

Lemma test n (l : list nat) : n \in l -> 0 < count_mem n l.
Proof. by rewrite lt0n => /count_memPn/eqP. Qed.

count和的不同定义contains可能被证明是有用的：

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => Nat.eqb h n || contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil    => 0
  | h :: t => Nat.b2n (Nat.eqb h n) + (count n t)
  end.
于 2017-04-17T13:23:12.420 回答