Definition admit {T: Type} : T. Admitted.
(** **** Exercise: 1 star (nandb) *)
(** Complete the definition of the following function, then make
sure that the [Example] 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 :=
match b1, b2 with
| false, _ => true
| _, false => true
| _, _ => false
end.
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.
(** **** Exercise: 1 star (andb3) *)
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool := andb b1 (andb b2 b3).
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.
(** **** Exercise: 1 star (factorial) *)
(** Recall the standard factorial function:
<<
factorial(0) = 1
factorial(n) = n * factorial(n-1) (if n>0)
>>
Translate this into Coq. *)
Fixpoint factorial (n:nat) : nat :=
match n with
| 0 => 1
| S n' => (S n') * factorial n'
end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.
(** **** Exercise: 2 stars (blt_nat) *)
(** The [blt_nat] function tests [nat]ural numbers for [l]ess-[t]han,
yielding a [b]oolean.
Note: If you have trouble with the [simpl] tactic, try using
[compute], which is like [simpl] on steroids. However, there is a
simple, elegant solution for which [simpl] suffices.
*)
Fixpoint ble_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition blt_nat (n m : nat) : bool := negb (ble_nat m n).
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.
(** **** Exercise: 1 star, optional (simpl_plus) *)
(** What will Coq print in response to this query? *)
(* Eval simpl in (forall n:nat, n + 0 = n). *)
(* R: exactly the original proposition, i.e, ∀n:nat, n + 0 = n. *)
(** What about this one? *)
(* Eval simpl in (forall n:nat, 0 + n = n). *)
(* R: ∀n:nat, n = n. *)
(** Explain the difference. [] *)
(* R: In the first case, Coq was NOT able to perform the simplification
* (beta reduction), because the function plus is defined using pattern
* matching on the FIRST argument. *)
(** **** Exercise: 1 star (plus_id_exercise) *)
(** Remove "[Admitted.]" and fill in the proof. *)
Theorem plus_id_exercise :
forall n m o : nat, n = m -> m = o -> n + m = m + o.
Proof.
intros n m o.
intros NM.
intros MO.
rewrite -> NM.
rewrite <- MO.
reflexivity.
Qed.
(** **** Exercise: 2 stars, recommended (mult_1_plus) *)
Theorem mult_1_plus:
forall n m : nat, (1 + n) * m = m + (n * m).
Proof.
intros.
simpl.
reflexivity.
Qed.
(** [] *)
(** **** Exercise: 1 star (zero_nbeq_plus_1) *)
Fixpoint beq_nat (n m : nat) : 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.
Theorem zero_nbeq_plus_1:
forall n : nat, beq_nat 0 (n + 1) = false.
Proof.
destruct n; reflexivity.
Qed.
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" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
(** **** Exercise: 2 stars (andb_true_elim2) *)
(** Prove [andb_true_elim2], marking cases (and subcases) when
you use [destruct]. *)
Theorem andb_true_elim2 :
forall b c : bool, andb b c = true -> c = true.
Proof.
intros b c.
destruct b.
Case "b = true".
tauto.
Case "b = false".
destruct c; tauto.
Qed.
(** **** Exercise: 2 stars, recommended (basic_induction) *)
Theorem mult_0_r :
forall n:nat, n * 0 = 0.
Proof.
intros n.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite -> IHn.
reflexivity.
Qed.
Theorem plus_n_Sm :
forall n m : nat, S (n + m) = n + (S m).
Proof.
intros n m.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite IHn.
reflexivity.
Qed.
Theorem plus_0_ident:
forall n:nat, n + 0 = n.
Proof.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite -> IHn.
reflexivity.
Qed.
Theorem plus_comm :
forall n m : nat, n + m = m + n.
Proof.
intros n m.
induction m.
Case "base m".
simpl.
rewrite -> plus_0_ident.
reflexivity.
Case "inductive m".
simpl.
rewrite <- plus_n_Sm.
rewrite -> IHm.
reflexivity.
Qed.
(** **** Exercise: 2 stars (double_plus) *)
Fixpoint double (n:nat) :=
match n with
| O => O
| S n' => S (S (double n'))
end.
Lemma double_plus :
forall n, double n = n + n .
Proof.
intros n.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite -> IHn.
rewrite plus_n_Sm.
reflexivity.
Qed.
(** [] *)
(** **** Exercise: 1 star, optional (beq_nat_refl) *)
Theorem beq_nat_refl :
forall n : nat, true = beq_nat n n.
Proof.
intros n.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite <- IHn.
reflexivity.
Qed.
(** **** Exercise: 4 stars, recommended (mult_comm) *)
(** Use [assert] to help prove this theorem. You shouldn't need to
use induction. *)
Theorem plus_assoc :
forall n m p : nat, n + (m + p) = (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.
Theorem plus_swap :
forall n m p : nat, n + (m + p) = m + (n + p).
Proof.
intros.
rewrite plus_assoc, plus_assoc.
assert (n + m = m + n) as MN_comm.
Case "Proof assertion m n".
rewrite plus_comm.
reflexivity.
rewrite MN_comm.
reflexivity.
Qed.
(** Now prove commutativity of multiplication. (You will probably
need to define and prove a separate subsidiary theorem to be used
in the proof of this one.) You may find that [plus_swap] comes in
handy. *)
Theorem mult_zero_r :
forall m : nat, m * 0 = 0.
Proof.
intros m.
induction m; [ reflexivity | simpl; rewrite IHm; reflexivity ].
Qed.
Theorem mult_comm :
forall m n : nat, m * n = n * m.
Proof.
induction m.
Case "base m".
intros n.
simpl; rewrite mult_zero_r; reflexivity.
Case "inductive m".
intros n.
simpl.
rewrite IHm.
induction n.
SCase "base n".
reflexivity.
SCase "inductive n".
simpl.
rewrite <- IHn, plus_swap.
reflexivity.
Qed.
(** **** Exercise: 2 stars, optional (evenb_n__oddb_Sn) *)
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Theorem negb_involutive :
forall b : bool, negb (negb b) = b.
Proof.
intros b.
destruct b; reflexivity.
Qed.
Theorem evenb_n__oddb_Sn :
forall n : nat, evenb n = negb (evenb (S n)).
Proof.
induction n.
Case "base n".
reflexivity.
Case "inductive n".
simpl.
rewrite IHn.
destruct n.
SCase "n = 0".
reflexivity.
SCase "n != 0".
rewrite negb_involutive; reflexivity.
Qed.
(** **** Exercise: 2 stars, optional (plus_swap') *)
(** The [replace] tactic allows you to specify a particular subterm to
rewrite and what you want it rewritten to. More precisely,
[replace (t) with (u)] replaces (all copies of) expression [t] in
the goal by expression [u], and generates [t = u] as an additional
subgoal. This is often useful when a plain [rewrite] acts on the wrong
part of the goal.
Use the [replace] tactic to do a proof of [plus_swap'], just like
[plus_swap] but without needing [assert (n + m = m + n)].
*)
Theorem plus_swap':
forall n m p : nat, n + (m + p) = m + (n + p).
Proof.
intros.
rewrite plus_assoc, plus_assoc.
replace (m + n) with (n + m).
- reflexivity.
- rewrite plus_comm; reflexivity.
Qed.
(** **** Exercise: 4 stars, recommended (binary) *)
(** Consider a different, more efficient representation of natural
numbers using a binary rather than unary system. That is, instead
of saying that each natural number is either zero or the successor
of a natural number, we can say that each binary number is either
- zero,
- twice a binary number, or
- one more than twice a binary number.
(a) First, write an inductive definition of the type [bin]
corresponding to this description of binary numbers.
(Hint: recall that the definition of [nat] from class,
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
says nothing about what [O] and [S] "mean". It just says "[O] is
a nat (whatever that is), and if [n] is a nat then so is [S n]".
The interpretation of [O] as zero and [S] as successor/plus one
comes from the way that we use nat values, by writing functions to
do things with them, proving things about them, and so on. Your
definition of [bin] should be correspondingly simple; it is the
functions you will write next that will give it mathematical
meaning.)
(b) Next, write an increment function for binary numbers, and a
function to convert binary numbers to unary numbers.
(c) Finally, prove that your increment and binary-to-unary
functions commute: that is, incrementing a binary number and
then converting it to unary yields the same result as first
converting it to unary and then incrementing.
*)
Inductive bin : Type :=
| Z : bin
| T : bin -> bin
| P : bin -> bin.
Fixpoint incrbin (n : bin) : bin :=
match n with
| Z => P Z
| T h' => P h'
| P hp' => T (incrbin hp')
end.
Fixpoint bin2nat (n : bin) : nat :=
match n with
| Z => O
| T h' => double (bin2nat h')
| P hp' => S (double (bin2nat hp'))
end.
Example nine_bin_nat : (bin2nat (P (T (T (P Z)))) = 9).
Proof. reflexivity. Qed.
Example seven_bin_nat : (bin2nat (P (P (P Z))) = 7).
Proof. reflexivity. Qed.
Example four_bin_nat : (bin2nat (T (T (P Z))) = 4).
Proof. reflexivity. Qed.
Theorem bin2nat_incrbin_comm:
forall n:bin, bin2nat (incrbin n) = S (bin2nat n).
Proof.
induction n.
Case "zero n".
reflexivity.
Case "twice n".
reflexivity.
Case "one past twice n".
simpl.
rewrite IHn.
reflexivity.
Qed.
(** **** Exercise: 5 stars (binary_inverse) *)
(** This exercise is a continuation of the previous exercise about
binary numbers. You will need your definitions and theorems from
the previous exercise to complete this one.
(a) First, write a function to convert natural numbers to binary
numbers. Then prove that starting with any natural number,
converting to binary, then converting back yields the same
natural number you started with.
(b) You might naturally think that we should also prove the
opposite direction: that starting with a binary number,
converting to a natural, and then back to binary yields the
same number we started with. However, it is not true!
Explain what the problem is.
(c) Define a function [normalize] from binary numbers to binary
numbers such that for any binary number b, converting to a
natural and then back to binary yields [(normalize b)]. Prove
it.
*)
Fixpoint nat2bin (n : nat) : bin :=
match n with
| O => Z
| S m => incrbin (nat2bin m)
end.
Example nine_nat_bin : (P (T (T (P Z))) = nat2bin 9).
Proof. reflexivity. Qed.
Example seven_nat_bin : (P (P (P Z)) = nat2bin 7).
Proof. reflexivity. Qed.
Example four_nat_bin : (T (T (P Z)) = nat2bin 4).
Proof. reflexivity. Qed.
(** **** Exercise: 2 stars, optional (decreasing) *)
(** The requirement that some argument to each function be
"decreasing" is a fundamental feature of Coq's design: In
particular, it guarantees that every function that can be defined
in Coq will terminate on all inputs. However, because Coq's
"decreasing analysis" is not very sophisticated, it is sometimes
necessary to write functions in slightly unnatural ways.
To get a concrete sense of this, find a way to write a sensible
[Fixpoint] definition (of a simple function on numbers, say) that
_does_ terminate on all inputs, but that Coq will _not_ accept
because of this restriction. *)
(* FILL IN HERE *)
(** [] *)