【函数语言程序设计】Hw7 - Coq5
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.
【学习】函数语言程序设计 文章被收录于专栏
函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】
