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

(** Directions for using this file to check your solutions:
  - Have your solutions in a file named [Sol2.v].
  - Run [coqc Sol2] from the command line.
  - With the file you're reading now in the same directory, run [coqc Check2].
  - If you don't see any error messages, then you're done!
    (Actually, Coq will allow you to use the [Axiom] command and its synonyms to
    assert facts without justification, but just avoid using these and you can
    rely on this checker. [:-)])
  *)

Require Import Arith.

Module Type HW2_SIG.
  Parameter bool_not : bool -> bool.
  Parameter bool_xor : bool -> bool -> bool.
  Parameter bool_and : bool -> bool -> bool.
  Parameter bool_or : bool -> bool -> bool.
  Parameter bool_eq : bool -> bool -> bool.

  Axiom xor_not_eq : forall b1 b2,
    bool_xor b1 b2 = bool_not (bool_eq b1 b2).
  Axiom not_and_or_not : forall b1 b2,
    bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2).

  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.

  Axiom reverse'_correct : forall ls, reverse' ls = reverse ls.

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

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

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

  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.

  Axiom insert_increases : forall (n : nat) (t : tree),
    size (insert n t) = S (size t).

  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.

  Axiom insert_ordered : forall (n : nat) (t : tree),
    ordered t -> ordered (insert n t).

  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.

  Parameter constant_fold : exp -> exp.

  Axiom constant_fold_simplifies : forall (e : exp),
    constant_folded (constant_fold e).

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

Require Sol2.

Module Sol2_Verified : HW2_SIG := Sol2.