(* Basic programming and reasoning about programs in Coq
Version of 1/14/2009
*)
(* HOMEWORK INSTRUCTIONS:
Submit homeworks using Blackboard:
Solution files that Coq rejects will NOT be graded.
You should be able to run CoqIDE/ProofGeneral to the
end of the file, or run coqc without any errors. If you
can't solve one of the problems, leave an [Admitted] in
the file.
If you have any questions about the homework, please
e-mail the TAs.
Have fun!
*)
(* ------------------------------------------------------- *)
(* Days of the week *)
Inductive day : Set :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Eval simpl in (next_weekday friday).
Eval simpl in (next_weekday (next_weekday saturday)).
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
(* -------------------------------------------------------------- *)
(* Booleans *)
Inductive bool : Set :=
| true : bool
| false : bool.
Definition negb (b:bool) := if b then false else true.
Definition ifb (b1 b2 b3:bool) : bool :=
match b1 with
| true => b2
| false => b3
end.
Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
Definition orb (b1 b2:bool) : bool := ifb b1 true b2.
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true ) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true ) = true.
Proof. simpl. reflexivity. Qed.
(* Exercise: Uncomment and then complete the definitions
of the following functions, making sure that the
assertions below each can be verified by Coq. *)
(** <<
(* This function should return [true] if either or both of
its inputs are [false]. *)
Definition norb (b1:bool) (b2:bool) : bool :=
FILL IN HERE
Example test_norb1: (norb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_norb2: (norb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_norb3: (norb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_norb4: (norb true true) = false.
Proof. simpl. reflexivity. Qed.
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
FILL IN HERE
Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.
>> *)
(* ----------------------------------------------------- *)
(* Numbers *)
(* Technical note: Coq provides a fairly fancy module
system, to aid in organizing large and complex
developments. In this course, we won't need most of
its features, but one is useful: if we enclose a
collection of declarations between [Module X] and [End
X] markers, then, in the remainder of the file after
the [End], all these definitions will be referred to by
names like [X.foo] instead of just [foo]. This means
that the new definition will not clash with the
unqualified name [foo] later, which would otherwise be
an error (a name can only be defined once in a given
scope).
Here, we use this feature to introduce the definition
of [nat] in an inner module so that it does not shadow
the one from the standard library, which provides a
little bit of magic for writing numbers using standard
arabic numerals. *)
Module Nat.
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
End Nat.
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Check (S (S (S (S O)))).
Eval simpl in (minustwo 4).
Check pred.
Check minustwo.
Check S.
Fixpoint evenb (n:nat) {struct n} : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Definition oddb (n:nat) : bool := negb (evenb n).
Example test_oddb1: (oddb (S O)) = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: (oddb (S (S (S (S O))))) = false.
Proof. simpl. reflexivity. Qed.
Fixpoint plus (n : nat) (m : nat) {struct n} : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Eval simpl in (plus (S (S (S O))) (S (S O))).
Fixpoint mult (n m : nat) {struct n} : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Fixpoint minus (n m : nat) {struct m} : nat :=
match m with
| O => n
| S m' => minus (pred n) m'
end.
Fixpoint exp (base power : nat) {struct power} : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.
(** Exercise *)
(** <<
Fixpoint factorial (n:nat) {struct n} : nat :=
FILL IN HERE
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.
>> *)
Fixpoint beq_nat (n m : nat) {struct n} : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
(* Exercise *)
(** <<
Fixpoint ble_nat (n m : nat) {struct n} : bool :=
FILL IN HERE
Example test_ble_nat1: (ble_nat 2 2) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat2: (ble_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat3: (ble_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.
Definition blt_nat (n m : nat) :=
FILL IN HERE
Example test_blt_nat1: (blt_nat 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat2: (blt_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat3: (blt_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.
>> *)
(* -------------------------------------------------- *)
(* Reasoning by "partial evaluation" *)
Theorem plus_0_l : forall n:nat, plus 0 n = n.
Proof.
simpl. reflexivity.
Qed.
(* The [reflexivity] tactic implicitly simplifies both
sides of the equality before testing to see if they are
the same... *)
Theorem plus_0_l' : forall n:nat, plus 0 n = n.
Proof.
reflexivity.
Qed.
Theorem plus_1_l : forall n:nat, plus 1 n = S n.
Proof.
intros n. reflexivity.
Qed.
Theorem mult_0_l : forall n:nat, mult 0 n = 0.
Proof.
intros n. reflexivity.
Qed.
(* ------------------------------------------------------- *)
(* The [intros] tactic *)
(* Another proof of plus_0_l, using [intros] *)
Theorem plus_0_l'' : forall n:nat, plus 0 n = n.
Proof.
intros n. reflexivity.
Qed.
(* ------------------------------------------------------- *)
(* The [rewrite] tactic *)
(* A more interesting proof involving [rewrite]. *)
Theorem plus_id_example : forall n m:nat,
n = m -> plus n n = plus m m.
Proof.
intros n m. (* move both quantifiers into the context *)
intros H. (* move the hypothesis into the context *)
rewrite -> H. (* Rewrite the goal using the hypothesis *)
reflexivity.
Qed.
(* One for you: *)
Theorem plus_id_exercise : forall n m o : nat,
n = m -> m = o -> plus n m = plus m o.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Using [rewrite] with a previously proved lemma... *)
Theorem mult_0_plus : forall n m : nat,
mult (plus 0 n) m = mult n m.
Proof.
intros n m.
rewrite -> plus_0_l.
reflexivity.
Qed.
Theorem mult_1_plus : forall n m : nat,
mult (plus 1 n) m = plus m (mult n m).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ----------------------------------------------------- *)
(* Case analysis *)
(* Sometimes simplification and rewriting are not
enough... *)
Theorem plus_1_neq_0_firsttry : forall n,
beq_nat (plus n 1) 0 = false.
Proof.
intros n. simpl. (* does nothing! *)
Admitted.
(* Using [destruct] to perform case analysis *)
Theorem plus_1_neq_0 : forall n,
beq_nat (plus n 1) 0 = false.
Proof.
intros n. destruct n as [| n'].
reflexivity.
reflexivity.
Qed.
(* Another example (using booleans) *)
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
reflexivity.
reflexivity.
Qed.
(* One for you *)
Theorem zero_nbeq_plus_1 : forall n,
beq_nat 0 (plus n 1) = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* The [Case] annotation *)
(* One of the less nice things about Coq's mechanisms for
interactive proof is the way subgoals seem to come and
go almost at random, with no explicit indication of
where we are -- which case of an induction or case
analysis we are in -- at any given moment. In very
short proofs, this is not a big deal. But in more
complex proofs it can become quite difficult to stay
oriented.
Here is a simple hack that helps things quite a bit.
It uses some facilities of Coq that we have not
discussed -- the string library (just for the concrete
syntax of quoted strings) and the [Ltac] command, which
allows us to declare custom tactics. We will come back
to [Ltac] in more detail later. For now, don't worry
about the details of this declaration. *)
Require String. Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case." ].
Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.
Ltac SSCase name := Case_aux SSCase name.
Ltac SSSCase name := Case_aux SSSCase name.
Ltac SSSSCase name := Case_aux SSSSCase name.
Ltac SSSSSCase name := Case_aux SSSSSCase name.
Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
(* Step through the following proof and observe how the
context changes. *)
Theorem andb_true_l : forall b c,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity.
Qed.
(* Exercise: prove andb_true_r, marking cases (and
subcases) when you use [destruct]. *)
Theorem andb_true_r : forall b c,
andb b c = true -> c = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ---------------------------------------------------- *)
(* Induction on numbers *)
(* The fact that 0 is also a neutral element for plus on
the RIGHT cannot be proved with just
simplification... *)
Theorem plus_0_r_firsttry : forall n:nat,
plus n 0 = n.
Proof.
intros n.
simpl. (* Does nothing! *)
Admitted.
(* Case analysis gets us a little further, but not all the
way. *)
Theorem plus_0_r_secondtry : forall n:nat,
plus n 0 = n.
Proof.
intros n. destruct n as [| n'].
Case "n = 0".
reflexivity. (* so far so good... *)
Case "n = S n'".
simpl. (* ...but here we are stuck again *)
Admitted.
(* We need a bigger hammer... *)
(* The PRINCIPLE OF INDUCTION over natural numbers:
If [P(n)] is some proposition involving a natural
number n, and we want to show that P holds for ALL
numbers n, we can reason like this:
- show that [P(O)] holds
- show that, if [P(n)] holds, then so does [P(S n)]
- conclude that [P(n)] holds for all n.
In Coq, the style of reasoning is "backwards": we begin
with the goal of proving [P(n)] for all n and break it
down (by applying the [induction] tactic) into two
separate subgoals: first showing P(O) and then showing
[P(n) -> P(S n)]. *)
(* For example... *)
Theorem plus_0_r : forall n:nat, plus n 0 = n.
Proof.
intros n. induction n as [| n'].
Case "n = 0". reflexivity.
Case "n = S n'". simpl. rewrite -> IHn'. reflexivity.
Qed.
(* An exercise to be worked together: *)
Theorem minus_n_n : forall n,
minus n n = 0.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* And some for you... *)
Theorem mult_0_r : forall n:nat,
mult n 0 = 0.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem plus_assoc : forall n m p : nat,
plus n (plus m p) = plus (plus n m) p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem plus_n_Sm : forall n m : nat,
S (plus n m) = plus n (S m).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem plus_comm : forall n m : nat,
plus n m = plus m n.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ----------------------------------------------------------------------- *)
(* The [assert] tactic *)
(* An alternate proof of [mult_0_plus], using an
in-line assertion instead of a separate lemma. *)
Theorem mult_0_plus' : forall n m : nat,
mult (plus 0 n) m = mult n m.
Proof.
intros n m.
assert (plus 0 n = n).
Case "Proof of assertion". reflexivity.
rewrite -> H.
reflexivity.
Qed.
Theorem plus_rearrange_firsttry : forall n m p q : nat,
plus (plus n m) (plus p q) = plus (plus m n) (plus p q).
Proof.
intros n m p q.
(* We just need to swap (plus n m) for (plus m n)...
it seems like plus_comm should do the trick! *)
rewrite -> plus_comm.
(* Doesn't work...Coq rewrote the wrong plus! *)
Admitted.
Theorem plus_rearrange : forall n m p q : nat,
plus (plus n m) (plus p q) = plus (plus m n) (plus p q).
Proof.
intros n m p q.
assert (plus n m = plus m n).
Case "Proof of assertion".
rewrite -> plus_comm. reflexivity.
rewrite -> H. reflexivity.
Qed.
(* Use assert to help prove this theorem. *)
Theorem plus_swap : forall n m p : nat,
plus n (plus m p) = plus m (plus n p).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Exercise: prove commutativity of multiplication. (You
will probably need to define and prove a subsidiary
theorem to be used in the proof of this one. Either
give it a separate name or else use an in-line
[assert].) You may find that [plus_swap] comes in handy. *)
Theorem mult_comm : forall m n : nat,
mult m n = mult n m.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem evenb_n__oddb_Sn : forall n,
evenb n = negb (evenb (S n)).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* ------------------------------------------------------- *)
(* More exercises *)
(* In this set of exercises, you should think about which
theorems need induction, which need [destruct], and
which can be proved using just the [simpl] and
[reflexivity] tactics and existing lemmas? Make your
prediction before attempting the proof in Coq. *)
Theorem ble_nat_refl : forall n,
true = ble_nat n n.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem zero_nbeq_S : forall n:nat,
beq_nat 0 (S n) = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem andb_false_r : forall b : bool,
andb b false = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem plus_ble_compat_l : forall n m p,
ble_nat n m = true -> ble_nat (plus p n) (plus p m) = true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem S_nbeq_0 : forall n:nat,
beq_nat (S n) 0 = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem mult_1_l : forall n:nat, mult 1 n = n.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem all3_spec : forall b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem mult_plus_distr_r : forall n m p : nat,
mult (plus n m) p = plus (mult n p) (mult m p).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
Theorem mult_assoc : forall n m p : nat,
mult n (mult m p) = mult (mult n m) p.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* -------------------------------------------------- *)
(* A few more miscellaneous facts that we'll need later on
in the course... *)
Theorem orb_true_r : forall b,
orb b true = true.
Proof.
intros b.
destruct b.
reflexivity.
reflexivity.
Qed.
Theorem negb_flip : forall b1 b2,
negb b1 = b2 ->
b1 = negb b2.
Proof.
intros b1 b2. intros H.
rewrite <- H.
rewrite -> negb_involutive.
reflexivity.
Qed.
Theorem plus_1_r : forall n:nat,
plus n 1 = S n.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity.
Qed.
Theorem mult_1_r : forall n:nat,
mult n 1 = n.
Proof.
intros n. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite -> IHn'. reflexivity.
Qed.