更多练习 More Exercises

10: 1 star, standard (identity_fn_applied_twice)

使用您迄今学到的策略来证明有关 Boolean 函数以下定理。

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Proof.
  intros f.
  intros x.
  intros b0.
  rewrite -> x.
  rewrite -> x.
  reflexivity.
Qed.

Coq运行截图

alt

11: 1 star, standard (negation_fn_applied_twice)

现在说明和证明定理 negation_fn_applied_twice 类似于上一个，但其中第二个假设说，功能 f 有属性，f x = negb x。

(* FILL IN HERE *)

(* Do not modify the following line: *)
Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := None.
(** (The last definition is used by the autograder.)

Coq代码

Theorem negation_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = negb x) ->
forall (b : bool), f (f b) = b.
Proof.
	intros f.
	intros x.
	intros [].
		- rewrite -> x.
  		 rewrite -> x.
  		 reflexivity.
  		- rewrite -> x.
  		 rewrite -> x.
  		 reflexivity.
Qed.

Coq运行截图

alt

12: 3 stars, standard, optional (andb_eq_orb)

证明以下定理。（提示：这个可能有点棘手，这取决于你如何接近它。您可能需要 destruct 和 rewrite ，但破坏眼前的一切并不是最好的方法。

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Proof.
intros [] [] .
  -simpl. reflexivity.
  -simpl. intros A. rewrite <- A. reflexivity.
  -simpl. intros B. rewrite <- B. reflexivity.
  - reflexivity.
Qed.

Coq运行截图

alt

13: 3 stars, standard (binary)

我们可以通过将二进制数字视为由 Z 终止的构造器 B0 和 B1（表示0s和1s）的序列，将自然数字的一元表示概括为更高效的二进制表示。为了进行比较，在一元表示中，数字是被 O 终止的 S 构造器序列。 例如：

decimal               binary                          unary
           0                       Z                              O
           1                    B1 Z                            S O
           2                B0 (B1 Z)                        S (S O)
           3                B1 (B1 Z)                     S (S (S O))
           4            B0 (B0 (B1 Z))                 S (S (S (S O)))
           5            B1 (B0 (B1 Z))              S (S (S (S (S O))))
           6            B0 (B1 (B1 Z))           S (S (S (S (S (S O)))))
           7            B1 (B1 (B1 Z))        S (S (S (S (S (S (S O))))))
           8        B0 (B0 (B0 (B1 Z)))    S (S (S (S (S (S (S (S O)))))))

请注意，低阶位位于左侧，高阶位位于右侧- 与二进制数字通常的编写方式相反。此选择使他们更容易操作。

 Inductive bin : Type :=
 | Z
 | B0 (n : bin)
 | B1 (n : bin).

完成以下二进制数字增量函数 incr 的定义，以及将二进制数字转换为一元数字的函数 bin_to_nat 。

在正确定义这些函数后，应通过以下"单位测试"，以测试您的增量和二进制到单一功能。当然，单位测试并不能充分证明您的功能正确性！我们将在下一章结束时回到这个想法。

Example test_bin_incr1 : (incr (B1 Z)) = B0 (B1 Z).
(* FILL IN HERE *) Admitted.

Example test_bin_incr2 : (incr (B0 (B1 Z))) = B1 (B1 Z).
(* FILL IN HERE *) Admitted.

Example test_bin_incr3 : (incr (B1 (B1 Z))) = B0 (B0 (B1 Z)).
(* FILL IN HERE *) Admitted.

Example test_bin_incr4 : bin_to_nat (B0 (B1 Z)) = 2.
(* FILL IN HERE *) Admitted.

Example test_bin_incr5 :
      bin_to_nat (incr (B1 Z)) = 1 + bin_to_nat (B1 Z).
(* FILL IN HERE *) Admitted.

Example test_bin_incr6 :
      bin_to_nat (incr (incr (B1 Z))) = 2 + bin_to_nat (B1 Z).
(* FILL IN HERE *) Admitted.

Fixpoint incr

  Fixpoint incr (m:bin) : bin
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Coq代码

Coq运行截图

Fixpoint bin_to_nat

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

Coq代码

Coq运行截图