Library Basics
(* Basic programming and reasoning about programs in Coq
Version of 4/28/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. Style, readability, and
elegance count.
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) :=
match b with
| true => false
| false => true
end.
Definition ifb (b1 b2 b3:bool) : bool :=
match b1 with
| true => b2
| false => b3
end.
Definition andb (b1:bool) (b2:bool) : bool := ifb b1 b2 false.
Definition orb (b1:bool) (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.
Version of 4/28/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. Style, readability, and
elegance count.
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) :=
match b with
| true => false
| false => true
end.
Definition ifb (b1 b2 b3:bool) : bool :=
match b1 with
| true => b2
| false => b3
end.
Definition andb (b1:bool) (b2:bool) : bool := ifb b1 b2 false.
Definition orb (b1:bool) (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.
(* Uncomment and then complete the definitions of the
following functions, making sure that the assertions
below each can be verified by Coq. *)
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 nandb (b1:bool) (b2:bool) : bool := (* FILL IN HERE *) Example test_nandb1: (nandb true false) = true. Proof. simpl. reflexivity. Qed. Example test_nandb2: (nandb false false) = true. Proof. simpl. reflexivity. Qed. Example test_nandb3: (nandb false true) = true. Proof. simpl. reflexivity. Qed. Example test_nandb4: (nandb true true) = false. Proof. simpl. reflexivity. Qed. (* A NOTE ON NOTATION: We will often use square brackets [...] to delimit fragments of Coq code in comments in .v files; this convention, which is also used by the coqdoc documentation tool, keeps them visually separate from the surrounding text. In the typeset notes, typewriter font is used for the same purpose. *) 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.
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.
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.
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.
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) := (* 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.
(* ------------------------------------------------------- *)
(* 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.
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 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.
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.
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.
Theorem zero_nbeq_plus_1 : forall n,
beq_nat 0 (plus n 1) = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
beq_nat 0 (plus n 1) = false.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.
(* Recall the definition of plus:
Fixpoint plus (m : nat) (n : nat) {struct m} : nat :=
match m with
| O => n
| S m' => S (plus m' n)
end.
What will Coq print in response to this query?
Eval simpl in (forall n, plus n 0 = n).
What will Coq print in response to this query?
Eval simpl in (forall n, plus 0 n = n).
Briefly explain the difference.
*)
(* ------------------------------------------------------- *)
(* 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.
Fixpoint plus (m : nat) (n : nat) {struct m} : nat :=
match m with
| O => n
| S m' => S (plus m' n)
end.
What will Coq print in response to this query?
Eval simpl in (forall n, plus n 0 = n).
What will Coq print in response to this query?
Eval simpl in (forall n, plus 0 n = n).
Briefly explain the difference.
*)
(* ------------------------------------------------------- *)
(* 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.
(* 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.
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'].
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.
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.
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'].
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_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.
(* ----------------------------------------------------------------------- *)
(* 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.
*)
Theorem mult_0_r : forall n:nat,
mult n 0 = 0.
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.
(* ----------------------------------------------------------------------- *)
(* 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 your solution for
plus_comm into an informal proof. *)
(* Informal proof:
Theorem: plus is commutative.
Proof:
(* FILL IN HERE *)
- 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.
*)
(* 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 definition 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 the definition of
beq_nat.
*)
plus_comm into an informal proof. *)
(* Informal proof:
Theorem: plus is commutative.
Proof:
(* FILL IN HERE *)
- 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.
*)
(* 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 definition 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 the definition of
beq_nat.
*)
Theorem beq_nat_refl : forall n : nat,
true = beq_nat n 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.
true = beq_nat n 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.
(* 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 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.
(* 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 *)
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.
Fixpoint factorial (n:nat) {struct n} : nat :=
match n with
| O => 1
| S n' => mult n (factorial n')
end.
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.
Fixpoint factorial (n:nat) {struct n} : nat :=
match n with
| O => 1
| S n' => mult n (factorial n')
end.