(** Homework Assignment 2 checker#
# ##Interactive Computer Theorem Proving#
# CS294-9, Fall 2006#
# 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.