Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (** * Lists: Working with Structured Data *)
- Require Export Induction.
- Module NatList.
- (* ################################################################# *)
- (** * Pairs of Numbers *)
- (** In an [Inductive] type definition, each constructor can take
- any number of arguments -- none (as with [true] and [O]), one (as
- with [S]), or more than one, as here: *)
- Inductive natprod : Type :=
- | pair : nat -> nat -> natprod.
- (** This declaration can be read: "There is just one way to
- construct a pair of numbers: by applying the constructor [pair] to
- two arguments of type [nat]." *)
- Check (pair 3 5).
- (** Here are two simple functions for extracting the first and
- second components of a pair. The definitions also illustrate how
- to do pattern matching on two-argument constructors. *)
- Definition fst (p : natprod) : nat :=
- match p with
- | pair x y => x
- end.
- Definition snd (p : natprod) : nat :=
- match p with
- | pair x y => y
- end.
- Compute (fst (pair 3 5)).
- (* ===> 3 *)
- (** Since pairs are used quite a bit, it is nice to be able to
- write them with the standard mathematical notation [(x,y)] instead
- of [pair x y]. We can tell Coq to allow this with a [Notation]
- declaration. *)
- Notation "( x , y )" := (pair x y).
- (** The new pair notation can be used both in expressions and in
- pattern matches (indeed, we've actually seen this already in the
- [Basics] chapter, in the definition of the [minus] function --
- this works because the pair notation is also provided as part of
- the standard library): *)
- Compute (fst (3,5)).
- Definition fst' (p : natprod) : nat :=
- match p with
- | (x,y) => x
- end.
- Definition snd' (p : natprod) : nat :=
- match p with
- | (x,y) => y
- end.
- Definition swap_pair (p : natprod) : natprod :=
- match p with
- | (x,y) => (y,x)
- end.
- (** Let's try to prove a few simple facts about pairs.
- If we state things in a particular (and slightly peculiar) way, we
- can complete proofs with just reflexivity (and its built-in
- simplification): *)
- Theorem surjective_pairing' : forall (n m : nat),
- (n,m) = (fst (n,m), snd (n,m)).
- Proof.
- reflexivity. (* [reflexivity] can expand the definitions of [fst] and [snd]
- to resolve this. *)
- Qed.
- (* Informal proof:
- Theorem: [forall n m : nat, (n, m) = (fst (n, m), snd (n, m))].
- Proof: by definition of [fst] and [snd].
- - The [fst] of [(n, m)] is [n], and the [snd] of [(n, m)] is [m].
- But that yields [(n, m)], which matches the left side of the equation.
- - So the theorem is true for [n] and [m], by the reflexivity of equality.
- - Since we've shown that the theorem holds for an arbitrary [n] and [m],
- we've shown that it holds for all [n]s and [m]s. []
- *)
- (** But [reflexivity] is not enough if we state the lemma in a more
- natural way: *)
- Theorem surjective_pairing_stuck : forall (p : natprod),
- p = (fst p, snd p). (* Note that [fst p] and [snd p] are not in a form that
- matches a constructor pattern. The constructors need a pair
- of the form [fst (_, _)]. But here, we only have [p],
- and there is not enough information in this theorem for
- Coq to match [p] to the structure [(_, _)]. *)
- Proof.
- simpl. (* Doesn't reduce anything! *)
- Abort.
- (** We have to expose the structure of [p] so that [simpl] can
- perform the pattern match in [fst] and [snd]. We can do this with
- [destruct]. *)
- Theorem surjective_pairing : forall (p : natprod),
- p = (fst p, snd p).
- Proof.
- intros p. (* Suppose [p] is a fixed pair. *)
- destruct p as [n m]. (* Let's proceed by case analysis. That is, let's consider
- the different forms that [p] can have. If we look at the [natprod]
- constructor, we can see it only has one constructor. So there's
- only one case here: [pair _ _]. Let's name the first item [n],
- and the second item [m]. So this will generate a goal
- where [p] is replaced with [(n, m)]. That is, the goal
- will become [(n, m) = (fst (n, m), snd (n, m))]. *)
- simpl. (* Then [simpl] can match [fst (n, m)] and [snd (n, m)] to simplify
- the right hand side of the quation to [(n, m)]. *)
- reflexivity. (* Now both sides of the equation match. *)
- Qed.
- (* Informal proof:
- Theorem: [forall p : natprod, p = (fst p, snd p)].
- Proof: by case analysis on [p].
- - Let [p] be a fixed pair. There is just one form that [p] can take: [(n, m)],
- where [n] and [m] are fixed numbers.
- - So let us replace every [p] with [(n, m)] in the theorem.
- - Then both sides of the equation are the same, which follows from
- the definition of [fst] and [snd].
- - So the theorem is true for [p], by the reflexivity of equality.
- - Since we've shown that the theorem holds for an arbitrary [p],
- we've shown that it holds for all [p]s. []
- *)
- (** Notice that, unlike its behavior with [nat]s, [destruct]
- generates just one subgoal here. That's because [natprod]s can
- only be constructed in one way. *)
- (** **** Exercise: 1 star (snd_fst_is_swap) *)
- Theorem snd_fst_is_swap : forall (p : natprod),
- (snd p, fst p) = swap_pair p.
- Proof.
- intros p. (* Suppose [p] is a fixed pair. *)
- destruct p as [n m]. (* By case analysis, let's consider the one case it can have: [(n, m)].
- That converts the goal to [(snd (n, m,), fst (n, m)) = swap_pair (n, m)]. *)
- simpl. (* [simpl] can now match the constructors for [snd], [fst], and [swap_pair], and simplify. *)
- reflexivity. (* Both sides of the equation are the same now. *)
- Qed.
- (** [] *)
- (* Informal proof:
- Theorem: [forall p : natprod, (snd p, fst p) = swap_pair p].
- Proof: by case analysis on [p].
- - Suppose [p] be is a fixed pair. Then [p] can have the form [(n, m)], where
- [n] and [m] are fixed numbers.
- - By the definition of [fst] and [snd], the left side of the equation reduces to [(m, n)],
- and by the definition of [swap_pair], the right hand side reduces to [(m, n)].
- - So the theorem is true for [p], by the reflexivity of equality.
- - Since we've shown that the theorem holds for an arbitrary [p],
- we've shown that it holds for all [p]s. []
- *)
- (** **** Exercise: 1 star, optional (fst_swap_is_snd) *)
- Theorem fst_swap_is_snd : forall (p : natprod),
- fst (swap_pair p) = snd p.
- Proof.
- intros p. (* Suppose [p] is a fixed pair. *)
- destruct p as [n m]. (* Consider the one form it can have: [(n, m)]. *)
- simpl. (* [simpl] can match the constructors of [swap_pair], [fst], and [snd] to simplify. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- Qed.
- (** [] *)
- (* ################################################################# *)
- (** * Lists of Numbers *)
- (** Generalizing the definition of pairs, we can describe the
- type of _lists_ of numbers like this: "A list is either the empty
- list or else a pair of a number and another list." *)
- Inductive natlist : Type :=
- | nil : natlist
- | cons : nat -> natlist -> natlist.
- (** For example, here is a three-element list: *)
- Definition mylist := cons 1 (cons 2 (cons 3 nil)).
- (** As with pairs, it is more convenient to write lists in
- familiar programming notation. The following declarations
- allow us to use [::] as an infix [cons] operator and square
- brackets as an "outfix" notation for constructing lists. *)
- Notation "x :: l" := (cons x l)
- (at level 60, right associativity).
- Notation "[ ]" := nil.
- Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
- (** It is not necessary to understand the details of these
- declarations, but in case you are interested, here is roughly
- what's going on. The [right associativity] annotation tells Coq
- how to parenthesize expressions involving several uses of [::] so
- that, for example, the next three declarations mean exactly the
- same thing: *)
- Definition mylist1 := 1 :: (2 :: (3 :: nil)).
- Definition mylist2 := 1 :: 2 :: 3 :: nil.
- Definition mylist3 := [1;2;3].
- (** The [at level 60] part tells Coq how to parenthesize
- expressions that involve both [::] and some other infix operator.
- For example, since we defined [+] as infix notation for the [plus]
- function at level 50,
- Notation "x + y" := (plus x y)
- (at level 50, left associativity).
- the [+] operator will bind tighter than [::], so [1 + 2 :: [3]]
- will be parsed, as we'd expect, as [(1 + 2) :: [3]] rather than [1
- + (2 :: [3])].
- (Expressions like "[1 + 2 :: [3]]" can be a little confusing when
- you read them in a [.v] file. The inner brackets, around 3, indicate
- a list, but the outer brackets, which are invisible in the HTML
- rendering, are there to instruct the "coqdoc" tool that the bracketed
- part should be displayed as Coq code rather than running text.)
- The second and third [Notation] declarations above introduce the
- standard square-bracket notation for lists; the right-hand side of
- the third one illustrates Coq's syntax for declaring n-ary
- notations and translating them to nested sequences of binary
- constructors. *)
- (* ----------------------------------------------------------------- *)
- (** *** Repeat *)
- (** A number of functions are useful for manipulating lists.
- For example, the [repeat] function takes a number [n] and a
- [count] and returns a list of length [count] where every element
- is [n]. *)
- Fixpoint repeat (n count : nat) : natlist :=
- match count with
- | O => nil (* If [count] is [0], return the empty list. *)
- | S count' => n :: (repeat n count') (* If [count] is the successor of [count'],
- put [n] in front of the list,
- and then [repeat n] again [count'] times. *)
- end.
- (* ----------------------------------------------------------------- *)
- (** *** Length *)
- (** The [length] function calculates the length of a list. *)
- Fixpoint length (l:natlist) : nat :=
- match l with
- | nil => O (* If [l] is empty, the length is [0]. *)
- | h :: t => S (length t) (* If [l] has a head [h] and a tail [t], then
- the length will be one more than (the successor [S] of)
- the length of the tail [t]. *)
- end.
- (* ----------------------------------------------------------------- *)
- (** *** Append *)
- (** The [app] function concatenates (appends) two lists. *)
- Fixpoint app (l1 l2 : natlist) : natlist :=
- match l1 with
- | nil => l2 (* If [l1] is empty, just return [l2]. *)
- | h :: t => h :: (app t l2) (* If [l2] has a head [h] and a tail [t], put [h] at the front
- of the list, and then append the tail [t] to [l2]. *)
- end.
- (** Actually, [app] will be used a lot in some parts of what
- follows, so it is convenient to have an infix operator for it. *)
- Notation "x ++ y" := (app x y)
- (right associativity, at level 60).
- Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
- Proof. reflexivity. Qed.
- Example test_app2: nil ++ [4;5] = [4;5].
- Proof. reflexivity. Qed.
- Example test_app3: [1;2;3] ++ nil = [1;2;3].
- Proof. reflexivity. Qed.
- (* ----------------------------------------------------------------- *)
- (** *** Head (with default) and Tail *)
- (** Here are two smaller examples of programming with lists.
- The [hd] function returns the first element (the "head") of the
- list, while [tl] returns everything but the first
- element (the "tail").
- Of course, the empty list has no first element, so we
- must pass a default value to be returned in that case. *)
- Definition hd (default:nat) (l:natlist) : nat :=
- match l with
- | nil => default (* If [l] is empty, return the [default]. *)
- | h :: t => h (* If [l] has a head [h] and a tail [t], return the head [h]. *)
- end.
- Definition tl (l:natlist) : natlist :=
- match l with
- | nil => nil (* If [l] is empty, there is no tail, so return an empty list. *)
- | h :: t => t (* If [l] has a head [h] and a tail [t], return the tail [t]. *)
- end.
- Example test_hd1: hd 0 [1;2;3] = 1.
- Proof.
- simpl. (* [simpl] can match the constructors/cases of [hd] to simplify. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- Qed.
- Example test_hd2: hd 0 [] = 0.
- Proof.
- reflexivity. (* [reflexivity] can do the simplification too. *)
- Qed.
- Example test_tl: tl [1;2;3] = [2;3].
- Proof. reflexivity. Qed.
- (* ----------------------------------------------------------------- *)
- (** *** Exercises *)
- (** **** Exercise: 2 stars, recommended (list_funs) *)
- (** Complete the definitions of [nonzeros], [oddmembers] and
- [countoddmembers] below. Have a look at the tests to understand
- what these functions should do. *)
- Fixpoint nonzeros (l:natlist) : natlist :=
- match l with
- | nil => nil (* If [l] is empty, return the empty list. *)
- | h :: t => match beq_nat h 0 with (* If [l] has a head [h] and a tail [t], then
- check if the head [h] is [0]. *)
- | true => nonzeros t (* If it is, then ignore [h] and
- check for nonzeros in the tail [t]. *)
- | false => h :: (nonzeros t) (* If it isn't, put [h] at the front of the return
- list, and check for nonzeros in the tail [t]. *)
- end
- end.
- Example test_nonzeros:
- nonzeros [0;1;0;2;3;0;0] = [1;2;3].
- Proof.
- reflexivity. (* [reflexivity] can match the constructors/cases and simplify
- until both sides of the equation are the same. *)
- Qed.
- Fixpoint oddmembers (l:natlist) : natlist :=
- match l with
- | nil => nil
- | h :: t => match oddb h with
- | false => oddmembers t
- | true => h :: (oddmembers t)
- end
- end.
- Example test_oddmembers:
- oddmembers [0;1;0;2;3;0;0] = [1;3].
- Proof. reflexivity. Qed.
- Definition countoddmembers (l:natlist) : nat :=
- length (oddmembers l).
- Example test_countoddmembers1:
- countoddmembers [1;0;3;1;4;5] = 4.
- Proof. reflexivity. Qed.
- Example test_countoddmembers2:
- countoddmembers [0;2;4] = 0.
- Proof. reflexivity. Qed.
- Example test_countoddmembers3:
- countoddmembers nil = 0.
- Proof. reflexivity. Qed.
- (** [] *)
- (** **** Exercise: 3 stars, advanced (alternate) *)
- (** Complete the definition of [alternate], which "zips up" two lists
- into one, alternating between elements taken from the first list
- and elements from the second. See the tests below for more
- specific examples.
- Note: one natural and elegant way of writing [alternate] will fail
- to satisfy Coq's requirement that all [Fixpoint] definitions be
- "obviously terminating." If you find yourself in this rut, look
- for a slightly more verbose solution that considers elements of
- both lists at the same time. (One possible solution requires
- defining a new kind of pairs, but this is not the only way.) *)
- Fixpoint alternate (l1 l2 : natlist) : natlist :=
- match l1, l2 with
- | nil, nil => nil (* If [l1] and [l2] are both empty, there's nothing to zip up,
- so return an empty list. *)
- | nil, h :: t => l2 (* If [l1] is empty, but [l2] has a head [h] and a tail [t], then
- [l2] has some contents, so we can just return that. *)
- | h :: t, nil => l1 (* Ditto if [l1] has contents and [l2] is empty. *)
- | h1 :: t1, h2 :: t2 => h1 :: (h2 :: (alternate t1 t2)) (* If [l1] has head [h1] and a tail [t1],
- and [l2] has a head [h2] and a tail [t2], then put [h1] and [h2] as the
- first items of the return list, and then alternate the tails [t1] and [t2]. *)
- end.
- Example test_alternate1:
- alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
- Proof. reflexivity. Qed.
- Example test_alternate2:
- alternate [1] [4;5;6] = [1;4;5;6].
- Proof. reflexivity. Qed.
- Example test_alternate3:
- alternate [1;2;3] [4] = [1;4;2;3].
- Proof. reflexivity. Qed.
- Example test_alternate4:
- alternate [] [20;30] = [20;30].
- Proof. reflexivity. Qed.
- (** [] *)
- (* ----------------------------------------------------------------- *)
- (** *** Bags via Lists *)
- (** A [bag] (or [multiset]) is like a set, except that each element
- can appear multiple times rather than just once. One possible
- implementation is to represent a bag of numbers as a list. *)
- Definition bag := natlist.
- (** **** Exercise: 3 stars, recommended (bag_functions) *)
- (** Complete the following definitions for the functions
- [count], [sum], [add], and [member] for bags. *)
- Fixpoint count (v:nat) (s:bag) : nat :=
- match s with
- | nil => 0 (* If [s] is empty, then there are no [v]s in it. *)
- | h :: t => match beq_nat h v with (* If [s] has a head [h] and a tail [t], then check if
- the head [h] is the same value as [v]. *)
- | false => count v t (* If it's not, then ignore [h], and
- count the [v]s in the tail [t]. *)
- | true => S (count v t) (* If it is, then the number of [v]s in [s] will be one more
- (the successor [S]) than the count of [v]s in the tail [t]. *)
- end
- end.
- (** All these proofs can be done just by [reflexivity]. *)
- Example test_count1: count 1 [1;2;3;1;4;1] = 3.
- Proof. reflexivity. Qed.
- Example test_count2: count 6 [1;2;3;1;4;1] = 0.
- 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
- [union] on multisets a little bit differently -- using max instead
- of sum -- which is why we don't use that name for this operation.)
- For [sum] we're giving you a header that does not give explicit
- names to the arguments. Moreover, it uses the keyword
- [Definition] instead of [Fixpoint], so even if you had names for
- the arguments, you wouldn't be able to process them recursively.
- The point of stating the question this way is to encourage you to
- think about whether [sum] can be implemented in another way --
- perhaps by using functions that have already been defined. *)
- Definition sum : bag -> bag -> bag := app. (* We can just append all the bags together. *)
- Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
- Proof.
- reflexivity. (* [reflexivity] can still just match the constructors/cases and simplify. *)
- Qed.
- Definition add (v:nat) (s:bag) : bag := v :: s. (* We can just put [v] at the front of the bag [s]. *)
- Example test_add1: count 1 (add 1 [1;4;1]) = 3.
- Proof. reflexivity. Qed.
- Example test_add2: count 5 (add 1 [1;4;1]) = 0.
- Proof. reflexivity. Qed.
- Definition member (v:nat) (s:bag) : bool :=
- match count v s with (* Count how many [v]s are in [s]. *)
- | 0 => false (* If there are zero [v]s in [s], then [v] is not a member of [s]. *)
- | _ => true (* If there is any (other) number of [v]s in [s], then [v] is a member of [s]. *)
- end.
- Example test_member1: member 1 [1;4;1] = true.
- Proof. reflexivity. Qed.
- Example test_member2: member 2 [1;4;1] = false.
- Proof. reflexivity. Qed.
- (** [] *)
- (** **** Exercise: 3 stars, optional (bag_more_functions) *)
- (* Do not modify the following line: *)
- Definition manual_grade_for_bag_theorem : option (prod nat string) := None.
- (** Here are some more [bag] functions for you to practice with. *)
- (** When [remove_one] is applied to a bag without the number to remove,
- it should return the same bag unchanged. *)
- Fixpoint remove_one (v:nat) (s:bag) : bag :=
- match s with
- | nil => nil (* If the bag [s] is empty, there are no [v]s to remove. Just return the empty list. *)
- | h :: t => match beq_nat h v with (* If the bag [s] has a head [h] and a tail [t], check if
- the head [h] is the same value as [v]. *)
- | true => t (* If it is, drop [h] and return just the tail [t]. *)
- | false => h :: (remove_one v t) (* If it's not, put [h] at the front of the return
- list, and then remove one [v] from the tail [t]. *)
- end
- end.
- Example test_remove_one1:
- count 5 (remove_one 5 [2;1;5;4;1]) = 0.
- Proof. reflexivity. Qed.
- Example test_remove_one2:
- count 5 (remove_one 5 [2;1;4;1]) = 0.
- Proof. reflexivity. Qed.
- Example test_remove_one3:
- count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
- Proof. reflexivity. Qed.
- Example test_remove_one4:
- count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
- Proof. reflexivity. Qed.
- Fixpoint remove_all (v:nat) (s:bag) : bag :=
- match s with
- | nil => nil (* If [s] is empty, there are no [v]s to remove. So just return the empty list. *)
- | h :: t => match beq_nat h v with (* If [s] has a head [h] and a tail [t], check if [h]
- has the same value as [v]. *)
- | true => (remove_all v t) (* If it does, then drop the [h], and then remove all
- [v]s from the tail. *)
- | false => h :: (remove_all v t) (* If it doesn't, put the [h] at the front of the
- return list, and remove all [v]s from [t]. *)
- end
- end.
- Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
- Proof. reflexivity. Qed.
- 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.
- (* Note: an empty multiset is a subset of every other multiset. *)
- Fixpoint subset (s1:bag) (s2:bag) : bool :=
- match s1, s2 with
- | nil, nil => true (* If [s1] and [s2] are empty, then the first is a subset of the other. *)
- | nil, h :: t => true (* If [s1] is empty and [s2] has some contents (because it has a head [h]
- and a tail [t]), then [s1] is a subset of [s2]. *)
- | h :: t, nil => false (* If [s1] has contents (because it has a head [h] and a tail [t]) and [s2]
- is empty, then [s1] is not a subset of [s2]. *)
- | h1 :: t1, h2 :: t2 => match member h1 s2 with (* If [s1] has a head [h1] and a tail [t1], and if
- [s2] has a head [h2] and a tail [t2], then check if the head [h1] of the
- first bag is a member of [s2]. *)
- | true => subset t1 (remove_one h1 s2) (* If it is, then remove [h1] from
- [s2], and check if the tail [t1] of the first bag is a subset of that. *)
- | false => false (* If [h1] is not a member of [s2], then we've found an
- element in [s1] that's not in [s2]. This means [s1] cannot be a subset
- of [s2], since to be a subset requires that all members of [s1] are
- members of [s2]. *)
- end
- end.
- Compute subset [1;2;2] [2;1;4;1].
- Example test_subset1: subset [1;2] [2;1;4;1] = true.
- Proof. reflexivity. Qed.
- Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
- Proof. reflexivity. Qed.
- (** [] *)
- (** **** Exercise: 3 stars, recommended (bag_theorem) *)
- (** Write down an interesting theorem [bag_theorem] about bags
- involving the functions [count] and [add], and prove it. Note
- that, since this problem is somewhat open-ended, it's possible
- that you may come up with a theorem which is true, but whose proof
- requires techniques you haven't learned yet. Feel free to ask for
- help if you get stuck! *)
- (*
- Theorem bag_theorem : ...
- Proof.
- ...
- Qed.
- *)
- Theorem my_bag_theorem : forall s : bag, count 0 (add 0 s) = S (count 0 s).
- Proof.
- intros s. (* Suppose [s] is a fixed bag. *)
- simpl. (* [simpl] can reduce the left hand side to [S (count 0 s). *)
- reflexivity. (* So both sides of the equation are the same. *)
- Qed.
- (** [] *)
- (* Informal proof:
- Theorem: [forall s : bag, count 0 (add 0 s) = S (count 0 s)].
- Proof: by the definition of [count] and [add] for bags.
- - Suppose [s] is a fixed bag of numbers.
- - Adding a [0] to [s], and then counting the zeros in [s], means that the
- number of [0]s in [s] will be one more than (the successor [S] of) counting
- the [0]s is [s], which is exactly what the other side of the equation says.
- - So both sides of the equation are the same. The theorem is true for [s] by the
- reflexivity of equality.
- - Since we've shown that the theorem holds for an arbitrary [s], we've shown that
- it holds for all [s]s. []
- *)
- (* ################################################################# *)
- (** * Reasoning About Lists *)
- (** As with numbers, simple facts about list-processing
- functions can sometimes be proved entirely by simplification. For
- example, the simplification performed by [reflexivity] is enough
- for this theorem... *)
- Theorem nil_app : forall l:natlist,
- [] ++ l = l.
- Proof.
- reflexivity. (* [reflexivity] can match the constructors of [++] to simplify this. *)
- Qed.
- (** ...because the [[]] is substituted into the
- "scrutinee" (the expression whose value is being "scrutinized" by
- the match) in the definition of [app], allowing the match itself
- to be simplified. *)
- (** Also, as with numbers, it is sometimes helpful to perform case
- analysis on the possible shapes (empty or non-empty) of an unknown
- list. *)
- Theorem tl_length_pred : forall l:natlist,
- pred (length l) = length (tl l).
- Proof.
- intros l. (* Suppose [l] is a fixed list. *)
- destruct l as [| n l']. (* Let's consider the possible shapes a list can take. If you look
- at the constructors for lists, there are two cases. One where
- [l] is empty [nil], and the other where it [cons]s a number [n]
- to another list [l']. Let's consider both cases. For the second
- case, let's call the number [n] and the other list [l']. *)
- - (* Case: [l = nil] *)
- (* We need to show that one less than (i.e., the predecessor of) the length of [[]]
- is the same as the length of the tail of [[]]. *)
- reflexivity. (* The length of [[]] is [0], and the predessor of [0] is [0]. The tail of [[]]
- is also an empty list [[]], so it's length is [0] too.
- Both sides of the equation are the same. [reflexivity] can match these
- cases in the constructors/definitions to simplify. *)
- - (* Case: [l = cons n l'] *)
- (* We need to show that one less than (i.e., the predecessor of) the length of [n :: l']
- is the same as the length of the tail of [n :: l']. *)
- simpl. (* We can simplify out (or "cancel out") the [pred] and [n] on the left side of the
- equation. That makes the left side just [length l']. Similarly, on the right hand
- side, we can take just the tail of [n :: l'], and get the length of that. So the
- right hand side of the equation is als [length l']. *)
- reflexivity. (* Both sides of the equation are the same now. *)
- Qed.
- (* Informal proof:
- Theorem: [forall l: natlist, pred (length l) = length (tl l)].
- Proof: By case analysis on [l].
- - Suppose [l] is a fixed list of numbers.
- - Let's proceed by case analysis on [l].
- - First, suppose [l] is the empty list [[]].
- - On the left hand side of the equation: then the length of [[]] is [0],
- and the predecessor [pred] of [0] is [0].
- - On the right hand side of the equation: the tail of [[]] is [[]],
- whose length is [0].
- - Since both sides of the equation are the same, the theorem holds in this
- case by the reflexivity of equality.
- - Second, suppose [l] is [cons n l'].
- - On the left hand side of the equation, the predesesor of the length of [n :: l']
- will be the length of [l'].
- - On the right hand side of the equation, the length of the tail of [n :: l']
- will be the length of [l'].
- - Since both sides of the equation are the same, the theorem holds in this
- case by the reflexivity of equality.
- - So the theorem holds for all shapes of [l].
- - Since we've shown that the theorem holds for an arbitrary [l], we've shown that
- it holds for all [l]s. []
- *)
- (** Here, the [nil] case works because we've chosen to define
- [tl nil = nil]. Notice that the [as] annotation on the [destruct]
- tactic here introduces two names, [n] and [l'], corresponding to
- the fact that the [cons] constructor for lists takes two
- arguments (the head and tail of the list it is constructing). *)
- (** Usually, though, interesting theorems about lists require
- induction for their proofs. *)
- (* ----------------------------------------------------------------- *)
- (** *** Micro-Sermon *)
- (** Simply reading example proof scripts will not get you very far!
- It is important to work through the details of each one, using Coq
- and thinking about what each step achieves. Otherwise it is more
- or less guaranteed that the exercises will make no sense when you
- get to them. 'Nuff said. *)
- (* ================================================================= *)
- (** ** Induction on Lists *)
- (** Proofs by induction over datatypes like [natlist] are a
- little less familiar than standard natural number induction, but
- the idea is equally simple. Each [Inductive] declaration defines
- a set of data values that can be built up using the declared
- constructors: a boolean can be either [true] or [false]; a number
- can be either [O] or [S] applied to another number; a list can be
- either [nil] or [cons] applied to a number and a list.
- Moreover, applications of the declared constructors to one another
- are the _only_ possible shapes that elements of an inductively
- defined set can have, and this fact directly gives rise to a way
- of reasoning about inductively defined sets: a number is either
- [O] or else it is [S] applied to some _smaller_ number; a list is
- either [nil] or else it is [cons] applied to some number and some
- _smaller_ list; etc. So, if we have in mind some proposition [P]
- that mentions a list [l] and we want to argue that [P] holds for
- _all_ lists, we can reason as follows:
- - First, show that [P] is true of [l] when [l] is [nil].
- - Then show that [P] is true of [l] when [l] is [cons n l'] for
- some number [n] and some smaller list [l'], assuming that [P]
- is true for [l'].
- Since larger lists can only be built up from smaller ones,
- eventually reaching [nil], these two arguments together establish
- the truth of [P] for all lists [l]. Here's a concrete example: *)
- Theorem app_assoc : forall l1 l2 l3 : natlist,
- (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
- Proof.
- intros l1 l2 l3. (* Suppose that [l1], [l2], and [l3] are fixed natural numbers. *)
- induction l1 as [| n l1' IHl1']. (* Let's proceed by case analysis on [l1].
- [l1] can have the form [[]], or [n :: l1'].
- Also, let's assume that the theorem holds for
- [l1']. Let's call that [IHl1']. *)
- - (* Case: [l1 = nil] *)
- (* We need to show that [([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)]. *)
- reflexivity. (* [reflexivity] can remove the empty list from the equation by simplifying it,
- and then both sides of the equation are the same. *)
- - (* Case [l1 = cons n l1'] *)
- (* We need to show that [((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ l2 ++ l3],
- when [(l1' ++ l2) ++ l3 = l1' ++ l2 ++ l3] (the induction hypothesis. *)
- simpl. (* [simpl] can move the [n] out front. I'm not sure how it does this. *)
- rewrite -> IHl1'. (* But now the induction hypothesis matches par of the left hand side
- of the equation. So, we can replace the matching part. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- Qed.
- (* Informal proof:
- Theorem: [forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
- Proof: by inductionon [l1].
- - Suppose [l1], [l2], and [l3] are each a fixed list of numbers.
- - First, consider the case where [l1] = [nil]. We need to show:
- [([] ++ l2) ++ l3 = [] ++ l2 ++ l3].
- - By the definition of [++], appending empty lists to other lists has
- no effect, so we can drop the empty lists. That yields
- [l2 ++ l3 = l2 ++ l3].
- - Then both sides of the equation are the same, so the theorem holds
- for this case, by the reflexivity of equality.
- - Second, consider the case where [l1] is a list with a head element [n]
- and a tail list [l1'], and assume the induction hypothesis:
- [(l1' ++ l2) ++ l3 = l1' ++ l2 ++ l3]
- - We need to show that:
- [((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ l2 ++ l3]
- - By the definition of [cons], we can move the [n] up front on both sides
- of the equation, which yields:
- [n :: (l1' ++ l2) ++ l3 = n :: l1' ++ l2 ++ l3]
- - The induction hypothesis says [(l1' ++ l2) ++ l3] is the same as
- [l1' ++ l2 ++ l3], so we can replace [l1' ++ l2 ++ l3] with
- [(l1' ++ l2) ++ l3]. That yields:
- [n :: (l1' ++ l2) ++ l3 = n :: (l1' ++ l2) ++ l3]
- - Both sides of the equation are the same, so the theorem holds for
- this case too, by the reflexivity of equality.
- - We've shown that the theorem holds for all shapes that [l1] can take.
- - Since we've shown that the theorem holds for an arbitrary [l1], [l2], and [l3],
- we've shown that the theorem holds for all [l1], [l2], and [l3]. []
- *)
- (** Notice that, as when doing induction on natural numbers, the
- [as...] clause provided to the [induction] tactic gives a name to
- the induction hypothesis corresponding to the smaller list [l1']
- in the [cons] case. Once again, this Coq proof is not especially
- illuminating as a static written document -- it is easy to see
- what's going on if you are reading the proof in an interactive Coq
- session and you can see the current goal and context at each
- point, but this state is not visible in the written-down parts of
- the Coq proof. So a natural-language proof -- one written for
- human readers -- will need to include more explicit signposts; in
- particular, it will help the reader stay oriented if we remind
- them exactly what the induction hypothesis is in the second
- case. *)
- (** For comparison, here is an informal proof of the same theorem. *)
- (** _Theorem_: For all lists [l1], [l2], and [l3],
- [(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
- _Proof_: By induction on [l1].
- - First, suppose [l1 = []]. We must show
- ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),
- which follows directly from the definition of [++].
- - Next, suppose [l1 = n::l1'], with
- (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
- (the induction hypothesis). We must show
- ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).
- By the definition of [++], this follows from
- n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),
- which is immediate from the induction hypothesis. [] *)
- (* ----------------------------------------------------------------- *)
- (** *** Reversing a List *)
- (** For a slightly more involved example of inductive proof over
- lists, suppose we use [app] to define a list-reversing function
- [rev]: *)
- Fixpoint rev (l:natlist) : natlist :=
- match l with
- | nil => nil (* If [l] is empty, there's nothing to reverse. *)
- | h :: t => rev t ++ [h] (* If [l] has head [h] and a tail [t], reverse the tail [t],
- then append the head [h] to the end of that. *)
- end.
- Example test_rev1: rev [1;2;3] = [3;2;1].
- Proof. reflexivity. Qed.
- Example test_rev2: rev nil = nil.
- Proof. reflexivity. Qed.
- (* ----------------------------------------------------------------- *)
- (** *** Properties of [rev] *)
- (** Now let's prove some theorems about our newly defined [rev].
- For something a bit more challenging than what we've seen, let's
- prove that reversing a list does not change its length. Our first
- attempt gets stuck in the successor case... *)
- Theorem rev_length_firsttry : forall l : natlist,
- length (rev l) = length l.
- Proof.
- intros l. (* Suppose [l] is a fixed list of numbers. *)
- induction l as [| n l' IHl'].
- - (* l = [] *)
- reflexivity.
- - (* l = n :: l' *)
- (* This is the tricky case. Let's begin as usual
- by simplifying. *)
- simpl.
- (* Now we seem to be stuck: the goal is an equality
- involving [++], but we don't have any useful equations
- in either the immediate context or in the global
- environment! We can make a little progress by using
- the IH to rewrite the goal... *)
- rewrite <- IHl'.
- (* ... but now we can't go any further. *)
- Abort.
- (** So let's take the equation relating [++] and [length] that
- would have enabled us to make progress and prove it as a separate
- lemma. *)
- Theorem app_length : forall l1 l2 : natlist,
- length (l1 ++ l2) = (length l1) + (length l2).
- Proof.
- (* WORKED IN CLASS *)
- intros l1 l2. (* Suppose [l1] and [l2] are each a fixed list of numbers. *)
- induction l1 as [| n l1' IHl1']. (* Let's proceed by induction on [l1]. [l1] can either be an
- empty list [nil], or it can have a head [n] and a tail [l1']. Let's assume (the
- induction hypothesis [IHl1'] that [length (l1' ++ l2) = (length l1) + (length l2)]. *)
- - (* Case: [l1 = nil] *)
- (* We must show that [length ([] ++ l2) = length [] + length l2] *)
- reflexivity. (* [reflexivity] can simplify the [[]] and [length []] cases.
- And then the equation is the same on both sides. *)
- - (* Case: [l1 = cons n l1'] *)
- (* We must show that [length ((n :: l1') ++ l2) = length (n :: l1') ++ length l2], with an
- induction hypothesis: [length (l1' ++ l2) = length l1' ++ length l2]. *)
- simpl. (* [simpl] can match the [length] case and see that length [n :: l1'] is the same as
- the successor [S] of the length of [l1']. *)
- rewrite -> IHl1'. (* Now we can use the inductive hypothesis to rewrite the left hand side
- of the equation. *)
- reflexivity. (* And now both sides of the equation are the same. *)
- Qed.
- (* Informal proof:
- Theorem: [forall l1 l2 : natlist, length (l1 ++ l2) = (length l1) + (length l2)].
- Proof: by induction on [l1].
- - Suppose [l1] and [l2] are fixed lists of numbers.
- - Let's show that the theorem holds for all shapes that [l1] can take (i.e., let's
- prove this by induction). [l1] can take two shapes: it can be an empty list [nil],
- or it can have a head [n] and a tail [l1'].
- - First, consider the case where [l1] is empty.
- We need to show [length ([] ++ l2) = (length []) + (length l2)].
- - By the definition of [++], [[] ++ l2] is the same as [l2], and [length []]
- is [0]. So that yields:
- [length l2 = length l2]
- - Both sides of the equation are the same, so the theorem holds for this case
- by the reflexivity of equality.
- - Second, consider the case where [l1] has a head [n] and a tail [l1'], and suppose
- an induction hypothesis:
- [length (l1' ++ l2) = (length l1') + (length l2)]
- We need to show:
- [length ((n :: l1') ++ l2) = (length (n :: l1')) + (length l2)]
- - By the definition of [length], the length of [n :: l1'] is the same as the
- successor [S] of the length of [l1']. So we can rewrite:
- [S (length (l1' ++ l2)) = S (length l1' + length l2)]
- - The induction hypothesis says that [length (l1' ++ l2)] is the same as
- [length l1' + length l2]. So we can replace the one with the other, which yields:
- [S (length (l1' ++ l2)) = S (length (l1' ++ l2))]
- - Both sides of the equation are the same, so the theorem holds for this case
- by the reflexivity of equality too.
- - We have shown that the theorem holds for all the shapes [l1] can take.
- - Since we have shown that the theorem holds for an arbitrary [l1] and [l2],
- we have shown that it holds for all [l1] and [l2]s. []
- *)
- (** Note that, to make the lemma as general as possible, we
- quantify over _all_ [natlist]s, not just those that result from an
- application of [rev]. This should seem natural, because the truth
- of the goal clearly doesn't depend on the list having been
- reversed. Moreover, it is easier to prove the more general
- property. *)
- (** Now we can complete the original proof. *)
- Theorem rev_length : forall l : natlist,
- length (rev l) = length l.
- Proof.
- intros l. induction l as [| n l' IHl'].
- - (* l = nil *)
- reflexivity.
- - (* l = cons *)
- simpl.
- (* rewrite -> app_length. rewrite -> plus_comm. *)
- rewrite -> app_length, plus_comm. (* you can do [rewrite -> app_length], then
- [rewrite -> plus_comm], to see the details. *)
- simpl.
- rewrite -> IHl'.
- reflexivity. Qed.
- (** For comparison, here are informal proofs of these two theorems:
- _Theorem_: For all lists [l1] and [l2],
- [length (l1 ++ l2) = length l1 + length l2].
- _Proof_: By induction on [l1].
- - First, suppose [l1 = []]. We must show
- length ([] ++ l2) = length [] + length l2,
- which follows directly from the definitions of
- [length] and [++].
- - Next, suppose [l1 = n::l1'], with
- length (l1' ++ l2) = length l1' + length l2.
- We must show
- length ((n::l1') ++ l2) = length (n::l1') + length l2).
- This follows directly from the definitions of [length] and [++]
- together with the induction hypothesis. [] *)
- (** _Theorem_: For all lists [l], [length (rev l) = length l].
- _Proof_: By induction on [l].
- - First, suppose [l = []]. We must show
- length (rev []) = length [],
- which follows directly from the definitions of [length]
- and [rev].
- - Next, suppose [l = n::l'], with
- length (rev l') = length l'.
- We must show
- length (rev (n :: l')) = length (n :: l').
- By the definition of [rev], this follows from
- length ((rev l') ++ [n]) = S (length l')
- which, by the previous lemma, is the same as
- length (rev l') + length [n] = S (length l').
- This follows directly from the induction hypothesis and the
- definition of [length]. [] *)
- (** The style of these proofs is rather longwinded and pedantic.
- After the first few, we might find it easier to follow proofs that
- give fewer details (which can easily work out in our own minds or
- on scratch paper if necessary) and just highlight the non-obvious
- steps. In this more compressed style, the above proof might look
- like this: *)
- (** _Theorem_:
- For all lists [l], [length (rev l) = length l].
- _Proof_: First, observe that [length (l ++ [n]) = S (length l)]
- for any [l] (this follows by a straightforward induction on [l]).
- The main property again follows by induction on [l], using the
- observation together with the induction hypothesis in the case
- where [l = n'::l']. [] *)
- (** Which style is preferable in a given situation depends on
- the sophistication of the expected audience and how similar the
- proof at hand is to ones that the audience will already be
- familiar with. The more pedantic style is a good default for our
- present purposes. *)
- (* ================================================================= *)
- (** ** [Search] *)
- (** We've seen that proofs can make use of other theorems we've
- already proved, e.g., using [rewrite]. But in order to refer to a
- theorem, we need to know its name! Indeed, it is often hard even
- to remember what theorems have been proven, much less what they
- are called.
- Coq's [Search] command is quite helpful with this. Typing
- [Search foo] will cause Coq to display a list of all theorems
- involving [foo]. For example, try uncommenting the following line
- to see a list of theorems that we have proved about [rev]: *)
- (* Search rev. *)
- (** Keep [Search] in mind as you do the following exercises and
- throughout the rest of the book; it can save you a lot of time!
- If you are using ProofGeneral, you can run [Search] with [C-c
- C-a C-a]. Pasting its response into your buffer can be
- accomplished with [C-c C-;]. *)
- (* ================================================================= *)
- (** ** List Exercises, Part 1 *)
- (** **** Exercise: 3 stars (list_exercises) *)
- (** More practice with lists: *)
- Theorem app_nil_r : forall l : natlist,
- l ++ [] = l.
- Proof.
- intros l. (* Suppose [l] is a fixed list. *)
- induction l as [| n l' IHl']. (* Let's proceed by induction on [l]. *)
- - (* Case: [l = []]. *)
- (* We must show that [[] ++ [] = []]. *)
- reflexivity. (* after simplifying, both sides of the equation are the same. *)
- - (* Case: [l = [n :: l'], with the induction hypothesis: [n :: l' ++ [] = n :: l']. *)
- simpl. (* [simpl] removes the parentheses. Why? *)
- rewrite -> IHl'. (* The induction hypothesis says [l' ++ []] is the same as [l'].
- So let's replace [l' ++ []] with [l']. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- Qed.
- (* Informal proof:
- Theorem: [forall l : natlist, l ++ [] = l].
- Proof: by inductiont on [l].
- - Suppose [l] is a fixed list of numbers.
- - Let's proceed by induction on [l].
- - First consider the case where [l] is [[]].
- We must show that [[] ++ [] = []].
- - By the definition of [++], [[] ++ []] is the same as []].
- - Then both sides of the equation are the same.
- - So the theorem holds for this case, by the reflexivity of equality.
- - Now consider the case where [l] has a head [n] and a tail [l1],
- and assume an induction hypothesis:
- [l' ++ [] = l'].
- We must show that [n :: l' ++ [] = n :: l'].
- - The induction hypothesis says that [l' ++ []] is the same as [l'].
- So we can replace [l' ++ []] with [l']. That yields [n :: l' = n :: l'].
- - Both sides of the equation are the same, so this theorem holds
- for this case too, by the reflexivity of equality.
- - We've shown that the theorem holds for all shapes that [l] can take.
- - Since we've shown that the theorem holds for an arbitrary [l],
- we've shown that it holds for all [l]s. []
- *)
- Theorem rev_app_distr: forall l1 l2 : natlist,
- rev (l1 ++ l2) = rev l2 ++ rev l1.
- Proof.
- intros l1 l2. (* Suppose [l1] and [l2] are fixed numbers. *)
- induction l1 as [| n' l1' IHl1']. (* Proceed by induction on [l1]. *)
- - (* Case: [l1 = []]. *)
- (* We must show that [rev ([] ++ l2) = rev l2 ++ rev []]. *)
- simpl. (* By the definition of [++], [simpl] can reduce [[] ++ l2] to [l2] on the left side
- of the equation. By the definition of [rev], it can reduce [rev []] on the right
- side of the equation to []. *)
- rewrite -> app_nil_r. (* By [app_nil_r], [rev l2 ++ []] is the same as [rev l2]. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- - (* Case: [l1 = n' :: l1], with induction hypothesis: [rev (l1' ++ l2) = rev l2 ++ rev l1']. *)
- (* We need to show that [rev ((n' :: l2) ++ l2) = rev l2 ++ rev (n' :: l2)]. *)
- simpl. (* By the definition of [rev], [simpl] can see that [rev n' :: l1'] is the same as
- [rev l1' ++ [n']]. So it does that replacement. *)
- rewrite -> IHl1'. (* The induction hypothesis says that [rev (l1' ++ l2)] is the same as
- [rev l2 ++ rev l1']. So we can replace the one with the other. *)
- rewrite -> app_assoc. (* Now the only difference between the two sides of the equation is
- the parentheses. But we have a lemma which says that [++] is
- associative. So we can rewrite the left side of the equation
- with different parentheses. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- Qed.
- (* Informal proof:
- Theorem: [forall l1 l2 : nat, rev (l1 ++ l2) = rev l2 ++ rev l1].
- Proof: by induction on [l1].
- - Suppose [l1] and [l2] are each a fixed list of numbers.
- - Let's proceed by induction on [l1]. That is, let's consider all the shapes that
- [l1] can take.
- - First, consider the case where [l1] is the empty list [[]].
- We must show [rev ([] ++ l2) = rev l2 ++ rev []].
- - By the definition of [++], [[] ++ l2] is the same as [l2]. And by the definition of
- [rev], [rev []] is the same as [[]]. Both of those replacements yield:
- [rev l2 = rev l2 ++ []]
- - By the lemma [app_nil_r], [rev l2 ++ []] is the same as [rev l2].
- - Now both sides of the equation are the same, so the theorem holds for this case
- by the reflexivity of equality.
- - Second, consider the case where [l1] has a head [n'] and a tail [l1'],
- with an induction hypothesis:
- [rev (l1' ++ l2) = rev l2 ++ rev l1'].
- We must show:
- [rev ((n' :: l1') ++ l2) = rev l2 ++ rev (n' :: l1')].
- - By the definition of [rev], [rev (n' :: l1')] is the same as [rev l1' ++ [n']].
- So if we make that replacement, that yields:
- [rev ((l1' ++ [n']) ++ l2) = rev l2 ++ (rev l1' ++ [n'])].
- - Again, [rev ((l1' ++ n') ++ l2)] is the same as [(rev l2 ++ rev l1') ++ [n']].
- So that yields:
- [(rev l2 ++ rev l1') ++ [n'] = rev l2 ++ rev l1' ++ [n']].
- - By the lemma [app_assoc], [++] is associative, so we can arrange the parentheses
- to make the left side of the equation match the right side.
- - Both sides of the equation are the same, so the theorem holds for this case too,
- by the reflexivity of equality.
- - We've shown that the theorem holds for all shapes that [l1] can take.
- - Since we've shown that the theorem holds for an arbitrary [l1], we've shown that
- it holds for all [l1]s. []
- *)
- 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.
- (** 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
- way. *)
- 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 [| n1 l1' IHl1'].
- - simpl. rewrite -> app_assoc. reflexivity.
- - simpl. rewrite <- IHl1'. reflexivity.
- Qed.
- (** An exercise about your implementation of [nonzeros]: *)
- Lemma nonzeros_app : forall l1 l2 : natlist,
- nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
- Proof.
- intros l1 l2.
- induction l1 as [| n1 l1' IHl1'].
- - simpl. reflexivity.
- - induction n1 as [| n1' IHn1'].
- + simpl. rewrite -> IHl1'. reflexivity.
- + simpl. rewrite <- IHl1'. reflexivity.
- Qed.
- (** [] *)
- (** **** Exercise: 2 stars (beq_natlist) *)
- (** Fill in the definition of [beq_natlist], which compares
- lists of numbers for equality. Prove that [beq_natlist l l]
- yields [true] for every list [l]. *)
- Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
- match l1, l2 with
- | nil, nil => true
- | nil, h :: t => false
- | h :: t, nil => false
- | h1 :: t1, h2 :: t2 => match beq_nat h1 h2 with
- | true => beq_natlist t1 t2
- | false => false
- end
- end.
- Example test_beq_natlist1 :
- (beq_natlist nil nil = true).
- Proof. reflexivity. Qed.
- Example test_beq_natlist2 :
- beq_natlist [1;2;3] [1;2;3] = true.
- Proof. reflexivity. Qed.
- Example test_beq_natlist3 :
- beq_natlist [1;2;3] [1;2;4] = false.
- Proof. reflexivity. Qed.
- Theorem beq_natlist_refl : forall l:natlist,
- true = beq_natlist l l.
- Proof.
- intros l.
- induction l as [| n l' IHl'].
- - reflexivity.
- - destruct n.
- + simpl.
- rewrite -> IHl'.
- reflexivity.
- + simpl.
- rewrite <- beq_nat_refl.
- rewrite -> IHl'.
- reflexivity.
- Qed.
- (** [] *)
- (* ================================================================= *)
- (** ** List Exercises, Part 2 *)
- (** Here are a couple of little theorems to prove about your
- definitions about bags above. *)
- (** **** Exercise: 1 star (count_member_nonzero) *)
- Theorem count_member_nonzero : forall (s : bag),
- leb 1 (count 1 (1 :: s)) = true.
- Proof.
- intros s.
- simpl.
- reflexivity.
- Qed.
- (** [] *)
- (** The following lemma about [leb] might help you in the next exercise. *)
- Theorem ble_n_Sn : forall n,
- leb n (S n) = true.
- Proof.
- intros n. induction n as [| n' IHn'].
- - (* 0 *)
- simpl. reflexivity.
- - (* S n' *)
- simpl. rewrite IHn'. reflexivity. Qed.
- (** **** Exercise: 3 stars, advanced (remove_decreases_count) *)
- Theorem remove_decreases_count: forall (s : bag),
- leb (count 0 (remove_one 0 s)) (count 0 s) = true.
- Proof.
- intros s.
- Search count.
- induction s as [| n s' IHs'].
- - simpl. reflexivity.
- - simpl.
- destruct n.
- + simpl. rewrite -> ble_n_Sn. reflexivity.
- + simpl. rewrite -> IHs'. reflexivity.
- Qed.
- (** [] *)
- (** **** Exercise: 3 stars, optional (bag_count_sum) *)
- (** Write down an interesting theorem [bag_count_sum] about bags
- involving the functions [count] and [sum], and prove it using
- Coq. (You may find that the difficulty of the proof depends on
- how you defined [count]!) *)
- Theorem bag_count_sum : forall s1 s2 : bag,
- count 0 s1 + count 0 s2 = count 0 (sum s1 s2).
- Proof.
- intros s1 s2. (* Suppose [s1] and [s2] are fixed bags of numbers. *)
- induction s1 as [| n s1' IHs1']. (* Let's proceed by induction on [s1]. *)
- - (* Case: [s1 = []]. *)
- (* We need to show that [count 0 [] + count 0 s2 = count 0 (sum [] s2)]. *)
- simpl. (* By the definition of [count] and [sum], we can drop the empty lists. *)
- reflexivity. (* That renders both sides of the equation the same. *)
- - (* Case: [s1 = [n :: s1'],
- with induction hypothesis: [count 0 s1' + count 0 s2 = count 0 (sum s1' s2)]. *)
- (* We need to show that:
- [count 0 (n :: s1') + count 0 s2 = count 0 (sum (n :: s1') s2)]. *)
- destruct n as [| n']. (* Let's proceed by case analysis on [n]. That is, let's prove the goal
- holds for each shape of [n]. *)
- + (* Case: [n = 0]. *)
- (* We need to show that:
- [count 0 (0 :: s1') + count 0 s2 = count 0 (sum(0 :: s1') s2)]. *)
- simpl. (* [simpl] can use the definition of [count] and the assumption that [n = 0]
- to figure out that the [count 0] of [n :: sl'] is the successor [S]
- of (count 0 s1'). *)
- rewrite -> IHs1'. (* The induction hypothesis tells us that [count 0 s1' + count 0 s2]
- is the same as [count 0 (sum s1' s2)]. So we can rewrite. *)
- reflexivity. (* Now both sides of the equation are the same. *)
- + (* Case: [n = S n']. *)
- (* We must show that:
- [(count 0 (S n' :: s1') + count 0 s2 = count 0 (sum (S n' :: s1') s2)]. *)
- simpl. (* [simpl] can see in [S n' :: s1'] that the head of the list [S n'] is not [0].
- So it won't count any [0]s in the head of the list! Because of that, it removes
- the head [S n'] of the list and just considers [s1'] on both sides of the
- equation. *)
- rewrite -> IHs1'. (* But now the equation looks just like the inductive hypothesis.
- So we can rewrite. *)
- reflexivity. (* Now both sides of the equation both look the same. *)
- Qed.
- (** [] *)
- (** **** Exercise: 4 stars, advanced (rev_injective) *)
- (* Do not modify the following line: *)
- Definition manual_grade_for_rev_injective : option (prod nat string) := None.
- (** Prove that the [rev] function is injective -- that is,
- forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
- (There is a hard way and an easy way to do this.) *)
- (* FILL IN HERE *)
- (** [] *)
- (* ################################################################# *)
- (** * Options *)
- (** Suppose we want to write a function that returns the [n]th
- element of some list. If we give it type [nat -> natlist -> nat],
- then we'll have to choose some number to return when the list is
- too short... *)
- Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
- match l with
- | nil => 42 (* arbitrary! *)
- | a :: l' => match beq_nat n O with
- | true => a
- | false => nth_bad l' (pred n)
- end
- end.
- (** This solution is not so good: If [nth_bad] returns [42], we
- can't tell whether that value actually appears on the input
- without further processing. A better alternative is to change the
- return type of [nth_bad] to include an error value as a possible
- outcome. We call this type [natoption]. *)
- Inductive natoption : Type :=
- | Some : nat -> natoption
- | None : natoption.
- (** We can then change the above definition of [nth_bad] to
- return [None] when the list is too short and [Some a] when the
- list has enough members and [a] appears at position [n]. We call
- this new function [nth_error] to indicate that it may result in an
- error. *)
- Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
- match l with
- | nil => None
- | a :: l' => match beq_nat n O with
- | true => Some a
- | false => nth_error l' (pred n)
- end
- end.
- Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
- Proof. reflexivity. Qed.
- Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
- Proof. reflexivity. Qed.
- Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
- Proof. reflexivity. Qed.
- (** (In the HTML version, the boilerplate proofs of these
- examples are elided. Click on a box if you want to see one.)
- This example is also an opportunity to introduce one more small
- feature of Coq's programming language: conditional
- expressions... *)
- Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
- match l with
- | nil => None
- | a :: l' => if beq_nat n O then Some a
- else nth_error' l' (pred n)
- end.
- (** Coq's conditionals are exactly like those found in any other
- language, with one small generalization. Since the boolean type
- is not built in, Coq actually supports conditional expressions over
- _any_ inductively defined type with exactly two constructors. The
- guard is considered true if it evaluates to the first constructor
- in the [Inductive] definition and false if it evaluates to the
- second. *)
- (** The function below pulls the [nat] out of a [natoption], returning
- a supplied default in the [None] case. *)
- Definition option_elim (d : nat) (o : natoption) : nat :=
- match o with
- | Some n' => n'
- | None => d
- end.
- (** **** Exercise: 2 stars (hd_error) *)
- (** 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 :=
- match l with
- | nil => None
- | h :: t => Some h
- end.
- Example test_hd_error1 : hd_error [] = None.
- Proof. reflexivity. Qed.
- Example test_hd_error2 : hd_error [1] = Some 1.
- Proof. reflexivity. Qed.
- Example test_hd_error3 : hd_error [5;6] = Some 5.
- Proof. reflexivity. Qed.
- (** [] *)
- (** **** Exercise: 1 star, optional (option_elim_hd) *)
- (** This exercise relates your new [hd_error] to the old [hd]. *)
- Theorem option_elim_hd : forall (l:natlist) (default:nat),
- hd default l = option_elim default (hd_error l).
- Proof.
- intros l default.
- induction l as [ | h l' IHl' ].
- - reflexivity.
- - reflexivity.
- Qed.
- (** [] *)
- End NatList.
- (* ################################################################# *)
- (** * Partial Maps *)
- (** As a final illustration of how data structures can be defined in
- Coq, here is a simple _partial map_ data type, analogous to the
- map or dictionary data structures found in most programming
- languages. *)
- (** First, we define a new inductive datatype [id] to serve as the
- "keys" of our partial maps. *)
- Inductive id : Type :=
- | Id : nat -> id.
- (** Internally, an [id] is just a number. Introducing a separate type
- by wrapping each nat with the tag [Id] makes definitions more
- readable and gives us the flexibility to change representations
- later if we wish. *)
- (** We'll also need an equality test for [id]s: *)
- Definition beq_id (x1 x2 : id) :=
- match x1, x2 with
- | Id n1, Id n2 => beq_nat n1 n2
- end.
- (** **** Exercise: 1 star (beq_id_refl) *)
- Theorem beq_id_refl : forall x, true = beq_id x x.
- Proof.
- intros x.
- induction x as [n].
- - simpl.
- induction n as [| n' IHn'].
- + reflexivity.
- + simpl. rewrite <- IHn'. reflexivity.
- Qed.
- (** [] *)
- (** Now we define the type of partial maps: *)
- Module PartialMap.
- Export NatList.
- Inductive partial_map : Type :=
- | empty : partial_map
- | record : id -> nat -> partial_map -> partial_map.
- (** This declaration can be read: "There are two ways to construct a
- [partial_map]: either using the constructor [empty] to represent an
- empty partial map, or by applying the constructor [record] to
- a key, a value, and an existing [partial_map] to construct a
- [partial_map] with an additional key-to-value mapping." *)
- (** The [update] function overrides the entry for a given key in a
- partial map (or adds a new entry if the given key is not already
- present). *)
- Definition update (d : partial_map)
- (x : id) (value : nat)
- : partial_map :=
- record x value d.
- (** Last, the [find] function searches a [partial_map] for a given
- key. It returns [None] if the key was not found and [Some val] if
- the key was associated with [val]. If the same key is mapped to
- multiple values, [find] will return the first one it
- encounters. *)
- Fixpoint find (x : id) (d : partial_map) : natoption :=
- match d with
- | empty => None
- | record y v d' => if beq_id x y
- then Some v
- else find x d'
- end.
- (** **** Exercise: 1 star (update_eq) *)
- Theorem update_eq :
- forall (d : partial_map) (x : id) (v: nat),
- find x (update d x v) = Some v.
- Proof.
- intros d x v.
- induction d as [| x' v' d' IHd' ].
- - simpl. rewrite <- beq_id_refl. reflexivity.
- - simpl. rewrite <- beq_id_refl. reflexivity.
- Qed.
- (** [] *)
- (** **** Exercise: 1 star (update_neq) *)
- Theorem update_neq :
- forall (d : partial_map) (x y : id) (o: nat),
- beq_id x y = false -> find x (update d y o) = find x d.
- Proof.
- intros d x y o.
- intros H.
- simpl.
- rewrite -> H.
- reflexivity.
- Qed.
- (** [] *)
- End PartialMap.
- (** **** Exercise: 2 stars (baz_num_elts) *)
- (** Consider the following inductive definition: *)
- Inductive baz : Type :=
- | Baz1 : baz -> baz
- | Baz2 : baz -> bool -> baz.
- (** How _many_ elements does the type [baz] have?
- (Explain your answer in words, preferrably English.) *)
- (* I think this type has zero elements, because there is no constructor to create one.
- [Baz1] takes a [baz] as an argument, but where'd we get _that_ [baz]? The same goes
- for [Baz2]. *)
- (* Do not modify the following line: *)
- Definition manual_grade_for_baz_num_elts : option (prod nat string) := None.
- (** [] *)
Add Comment
Please, Sign In to add comment