(** Homework Assignment 2#<br>#
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

(** Submit your solution file for this assignment as an attachment
  #<a href="mailto:adamc@cs.berkeley.edu?subject=ICTP HW2">#by e-mail#</a># with
  the subject "ICTP HW2" by the start of class on September 14.
  You should write your solutions entirely on your own.

  #<a href="HW2.v">#Template source file#</a>#
  *)

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
  #<a href="http://coq.inria.fr/doc/tactic-index.html">#the manual's tactic index#</a>#.

  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 #<i>#more#</i># 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 #<i>#combining#</i># tactics.
  - The notation [t1; t2] means "run [t1] on the current goal and then run [t2]
    on #<b>#all#</b># 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 *)

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

(** 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!
  *)