Coq theorem prover: Lesson 1, HW 1
No content. Curious to see how the code will be highlighted.
(* Basic programming and reasoning about programs in Coq
Version of 1/14/2009
*)
(* HOMEWORK INSTRUCTIONS:
Submit homeworks using Blackboard:
<https://courseweb.library.upenn.edu/>
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 :=
match b1 with
| true => negb b2
| false => true
end.
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 :=
match b1 with
|true => andb b2 b3
|false => false
end.
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 :=
match n with
| O => S O
| S p => mult n (factorial p)
end.
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 :=
match n with
| O => true
| S n' => match m with
| O => false
| S m' => ble_nat n' m'
end
end.
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) := andb (ble_nat n m) (negb (beq_nat n m)).
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.
intros.
rewrite H.
rewrite H0.
reflexivity.
Qed.
(* 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.
simpl.
reflexivity.
Qed.
(* ----------------------------------------------------- *)
(* 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.
intros. destruct n.
simpl. reflexivity.
simpl. reflexivity.
Qed.
(* ------------------------------------------------------- *)
(* 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 s
