(** Homework Assignment 2#
# ##Interactive Computer Theorem Proving#
# CS294-9, Fall 2006#
# UC Berkeley *) Require Import Arith Omega. (** Submit your solution file for this assignment ##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## *) (** * 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.