(** * Lab: Verification in Coq *) Require Import Bool Arith. (**********************************************************************) (* 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. Then extract your verified implementation. _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 *) End MyList. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive nat => int [ "0" "succ" ]. Extraction "mylist.ml" MyList.