Homework Assignment 2 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Submit your solution file for this assignment as an attachment
by email with
the subject "ICTP HW2" by the start of class on September 14.
You should write your solutions entirely on your own.
Template source file 
Require
Import
Arith Omega.
Some useful modules for dealing with arithmetic 
Here's a list of tactics that should be sufficient to solve the problems in
this assignment. You're free to use any tactics except in sections that give
explicit restrictions, though. In particular, all of that stuff you did
manually in HW1 should be left to automation now, through liberal use of
tactics like intuition (described below). Whenever a goal has some
nontrivial propositional structure, starting off with intuition (possibly
following a named intros , though intuition subsumes intros without
arguments) is a sound idea.
More detailed information on tactics can be found in the manual's tactic index. Basic goal manipulation:
Equality:
Simplification:
Working with inductive types:
Automation:
For some of the theorems in this assignment, it will be very useful to use some of the ways of combining tactics.
Finally, don't forget these other general theorem proving tools:

Booleans 
Some boolean functions 
Fill in some definitions for the following functions over bool s.
We saw the definition of this standard type in lecture.
I hope that the names of the functions convey their intended semantics.

Definition
bool_not : bool > bool.
Admitted.
Definition
bool_xor : bool > bool > bool.
Admitted.
Definition
bool_and : bool > bool > bool.
Admitted.
Definition
bool_or : bool > bool > bool.
Admitted.
Definition
bool_eq : bool > bool > bool.
Admitted.
Correctness properties 
Prove these "obvious" theorems about your definitions. 
Theorem
xor_not_eq : forall b1 b2,
bool_xor b1 b2 = bool_not (bool_eq b1 b2).
Admitted.
Theorem
not_and_or_not : forall b1 b2,
bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2).
Admitted.
Lists 
Here's our old friend the list of natural numbers. 
Inductive
list : Set :=
 nil : list
 cons : nat > list > list.
And here's the list append function from HW0. 
Fixpoint
append (ls1 ls2 : list) {struct ls1} : list :=
match ls1 with
 nil => ls2
 cons h t => cons h (append t ls2)
end.
This is the most straightforward definition of list reverse. 
Fixpoint
reverse (ls : list) : list :=
match ls with
 nil => nil
 cons h t => append (reverse t) (cons h nil)
end.
Unfortunately, it has quadratic running time, so we'd like something better. The next two definitions provide a lineartime implementation. 
Fixpoint
reverse'_helper (ls acc : list) {struct ls} : list :=
match ls with
 nil => acc
 cons h t => reverse'_helper t (cons h acc)
end.
Definition
reverse' (ls : list) : list := reverse'_helper ls nil.
Here's a copy of the append associativity proof from HW0.
You'll probably want to use it somewhere....

Theorem
append_associative : forall ls1 ls2 ls3,
append (append ls1 ls2) ls3 = append ls1 (append ls2 ls3).
induction ls1; simpl; intuition.
rewrite IHls1; trivial.
Qed
.
Equivalence of the two

Prove this theorem, showing that the faster reverse' produces identical
outputs to the more clearly correct reverse .

Theorem
reverse'_correct : forall ls, reverse' ls = reverse ls.
Admitted.
Trees 
Here's the definition of binary trees of natural numbers from lecture. 
Inductive
tree : Set :=
 Leaf : tree
 Node : tree > nat > tree > tree.
Sanity checks on properties of constructors 
For the next two theorems, to make things interesting, you can only use
these tactics:
And you might find it helpful to create a or two.

Theorem
Leaf_neq_Node : forall t1 n t2, Leaf <> Node t1 n t2.
Admitted.
Theorem
Node_inj : forall t11 n1 t12 t21 n2 t22,
Node t11 n1 t12 = Node t21 n2 t22
> t11 = t21.
Admitted.
Inserting nodes and preserving ordering 
Here's a standard function for insertion into a binary tree.
There are two new things here.
First, we have a use of the le_lt_dec function from the Arith library.
For the purposes of this assignment, you can treat it as a fancy version of
a standard <= operator.
Second, we have an if expression. The if below is just syntactic sugar
for:

match le_lt_dec n n' with
 true => Node (insert n tle) n' tgt
 false => Node tle n' (insert n tgt)
end
(Actually, le_lt_dec returns a fancier type than bool , but that doesn't
matter here.)
The right way to simplify an if is to perform a case analysis (i.e., the
destruct tactic) on its test expression.

Fixpoint
insert (n : nat) (t : tree) {struct t} : tree :=
match t with
 Leaf => Node Leaf n Leaf
 Node tle n' tgt =>
if le_lt_dec n n'
then Node (insert n tle) n' tgt
else Node tle n' (insert n tgt)
end.
Here's a function to count the number of internal nodes in a tree. 
Fixpoint
size (t : tree) : nat :=
match t with
 Leaf => 0
 Node tle _ tgt => S (size tle + size tgt)
end.
Insertion increases size 
Prove this theorem: 
Theorem
insert_increases : forall (n : nat) (t : tree),
size (insert n t) = S (size t).
Admitted.
Insertion preserves ordering 
We define what it means for a tree to be a binary search tree where
all values fall into a particular range of natural numbers.
Here option nat is a type that we haven't seen before.
It's the type of optional natural numbers.
A value of that type is either None or Some n for some natural number n .
Options are inductive types that can be used via pattern matching like usual.
The other thing that might be surprising here is that we are defining a recursive function that returns logical propositions, written as Prop .
Besides the initial novelty of the idea, there's nothing different here from
writing recursive functions that return normal types.

Fixpoint
ordered' (min : nat) (max : option nat) (t : tree) {struct t} : Prop :=
match t with
 Leaf => True
 Node t1 n t2 =>
min <= n
/\ match max with
 None => True
 Some max => n <= max
end
/\ ordered' min (Some n) t1
/\ ordered' (S n) max t2
end.
We use ordered' to define what it means for a tree to be a BST in
general.

Definition
ordered (t : tree) : Prop :=
ordered' O None t.
Prove this theorem: 
Theorem
insert_ordered : forall (n : nat) (t : tree),
ordered t > ordered (insert n t).
Admitted.
Expression evaluation 
In this section, we'll define a tiny "programming language" of arithmetic expressions, write some "compiler optimizations" for it, and prove that our optimizations are sound. 
We represent variables as natural numbers. Any infinite Set would do.

Definition
var := nat.
Expressions are built from constants, variables, addition, and multiplication. 
Inductive
exp : Set :=
 Const : nat > exp
 Var : var > exp
 Plus : exp > exp > exp
 Times : exp > exp > exp.
Here's the meaning of expressions. The inputs to the fucnction are the expression to evaluate and an environment giving values to the variables. The environment is just a function from variables to natural numbers. 
Fixpoint
eval (e : exp) (ctx : var > nat) {struct e} : nat :=
match e with
 Const n => n
 Var x => ctx x
 Plus e1 e2 => eval e1 ctx + eval e2 ctx
 Times e1 e2 => eval e1 ctx * eval e2 ctx
end.
Constant folding 
Expressions may contain some pieces without variables that can be evaluated "once and for all." This is called "constant folding" in the world of compilers. 
This function implements a check to see if an expression has any opportunities for constant folding. It returns a proposition equivalent to the statement that the input expression has no more places to simplify by constant folding. 
Fixpoint
constant_folded (e : exp) : Prop :=
match e with
 Const _ => True
 Var _ => True
 Plus (Const _) (Const _) => False
 Plus e1 e2 => constant_folded e1 /\ constant_folded e2
 Times (Const _) (Const _) => False
 Times e1 e2 => constant_folded e1 /\ constant_folded e2
end.
Define a function that performs all possible constant foldings in an expression. 
Definition
constant_fold : exp > exp.
Admitted.
Prove that your function doesn't miss any opportunities to simplify. 
On this and the rest of the problems on this assignment, you'll probably
find it very helpful to use the t1; t2 and try t tactic notations
mentioned at the start of this document. Otherwise, you'll be doing a lot of
typing, since you'll probably end up with many very similar cases to consider.
A general pattern is t1; try t2; try t3; t4 , when you want to run a tactic
t1 that will generate a set of subgoals where each is solvable by at least
one of t2 , t3 , and t4 .
At the same time, it's often helpful to start proving the goal without using the semicolon notation in some places, so that you can see interactively what form the subgoals take. After you figure out the pattern and a general way of solving them with tactics, you can convert your mess of tactics into a nice single line with semicolons. 
Theorem
constant_fold_simplifies : forall (e : exp),
constant_folded (constant_fold e).
Admitted.
Prove that your function is meaningpreserving. 
Theorem
constant_fold_sound : forall (ctx : var > nat) (e : exp),
eval (constant_fold e) ctx = eval e ctx.
Admitted.
Arithmetic identities 
This section is optional. 
We would also like to simplify any additions of 0 and multiplications by 1. This function formalizes what it means for an expression not to contain any such pieces: 
Fixpoint
no_identities (e : exp) : Prop :=
match e with
 Const _ => True
 Var _ => True
 Plus (Const 0) _ => False
 Plus _ (Const 0) => False
 Plus e1 e2 => no_identities e1 /\ no_identities e2
 Times (Const 1) _ => False
 Times _ (Const 1) => False
 Times e1 e2 => no_identities e1 /\ no_identities e2
end.
Define a function for applying the identity simplification rules. 
Definition
simplify_identities : exp > exp.
Admitted.
Prove that your function doesn't miss any opportunities. 
Theorem
simplify_identities_simplifies : forall (e : exp),
no_identities (simplify_identities e).
Admitted.
Prove that your function is meaningpreserving. 
Theorem
simplify_identities_sound : forall (ctx : var > nat) (e : exp),
eval (simplify_identities e) ctx = eval e ctx.
Admitted.
OK, you're done if there are no more occurrences of "Admitted " in your
solution file and you haven't changed the specifications!
