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

Require Import Arith Omega.

(** Submit your solution file for this assignment
  #<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>#
  *)

(** * Booleans *)

Definition bool_not (b : bool) :=
  match b with
    | false => true
    | true => false
  end.

Definition bool_xor (b1 b2 : bool) :=
  match b1 with
    | false => b2
    | true => bool_not b2
  end.

Definition bool_and (b1 b2 : bool) :=
  match b1 with
    | false => false
    | true => b2
  end.

Definition bool_or (b1 b2 : bool) :=
  match b1 with
    | false => b2
    | true => true
  end.

Definition bool_eq (b1 b2 : bool) :=
  match b1 with
    | false => bool_not b2
    | true => b2
  end.

Theorem xor_not_eq : forall b1 b2,
  bool_xor b1 b2 = bool_not (bool_eq b1 b2).
  destruct b1; destruct b2; trivial.
Qed.

Theorem not_and_or_not : forall b1 b2,
  bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2).
  destruct b1; destruct b2; trivial.
Qed.


(** * Lists *)

Inductive list : Set :=
  | nil : list
  | cons : nat -> list -> list.

Fixpoint append (ls1 ls2 : list) {struct ls1} : list :=
  match ls1 with
    | nil => ls2
    | cons h t => cons h (append t ls2)
  end.

Fixpoint reverse (ls : list) : list :=
  match ls with
    | nil => nil
    | cons h t => append (reverse t) (cons h nil)
  end.

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.

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.

Lemma reverse'_helper_correct : forall ls acc,
  reverse'_helper ls acc = append (reverse ls) acc.
  induction ls; simpl; intuition.
  rewrite IHls.
  rewrite append_associative.
  trivial.
Qed.

Lemma append_nil : forall ls, append ls nil = ls.
  induction ls; simpl; intuition.
  congruence.
Qed.

Theorem reverse'_correct : forall ls, reverse' ls = reverse ls.
  intros.
  unfold reverse'.
  rewrite reverse'_helper_correct.
  apply append_nil.
Qed.


(** * Trees *)

Inductive tree : Set :=
  | Leaf : tree
  | Node : tree -> nat -> tree -> tree.

Definition isLeaf (t : tree) :=
  match t with
    | Leaf => True
    | Node _ _ _ => False
  end.

Theorem Leaf_neq_Node : forall t1 n t2, Leaf <> Node t1 n t2.
  intros t1 n t2 H.
  change (isLeaf (Node t1 n t2)).
  rewrite <- H.
  change True.
  trivial.
Qed.

Definition leftChild (t : tree) :=
  match t with
    | Leaf => Leaf
    | Node t' _ _ => t'
  end.

Theorem Node_inj : forall t11 n1 t12 t21 n2 t22,
  Node t11 n1 t12 = Node t21 n2 t22
  -> t11 = t21.
  intros t11 n1 t12 t21 n2 t22 H.
  change (leftChild (Node t11 n1 t12) = leftChild (Node t21 n2 t22)).
  rewrite H.
  reflexivity.
Qed.

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.

Fixpoint size (t : tree) : nat :=
  match t with
    | Leaf => 0
    | Node tle _ tgt => S (size tle + size tgt)
  end.

Theorem insert_increases : forall (n : nat) (t : tree),
  size (insert n t) = S (size t).
  induction t; simpl; intuition.
  destruct (le_lt_dec n n0); simpl; omega.
Qed.

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.

Definition ordered (t : tree) : Prop :=
  ordered' O None t.

Lemma insert_ordered' : forall (n : nat) (t : tree) (min : nat) (max : option nat),
  min <= n
  -> match max with
       | None => True
       | Some max => n <= max
     end
  -> ordered' min max t
  -> ordered' min max (insert n t).
  induction t; simpl; intuition.
  destruct (le_lt_dec n n0); simpl; intuition.
Qed.

Theorem insert_ordered : forall (n : nat) (t : tree),
  ordered t -> ordered (insert n t).
  unfold ordered; intros.
  apply insert_ordered'; intuition.
Qed.


(** * Expression evaluation *)

Definition var := nat.

Inductive exp : Set :=
  | Const : nat -> exp
  | Var : var -> exp
  | Plus : exp -> exp -> exp
  | Times : exp -> exp -> exp.

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.

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.

Fixpoint constant_fold (e : exp) : exp :=
  match e with
    | Const _ => e
    | Var _ => e
    | Plus e1 e2 =>
      match constant_fold e1, constant_fold e2 with
	| Const n1, Const n2 => Const (n1 + n2)
	| e1', e2' => Plus e1' e2'
      end
    | Times e1 e2 =>
      match constant_fold e1, constant_fold e2 with
	| Const n1, Const n2 => Const (n1 * n2)
	| e1', e2' => Times e1' e2'
      end
  end.

Theorem constant_fold_simplifies : forall (e : exp),
  constant_folded (constant_fold e).
  induction e; simpl; intuition;
    destruct (constant_fold e1);
      destruct (constant_fold e2);
	simpl in *; intuition.
Qed.

Theorem constant_fold_sound : forall (ctx : var -> nat) (e : exp),
  eval (constant_fold e) ctx = eval e ctx.
  induction e; simpl; intuition;
    destruct (constant_fold e1); destruct (constant_fold e2);
      simpl; intuition.
Qed.

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.

Fixpoint simplify_identities (e : exp) : exp :=
  match e with
    | Const _ => e
    | Var _ => e
    | Plus e1 e2 =>
      match simplify_identities e1, simplify_identities e2 with
	| Const 0, e' => e'
	| e', Const 0 => e'
	| e1', e2' => Plus e1' e2'
      end
    | Times e1 e2 =>
      match simplify_identities e1, simplify_identities e2 with
	| Const 1, e' => e'
	| e', Const 1 => e'
	| e1', e2' => Times e1' e2'
      end
  end.

Theorem simplify_identities_simplifies : forall (e : exp),
  no_identities (simplify_identities e).
  induction e; simpl; intuition.
  destruct (simplify_identities e1);
    destruct (simplify_identities e2);
      try destruct n; try destruct n0;
	simpl in *; intuition.

  destruct (simplify_identities e1);
    destruct (simplify_identities e2);
      try destruct n; try destruct n0; try destruct n; try destruct n0;
	simpl in *; intuition.
Qed.

Theorem simplify_identities_sound : forall (ctx : var -> nat) (e : exp),
  eval (simplify_identities e) ctx = eval e ctx.
  induction e; simpl; intuition;
    [destruct (simplify_identities e1);
      destruct (simplify_identities e2); simpl in *; subst;
	destruct (eval e1 ctx); destruct (eval e2 ctx); simpl; intuition
      | destruct (simplify_identities e1);
	destruct (simplify_identities e2); rewrite <- IHe1; rewrite <- IHe2;
	  simpl in *; subst; intuition;
	    destruct (eval e1 ctx); destruct (eval e2 ctx);
	      try destruct n; try destruct n0; simpl; intuition].
Qed.