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 *) (* Program a function rcons : forall A, A -> list A -> list A which *) (*add an element at the end of a list *) Require Import List. Fixpoint rcons (A : Type)(a : A)(l : list A) : list A := match l with |nil => a :: nil |hd :: tl => hd :: (rcons A a tl) end. (* Use an inductive predicate to characterize lists of natural numbers *) (*that are palindromes *) Inductive palindrome : list nat -> Prop := |Empty : palindrome nil |Single : forall n, palindrome (n :: nil) |Rcons : forall (n : nat)(l : list nat), palindrome (n :: (rcons nat n l)). (* 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. Section perms. Variable A : Set. Lemma perm_refl : reflexive _ perm. Lemma perm_trans : transitive _ perm. Lemma perm_sym : symmetric _ perm. Theorem equiv_perm : equiv _ perm. End perms. *) Require Import Relations. Section perms. Variable A : Set. Inductive transpose : list A -> list A -> Prop := | transpose_hd : forall (a b:A) (l:list A), transpose (a :: b :: l) (b :: a :: l) | transpose_tl : forall (a:A) (l l':list A), transpose l l' -> transpose (a :: l) (a :: l'). Inductive perm (l:list A) : list A -> Prop := | perm_id : perm l l | perm_tr : forall l' l'':list A, perm l l' -> transpose l' l'' -> perm l l''. Lemma perm_refl : reflexive _ perm. Proof. unfold reflexive; left. Qed. Lemma perm_intro_r : forall l l1 l2:list A, transpose l l1 -> perm l1 l2 -> perm l l2. Proof. intros l l1 l2 H H0; elim H0. eapply perm_tr; eauto. left. intros l' l''; intros; right with l'; auto. Qed. Lemma perm_trans : transitive _ perm. Proof. unfold transitive; intros l l' l'' H; generalize l''. elim H. trivial. intros l'0 l''0 H0 H1; intros. apply H1;eapply perm_intro_r; eauto. Qed. Lemma transpose_sym : forall l l':list A, transpose l l' -> transpose l' l. Proof. intros l l' H;elim H; [ left | right; auto ]. Qed. Lemma perm_sym : symmetric _ perm. Proof. unfold symmetric; intros l l' H; elim H. left. intros; eapply perm_intro_r. eapply transpose_sym; eauto. auto. Qed. Theorem equiv_perm : equiv _ perm. Proof. repeat split. apply perm_refl. apply perm_trans. apply perm_sym. Qed. End perms. (* Exercise 3 : 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). Proof. intros t1 t1' t2 h12; revert t2. induction h12; intros t3; simpl. constructor. constructor. constructor. trivial. constructor. constructor. trivial. Qed. (* Prove that evaluation is deterministic: *) Lemma eval_det : forall t n1 n2, eval t n1 -> eval t n2 -> n1 = n2. Proof. intros t n1 n2 h1 h2. revert n2 h2. induction h1. intros n2; simpl. inversion 1. trivial. intros n3 h3. inversion_clear h3. rewrite (IHh1_1 n0 H). rewrite (IHh1_2 n4 H0). trivial. Qed. (* 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. Proof. intros t t1 t2 Ht1 Ht2. revert t2 Ht2. induction Ht1. intros t3 ht3. inversion ht3. reflexivity. inversion H2. inversion H2. intros t3 Ht3. inversion Ht3. rewrite <- H0 in Ht1. inversion Ht1. rewrite <- (IHHt1 t1'0); trivial. rewrite <- H in Ht1. inversion Ht1. intros t3 Ht3. inversion Ht3. rewrite <- H1 in Ht1. inversion Ht1. inversion H2. rewrite <- (IHHt1 t2'0); trivial. Qed.