some induction + lists
This commit is contained in:
parent
3432fc448c
commit
974ab5422b
GPG key ID:
BDA47A31A3C8EE6B
3 changed files with 109 additions and 63 deletions
38
Induction.v
38
Induction.v
|
|
@ -197,23 +197,38 @@ Proof.
|
|||
Theorem mult_0_r : forall n:nat,
|
||||
n * 0 = 0.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
induction n.
|
||||
- reflexivity.
|
||||
- simpl. rewrite -> IHn. reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem plus_n_Sm : forall n m : nat,
|
||||
S (n + m) = n + (S m).
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
induction n. induction m.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- intros m. simpl. rewrite -> IHn. reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem plus_comm : forall n m : nat,
|
||||
n + m = m + n.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
induction n. induction m.
|
||||
- reflexivity.
|
||||
- simpl. rewrite <- IHm. reflexivity.
|
||||
- intros m. simpl. rewrite <- plus_n_Sm. rewrite -> IHn. reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem plus_assoc : forall n m p : nat,
|
||||
n + (m + p) = (n + m) + p.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
induction n. induction m. induction p.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- intros p. reflexivity.
|
||||
- intros m p. simpl. rewrite <- IHn. reflexivity.
|
||||
Qed.
|
||||
|
||||
(** **** Exercise: 2 stars, standard (double_plus)
|
||||
|
||||
|
|
@ -229,8 +244,10 @@ Fixpoint double (n:nat) :=
|
|||
|
||||
Lemma double_plus : forall n, double n = n + n .
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
induction n.
|
||||
- reflexivity.
|
||||
- simpl. rewrite -> IHn. rewrite <- plus_n_Sm. reflexivity.
|
||||
Qed.
|
||||
|
||||
(** **** Exercise: 2 stars, standard, optional (evenb_S)
|
||||
|
||||
|
|
@ -244,8 +261,9 @@ Proof.
|
|||
Theorem evenb_S : forall n : nat,
|
||||
evenb (S n) = negb (evenb n).
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
induction n.
|
||||
- reflexivity.
|
||||
- simpl.
|
||||
|
||||
(** **** Exercise: 1 star, standard (destruct_induction)
|
||||
|
||||
|
|
@ -256,7 +274,7 @@ Proof.
|
|||
*)
|
||||
|
||||
(* Do not modify the following line: *)
|
||||
Definition manual_grade_for_destruct_induction : option (nat*string) := None.
|
||||
Definition manual_grade_for_destruct_induction : option (nat*string) := None..
|
||||
(** [] *)
|
||||
|
||||
(* ################################################################# *)
|
||||
|
|
|
|||
133
Lists.v
133
Lists.v
|
|
@ -134,15 +134,19 @@ Proof.
|
|||
Theorem snd_fst_is_swap : forall (p : natprod),
|
||||
(snd p, fst p) = swap_pair p.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
intros p.
|
||||
destruct p as [n m].
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(** **** Exercise: 1 star, standard, optional (fst_swap_is_snd) *)
|
||||
Theorem fst_swap_is_snd : forall (p : natprod),
|
||||
fst (swap_pair p) = snd p.
|
||||
Proof.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
intros p.
|
||||
destruct p as [n m].
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ################################################################# *)
|
||||
(** * Lists of Numbers *)
|
||||
|
|
@ -290,34 +294,41 @@ Proof. reflexivity. Qed.
|
|||
[countoddmembers] below. Have a look at the tests to understand
|
||||
what these functions should do. *)
|
||||
|
||||
Fixpoint nonzeros (l:natlist) : natlist
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint nonzeros (l:natlist) : natlist :=
|
||||
match l with
|
||||
| nil => nil
|
||||
| 0 :: t => nonzeros t
|
||||
| n :: t => n :: nonzeros t
|
||||
end.
|
||||
|
||||
Example test_nonzeros:
|
||||
nonzeros [0;1;0;2;3;0;0] = [1;2;3].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Fixpoint oddmembers (l:natlist) : natlist
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint oddmembers (l:natlist) : natlist :=
|
||||
match l with
|
||||
| nil => nil
|
||||
| n :: t => if oddb n then n :: oddmembers t else oddmembers t
|
||||
end.
|
||||
|
||||
Example test_oddmembers:
|
||||
oddmembers [0;1;0;2;3;0;0] = [1;3].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Definition countoddmembers (l:natlist) : nat
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition countoddmembers (l:natlist) : nat :=
|
||||
length (oddmembers l).
|
||||
|
||||
Example test_countoddmembers1:
|
||||
countoddmembers [1;0;3;1;4;5] = 4.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_countoddmembers2:
|
||||
countoddmembers [0;2;4] = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_countoddmembers3:
|
||||
countoddmembers nil = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 3 stars, advanced (alternate)
|
||||
|
|
@ -334,24 +345,29 @@ Example test_countoddmembers3:
|
|||
of both lists at the same time. One possible solution involves
|
||||
defining a new kind of pairs, but this is not the only way.) *)
|
||||
|
||||
Fixpoint alternate (l1 l2 : natlist) : natlist
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint alternate (l1 l2 : natlist) : natlist :=
|
||||
match l1, l2 with
|
||||
| nil, nil => nil
|
||||
| _ :: _, nil => l1
|
||||
| nil, _ :: _ => l2
|
||||
| h1 :: t1, h2 :: t2 => h1 :: h2 :: alternate t1 t2
|
||||
end.
|
||||
|
||||
Example test_alternate1:
|
||||
alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_alternate2:
|
||||
alternate [1] [4;5;6] = [1;4;5;6].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_alternate3:
|
||||
alternate [1;2;3] [4] = [1;4;2;3].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_alternate4:
|
||||
alternate [] [20;30] = [20;30].
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
(** [] *)
|
||||
|
||||
(* ----------------------------------------------------------------- *)
|
||||
|
|
@ -368,15 +384,18 @@ Definition bag := natlist.
|
|||
Complete the following definitions for the functions
|
||||
[count], [sum], [add], and [member] for bags. *)
|
||||
|
||||
Fixpoint count (v:nat) (s:bag) : nat
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint count (v:nat) (s:bag) : nat :=
|
||||
match s with
|
||||
| nil => 0
|
||||
| h :: t => if v =? h then 1 + count v t else count v t
|
||||
end.
|
||||
|
||||
(** All these proofs can be done just by [reflexivity]. *)
|
||||
|
||||
Example test_count1: count 1 [1;2;3;1;4;1] = 3.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
(** Multiset [sum] is similar to set [union]: [sum a b] contains all
|
||||
the elements of [a] and of [b]. (Mathematicians usually define
|
||||
|
|
@ -390,29 +409,28 @@ Example test_count2: count 6 [1;2;3;1;4;1] = 0.
|
|||
think about whether [sum] can be implemented in another way --
|
||||
perhaps by using functions that have already been defined. *)
|
||||
|
||||
Definition sum : bag -> bag -> bag
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition sum : bag -> bag -> bag :=
|
||||
app.
|
||||
|
||||
Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Definition add (v:nat) (s:bag) : bag
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition add (v:nat) (s:bag) : bag :=
|
||||
v :: s.
|
||||
|
||||
Example test_add1: count 1 (add 1 [1;4;1]) = 3.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Definition member (v:nat) (s:bag) : bool
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Definition member (v:nat) (s:bag) : bool :=
|
||||
negb ((count v s) =? 0).
|
||||
|
||||
Example test_member1: member 1 [1;4;1] = true.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_member2: member 2 [1;4;1] = false.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
(** [] *)
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
(** **** Exercise: 3 stars, standard, optional (bag_more_functions)
|
||||
|
||||
|
|
@ -424,44 +442,53 @@ Example test_member2: member 2 [1;4;1] = false.
|
|||
to fill in the definition of [remove_one] for a later
|
||||
exercise.) *)
|
||||
|
||||
Fixpoint remove_one (v:nat) (s:bag) : bag
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint remove_one (v:nat) (s:bag) : bag :=
|
||||
match s with
|
||||
| nil => nil
|
||||
| h :: t => if eqb v h then t else h :: remove_one v t
|
||||
end.
|
||||
|
||||
Example test_remove_one1:
|
||||
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_remove_one2:
|
||||
count 5 (remove_one 5 [2;1;4;1]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_remove_one3:
|
||||
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Example test_remove_one4:
|
||||
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Fixpoint remove_all (v:nat) (s:bag) : bag
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint remove_all (v:nat) (s:bag) : bag :=
|
||||
match s with
|
||||
| nil => nil
|
||||
| h :: t => if v =? h then remove_all v t else h :: remove_all v t
|
||||
end.
|
||||
|
||||
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
Fixpoint subset (s1:bag) (s2:bag) : bool
|
||||
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
|
||||
Fixpoint subset (s1:bag) (s2:bag) : bool :=
|
||||
match s1 with
|
||||
| nil => true
|
||||
| h :: t => if count h s2 =? 0 then false else subset t (remove_one h s2)
|
||||
end.
|
||||
|
||||
Example test_subset1: subset [1;2] [2;1;4;1] = true.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
|
||||
(* FILL IN HERE *) Admitted.
|
||||
Proof. reflexivity. Qed.
|
||||
(** [] *)
|
||||
|
||||
(** **** Exercise: 2 stars, standard, recommended (bag_theorem)
|
||||
|
|
|
|||
1
_CoqProject
Normal file
1
_CoqProject
Normal file
|
|
@ -0,0 +1 @@
|
|||
-Q . LF
|
||||
Loading…
Reference in a new issue