关于列表的推理 Reasoning About Lists

与数字一样，关于列表处理函数的简单事实有时完全可以通过简化来证明。例如，对于这个定理来说，仅仅通过自反性进行简化就足够了。。。

Theorem nil_app : forall l : natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

…因为在app的定义中，[]被替换为“scrutinee”（其值被匹配项“仔细检查”的表达式），从而简化了匹配项本身。

此外，与数字一样，对未知列表的可能形状（空或非空）执行案例分析有时也很有用。

Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)

在这里，nil的情况是有效的，因为我们选择定义tl nil=nil。注意，这里析构函数策略上的as注释引入了两个名称，n和l'，对应于列表的cons构造函数接受两个参数（它正在构造的列表的头和尾）。

然而，关于列表的有趣定理通常需要归纳来证明。我们将看看下一步如何做。

（微布道：随着我们对这篇材料的深入，简单地阅读校对脚本不会让你走得太远！重要的是使用Coq逐步了解每一步的细节，并思考每一步的效果。否则，或多或少可以保证当你接触到它们时，这些练习毫无意义。”努夫说。）

列表归纳 Induction on Lists

通过natlist之类的数据类型进行归纳的证明比标准的自然数归纳稍微不那么熟悉，但其思想同样简单。每个归纳声明定义了一组数据值，这些数据值可以使用声明的构造函数构建。例如，布尔值可以是true或false；一个数字可以是O或S应用于另一个数字；列表可以是nil，也可以是cons，用于数字和列表。此外，声明的构造函数相互之间的应用是归纳定义集的元素可以具有的唯一可能的形状。

这最后一个事实直接导致了一种关于归纳定义集的推理方式：一个数字要么是O，要么应用于某个较小的数字；一个列表要么为零，要么它被应用于一些数字和一些较小的列表；等等，如果我们想到一个命题P，它提到了一个列表l，我们想证明P对所有列表都成立，我们可以这样推理：

首先，当l为零时，证明P对l是真的。

然后证明P对l是真的，当l对一些数字n和一些较小的列表l是cons n l'时，假设P对l是真的。

由于较大的列表总是可以分解为较小的列表，最终达到零，这两个参数共同建立了所有列表l的P的真理。下面是一个具体的例子：

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons n l1' *)
    simpl. rewrite -> IHl1'. reflexivity.  Qed.

注意，当对自然数进行归纳时，as。。。提供给归纳策略的子句给出了归纳假设的名称，对应于cons情况下较小的列表l1’。

再一次，作为一个静态文档，这个Coq证明并不是特别有启发性——如果你在一个交互式Coq会话中阅读证明，你很容易看到发生了什么，你可以在每个点上看到当前的目标和上下文，但是这个状态在Coq证明的记录部分是不可见的。因此，自然语言证明——为人类读者编写的证明——需要包括更明确的路标；特别是，如果我们提醒读者第二种情况下的归纳假设是什么，这将有助于读者保持导向。

为了比较，这里是同一定理的非正式证明。

Theorem: For all lists l1, l2, and l3, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof: By induction on l1.
First, suppose l1 = []. We must show
       ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),
which follows directly from the definition of ++.
Next, suppose l1 = n::l1', with
       (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
(the induction hypothesis). We must show
       ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).
By the definition of ++, this follows from
       n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),
which is immediate from the induction hypothesis.

反转列表 Reversing a List

对于一个稍微复杂的列表归纳证明示例，假设我们使用app定义一个列表反转函数rev:

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒ rev t ++ [h]
  end.
Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

对于比我们到目前为止看到的证明更具挑战性的内容，让我们证明反转列表不会改变其长度。我们的第一次尝试在后续案例中受阻。。。

Theorem rev_length_firsttry : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = n :: l' *)
    (* This is the tricky case.  Let's begin as usual
       by simplifying. *)
    simpl.
    (* Now we seem to be stuck: the goal is an equality
       involving [++], but we don't have any useful equations
       in either the immediate context or in the global
       environment!  We can make a little progress by using
       the IH to rewrite the goal... *)
    rewrite <- IHl'.
    (* ... but now we can't go any further. *)
Abort.

那么让我们用一个关于++和长度的方程，它可以使我们在遇到困难的时候取得进展，并把它作为一个单独的引理来表述。

Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  (* WORKED IN CLASS *)
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons *)
    simpl. rewrite -> IHl1'. reflexivity.  Qed.

注意，为了使引理尽可能一般化，我们对所有的natlists进行了量化，而不仅仅是那些应用rev得到的结果。这似乎很自然，因为目标的真实性显然并不取决于列表是否颠倒。此外，更容易证明更一般的性质。

现在我们可以完成原始证明了。

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> app_length.
    simpl. rewrite -> IHl'. rewrite add_comm.
    reflexivity.
Qed.

为了进行比较，以下是这两个定理的非正式证明：

Theorem: For all lists l1 and l2, length (l1 ++ l2) = length l1 + length l2.
Proof: By induction on l1.
First, suppose l1 = []. We must show
        length ([] ++ l2) = length [] + length l2,
which follows directly from the definitions of length, ++, and plus.
Next, suppose l1 = n::l1', with
        length (l1' ++ l2) = length l1' + length l2.
We must show
        length ((n::l1') ++ l2) = length (n::l1') + length l2.
This follows directly from the definitions of length and ++ together with the induction hypothesis.

Theorem: For all lists l, length (rev l) = length l.
Proof: By induction on l.
First, suppose l = []. We must show
          length (rev []) = length [],
which follows directly from the definitions of length and rev.
Next, suppose l = n::l', with
          length (rev l') = length l'.
We must show
          length (rev (n :: l')) = length (n :: l').
By the definition of rev, this follows from
          length ((rev l') ++ [n]) = S (length l')
which, by the previous lemma, is the same as
          length (rev l') + length [n] = S (length l').
This follows directly from the induction hypothesis and the definition of length.

这些校样的风格相当冗长和迂腐。在阅读了这样的几篇文章之后，我们可能会发现遵循给出较少细节的证明（我们可以很容易地在自己的头脑中或在草稿纸上找到这些细节，如果必要的话）更容易，只需强调不明显的步骤。在这种更为压缩的样式中，上述证明可能如下所示：

Theorem: For all lists l, length (rev l) = length l.
Proof: First, observe that length (l ++ [n]) = S (length l) for any l, by a straightforward induction on l. The main property again follows by induction on l, using the observation together with the induction hypothesis in the case where l = n'::l'.

在特定情况下，哪种风格更可取取决于预期观众的复杂程度，以及手头的证据与他们已经熟悉的证据有多相似。对于我们目前的目的来说，更迂腐的风格是一个很好的默认。

搜索 Search

我们已经看到，证明可以利用我们已经证明的其他定理，例如，使用重写。但是为了引用一个定理，我们需要知道它的名字！事实上，人们甚至很难记住已经证明了哪些定理，更不用说它们被称为什么了。

Coq的搜索命令在这方面非常有用。假设你忘记了一个关于rev的定理的名字。Search rev命令将使Coq显示所有涉及rev的定理的列表。

Search rev.

alt

或者说你忘记了证明加号是可交换的定理的名字。您可以使用模式来搜索所有涉及两个加法相等的定理。

Search (_ + _ = _ + _).

alt

您将在那里看到许多结果，几乎所有结果都来自标准库。要限制结果，您可以在特定模块内搜索：

Search (_ + _ = _ + _) inside Induction.

alt

还可以在搜索模式中使用变量而不是通配符，从而使搜索更精确：

Search (?x + ?y = ?y + ?x).

alt

变量前面的问号需要表明它是搜索模式中的变量，而不是当前预期在范围内的变量。

在做以下练习和阅读本书其余部分时，请牢记搜索；它可以节省你很多时间！ Your IDE likely has its own functionality to help with searching. For example, in ProofGeneral, you can run [Search] with [C-c C-a C-a], and paste its response into your buffer with [C-c C-;].

List Exercises, Part 1

33: 3 stars, standard (list_exercises)

更多列表练习：

Theorem app_nil_r

Theorem app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
intros l. induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl. rewrite -> IHl'. reflexivity.
Qed.

Theorem rev_app_distr

Theorem rev_app_distr: forall l1 l2 : natlist,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem rev_app_distr: forall l1 l2 : natlist,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros l1 l2. induction l1 as [| n l1' IHl1'].
- simpl. rewrite -> app_nil_r. reflexivity.
- simpl. rewrite -> IHl1'. rewrite -> app_assoc. reflexivity.
Qed.

Theorem rev_involutive

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem rev_involutive : forall l : natlist,
rev (rev l) = l.
Proof.
intros l. induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl.  rewrite -> rev_app_distr. simpl.  rewrite -> IHl'. reflexivity.
Qed.

下一个问题有一个简短的解决方案。如果你发现自己陷入困境，退后一步，尝试寻找一种更简单的方法。

Theorem app_assoc4

Theorem app_assoc4 : ∀ l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
intros l1 l2 l3 l4. induction l1 as [| n l1' IHl1'].
  - induction l2 as [| n l2' IHl2']. (* l1 = nil *)
  -- simpl. reflexivity. (* l2 = nil *)
  -- simpl.  rewrite -> app_assoc. reflexivity. (* l2 = cons n l2' *)
  - simpl. rewrite -> app_assoc. rewrite -> app_assoc. reflexivity.  Qed.

Lemma nonzeros_app 关于[非零]实现的练习：

Lemma nonzeros_app : forall l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem nonzeros_nil : forall l : natlist,
nonzeros l ++ [] = nonzeros l ++ nonzeros [].
Proof. 
intros l. induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

Lemma nonzeros_app : forall l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
intros l1 l2. induction l1 as [| n l1' IHl1'].
- simpl. reflexivity.
- simpl. rewrite -> IHl1'. induction l2 as [| n' l2' IHl2'].
-- simpl.  rewrite -> app_nil_r. destruct n as [| n'] eqn:E.
  --- simpl. rewrite -> nonzeros_nil.  rewrite <- IHl1'. rewrite -> app_nil_r. reflexivity.
  --- simpl. rewrite -> nonzeros_nil.  rewrite <- IHl1'. rewrite -> app_nil_r. reflexivity.
-- simpl. destruct n as [| n''] eqn:E.
  --- simpl. reflexivity.
  --- simpl. reflexivity.
Qed.

34: 2 stars, standard (eqblist)

填写[eqblist]的定义，它比较数字列表是否相等。证明[eqblist l]对每个列表[l]都产生[true]。

Fixpoint eqblist (l1 l2 : natlist) : bool

Fixpoint eqblist (l1 l2 : natlist) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_eqblist1 :
(eqblist nil nil = true).
(* FILL IN HERE *) Admitted.

Example test_eqblist2 :
eqblist [1;2;3] [1;2;3] = true.
(* FILL IN HERE *) Admitted.

Example test_eqblist3 :
eqblist [1;2;3] [1;2;4] = false.
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint eqblist (l1 l2 : natlist) : bool:=
match l1,l2 with
|nil,nil => true
|h :: t,nil => false
|nil,h' :: t'=>false
|h'' :: t'',h''' :: t'''=>if h'' =? h''' then eqblist t''  t'''
                       else false
end.

Example test_eqblist1 :
(eqblist nil nil = true).
Proof. reflexivity. Qed.

Example test_eqblist2 :
eqblist [1;2;3] [1;2;3] = true.
Proof. reflexivity. Qed.

Example test_eqblist3 :
eqblist [1;2;3] [1;2;4] = false.
Proof. reflexivity. Qed.

Theorem eqblist_refl

Theorem eqblist_refl : forall l:natlist,
true = eqblist l l.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Search (?n =? ?n).
Theorem eqblist_refl : forall l:natlist,
true = eqblist l l.
Proof.
intros l. induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl. rewrite <- IHl'. rewrite -> eqb_refl.  reflexivity.
Qed.

List Exercises, Part 2

35: 1 star, standard (count_member_nonzero)

Theorem count_member_nonzero

Theorem count_member_nonzero : forall (s : bag),
  1 <=? (count 1 (1 :: s)) = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem count_member_nonzero : forall (s : bag),
1 <=? (count 1 (1 :: s)) = true.
Proof.
intros s. induction s as [| n s' IHs'].
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

下面关于[ltrue.eb]的引理可能会在下一个练习中对您有所帮助（在后面的章节中也会很有用）。

Theorem leb_n_Sn

Theorem leb_n_Sn : forall n,
n <=? (S n) = true.
Proof.
intros n. induction n as [| n' IHn'].
- (* 0 *)
  simpl.  reflexivity.
- (* S n' *)
  simpl.  rewrite IHn'.  reflexivity.  Qed.

在做下一个练习之前，请确保您已经填写了上面[remove_one]的定义。

36: 3 stars, advanced (remove_does_not_increase_count)

Theorem remove_does_not_increase_count

Theorem remove_does_not_increase_count: forall (s : bag),
 (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
intros s. induction s as [| n s' IHs'].
- simpl. reflexivity.
- simpl. rewrite <- IHs'. 
 (* FILL IN HERE *) Admitted.

Coq代码

Theorem remove_does_not_increase_count: forall (s : bag),
(count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
intros s. induction s as [| n s' IHs'].
- simpl. reflexivity.
-  simpl. destruct n as [| n'] eqn:E.
-- simpl. rewrite -> leb_n_Sn. reflexivity.
-- simpl. rewrite -> IHs'. reflexivity.
Qed.

37: 3 stars, standard, optional (bag_count_sum)

写下一个关于涉及函数[count]和[sum]的包的有趣定理[bag_count_sum]，并用Coq证明它。（您可能会发现证明的难度取决于您如何定义[count]！提示：如果您使用[=？]定义[count]，您可能会发现知道[destruct]适用于任意表达式，而不仅仅是简单的标识符非常有用。

38: 4 stars, advanced (rev_injective)

证明[rev]函数是***的。要做到这一点，有一个艰难的方法，也有一个简单的方法。

Theorem rev_injective

Theorem rev_injective : forall (l1 l2 : natlist),
  rev l1 = rev l2 -> l1 = l2.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem rev_injective : forall (l1 l2 : natlist),
  rev l1 = rev l2 -> l1 = l2.
Proof.
intros l1 l2.
intros H.
rewrite <- rev_involutive.
rewrite <- H. 
rewrite -> rev_involutive.
reflexivity.
Qed.

【Coq】12 Lists III 关于列表的推理

关于列表的推理 Reasoning About Lists

列表归纳 Induction on Lists

反转列表 Reversing a List

搜索 Search

List Exercises, Part 1

33: 3 stars, standard (list_exercises)

Theorem app_nil_r

Coq代码

Theorem rev_app_distr

Coq代码

Theorem rev_involutive

Coq代码

Theorem app_assoc4

Coq代码

Lemma nonzeros_app 关于[非零]实现的练习：

Coq代码

34: 2 stars, standard (eqblist)

Fixpoint eqblist (l1 l2 : natlist) : bool

Coq代码

Theorem eqblist_refl

Coq代码

List Exercises, Part 2

35: 1 star, standard (count_member_nonzero)

Theorem count_member_nonzero

Coq代码

Theorem leb_n_Sn

36: 3 stars, advanced (remove_does_not_increase_count)

Theorem remove_does_not_increase_count

Coq代码

37: 3 stars, standard, optional (bag_count_sum)

38: 4 stars, advanced (rev_injective)

Theorem rev_injective

Coq代码