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

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 non-trivial 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:

intros: Transform a goal with implications and/or universal quantifications into a simpler goal, where the assumptions and quantified variables have moved into the assumptions above the double line. intros with no arguments performs this for all implications and foralls visible in the goal, while intros followed by a space-separated list of names performs this simplification as many times as there are names, using your list to pick the names of new assumptions instead of assigning them itself. You'll often want to use the named form of intros for goals involving negation and other syntactic abbreviations for implications. (Remember that ~P is defined as P -> False.)
apply name: Apply the named lemma/theorem name to the current goal, adding the premises of that lemma as subgoals, if there are any premises.
change e: When the goal is some term e', switch to proving e instead. e and e' must be equivalent through the computational reductions.

Equality:

reflexivity: Prove any equality between two equivalent terms.
rewrite H: Rewrite the goal using the equality proved by hypothesis H. You can also use rewrite H1 in H2 to do the rewriting in H2, and you can follow rewrite with <- to use the equality to rewrite from right to left instead of left to right.

Simplification:

simpl: Try to simplify the goal using computational reduction rules. You may also use simpl in H to simplify hypothesis H or simpl in * to simplify the goal and all hypotheses.
unfold name: Where name is a symbol assigned a meaning earlier in a Definition, expand all occurrences of that name in the goal into the definition. The same alternate syntaxes that work with simpl apply here, too. When considering using unfold, keep in mind that it can sometimes make the goal/hypothesis more complicated than it was before. simpl is generally better about avoiding that kind of thing.

Working with inductive types:

destruct e: Perform a case analysis on the expression e of inductive type. The goal is split into one subgoal per constructor of e's type, with e replaced by a generic application of that constructor to fresh variables. If e is the name of a variable bound in the goal rather than a variable bound in the assumptions above the double line, then intros is used automatically to move that variable and those that come before it above the double line.
induction e: Like destruct e, but the subgoals also have additional assumptions corresponding to inductive hypotheses where appropriate. You may also use induction on variables quantified in the goal.
discriminate: Prove any formula, given that your assumptions include an equality between terms built with different constructors of an inductive type.
injection H: Where H is a hypothesis equating two values built with the same constructor of an inductive type, add all of the equalities that this relationship applies.

Automation:

trivial: Prove a very obvious goal. The best way to get a handle on what this means is through experience.
tauto: Prove any propositional tautology. Remember that we're working in constructive logic, so not every formula that can be proved "true" using truth tables is actually true constructively!
intuition: A version of tauto that lets you take advantage of partial success. In particular, when it can't prove the goal completely, it will often split it into a set of simpler subgoals based on properties of the logical connectives.
firstorder: Version of intuition that has a limited ability to automate proofs in first-order logic
congruence: Prove a goal whose truth follows from the definition of equality and basic properties of inductive type constructors.
omega: Prove any goal that follows from properties of linear arithmetic.

For some of the theorems in this assignment, it will be very useful to use some of the ways of combining tactics.

The notation t1; t2 means "run t1 on the current goal and then run t2 on all of the subgoals generated by t1."
The notation try t means "try running t1 on the goal; if it fails, silently roll back to where we started instead of signaling an error to the user."

Finally, don't forget these other general theorem proving tools:

You can introduce a definition with Definition name := e..
When you want to define a recursive function, it's easiest to use the Fixpoint command.
Often a theorem will be easiest to prove if you prove some lemmas first. These are introduced with Lemma name : formula., followed by a proof script and Qed., just as for Theorem. (In fact, Theorem and Lemma are synonyms, with the choice of which to use serving only as documentation.)

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.

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

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:

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.

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 meaning-preserving.





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.