Library Lists
(* Lists and higher-order functions
Version of 4/28/2009
*)
(* This line imports all of our definitions from Basics.v.
For it to work, you need to compile Basics.v into
Basics.vo. (This is like making a .class file from a
.java file, or a .o file from a .c file.)
Here are two ways to compile your code:
- CoqIDE
1. Open Basics.v.
2. In the "Compile" menu, click on "Compile Buffer".
- Command line
1. Run: coqc Basics.v
*)
Require Export Basics.
(* -------------------------------------------------------------- *)
(* Pairs of numbers *)
(* Technical note: Here, we again use the Module feature
to wrap all of the definitions for pairs and lists of
numbers in a module so that, later, we can use the same
names for the generic ("polymorphic") versions of the
same operations. *)
Module NatList.
Inductive natprod : Set :=
pair : nat -> nat -> natprod.
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.
Notation "( x , y )" := (pair x y).
(* Eval simpl in (fst (3,4)). *)
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 and prove a few simple facts about pairs.
If we state the lemmas in a particular way, we can prove them
with just partial evaluation
*)
Theorem surjective_pairing' : forall (n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.
(* But that's not enough if we state the lemma in a more natural way: *)
Theorem surjective_pairing_stuck : forall (p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* Doesn't reduce anything! *)
Admitted.
(* We have to expose the structure of p so that simple can perform
the pattern match in fst and snd.
Notice that, unlike for nats, destruct doesn't generate
an extra subgoal here. That's because natprods can
only be constructed in one way.
*)
Theorem surjective_pairing : forall (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as (n,m). simpl. reflexivity. Qed.
(* Notice that Coq allows us to use the notation we
introduced for pairs in the "as..." pattern telling it
what variables to bind. *)
Version of 4/28/2009
*)
(* This line imports all of our definitions from Basics.v.
For it to work, you need to compile Basics.v into
Basics.vo. (This is like making a .class file from a
.java file, or a .o file from a .c file.)
Here are two ways to compile your code:
- CoqIDE
1. Open Basics.v.
2. In the "Compile" menu, click on "Compile Buffer".
- Command line
1. Run: coqc Basics.v
*)
Require Export Basics.
(* -------------------------------------------------------------- *)
(* Pairs of numbers *)
(* Technical note: Here, we again use the Module feature
to wrap all of the definitions for pairs and lists of
numbers in a module so that, later, we can use the same
names for the generic ("polymorphic") versions of the
same operations. *)
Module NatList.
Inductive natprod : Set :=
pair : nat -> nat -> natprod.
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.
Notation "( x , y )" := (pair x y).
(* Eval simpl in (fst (3,4)). *)
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 and prove a few simple facts about pairs.
If we state the lemmas in a particular way, we can prove them
with just partial evaluation
*)
Theorem surjective_pairing' : forall (n m : nat),
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity. Qed.
(* But that's not enough if we state the lemma in a more natural way: *)
Theorem surjective_pairing_stuck : forall (p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* Doesn't reduce anything! *)
Admitted.
(* We have to expose the structure of p so that simple can perform
the pattern match in fst and snd.
Notice that, unlike for nats, destruct doesn't generate
an extra subgoal here. That's because natprods can
only be constructed in one way.
*)
Theorem surjective_pairing : forall (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as (n,m). simpl. reflexivity. Qed.
(* Notice that Coq allows us to use the notation we
introduced for pairs in the "as..." pattern telling it
what variables to bind. *)
Theorem snd_fst_is_swap : forall (p : natprod),
(snd p, fst p) = swap_pair p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(snd p, fst p) = swap_pair p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem fst_swap_is_snd : forall (p : natprod),
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* -------------------------------------------------------------- *)
(* Lists of numbers *)
Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.
Definition l_123 := cons 1 (cons 2 (cons 3 nil)).
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Definition l_123' := 1 :: (2 :: (3 :: nil)).
Definition l_123'' := 1 :: 2 :: 3 :: nil.
Definition l_123''' := [1,2,3].
Fixpoint repeat (n count : nat) {struct count} : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.
Fixpoint length (l:natlist) {struct l} : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.
Definition hd (l:natlist) : nat :=
match l with
| nil => 0 (* arbitrarily *)
| h :: t => h
end.
Definition tl (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.
Fixpoint app (l1 l2 : natlist) {struct l1} : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.
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.
(* -------------------------------------------------------------- *)
(* Exercise: Bags via lists *)
Definition bag := natlist.
fst (swap_pair p) = snd p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* -------------------------------------------------------------- *)
(* Lists of numbers *)
Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.
Definition l_123 := cons 1 (cons 2 (cons 3 nil)).
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Definition l_123' := 1 :: (2 :: (3 :: nil)).
Definition l_123'' := 1 :: 2 :: 3 :: nil.
Definition l_123''' := [1,2,3].
Fixpoint repeat (n count : nat) {struct count} : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.
Fixpoint length (l:natlist) {struct l} : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.
Definition hd (l:natlist) : nat :=
match l with
| nil => 0 (* arbitrarily *)
| h :: t => h
end.
Definition tl (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.
Fixpoint app (l1 l2 : natlist) {struct l1} : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.
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.
(* -------------------------------------------------------------- *)
(* Exercise: Bags via lists *)
Definition bag := natlist.
Fixpoint count (v:nat) (s:bag) {struct s} : nat :=
(* FILL IN HERE *)
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.
Definition union :=
(* FILL IN HERE *)
Example test_union1: count 1 (union [1,2,3] [1,4,1]) = 3.
Proof. reflexivity. Qed.
Definition add (v:nat) (s:bag) : bag :=
(* FILL IN HERE *)
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 :=
(* FILL IN HERE *)
Example test_member1: member 1 [1,4,1] = true.
Proof. reflexivity. Qed.
Example test_member2: member 2 [1,4,1] = false.
Proof. reflexivity. Qed.
Fixpoint remove_one (v:nat) (s:bag) {struct s} : bag :=
(* FILL IN HERE *)
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) {struct s} : bag :=
(* FILL IN HERE *)
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]) = 0.
Proof. reflexivity. Qed.
Fixpoint subset (s1:bag) (s2:bag) {struct s1} : bool :=
(* FILL IN HERE *)
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.
(* ---------------------------------------------------------- *)
(* Reasoning about lists *)
(* Just like with numbers, we can do some proofs about
lists using just "partial evaluation"... *)
Theorem nil_app : forall l:natlist,
[] ++ l = l.
Proof.
reflexivity. Qed.
(* And, also like numbers, sometimes it helps to do case
analysis on the structure of the list. Here, we give
coq two names for the cons case - one for the first
element of the list and the other for the tail of the
list. *)
Theorem tl_length_pred : forall l:natlist,
pred (length l) = length (tl l).
Proof.
intros l. destruct l as [| n l'].
Case "l = nil".
reflexivity.
Case "l = cons n l'".
reflexivity. Qed.
(* The nil case works because we've chosen (tl nil = nil). *)
(* ---------------------------------------------------- *)
(* Induction on lists *)
(* We can do induction on any inductively defined type,
not just numbers: Coq generates an appropriate
induction principle when it processes the Inductive
declaration.
Here is the induction principle for lists:
If P l is some proposition involving a natlist l,
and we want to show that P holds for all l, we can
reason like this:
- show that P holds
- show that, for any element n:nat and any natlist
l', if P l' holds, then so does P (n::l')
- conclude that P l holds for all natlists l.
*)
Theorem ass_app : forall l1 l2 l3 : natlist,
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
intros l1 l2 l3. induction l1 as [| n l1'].
Case "l1 = nil".
reflexivity.
Case "l1 = cons n l1'".
simpl. rewrite -> IHl1'. reflexivity. Qed.
(* An exercise to be worked together: *)
Theorem app_length : forall l1 l2 : natlist,
length (l1 ++ l2) = plus (length l1) (length l2).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Fixpoint nonzeros (l:natlist) {struct l} : natlist :=
(* FILL IN HERE *)
Example test_nonzeros: nonzeros [0,1,0,2,3,0,0] = [1,2,3].
Proof. reflexivity. Qed.
Fixpoint oddmembers (l:natlist) {struct l} : natlist :=
(* FILL IN HERE *)
Example test_oddmembers: oddmembers [0,1,0,2,3,0,0] = [1,3].
Proof. reflexivity. Qed.
Fixpoint countoddmembers (l:natlist) {struct l} : nat :=
(* FILL IN HERE *)
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: 2 stars *)
Fixpoint alternate (l1 l2 : natlist) {struct l1} : natlist :=
(* FILL IN HERE *)
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.
(* snoc inserts an element at the end of a list *)
Fixpoint snoc (l:natlist) (v:nat) {struct l} : natlist :=
match l with
| nil => [v]
| h :: t => h :: (snoc t v)
end.
(* We can use snoc to reverse a list *)
Fixpoint rev (l:natlist) {struct l} : natlist :=
match l with
| nil => nil
| h :: t => snoc (rev t) h
end.
Example test_rev1: rev [1,2,3] = [3,2,1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.
(* Now some more list theorems using our newly defined snoc and rev.
Let's try something a little more intricate: proving that reversing
a list does not change its length. Our first attempt at this proof
gets stuck in the successor case... *)
Theorem rev_length_firsttry : forall l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l'].
Case "l = nil".
reflexivity.
Case "l = cons".
simpl. (* Here we get stuck: the goal is an equality
involving snoc, but we don't have any equations
in either the immediate context or the global
environment that have anything to do with
snoc! *)
Admitted.
(* So let's take the equation about snoc that would have
enabled us to make progress and prove it as a separate
lemma. *)
Theorem length_snoc : forall n : nat, forall l : natlist,
length (snoc l n) = S (length l).
Proof.
intros n l. induction l as [| n' l'].
Case "l = nil".
reflexivity.
Case "l = cons n' l'".
simpl. rewrite -> IHl'. reflexivity. Qed.
(* 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'].
Case "l = nil".
reflexivity.
Case "l = cons".
simpl. rewrite -> length_snoc. rewrite -> IHl'. reflexivity. Qed.
(* ------------------------------------------------------- *)
(* A bunch of exercises... *)
Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem rev_involutive : forall l : natlist,
rev (rev l) = l.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* There is a short solution to the next exercise. If you
find yourself getting tangled up, step back and try to
look for a simpler way... *)
Theorem ass_app4 : forall l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem snoc_append : forall (l:natlist) (n:nat),
snoc l n = l ++ [n].
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem append_snoc : forall l1 l2 : natlist, forall n : nat,
((snoc l1 n) ++ l2) = l1 ++ (n :: l2).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* An exercise about your implementation of nonzeros *)
Lemma nonzeros_length : forall l1 l2 : natlist, nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2). Proof. (* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* A couple more exercises *)
(* Design exercise:
- Write down a non-trivial theorem involving cons (::),
snoc, and append (++).
- Prove it.
(* FILL IN HERE *)
*)
- Write down a non-trivial theorem involving cons (::),
snoc, and append (++).
- Prove it.
(* FILL IN HERE *)
*)
(* If you did the optional exercise about bags above, here
are a couple of little theorems to prove about your
definitions *)
are a couple of little theorems to prove about your
definitions *)
Theorem count_member_nonzero : forall (s : bag),
ble_nat 0 (count 1 (1 :: s)) = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* The following lemma about ble_nat might help you below *)
Theorem ble_n_Sn : forall n,
ble_nat n (S n) = true.
Proof.
intros n. induction n as [| n'].
Case "0".
simpl. reflexivity.
Case "S n'".
simpl. rewrite IHn'. reflexivity. Qed.
Theorem remove_decreases_count: forall (s : bag),
ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* -------------------------------------------------------------- *)
(* Options *)
Inductive natoption : Set :=
| Some : nat -> natoption
| None : natoption.
Fixpoint index_bad (n:nat) (l:natlist) {struct l} : nat :=
match l with
| nil => 42 (* arbitrary! *)
| a :: l' => match beq_nat n O with
| true => a
| false => index_bad (pred n) l'
end
end.
Fixpoint index (n:nat) (l:natlist) {struct l} : natoption :=
match l with
| nil => None
| a :: l' => match beq_nat n O with
| true => Some a
| false => index (pred n) l'
end
end.
Example test_index1 : index 0 [4,5,6,7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 3 [4,5,6,7] = Some 7.
Proof. reflexivity. Qed.
Example test_index3 : index 10 [4,5,6,7] = None.
Proof. reflexivity. Qed.
Fixpoint index' (n:nat) (l:natlist) {struct l} : natoption :=
match l with
| nil => None
| a :: l' => if beq_nat n O then Some a else index (pred n) l'
end.
(* This function pulls the nat out of a natoption,
returning a supplied default in the None case. *)
Definition option_elim (o : natoption) (d : nat) : nat :=
match o with
| Some n' => n'
| None => d
end.
(* Using the same idea, fix the hd function from earlier so
we don't have to return an arbitrary element *)
we don't have to return an arbitrary element *)
Definition hd_opt (l : natlist) : natoption := (* FILL IN HERE *) Example test_hd_opt1 : hd_opt [] = None. Proof. reflexivity. Qed. Example test_hd_opt2 : hd_opt [1] = Some 1. Proof. reflexivity. Qed. Example test_hd_opt3 : hd_opt [5,6] = Some 5. Proof. reflexivity. Qed. (** **** Exercise: 2 stars *) (* An exercise relating your new hd_opt to the old hd *) Theorem option_elim_hd : forall l:natlist, hd l = option_elim (hd_opt l) 0. Proof. (* FILL IN HERE (and delete "Admitted") *) Admitted.
Fixpoint beq_natlist (l1 l2 : natlist) {struct l1} : bool :=
(* FILL IN HERE *)
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,
beq_natlist l l = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ----------------------------------------------------- *)
(* The apply tactic *)
(* We often encounter situations where the goal to be proved
is exactly the same as some hypothesis in the context or
some previously proved lemma. *)
Theorem silly1 : forall (n m o p : nat),
n = m
-> [n,o] = [n,p]
-> [n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
rewrite <- eq1.
(* At this point, we could finish with rewrite -> eq2. reflexivity. as we have done several times above.
But we can achieve the same effect in a single step by
using the apply tactic instead: *)
apply eq2. Qed.
(* The apply tactic also works with CONDITIONAL hypotheses
and lemmas: if the statement being applied is an
implication, then the premises of this implication will
be added to the list of subgoals needing to be proved. *)
Theorem silly2 : forall (n m o p : nat),
n = m
-> (forall (q r : nat), q = r -> [q,o] = [r,p])
-> [n,o] = [m,p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.
(* You may find it instructive to experiment with this proof
and see if there is a way to complete it using just
rewrite instead of apply. *)
(* Typically, when we use apply H, the statement H will
begin with a forall binding some "universal variables."
When Coq matches the current goal against the conclusion
of H, it will try to find appropriate values for these
variables. For example, when we do apply eq2 in in the
following proof, the universal variable q in eq2 gets
instantiated with (m,m) and r gets instantiated with
(n,n). *)
Theorem silly2a : forall (n m : nat),
(n,n) = (m,m)
-> (forall (q r : nat), (q,q) = (r,r) -> [q] = [r])
-> [n] = [m].
Proof.
intros n m eq1 eq2.
apply eq2. apply eq1. Qed.
(* Complete the following proof without using simpl. *)
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true)
-> evenb 3 = true
-> oddb 4 = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* To use the apply tactic, the (conclusion of the) fact
being applied must match the goal EXACTLY -- for example,
apply will not work if the left and right sides of the
equality are swapped. *)
Theorem silly3_firsttry : forall (n : nat),
true = beq_nat n 5
-> beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
simpl.
(* here we are stuck *)
Admitted.
(* When you find yourself in such a situation, one thing
to do is to go back and try reorganizing the statement
of whatever you are trying to prove so that things
appear the right way around when they are needed. But
if this is not possible or convenient, then the
following lemma can be used to swap the sides of an
equality statement in the goal so that some other lemma
can be applied. *)
Theorem sym_eq_bool : forall (b c : bool),
b = c -> c = b.
Proof.
intros b c H. rewrite -> H. reflexivity. Qed.
Theorem silly3 : forall (n : nat),
true = beq_nat n 5
-> beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
apply sym_eq_bool. (* NOTE that, just as with rewrite,
we can apply a lemma,
not just an assumption in the context *)
simpl. (* Actually, this line is unnecessary, since *)
apply H. (* apply will do a simpl step first. *) Qed.
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true)
-> evenb 3 = true
-> oddb 4 = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* To use the apply tactic, the (conclusion of the) fact
being applied must match the goal EXACTLY -- for example,
apply will not work if the left and right sides of the
equality are swapped. *)
Theorem silly3_firsttry : forall (n : nat),
true = beq_nat n 5
-> beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
simpl.
(* here we are stuck *)
Admitted.
(* When you find yourself in such a situation, one thing
to do is to go back and try reorganizing the statement
of whatever you are trying to prove so that things
appear the right way around when they are needed. But
if this is not possible or convenient, then the
following lemma can be used to swap the sides of an
equality statement in the goal so that some other lemma
can be applied. *)
Theorem sym_eq_bool : forall (b c : bool),
b = c -> c = b.
Proof.
intros b c H. rewrite -> H. reflexivity. Qed.
Theorem silly3 : forall (n : nat),
true = beq_nat n 5
-> beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
apply sym_eq_bool. (* NOTE that, just as with rewrite,
we can apply a lemma,
not just an assumption in the context *)
simpl. (* Actually, this line is unnecessary, since *)
apply H. (* apply will do a simpl step first. *) Qed.
(* Here are two exercises for you *)
Theorem rev_exercise1 : forall (l l' : natlist),
l = rev l'
-> l' = rev l.
Proof.
(* Remember you can use apply with previously defined lemmas,
not just hypotheses in the context. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* This one is a little tricky. The first line of the
proof is provided, because it uses an idea we haven't
seen before. Notice that we don't introduce m before
performing induction. This leave it general, so that
the IH doesn't specify a particular m, but lets us
pick. We'll talk more about this later in the course.
*)
Theorem beq_nat_sym : forall n m b,
beq_nat n m = b -> beq_nat m n = b.
Proof.
intros n. induction n as [| n'].
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem rev_exercise1 : forall (l l' : natlist),
l = rev l'
-> l' = rev l.
Proof.
(* Remember you can use apply with previously defined lemmas,
not just hypotheses in the context. *)
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* This one is a little tricky. The first line of the
proof is provided, because it uses an idea we haven't
seen before. Notice that we don't introduce m before
performing induction. This leave it general, so that
the IH doesn't specify a particular m, but lets us
pick. We'll talk more about this later in the course.
*)
Theorem beq_nat_sym : forall n m b,
beq_nat n m = b -> beq_nat m n = b.
Proof.
intros n. induction n as [| n'].
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Provide an informal proof of this lemma:
Informal proof of beq_nat_sym:
Theorem: For any nats n m and bool b, if beq_nat n m = b
then beq_nat m n = b.
Proof:
(* FILL IN HERE *)
*)
Informal proof of beq_nat_sym:
Theorem: For any nats n m and bool b, if beq_nat n m = b
then beq_nat m n = b.
Proof:
(* FILL IN HERE *)
*)
(* Briefly explain the difference between the tactics
apply and rewrite. Are there situations where
either one can be applied?
(* FILL IN HERE *)
*)
apply and rewrite. Are there situations where
either one can be applied?
(* FILL IN HERE *)
*)
(* Give an alternate proof of the associativity of ++ with
a more general induction hypothesis. Complete the
following (leaving the first line unchanged). *)
Theorem ass_app' : forall l1 l2 l3 : natlist,
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
intros l1. induction l1 as [ | n l1'].
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* Additional Exercises *)
a more general induction hypothesis. Complete the
following (leaving the first line unchanged). *)
Theorem ass_app' : forall l1 l2 l3 : natlist,
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
intros l1. induction l1 as [ | n l1'].
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* Additional Exercises *)
(* Briefly explain the difference between the tactics
destruct and induction.
(* FILL IN HERE *)
*)
End NatList.
(* Put beq_nat_sym into the top-level namespace, so that we can
use it later even if we're not importing the Lists
module. *)
Definition beq_nat_sym := NatList.beq_nat_sym.
destruct and induction.
(* FILL IN HERE *)
*)
End NatList.
(* Put beq_nat_sym into the top-level namespace, so that we can
use it later even if we're not importing the Lists
module. *)
Definition beq_nat_sym := NatList.beq_nat_sym.