(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 6 ***) (*** Solution ***) Ltac inv A := inversion A ; subst ; clear A. Inductive even : nat -> Prop := | evenO : even 0 | evenS : forall n, even n -> even (S (S n)). (*** Exercise 6.1(a) - with inversion ***) Goal ~even 1. Proof. intros A. now inversion A. Qed. (*** Exercise 6.1(a) - without inversion ***) Goal ~even 1. Proof. intros A. remember 1 as n. destruct A; discriminate. Qed. (*** Exercise 6.1(b) - with inversion, without induction ***) Goal forall n, even (S (S n)) -> even n. Proof. intros n A. inversion A. assumption. Qed. (*** Exercise 6.1(b) - without inversion, without induction ***) Goal forall n, even (S (S n)) -> even n. Proof. intros n A. remember (S (S n)) as m. destruct A; congruence. Qed. Inductive le (x:nat) : nat -> Prop := | lex : le x x | leS : forall y, le x y -> le x (S y). (*** Exercise 6.2 (a) ***) Lemma le_Sright x y : le x y -> le (S x) (S y). intros A. induction A. now apply lex. now apply leS. Qed. (*** Exercise 6.2 (b) ***) Goal forall x, le x 0 -> x = 0. Proof. intros x A. remember 0 as y. destruct A; congruence. Qed. Inductive le' : nat -> nat -> Prop := | lex' : forall x, le' x x | leS' : forall x y, le' x y -> le' x (S y). (*** Exercise 6.3 ***) Goal forall x, ~ le (S x) 0. Proof. intros x A. remember 0 as y. destruct A; congruence. Qed. Goal forall x, ~ le' (S x) 0. Proof. intros x A. remember (S x) as x'. remember 0 as y. destruct A; congruence. Qed. (*** Exercise 6.4 ***) Inductive F : Prop := | FI : F -> F. Goal F -> False. Proof. intros A. induction A. now apply IHA. Qed. (*** Exercise 6.5 ***) Section abstract_Imp. Variable state : Type. Definition action : Type := state -> state. Definition test : Type := state -> bool. Inductive com : Type := | Act : action -> com | Seq : com -> com -> com | If : test -> com -> com -> com | While : test -> com -> com. Inductive sem : com -> state -> state -> Prop := | semAct a s : sem (Act a) s (a s) | semSeq c1 c2 s s' s'' : sem c1 s s' -> sem c2 s' s'' -> sem (Seq c1 c2) s s'' | semIfTrue t c1 c2 s s' : t s = true -> sem c1 s s' -> sem (If t c1 c2) s s' | semIfFalse t c1 c2 s s' : t s = false -> sem c2 s s' -> sem (If t c1 c2) s s' | semWhileFalse t c s : t s = false -> sem (While t c) s s | semWhileTrue t c s s' s'': t s = true -> sem c s s' -> sem (While t c) s' s'' -> sem (While t c) s s''. Definition terminates c s : Prop := exists s', sem c s s'. (* forall c s, ter c s or ~ter c s is not provable without assumptions since termination is undecidable. *) Lemma functionality c s s' s'' : sem c s s' -> sem c s s'' -> s' = s''. Proof. intros A. revert s''. induction A ; intros s0 B ; inv B ; auto ; try congruence. (* ; *) assert (s' = s'0) by auto. subst. now auto. (* while true *) assert (s' =s'0) by auto. subst. auto. Qed. (* *** Equivalence *) Definition skip : com := Act (fun s => s). Definition TRUE : test := fun _ => true. Definition FALSE : test := fun _ => false. Definition div : com := While TRUE skip. Definition cap c c' : Prop := forall s s', sem c s s' -> sem c' s s'. Definition ceq c c' : Prop := cap c c' /\ cap c' c. Goal forall c c', ceq c c' <-> forall s s', sem c s s' <-> sem c' s s'. Proof. firstorder. Qed. Goal forall c, ceq (Seq skip c) c. Proof. split ; intros s s' A. inv A. inv H1. assumption. econstructor. now constructor. assumption. Qed. (*** Prove this. ***) Lemma Seq_assoc c1 c2 c3: ceq (Seq c1 (Seq c2 c3)) (Seq (Seq c1 c2) c3). Proof. split ; intros s s' A ; inv A. inv H4. econstructor. now econstructor ; eauto. assumption. inv H1. econstructor. eassumption. econstructor ; eauto. Qed. Goal forall c1 c2, ceq (If TRUE c1 c2) c1. Proof. split ; intros s s' A. inv A ; auto. discriminate. apply semIfTrue ; auto. Qed. Goal forall c, ceq (While FALSE c) skip. Proof. split ; intros s s' A. inv A. now constructor. discriminate. inv A. apply semWhileFalse. reflexivity. Qed. Goal forall t c, ceq (While t c) (If t (Seq c (While t c)) skip). Proof. split ; intros s s' A. inv A. apply semIfFalse. assumption. now constructor. apply semIfTrue. assumption. econstructor ; eassumption. inv A. inv H5. eapply semWhileTrue ; eassumption. inv H5. apply semWhileFalse ; assumption. Qed. Lemma div_term s : ~ terminates div s. Proof. intros [s' A]. remember div as c. induction A ; inv Heqc. discriminate. auto. Qed. (*** Prove this. ***) Lemma skip_div : (exists s : state, True) -> ~ ceq skip div. Proof. intros [s _] A. apply (div_term s). exists s. apply A. constructor. Qed. Goal forall c c', (forall s, terminates c s) -> cap c c' -> ceq c c'. Proof. intros c c' A B. split. assumption. intros s s' C. destruct (A s) as [s'' D]. assert (s' = s'') by (eapply functionality ; eauto). congruence. Qed. (* *** Monotonicity and Compatibility *) Definition monotone (f : com -> com) : Prop := forall c c', cap c c' -> cap (f c) (f c'). Lemma monotone_compatible (f : com -> com) c c' : monotone f -> ceq c c' -> ceq (f c) (f c'). Proof. firstorder. Qed. (*** Prove this. ***) Lemma monotone_while t : monotone (While t). Proof. intros c c' A s s' B. remember (While t c) as r ; induction B ; inv Heqr. apply semWhileFalse ; assumption. eapply semWhileTrue ; eauto. Qed. Lemma while_compatible t c c' : ceq c c' -> ceq (While t c) (While t c'). Proof. apply monotone_compatible, monotone_while. Qed. (* *** Optimization *) Fixpoint optimize (f : com -> com) (c : com) : com := match c with | Act a => f (Act a) | Seq c c' => f (Seq (optimize f c) (optimize f c')) | If t c c' => f (If t (optimize f c) (optimize f c')) | While t c => f (While t (optimize f c)) end. Theorem optimization1 (f : com -> com) : (forall c, cap c (f c)) -> forall c, cap c (optimize f c). Proof. intros A c. induction c ; simpl ; intros s s' B ; apply A ; inv B. now apply semAct. now eapply semSeq ; eauto. now apply semIfTrue ; auto. now apply semIfFalse ; auto. now apply semWhileFalse ; assumption. (*** Finish this proof. ***) eapply semWhileTrue ; eauto. revert H5. apply monotone_while ; auto. Qed. Theorem optimization2 (f : com -> com) : (forall c, cap (f c) c) -> forall c, cap (optimize f c) c. Proof. intros A c. induction c ; simpl ; intros s s' B ; apply A in B ; inv B. now apply semAct. now eapply semSeq ; eauto. now apply semIfTrue ; auto. now apply semIfFalse ; auto. now apply semWhileFalse ; assumption. eapply semWhileTrue ; eauto. revert H5. apply monotone_while ; auto. Qed. Theorem optimization3 (f : com -> com) : (forall c, ceq (f c) c) -> forall c, ceq (optimize f c) c. Proof. intros A c. split. now apply optimization2 ; firstorder. apply optimization1 ; firstorder. Qed. (* *** Evaluator *) Notation "'LETOPT' x <== e1 'IN' e2" := (match e1 with Some x => e2 | None => None end) (right associativity, at level 60). Definition approx (c c' : state -> option state) : Prop := forall s s', c s = Some s' -> c' s = Some s'. Fixpoint evalw (n : nat) (t : state -> bool) (c : state -> option state) (s : state) : option state := match n with | O => None | S n' => if t s then LETOPT s' <== c s IN evalw n' t c s' else Some s end. Lemma evalw_monotone m n t c c' : m<=n -> approx c c' -> approx (evalw m t c ) (evalw n t c'). Require Import Omega. Proof. revert n. induction m ; intros n A B s s' ; simpl. congruence. destruct n. exfalso. omega. (* omega needs exfalso because of options *) simpl. case_eq (t s) ; try congruence. case_eq (c s) ; try congruence. intros. erewrite B ; eauto. apply IHm ; auto ; omega. Qed. Fixpoint eval (n : nat) (c : com) (s : state) : option state := match c with | Act a => Some (a s) | Seq c1 c2 => LETOPT s' <== eval n c1 s IN eval n c2 s' | If t c1 c2 => if t s then eval n c1 s else eval n c2 s | While t c' => evalw n t (eval n c') s end. (*** Prove this. ***) Lemma eval_monotone m n c : m<=n -> approx (eval m c) (eval n c). Proof. intros A. induction c ; intros s s' ; simpl. (* a *) auto. (* ; *) case_eq (eval m c1 s) ; try congruence. intros. now erewrite IHc1 ; eauto. (* if *) now case_eq (t s) ; auto. (* while *) apply evalw_monotone ; auto. Qed. Corollary eval_monotone' m n c s s' s'' : eval m c s = Some s' -> eval n c s = Some s'' -> s' = s''. Proof. intros A B. assert (C : m<=n \/ n<= m) by omega. destruct C as [C|C]. assert (eval n c s = Some s') by (eapply eval_monotone ; eauto). congruence. assert (eval m c s = Some s'') by (eapply eval_monotone ; eauto). congruence. Qed. Lemma while_agrees n c k t s s' : (forall s s', eval n c s = Some s' -> sem c s s') -> evalw k t (eval n c) s = Some s' -> sem (While t c) s s'. Proof. intros H. revert s. induction k ; simpl. congruence. intros s. case_eq (t s). (* true *) case_eq (eval n c s) ; try congruence. intros s0 A B C. now eapply semWhileTrue ; eauto. (* false *) intros A B ; inv B. apply semWhileFalse ; auto. Qed. Theorem eval_agrees c s s' : sem c s s' <-> exists n, eval n c s = Some s'. Proof. split. (* -> *) intros A. induction A. (* a *) exists 1. reflexivity. (* ; *) destruct IHA1 as [n1 IH1]. destruct IHA2 as [n2 IH2]. exists (n1+n2). simpl. erewrite (eval_monotone n1) ; eauto ; try omega. apply (eval_monotone n2) ; auto ; omega. (* if true *) destruct IHA as [n IH]. exists n. simpl. rewrite H. assumption. (* if false *) destruct IHA as [n IH]. exists n. simpl. rewrite H. assumption. (* while false *) exists 1. simpl. rewrite H. reflexivity. (* while true *) destruct IHA1 as [n1 IH1]. destruct IHA2 as [n2 IH2]. exists (S(n1+n2)). simpl. rewrite H. erewrite eval_monotone with (m:=n1) ; eauto ; try omega. erewrite evalw_monotone with (m:=n2)(c:=eval n2 c) ; eauto; try omega. apply eval_monotone ; omega. (* <- *) intros [n A]. revert s s' A. induction c ; simpl ; intros s s'. (* a *) intros A ; inv A. now constructor. (* ; *) case_eq (eval n c1 s) ; intros ; try congruence. now econstructor ; eauto. (* if *) case_eq (t s) ; intros. now apply semIfTrue ; auto. now apply semIfFalse ; auto. (* while *) apply while_agrees. assumption. Qed. (*** Prove this. ***) Corollary eval_agrees_divergence c s : ~ terminates c s <-> forall n, eval n c s = None. Proof. split. intros A n. case_eq (eval n c s) ; auto. intros s' B. exfalso. apply A. exists s'. apply eval_agrees. now firstorder. intros A [s' B]. apply eval_agrees in B. destruct B as [n C]. assert (eval n c s = None) by auto. congruence. Qed.