(** * Exercises: Verification in Coq *) Require Import Bool Arith List. Import ListNotations. (**********************************************************************) (* Exercise: double even [2 star]. Prove the following theorem about the function [even]. Hint: you might find it helpful to create a lemma for the inductive case. *) Fixpoint even (n:nat) := match n with | 0 => true | 1 => false | S (S k) => even k end. Theorem double_even : forall n:nat, even(n + n) = true. Proof. Abort. (**********************************************************************) Module MyList. (* Exercise: verified list [3 star]. Here are some definitions for lists: *) Inductive list (A:Type) : Type := | nil : list A | cons : A -> list A -> list A. Arguments nil [A]. Arguments cons [A]. Infix "::" := cons (right associativity, at level 60). Fixpoint app {A : Type} (lst1 lst2 : list A) := match lst1 with | nil => lst2 | h::t => h :: (app t lst2) end. Infix "++" := app (right associativity, at level 60). (* Using those definitions, implement functions [hd], [tl], [empty], and [length], and prove in Coq that the following equations hold for those functions. _Hint_: many of these have been proved in previous lectures, notes, and/or labs, but reproving them now is good exercise. hd x nil = x hd _ (x::_) = x tl nil = nil tl (_::xs) = xs nil ++ xs = xs xs ++ nil = xs (x::xs) ++ ys = x :: (xs ++ ys) lst1 ++ (lst2 ++ lst3) = (lst1 ++ lst2) ++ lst3 empty nil = true empty (_::_) = false empty (xs ++ ys) = empty xs && empty ys length nil = 0 length (_::xs) = 1 + length xs length (xs ++ ys) = length xs + length ys *) (* Exercise: list mem [3 star]. Here is a definition of a [mem] function on lists: *) (* The [eqA] argument is needed to provide a boolean equality operator on the unknown type A. *) Fixpoint mem {A:Type} (eqA : A -> A -> bool) (x:A) (lst : list A) := match lst with | nil => false | h::t => (eqA x h) || mem eqA x t end. (* And here is an algebraic specification of it: << mem x nil = false mem x (y::ys) = x =? y || mem x ys mem x (xs ++ ys) = mem x xs || mem x ys >> State and prove theorems that show the implementation is correct. *) Theorem mem_nil : forall (A:Type) (eqA : A -> A -> bool) (x:A), @mem A eqA x nil = false. Proof. trivial. Qed. Theorem mem_cons : forall (A:Type) (eqA : A -> A -> bool) (x y:A) (ys : list A), mem eqA x (y::ys) = (eqA x y) || mem eqA x ys. Proof. trivial. Qed. Theorem mem_app : forall (A:Type) (eqA : A -> A -> bool) (x:A) (xs ys : list A), mem eqA x (xs ++ ys) = mem eqA x xs || mem eqA x ys. Proof. intros A eqA x xs ys. induction xs as [ | h t IH]. - trivial. - simpl. rewrite IH. rewrite orb_assoc. trivial. (* [orb_assoc] is a library theorem showing that [||] is associative *) Qed. End MyList. (**********************************************************************) (* Exercise: extend compiler [3 star]. Below, you will find the code for the verified compiler from the notes. Extend the source and target language with multiplication. Update the interpreters, compiler, and proofs to account for your extension. *) Module Compiler. Inductive expr : Type := | Const : nat -> expr | Plus : expr -> expr -> expr. Fixpoint eval_expr (e : expr) : nat := match e with | Const i => i | Plus e1 e2 => (eval_expr e1) + (eval_expr e2) end. Inductive instr : Type := | PUSH : nat -> instr | ADD : instr. Definition prog := list instr. Definition stack := list nat. Fixpoint eval_prog (p : prog) (s : stack) : option stack := match p,s with | PUSH n :: p', s => eval_prog p' (n :: s) | ADD :: p', x :: y :: s' => eval_prog p' (x + y :: s') | nil, s => Some s | _, _ => None end. Fixpoint compile (e : expr) : prog := match e with | Const n => [PUSH n] | Plus e1 e2 => compile e2 ++ compile e1 ++ [ADD] end. Lemma app_assoc_4 : forall (A:Type) (l1 l2 l3 l4 : list A), l1 ++ (l2 ++ l3 ++ l4) = (l1 ++ l2 ++ l3) ++ l4. Proof. intros A l1 l2 l3 l4. replace (l2 ++ l3 ++ l4) with ((l2 ++ l3) ++ l4); rewrite app_assoc; trivial. Qed. Lemma compile_helper : forall (e:expr) (s:stack) (p:prog), eval_prog (compile e ++ p) s = eval_prog p (eval_expr e :: s). Proof. intros e. induction e as [n | e1 IH1 e2 IH2]; simpl. - trivial. - intros s p. rewrite <- app_assoc_4. rewrite IH2. rewrite IH1. simpl. trivial. Qed. Theorem compile_correct : forall (e:expr), eval_prog (compile e) [] = Some [eval_expr e]. Proof. intros e. induction e as [n | e1 IH1 e2 IH2]; simpl. - trivial. - repeat rewrite compile_helper. simpl. trivial. Qed. End Compiler.