【函数语言程序设计】Hw6 - Coq4
1. 补充完整下面的定义，判断一个集合是否为另一个集合的子集。
Fixpoint subset (s1 : bag) (s2 : bag) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_subset1: subset [1;2] [2;1;4;1] = true.
(* FILL IN HERE *) Admitted.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
(* FILL IN HERE *) Admitted.
Coq代码
Fixpoint subset (s1 : bag) (s2 : bag) : bool:=
match s1,s2 with
|nil,nil => true
|nil,h::t => true
|h'::t',nil => false
|h''::t'',h'''::t''' => if member h'' s2 then subset t'' (remove_one h'' s2)
else false
end.
Example test_subset1: subset [1;2] [2;1;4;1] = true.
Proof. simpl. reflexivity. Qed.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
Proof. simpl. reflexivity. Qed.
2. 证明如下性质
Theorem app_assoc4 : ∀ l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
(* FILL IN HERE *) Admitted.
Coq代码
Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
intros l1 l2 l3 l4. induction l1 as [| n l1' IHl1'].
- induction l2 as [| n l2' IHl2']. (* l1 = nil *)
-- simpl. reflexivity. (* l2 = nil *)
-- simpl. rewrite -> app_assoc. reflexivity. (* l2 = cons n l2' *)
- simpl. rewrite -> app_assoc. rewrite -> app_assoc. reflexivity. Qed.
3. Before doing the next exercise, make sure you've filled in the definition of remove_one in the chapter Lists.
Theorem remove_does_not_increase_count: ∀ (s : bag),
(count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
(* FILL IN HERE *) Admitted.
Coq代码
Theorem remove_does_not_increase_count: forall (s : bag),
(count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
intros s. induction s as [| n s' IHs'].
- simpl. reflexivity.
- simpl. destruct n as [| n'] eqn:E.
-- simpl. rewrite -> leb_n_Sn. reflexivity.
-- simpl. rewrite -> IHs'. reflexivity.
Qed.
【学习】函数语言程序设计 文章被收录于专栏
函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】
