(* Lists and higher-order functions
Version of 1/21/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.
(* ----------------------------------------------------------------------- *)
(* Administrivia *)
(* Is everyone on the course mailing list? *)
(* Remember: This homework due Monday, not Wednesday *)
(* ----------------------------------------------------------------------- *)
(* Formal vs. informal proof *)
(* An unreadable formal proof *)
Theorem plus_assoc' : forall n m p : nat,
plus n (plus m p) = plus (plus n m) p.
Proof. intros n m p. induction n as [| n']. reflexivity.
simpl. rewrite -> IHn'. reflexivity. Qed.
(* A careful informal proof of the same theorem:
By induction on n.
- First, suppose n = 0. We must show
plus 0 (plus m p) = plus (plus 0 m) p.
This follows directly from the definition of plus.
- Next, suppose n = S n', with
plus n' (plus m p) = plus (plus n' m) p.
We must show
plus (S n') (plus m p) = plus (plus (S n') m) p.
By the definition of plus, this follows from
S (plus n' (plus m p)) = S (plus (plus n' m) p),
which is immediate from the induction hypothesis.
*)
(* As an exercise, try translating this solution from last week into
an informal proof: *)
Theorem plus_comm' : forall n m : nat,
plus n m = plus m n.
Proof.
intros n m. induction m as [| m'].
Case "m = 0".
simpl. rewrite -> plus_n_O. reflexivity.
Case "m = S m'".
simpl. rewrite <- IHm'. rewrite <- plus_n_Sm.
reflexivity.
Qed.
(* Informal proof:
Theorem: plus is commutative.
Proof:
(* EXERCISE... *)
Let natural numbers n and m be given. We show plus n m = plus m n
by induction on m.
- First, suppose m = 0. By the definition of plus, plus 0 n = 0.
More, we have already shown (lemma plus_n_0) that plus n 0 = 0.
Thus, plus n 0 = plus 0 n.
- Next, suppose m = S m' for some m' such that plus n m' = plus m' n.
By the definition of plus and the inductive hypothesis,
plus (S m') n = S (plus m' n) = S (plus n m'). It
remains to show plus n (S m') = S (plus n m') as well, but
this is precisely lemma plus_n_Sm.
(* ...TO HERE *)
*)
(* Exercise: write a formal proof of the following theorem, using
the provided informal proof as a guide
Theorem : For any n, true = beq_nat n n
Proof :
By induction on n.
- First, suppose n = 0. We must show
true = beq_nat n n.
This follows directly from the definitions of beq_nat.
- Next, suppose n = S n', with
true = beq_nat n' n'.
We must show
true = beq_nat (S n') (S n')
This follows directly from the IH and with the
definition beq_nat.
*)
Theorem beq_nat_refl : forall n : nat,
true = beq_nat n n.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* -------------------------------------------------------------- *)
(* 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.
Theorem fst_swap_is_snd : forall (p : natprod),
fst (swap_pair p) = snd p.
Proof.
(* OPTIONAL EXERCISE *) Admitted.
(* -------------------------------------------------------------- *)
(* Lists of numbers *)
Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.
Definition l123 := 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 l123' := 1 :: (2 :: (3 :: nil)).
Definition l123'' := 1 :: 2 :: 3 :: nil.
Definition l123''' := [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 (OPTIONALLY)
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 (OPTIONALLY)
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 (OPTIONALLY)
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 (OPTIONALLY)
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 (OPTIONALLY)
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 (OPTIONALLY)
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 (OPTIONALLY)
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.
(* OPTIONAL EXERCISE *) Admitted.
(* Exercises *)
(** <<
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.
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.
(* ------------------------------------------------------- *)
(* A couple more exercises *)
(* Design exercise:
- Write down a non-trivial theorem involving cons (::),
snoc, and append (++).
- Prove it.
FILL IN HERE
*)
(* 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.
>> *)
(* If you did the optional exercise about bags above, here
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.
(* OPTIONAL EXERCISE *) 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.
(* OPTIONAL EXERCISE *) 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 *)
(** <<
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.
(* 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.
>> *)
(* Another functional programming exercise *)
(** <<
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.
(* Exercise: 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.
(* 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.
(* As an exercise, also 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:
(* EXERCISE... *)
Let an arbitrary nat n be given. We go by induction on
n.
For the base case, we have n = 0. Let m and b be given
and assume beq_nat 0 m = b. Either m = 0 or not. In
the first case, we must show beq_nat 0 0 = b which is
exactly the assumption. In the second case, m = S m'
for some m'. By our assumption, it's enough to show
beq_nat (S m') 0 = beq_nat 0 (S m'), and by the
definition of beq_nat both are false.
In the inductive case, we have n = S n' for some n'.
Let m and b be given and assume beq_nat (S n') m = b.
Our IH is that, for any m and b, beq_nat n' m = b ->
beq_nat m n = b. We go by cases on m.
Suppose first m = 0. By the assumption, it's enough to
show beq_nat 0 (S n') = beq_nat (S n') 0. By the
definition of beq_nat, both sides are false.
Otherwise, m = S m' for some m'. By the assumption,
it's enough to show:
beq_nat (S m') (S n') = beq_nat (S n') (S m')
And, by the definition of beq_nat, this reduces to
showing:
beq_nat m' n' = beq_nat n' m'.
Picking m = m' and b = beq_nat n' m' in the
inductive hypothesis gives:
beq_nat n' m' = beq_nat n' m ->
beq_nat m' n' = beq_nat n' m'.
The premise is trivial, and the conclusion is exactly
what we wanted to show.
(* ...TO 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.
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.