1.

2.

把上面的函数maxPair改造成maxPair'，返回类型为option nat * option nat。当要找的数字不存在时用None而不是0替代。

Example test_maxPair‘1: maxPair’ [1;2;5;4;8;10;3] = (Some 5, Some 10).

Proof. reflexivity. Qed.

Example test_maxPair‘2: maxPair’ [2;4] = (None, Some 4).

Proof. reflexivity. Qed.

3.

Theorem rev_app_distr

Theorem rev_app_distr: ∀ X (l1 l2 : list X),
  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.

4.

Theorem rev_involutive

Theorem rev_involutive : ∀ X : Type, ∀ l : list X,
  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.