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.