Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* Exercise 1 *) (* Define an inductive type for the months in the gregorian calendar *) (*(the French 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. *) (** New recursive types **) (* 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 3 *) (* We use the inductive type defined in the lecture: Inductive natBinTree : Set := | Leaf : nat -> 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 if the value 0 is present in the tree. *) (* Exercise 4 *) (* 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. *)