oysteikt/sf1
0
0
Fork 0
forked from oysteikt/sf1-template
Code Pull Requests Activity

Complete Lists.v

Browse Source
This commit is contained in:
Oystein Kristoffer Tveit
2026-07-07 10:59:31 +09:00
parent 0e002ab32d
commit dd67c7d335
1 changed files with 230 additions and 97 deletions
Download Patch File Download Diff File Expand all files Collapse all files
Lists.v
+230 -97
View File
@@ -102,7 +102,8 @@ Definition swap_pair (p : natprod) : natprod :=
Theorem surjective_pairing' : forall (n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.
reflexivity.
Qed.
(** But just [reflexivity] is not enough if we state the lemma in a more
natural way: *)
@@ -120,7 +121,11 @@ Abort.
Theorem surjective_pairing : forall (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as [n m]. simpl. reflexivity. Qed.
intros p.
destruct p as [n m].
simpl.
reflexivity.
Qed.
(** Notice that, by contrast with the behavior of [destruct] on
[nat]s, where it generates two subgoals, [destruct] generates just
@@ -131,15 +136,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.
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.
reflexivity.
Qed.
(* ################################################################# *)
(** * Lists of Numbers *)
@@ -291,19 +300,26 @@ 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 odd 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.
(** For the next problem, [countoddmembers], we're giving you a header
that uses the keyword [Definition] instead of [Fixpoint]. The
@@ -311,21 +327,20 @@ Example test_oddmembers:
implement the function by using already-defined functions, rather
than writing your own recursive definition. *)
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)
@@ -341,25 +356,28 @@ Example test_countoddmembers3:
lists at the same time with the "multiple pattern" syntax we've
seen before. *)
Fixpoint alternate (l1 l2 : natlist) : natlist
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Fixpoint alternate (l1 l2 : natlist) : natlist :=
match l1, l2 with
| nil, l2 => l2
| l1, nil => l1
| n1 :: t1, n2 :: t2 => n1 :: n2 :: 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.
(* ----------------------------------------------------------------- *)
(** *** Bags via Lists *)
@@ -375,15 +393,19 @@ 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 => O
| x :: t => if eqb x v then S(count v t) else count v t
end.
(** All these proofs can be completed with [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 those of [b]. (Mathematicians usually
@@ -395,29 +417,30 @@ Example test_count2: count 6 [1;2;3;1;4;1] = 0.
names to the arguments. Implement [sum] in terms of an
already-defined function, without changing the header. *)
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.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Fixpoint member (v : nat) (s : bag) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
Proof. reflexivity. Qed.
Fixpoint member (v : nat) (s : bag) : bool :=
match s with
| nil => false
| x :: t => eqb x v || member v t
end.
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)
@@ -429,56 +452,73 @@ 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
| x :: t => if eqb v x then t else x :: (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
| x :: t => if eqb v x then (remove_all v t) else x :: (remove_all v t)
end.
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
(* FILL IN HERE *) Admitted.
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 included (s1 : bag) (s2 : bag) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
Proof. reflexivity. Qed.
Fixpoint included (s1 : bag) (s2 : bag) : bool :=
match s1, s2 with
| nil, _ => true
| _, x :: t => included (remove_one x s1) t
| _, nil => false
end.
Example test_included1: included [1;2] [2;1;4;1] = true.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_included2: included [1;2;2] [2;1;4;1] = false.
(* FILL IN HERE *) Admitted.
(** [] *)
Proof. reflexivity. Qed.
(** **** Exercise: 2 stars, standard, optional (add_inc_count)
Adding a value to a bag should increase the value's count by one.
State this as a theorem and prove it in Rocq. *)
(*
Theorem add_inc_count : ...
Theorem add_inc_count :
forall (n : nat) (s : bag),
length (n :: s) = (length s) + 1.
Proof.
...
intros n s.
rewrite -> add_comm.
simpl.
reflexivity.
Qed.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_add_inc_count : option (nat*string) := None.
@@ -881,19 +921,31 @@ Search (?x + ?y = ?y + ?x).
Theorem app_nil_r : forall l : natlist,
l ++ [] = l.
Proof.
(* FILL IN HERE *) Admitted.
intros l.
induction l as [| h tl IHl'].
- reflexivity.
- simpl. rewrite IHl'. reflexivity.
Qed.
Theorem rev_app_distr: forall l1 l2 : natlist,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
(* FILL IN HERE *) Admitted.
intros l1 l2.
induction l1 as [| hl1 tl1 IHl1].
- simpl. rewrite app_nil_r. reflexivity.
- simpl. rewrite IHl1, app_assoc. reflexivity.
Qed.
(** An _involution_ is a function that is its own inverse. That is,
applying the function twice yield the original input. *)
Theorem rev_involutive : forall l : natlist,
rev (rev l) = l.
Proof.
(* FILL IN HERE *) Admitted.
intros l.
induction l as [| h tl IHl].
- reflexivity.
- simpl. rewrite rev_app_distr, IHl. reflexivity.
Qed.
(** There is a short solution to the next one. If you find yourself
getting tangled up, step back and try to look for a simpler
@@ -902,14 +954,36 @@ Proof.
Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
(* FILL IN HERE *) Admitted.
intros l1 l2 l3 l4.
rewrite app_assoc, app_assoc.
reflexivity.
Qed.
(** An exercise about your implementation of [nonzeros]: *)
(* aux *)
Lemma cons_app_assoc : forall x l1 l2,
x :: (l1 ++ l2) = (x :: l1) ++ l2.
Proof.
intros x l1 l2.
destruct l1.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.
Lemma nonzeros_app : forall l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
(* FILL IN HERE *) Admitted.
intros l1 l2.
induction l1 as [| hl1 tl1 IHl1].
- simpl. reflexivity.
- simpl.
destruct hl1.
+ rewrite IHl1. reflexivity.
+ rewrite <- cons_app_assoc.
rewrite IHl1.
reflexivity.
Qed.
(** [] *)
(** **** Exercise: 2 stars, standard (eqblist)
@@ -918,26 +992,34 @@ Proof.
lists of numbers for equality. Prove that [eqblist l l]
yields [true] for every list [l]. *)
Fixpoint eqblist (l1 l2 : natlist) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Fixpoint eqblist (l1 l2 : natlist) : bool :=
match l1, l2 with
| nil, nil => true
| nil, _ => false
| _, nil => false
| h1 :: t1, h2 :: t2 => eqb h1 h2 && eqblist t1 t2
end.
Example test_eqblist1 :
(eqblist nil nil = true).
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_eqblist2 :
eqblist [1;2;3] [1;2;3] = true.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_eqblist3 :
eqblist [1;2;3] [1;2;4] = false.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Theorem eqblist_refl : forall l:natlist,
true = eqblist l l.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
intros l.
induction l as [| lh' lt' IHl'].
- reflexivity.
- simpl. rewrite <- IHl', eqb_refl. reflexivity.
Qed.
(* ================================================================= *)
(** ** List Exercises, Part 2 *)
@@ -949,8 +1031,8 @@ Proof.
Theorem count_member_nonzero : forall (s : bag),
1 <=? (count 1 (1 :: s)) = true.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
reflexivity.
Qed.
(** The following lemma about [leb] might help you in the next
exercise (it will also be useful in later chapters). *)
@@ -967,11 +1049,21 @@ Proof.
(** Before doing the next exercise, make sure you've filled in the
definition of [remove_one] above. *)
(** **** Exercise: 3 stars, advanced (remove_does_not_increase_count) *)
Theorem remove_does_not_increase_count: forall (s : bag),
(count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
intros s.
induction s as [| sh' sl' IHs'].
- reflexivity.
- simpl. destruct sh'.
+ simpl.
rewrite leb_n_Sn.
reflexivity.
+ simpl.
exact IHs'.
Qed.
(** **** Exercise: 3 stars, standard, optional (bag_count_sum)
@@ -984,9 +1076,24 @@ Proof.
to know that [destruct] works on arbitrary expressions, not just
simple identifiers.)
*)
(* FILL IN HERE
[] *)
Theorem bag_count_sum:
forall (s1 s2 : bag) (n : nat),
count n (sum s1 s2) = count n s1 + count n s2.
Proof.
intros s1 s2 n.
induction s1.
- simpl. reflexivity.
- destruct (n0 =? n) eqn:Heq.
+ simpl.
rewrite Heq.
rewrite IHs1.
reflexivity.
+ simpl.
rewrite Heq.
rewrite IHs1.
reflexivity.
Qed.
(** **** Exercise: 3 stars, advanced (involution_injective) *)
@@ -999,8 +1106,12 @@ Proof.
Theorem involution_injective : forall (f : nat -> nat),
(forall n : nat, n = f (f n)) -> (forall n1 n2 : nat, f n1 = f n2 -> n1 = n2).
Proof.
(* FILL IN HERE *) Admitted.
intros f Hinv n1 n2 Heq.
rewrite Hinv.
rewrite <- Heq.
rewrite <- Hinv.
reflexivity.
Qed.
(** [] *)
(** **** Exercise: 2 stars, advanced (rev_injective)
@@ -1013,7 +1124,12 @@ Proof.
Theorem rev_injective : forall (l1 l2 : natlist),
rev l1 = rev l2 -> l1 = l2.
Proof.
(* FILL IN HERE *) Admitted.
intros l1 l2 Heq.
rewrite <- rev_involutive.
rewrite <- Heq.
rewrite rev_involutive.
reflexivity.
Qed.
(** [] *)
(* ################################################################# *)
@@ -1091,18 +1207,20 @@ Definition option_elim (d : nat) (o : natoption) : nat :=
Using the same idea, fix the [hd] function from earlier so we don't
have to pass a default element for the [nil] case. *)
Definition hd_error (l : natlist) : natoption
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition hd_error (l : natlist) : natoption :=
match l with
| nil => None
| h :: t => Some h
end.
Example test_hd_error1 : hd_error [] = None.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error [1] = Some 1.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
Example test_hd_error3 : hd_error [5;6] = Some 5.
(* FILL IN HERE *) Admitted.
Proof. reflexivity. Qed.
(** [] *)
(** **** Exercise: 1 star, standard, optional (option_elim_hd)
@@ -1112,7 +1230,11 @@ Example test_hd_error3 : hd_error [5;6] = Some 5.
Theorem option_elim_hd : forall (l:natlist) (default:nat),
hd default l = option_elim default (hd_error l).
Proof.
(* FILL IN HERE *) Admitted.
intros l d.
destruct l as [| h t].
- reflexivity.
- reflexivity.
Qed.
(** [] *)
End NatList.
@@ -1146,7 +1268,10 @@ Definition eqb_id (x1 x2 : id) :=
(** **** Exercise: 1 star, standard (eqb_id_refl) *)
Theorem eqb_id_refl : forall x, eqb_id x x = true.
Proof.
(* FILL IN HERE *) Admitted.
intros n.
destruct n.
apply eqb_refl.
Qed.
(** [] *)
(** Now we define the type of partial maps: *)
@@ -1192,7 +1317,11 @@ Theorem update_eq :
forall (d : partial_map) (x : id) (v: nat),
find x (update d x v) = Some v.
Proof.
(* FILL IN HERE *) Admitted.
intros d x v.
simpl.
rewrite eqb_id_refl.
reflexivity.
Qed.
(** [] *)
(** **** Exercise: 1 star, standard (update_neq) *)
@@ -1200,7 +1329,11 @@ Theorem update_neq :
forall (d : partial_map) (x y : id) (o: nat),
eqb_id x y = false -> find x (update d y o) = find x d.
Proof.
(* FILL IN HERE *) Admitted.
intros d x y o Hneq.
simpl.
rewrite Hneq.
reflexivity.
Qed.
(** [] *)
End PartialMap.