(* Exercise 1 *) (* Program a function rcons : forall A, A -> list A -> list A which *) (*add an element at the end of a list *) Require Import List. (* Use an inductive predicate to characterize lists of natural numbers *) (*that are palindromes *) (* Exercise 2 *) (* Define inductively the following binary relations on types (list A): - the list l' is obtained form l by transposing two consecutive elements - the list l' is obtained form l by applying the above operation a finite number of times. Here we say that l' is a permutation of l. Show that the second relation is an equivalence relation : reflexive, symmetric, and transitive. *) Require Import Relations. (* Exercise 3 *) (* Consider the following definitions *) (* Note: any theorem --- either proven or admitted --- can be used for proving the following ones *) Require Import Omega. Inductive Even : nat -> Prop := | Ev0: Even 0 | Ev2 : forall n, Even n -> Even (S (S n)). Definition Odd n := Even (S n). (* Prove the following lemmas (remove the Admitted) *) Lemma E6: Even 6. Admitted. Lemma O7 : Odd 5. Admitted. Lemma E_double : forall n:nat, Even (2*n). Admitted. Lemma not_E1 : ~ Even 1. Admitted. Lemma Even_SS_inv : forall n, Even (S (S n)) -> Even n. Admitted. Lemma Odd_not_Even : forall n, Odd n -> ~ Even n. Admitted. Lemma Even_not_Odd : forall n, Even n -> ~ Odd n. Admitted. Lemma Even_double : forall n, Even n -> exists p:nat, n = p + p. Admitted. Lemma Odd_S_double : forall n, Odd n -> exists p:nat, n = S( p + p). Admitted. (* Consider the following function *) Fixpoint evenb (n: nat): bool := match n with O => true | 1 => false | S (S p) => evenb p end. Lemma evenb_Sn : forall n:nat, evenb (S n) = negb (evenb n). Admitted. Lemma evenb_if : forall n:nat, if evenb n then Even n else Odd n. Admitted. Lemma evenb_iff : forall n, evenb n = true <-> Even n. Admitted. Goal Even 560. rewrite <- evenb_iff. reflexivity. Qed. (* Exercise 4 : borrowed and adapted from B. Pierce course "Software Foundations"*) (* We define the following toy language: *) Inductive tm : Type := | tm_const : nat -> tm | tm_plus : tm -> tm -> tm. (* Here is a big step evaluator for this language *) Inductive eval : tm -> nat -> Prop := | E_Const : forall n, eval (tm_const n) n | E_Plus : forall t1 t2 n1 n2, eval t1 n1 -> eval t2 n2 -> eval (tm_plus t1 t2) (plus n1 n2). (* Here is a small step evaluator for this language *) Inductive step : tm -> tm -> Prop := | ST_PlusConstConst : forall n1 n2, step (tm_plus (tm_const n1) (tm_const n2)) (tm_const (plus n1 n2)) | ST_Plus1 : forall t1 t1' t2, (step t1 t1') -> step (tm_plus t1 t2) (tm_plus t1' t2) | ST_Plus2 : forall n1 t2 t2', (step t2 t2') -> step (tm_plus (tm_const n1) t2) (tm_plus (tm_const n1) t2'). (*A few things to notice: * We are defining just a single reduction step, in which one tm_plus node is replaced by its value. * Each step finds the leftmost tm_plus node that is "ready to go" (both of its operands are constants) and reduces it. The first rule tells how to reduce this tm_plus node itself; the other two rules tell how to find it. * A term that is just a constant cannot take a step. *) (* Prove that: *) Lemma step_plus_l : forall t1 t1' t2, step t1 t1' -> step (tm_plus t1 t2) (tm_plus t1' t2). (* Prove that evaluation is deterministic: *) Lemma eval_det : forall t n1 n2, eval t n1 -> eval t n2 -> n1 = n2. (* We can also prove that step is deterministic : We must show that if x steps to both y1 and y2 then y1 and y2 are *) (*equal. Consider the last rules used in the derivations of step x y1 *) (*and step x y2. * If both are ST_PlusConstConst, the result is immediate. * It cannot happen that one is ST_PlusConstConst and the other is ST_Plus1 or ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where both t1 and t2 are constants (by ST_PlusConstConst) AND one of t1 or t2 has the form tm_plus .... * Similarly, it cannot happen that one is ST_Plus1 and the other is ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where t1 has both the form tm_plus t1 t2 and the form tm_const n. * The cases when both derivations end with ST_Plus1 or ST_Plus2 follow by the induction hypothesis. *) Theorem step_deterministic : forall t t1 t2, step t t1 -> step t t2 -> t1 = t2. Admitted. (* Exercise 5 *) (* Prove the following theorems Note: any theorem --- either proven or admitted --- can be used for proving the following ones *) Require Import Arith. Require Import Max. Lemma le_leb_iff : forall n p, n <= p <-> leb n p=true. Lemma lt_lb_iff : forall n p, p < n <-> leb n p = false Use these lemmas for proving : Lemma leb_max : forall n p, max n p = if leb n p then p else n. (* Hint : execute the command SearchAbout [le max]. *)