(**
* 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.