# 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 `forall`s 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 `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

``` ```
``` 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. ```
 Prove that your function is meaning-preserving.
``` 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!
``` ```
Index