(* You are allowed to bring in verbatim some theorems and/or declarations from the book *)
(* Question 1 *)
Theorem identity_fn_applied_thrice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f (f b)) = b.
Proof.
Admitted.
(* Question 2 *)
Theorem andb_eq_orb :
forall (b c : bool),
(andb b c) = true -> (orb b c) = true.
Proof.
Admitted.
(* Question 3 *)
(** 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
in the set called [nat], and if [n] is in the set 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) Write some unit tests for your increment and binary-to-unary
functions. Notice that incrementing a binary number and
then converting it to unary should yield the same result as first
converting it to unary and then incrementing.
*)
Question 4.
(** Use [assert] to help prove this theorem. You shouldn't need to
use induction. You might find [plus_assoc] comes in handy.*)
Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Proof.
Admitted.
Question 5.
(** (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_comm : forall m n : nat,
m * n = n * m.
Proof.
Admitted.
Question 6.
Theorem app_nil_end : forall l : natlist,
l ++ [] = l.
Proof.
Admitted.
Question 7.
Theorem snoc_append : forall (l:natlist) (n:nat),
snoc l n = l ++ [n].
Proof.
Admitted.
Question 8.
(** You may find that [app_nil_end] and [snoc_append] comes in handy. *)
Theorem distr_rev : forall l1 l2 : natlist,
rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
Admitted.
Question 9.
(** A palindrome is a sequence that reads the same backwards as
forwards.
- Define an inductive proposition [pal] on natlist that
captures what it means to be a palindrome. (Hint: You'll need
three cases. Your definition should be based on the structure
of the list; just having a single constructor
c : forall l, l = rev l -> pal l
may seem obvious, but will not work very well.)
- Prove that
forall l, pal (l ++ rev l).
- Prove that
forall l, pal l -> l = rev l.
*)
Question 10.
(** State and Prove an interesting theorem of your choice.
Credit will be given based on the interesting nature of
the problem and the proof. *)