Library HW2

 Homework Assignment 2 Interactive Computer Theorem Proving CS294-9, Fall 2006 UC Berkeley

 Submit your solution file for this assignment as an attachment by e-mail 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

Booleans

Some boolean functions

 Fill in some definitions for the following functions over bools. 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.

Definition bool_xor : bool -> bool -> bool.

Definition bool_and : bool -> bool -> bool.

Definition bool_or : bool -> bool -> bool.

Definition bool_eq : bool -> bool -> bool.

Correctness properties

Theorem xor_not_eq : forall b1 b2,
bool_xor b1 b2 = bool_not (bool_eq b1 b2).

Theorem not_and_or_not : forall b1 b2,
bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2).

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 linear-time 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 reverse definitions

 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.

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: change intros reflexivity rewrite trivial And you might find it helpful to create a Definition or two.

Theorem Leaf_neq_Node : forall t1 n t2, Leaf <> Node t1 n t2.

Theorem Node_inj : forall t11 n1 t12 t21 n2 t22,
Node t11 n1 t12 = Node t21 n2 t22
-> t11 = t21.

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).

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).

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.

 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).

 Prove that your function is meaning-preserving.

Theorem constant_fold_sound : forall (ctx : var -> nat) (e : exp),
eval (constant_fold e) ctx = eval e ctx.

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.

 Prove that your function doesn't miss any opportunities.

Theorem simplify_identities_simplifies : forall (e : exp),
no_identities (simplify_identities e).