更多练习 More Exercises

20: 3 stars, standard, especially useful (mul_comm)

使用[assert]帮助证明[add_shuffle3]。你还不需要使用归纳法。

Theorem add_shuffle

Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
intros.
assert (H: n + (m + p) = (n + m) + p).
  { rewrite add_assoc. reflexivity. }
  rewrite H. assert (H': m + (n + p) = (m + n) + p).
  { rewrite add_assoc. reflexivity. }rewrite H'.  assert (H'': m + n = n + m).
  { rewrite add_comm. reflexivity. }rewrite H''.  reflexivity. Qed.

现在证明乘法的交换性。你可能想定义并证明一个“助手”定理，用于证明这个定理。提示：什么是n×（1+k）？

Theorem mul_commTheorem add_shuffle3 : forall n m p : nat,

Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem helper : forall n k : nat,
n * (1+k) = n + n * k.
Proof.
induction n as [| n' IHn']. 
- simpl. reflexivity.
- simpl. intros k. rewrite -> IHn'. rewrite add_assoc. rewrite add_shuffle3. rewrite add_assoc. reflexivity. 
Qed.

Theorem helper' : forall n : nat,
S n = n + 1.
Proof.
induction n as [| n' IHn']. 
- simpl. reflexivity.
- simpl. rewrite -> IHn'. reflexivity. 
Qed.

Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Proof.
intros. induction n as [| n' IHn'].
- simpl. rewrite mul_0_r. reflexivity.
- simpl. replace (S n') with (n' + 1).
-- rewrite add_comm. rewrite -> helper. rewrite -> IHn'. reflexivity.
-- rewrite <- helper'. reflexivity.
Qed.

21: 3 stars, standard, optional (more_exercises)

拿一张纸。对于以下每个定理，首先考虑（a）是否可以仅使用简化和重写来证明，（b）它还需要案例分析（析构函数），或者（c）它还需要归纳。写下你的预测。然后填写证明。（无需提交文件；这只是为了鼓励您在黑客攻击之前进行反思！）

Theorem leb_refl

Check leb.

Theorem leb_refl : forall n:nat,
  (n <=? n) = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem leb_refl : forall n:nat,
  (n <=? n) = true.
Proof.
intros. induction n as [| n' IHn'].
- simpl. reflexivity.
- simpl. rewrite -> IHn' . reflexivity.
Qed.

Theorem zero_neqb_S

Theorem zero_neqb_S : forall n:nat,
  0 =? (S n) = false.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem zero_neqb_S : forall n:nat,
  0 =? (S n) = false.
Proof.
intros []. 
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

Theorem andb_false_r

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
intros []. 
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

Theorem plus_leb_compat_l

Theorem plus_leb_compat_l : forall n m p : nat,
  n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem plus_leb_compat_l : forall n m p : nat,
  n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
intros. 
induction p as [| p' IHp'].
- simpl. rewrite -> H . reflexivity.
- simpl. rewrite -> IHp' . reflexivity.
Qed.

Theorem S_neqb_0

Theorem S_neqb_0 : forall n:nat,
  (S n) =? 0 = false.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem S_neqb_0 : forall n:nat,
  (S n) =? 0 = false.
Proof.
intros. 
induction n as [| n' IHn'].
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

Theorem mult_1_l

Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
intros. 
induction n as [| n' IHn'].
- simpl. reflexivity.
- simpl. assert (H:n' + 0 = 0 + n').
  { rewrite add_comm. reflexivity. }
  rewrite H. simpl.  reflexivity.
Qed.

Theorem all3_spec

Theorem all3_spec : forall b c : bool,
  orb
    (andb b c)
    (orb (negb b)
         (negb c))
  = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem all3_spec : forall b c : bool,
 orb
   (andb b c)
   (orb (negb b)
        (negb c))
 = true.
Proof.
intros [] [].
- simpl. reflexivity.
- simpl. reflexivity.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

Theorem mult_plus_distr_r

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
Proof.
induction n as [| n' IHn']. 
- simpl. reflexivity.
- simpl. intros m p. rewrite -> IHn'. rewrite add_assoc. reflexivity. 
Qed.

Theorem mult_assoc

Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
induction n as [| n' IHn']. 
- simpl. intros m p. reflexivity.
- simpl. intros m p. rewrite -> mult_plus_distr_r.  rewrite -> IHn'. reflexivity.
Qed.

22: 2 stars, standard, optional (eqb_refl)

Theorem eqb_refl

Theorem eqb_refl : forall n : nat,
  (n =? n) = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

   Theorem eqb_refl : forall n : nat,
 (n =? n) = true.
Proof.
induction n as [| n' IHn']. 
- simpl. reflexivity.
- simpl. rewrite -> IHn'. reflexivity.
Qed.回想一下您在[Basics]一章中为[binary]练习编写的[incr]和[bin_to_nat]函数。证明下图所示为通勤：

也就是说，增加一个二进制数，然后将其转换为（一元）自然数，得到的结果与首先将其转换为自然数，然后增加的结果相同。

命名你的定理[bin_to_nat_pres_incr]（“pres”代表“preserves”）。

在开始进行此练习之前，请将[incr]和[bin_to_nat]的定义从您的解决方案复制到此处的[binary]练习中，以便此文件可以自行分级。如果您想更改原始定义以使属性更易于证明，请随意更改！*）

23: 2 stars, standard, optional (add_shuffle3')

[replace]策略允许您指定要重写的特定子项以及要重写的内容：[replace（t）with（u）]用表达式[u]替换目标中表达式[t]的（所有副本），并生成[t=u]作为附加子目标。当简单的[重写]操作目标的错误部分时，这通常很有用。

使用[replace]策略对[add_shuffle3']进行证明，就像[add_shuffle3]一样，但不需要[assert].

Theorem add_shuffle3'

Theorem add_shuffle3' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem add_shuffle3' : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
intros.
replace (n + (m + p)) with ((n + m) + p).
replace (m + (n + p)) with ((m + n) + p).
- replace (m + n) with (n + m).
-- reflexivity. 
-- rewrite add_comm. reflexivity. 
- rewrite add_assoc. reflexivity. 
- rewrite add_assoc. reflexivity. 
Qed.

24: 3 stars, standard, especially useful (binary_commute)

回想一下您在[Basics]一章中为[binary]练习编写的[incr]和[bin_to_nat]函数。证明下图所示为通勤：

也就是说，增加一个二进制数，然后将其转换为（一元）自然数，得到的结果与首先将其转换为自然数，然后增加的结果相同。

命名你的定理[bin_to_nat_pres_incr]（“pres”代表“preserves”）。

在开始进行此练习之前，请将[incr]和[bin_to_nat]的定义从您的解决方案复制到此处的[binary]练习中，以便此文件可以自行分级。如果您想更改原始定义以使属性更易于证明，请随意更改！*）

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

25: 5 stars, advanced (binary_inverse)

这是先前关于二进制数练习的进一步延续。您可能会发现，您需要返回并更改早期的定义，以便在这里工作。

（a） 首先，编写一个函数将自然数转换为二进制数。

Fixpoint nat_to_bin (n:nat) : bin
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

证明，如果我们从任何nat开始，将其转换为二进制，再将其转换回，我们得到的nat与我们开始使用的相同。（提示：如果你对nat_to_bin的定义涉及任何额外的函数，你可能需要证明一个辅助引理，说明这些函数如何与nat_to_bin相关。）

Theorem nat_bin_nat : forall n, bin_to_nat (nat_to_bin n) = n.
Proof.
  (* FILL IN HERE *) Admitted.

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

（b） 人们可能会自然而然地认为我们也可以证明相反的方向——从一个二进制数开始，转换成一个自然数，然后返回到二进制数，应该得到与我们开始时相同的数。然而，事实并非如此！解释（在评论中）问题是什么。

(* FILL IN HERE *)
(* Do not modify the following line: *)

（c） 定义一个规范化函数——也就是说，一个函数直接从一个bin规范化到另一个bin规范化（即，不通过转换为nat和back），这样，对于任何二进制数b，将b转换为自然数，然后再转换回二进制产生（规范化b）。证明它。（警告：这部分有点棘手——你可能最终定义了几个辅助引理。找到你需要的一个好方法是从证明主语句开始，看看你在哪里卡住了，看看你是否能找到一个引理——可能需要它自己的归纳证明——这将使主证明取得进展。）不要用nat_to_bin和bin_to_nat来定义它！

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