涉及在 COQ 中展开两个递归函数的证明

Question

我已经开始学习 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).

我知道证明将涉及展开 count 和 contains 的定义，但我想说 "the list cannot be nil, as contains is true, so there must be an element x in l such that beq_nat h x is true"，我玩了一会儿但不知道如何使用策略来做到这一点。任何指导将不胜感激。

Answer 1

好吧，除了 IMO 在此处可能解决的问题之外，您还提出了很多关于 Coq 的基本问题。对于这个特定的问题，我会这样做（实际上我会使用 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.

我的"standard"解决方案：

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.

Answer 2

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

您认为证明应按如下方式进行：

The list cannot be nil, as contains is true, so there must be an element x in l such that beq_nat h x is true.

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

让我们证明，对于每个 n : nat 和 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'是false，根据contains和count的定义，我们需要证明contains n ns'意味着 count n 0 ns' > 0。这正是归纳假设给我们的，我们就完成了。

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

涉及在 COQ 中展开两个递归函数的证明

Proof involving unfolding two recursive functions in COQ

coq

proof

coq-tactic