(* Exercise 1 *) (**************) (* Define an inductive type for the months in the gregorian calendar *) (*(the english civil calendar) *) (* Define an inductive type for the four seasons *) (* What is the inductive principle generated in each case ?*) (* Define a function mapping each month to the season that contains *) (* most of its days, using pattern matching *) (* Exercise 2 *) (**************) (* Define the boolean functions bool_xor, bool_and, bool_eq of type *) (*bool -> bool -> bool, and the function bool_not of type bool -> bool *) (* prove the following theorems: Lemma bool_xor_not_eq : forall b1 b2 : bool, bool_xor b1 b2 = bool_not (bool_eq b1 b2). Lemma bool_not_and : forall b1 b2 : bool, bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2). Lemma bool_not_not : forall b : bool, bool_not (bool_not b) = b. Lemma bool_or_not : forall b : bool, bool_or b (bool_not b) = true. Lemma bool_id_eq : forall b1 b2 : bool, b1 = b2 <-> bool_eq b1 b2 = true. Lemma bool_not_or : forall b1 b2 : bool, bool_not (bool_or b1 b2) = bool_and (bool_not b1) (bool_not b2). Lemma bool_or_and : forall b1 b2 b3 : bool, bool_or (bool_and b1 b3) (bool_and b2 b3) = bool_and (bool_or b1 b2) b3. *) (* Exercise 3 *) (**************) (* Let us consider again the type color defined in the lecture :*) Inductive color:Type := | white | black | yellow | cyan | magenta | red | blue | green. (* let us define the complement of a color *) Definition compl (c : color) := match c with | white => black | black => white | yellow => blue | cyan => red | magenta => green | red => cyan | blue => yellow | green => magenta end. (* Prove the following results: Lemma compl_compl : forall c, compl (compl c)= c. Lemma compl_injective : forall c c', compl c = compl c' -> c = c'. Lemma compl_surjective : forall c, exists c', c = compl c'. *) (* Exercise 4 *) (**************) (* Define an inductive type formula : Type that represents the *) (*abstract language of propositional logic without variables: L = L /\ L | L \/ L | ~L | L_true | L_false *) (* Define a function formula_holds of type (formula -> Prop computing the *) (* Coq formula corresponding to an element of type formula *) (* Define a function isT_formula of type (formula -> bool) computing *) (* the intended truth value of (f : formula) *) (* prove that is (idT_formula f) evaluates to true, then its *) (*corresponding Coq formula holds ie.: Require Import Bool. Lemma isT_formula_correct : forall f : formula, isT_formula f = true <-> formula_holds f. *) (* Exercise 5 *) (**************) (* We use the inductive type defined in the lecture: *) Inductive natBinTree : Set := | Leaf : natBinTree | Node : nat -> natBinTree -> natBinTree -> natBinTree. (* Define a function which sums all the values present in the tree. Define a function is_zero_present : natBinTree -> bool, which tests whether the value 0 is present or not in the tree. Prove several simple statements about the fonctions mirror, tree_size and tree_height seen in the lecture It is possible to navigate in a binary tree. Given a tree t and a path like "from the root, go to the left subtree, then go to the right subtree, then go to the left subtree, etc. " Such a path can be easily represented by a list of directions Inductive direction : Set := L (* go left *) | R (* go right *). Define in coq a function get_label that takes a tree and some path, and returns the label at which one arrives following the path (if any) Fixpoint get_label (path : list direction)(t:natBinTree): option nat:= (* to complete *) Consider the following function : *) Require Import Arith. Require Import Bool. Fixpoint zero_present (t: natBinTree) : bool := match t with Leaf => false | Node n t1 t2 => beq_nat n 0 || zero_present t1 || zero_present t2 end. (* Prove that whenever zero_present t = true, then there exists some path p such that get_label p t = Some 0 *) (* Exercise 6 *) (* Require Import List. *) (* Define the function split : forall A B : Set, list A * B -> (list A) * (list B) which transforms a list of pairs into a pair of lists and the function combine : forall A B : Set, list A * list B -> list (A * B) which transforms a pair of lists into a list of pairs. Write and prove a theorem relating the two functions. *)