附加练习 Additional Exercises

57: 2 stars, standard (fold_length)

列表上的许多常见功能可以按折叠方式实现。例如，以下是长度的替代定义：

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.

证明折叠长度的正确性。（提示：了解自反性比siml更积极地简化表达式可能会有所帮助——也就是说，您可能会发现siml什么都不做，但自反性解决了目标。）

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
(* FILL IN HERE *) Admitted.

58: 3 stars, standard (fold_map)

我们也可以用fold来定义map。完成下面的fold_map。

Definition fold_map {X Y: Type} (f: X -> Y) (l: list X) : list Y
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

写下一个定理fold_map_correct，说明fold_map是正确的，并证明它。（提示：再一次，请记住，自反性比siml更积极地简化表达式。）

(* FILL IN HERE *)

(* Do not modify the following line: *)
Definition manual_grade_for_fold_map : option (nat*string) := None.

59: 2 stars, advanced (currying)

在Coq中，函数f:a→ B→ C真的有 A → (B → C)类型 。也就是说，如果你给f一个类型为a的值，它会给你函数f'：B→ C.如果你给f'一个类型为B的值，它将返回类型为C的值。这允许部分应用，如plus3。为纪念逻辑学家Haskell Curry，使用返回函数的函数处理参数列表被称为Curry。

相反，我们可以重新解释A→ B→ C类型为(A × B) → C 这叫做uncurrying。对于无载波二进制函数，两个参数必须同时成对给出；没有部分应用程序。

我们可以对currying的定义如下：

Definition prod_curry {X Y Z : Type}
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

作为一种练习，定义它的相反方向，即“prod_uncurry”。然后证明下面的定理，证明这两个定理是相反的。

Definition prod_uncurry {X Y Z : Type}
  (f : X -> Y -> Z) (p : X * Y) : Z
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

作为currying有用性的一个（微不足道的）例子，我们可以用它来缩短我们上面看到的一个例子：

Example test_map1': map (plus 3) [2;0;2] = [5;3;5].
Proof. reflexivity. Qed.

思考练习：在运行以下命令之前，您能否计算prod_curry和prod_uncurry的类型？

Check @prod_curry.
Check @prod_uncurry.

Theorem uncurry_curry : forall (X Y Z : Type)
                        (f : X -> Y -> Z)
                        x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem curry_uncurry : forall (X Y Z : Type)
                        (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  (* FILL IN HERE *) Admitted.

60: 2 stars, advanced (nth_error_informal)

回想一下 nth_error函数的定义：

Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
     match l with
     | [] => None
     | a :: l' => if n =? O then Some a else nth_error l' (pred n)
     end.

写出以下定理的非正式证明：

forall X l n, length l = n -> @nth_error X l n = None

(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_informal_proof : option (nat*string) := None.

下面的练习探索定义自然数的另一种方法，使用以数学家阿隆佐·丘奇命名的所谓丘奇数字。我们可以将一个自然数n表示为一个函数，该函数将函数f作为参数，并返回迭代n次的f。

Module Church.
Definition cnat := forall X : Type, (X -> X) -> X -> X.

让我们看看如何用这个符号写一些数字。对函数进行一次迭代应该与仅应用它相同。因此：

Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

同样地，[two]应该对其论点应用[f]两次：

Definition two : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

定义[zero]有点棘手：我们如何“应用函数零次”？答案其实很简单：只需原封不动地返回参数。

Definition zero : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

更一般地说，数字n可以写成fun X f x ⇒ f (f ... (f x) ...)，其中f出现n次。请特别注意，我们前面定义的doit3times函数实际上只是3的教堂表示。

Definition three : cnat := @doit3times.

完成以下函数的定义。通过自反性证明相应的单元测试，确保它们通过。

61: 1 star, advanced (church_succ)

自然数的后继数：给定一个教会数字n，后继数succ n是一个将其参数迭代一次超过n的函数。

Definition succ (n : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example succ_1 : succ zero = one.
Proof. (* FILL IN HERE *) Admitted.

Example succ_2 : succ one = two.
Proof. (* FILL IN HERE *) Admitted.

Example succ_3 : succ two = three.
Proof. (* FILL IN HERE *) Admitted.

62: 1 star, advanced (church_plus)

两个自然数相加：

Definition plus (n m : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example plus_1 : plus zero one = one.
Proof. (* FILL IN HERE *) Admitted.

Example plus_2 : plus two three = plus three two.
Proof. (* FILL IN HERE *) Admitted.

Example plus_3 :
  plus (plus two two) three = plus one (plus three three).
Proof. (* FILL IN HERE *) Admitted.

63: 2 stars, advanced (church_mult)

乘法：

Definition mult (n m : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example mult_1 : mult one one = one.
Proof. (* FILL IN HERE *) Admitted.

Example mult_2 : mult zero (plus three three) = zero.
Proof. (* FILL IN HERE *) Admitted.

Example mult_3 : mult two three = plus three three.
Proof. (* FILL IN HERE *) Admitted.

64: 2 stars, advanced (church_exp)

指数化：

（提示：多态性在这里起着至关重要的作用。但是，选择正确的类型进行迭代可能很棘手。如果遇到“宇宙不一致”错误，请尝试迭代其他类型。迭代cnat本身通常是有问题的。）

Definition exp (n m : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example exp_1 : exp two two = plus two two.
Proof. (* FILL IN HERE *) Admitted.

Example exp_2 : exp three zero = one.
Proof. (* FILL IN HERE *) Admitted.

Example exp_3 : exp three two = plus (mult two (mult two two)) one.
Proof. (* FILL IN HERE *) Admitted.