(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 7 ***) (*** Solution ***) (*** Exercise 7.1 ***) Inductive And (X Y : Prop) : Prop := | AndI : X -> Y -> And X Y. Check And_ind. (*** And_ind : forall X Y P : Prop, (X -> Y -> P) -> And X Y -> P ***) Inductive Eq (X : Type) : X -> X -> Prop := | EqI : forall x, Eq X x x. Check Eq_ind. (*** Eq_ind : forall (X : Type) (P : X -> X -> Prop), (forall x : X, P x x) -> forall y z : X, Eq X y z -> P y z ***) Inductive EQ (X : Type) (x : X) : X -> Prop := | EQI : EQ X x x. Check EQ_ind. (*** EQ_ind : forall (X : Type) (x : X) (P : X -> Prop), P x -> forall y : X, EQ X x y -> P y ***) (*** Exercise 7.2 ***) Inductive le2 : nat -> nat -> Prop := | le2x : forall x, le2 x x | le2S : forall x y, le2 x y -> le2 x (S y). Check le2_ind. (*** le2_ind : forall P : nat -> nat -> Prop, (forall x : nat, P x x) -> (forall x y : nat, le2 x y -> P x y -> P x (S y)) -> forall n m : nat, le2 n m -> P n m ***) Section Star. Variable X : Type. Variable R : X -> X -> Prop. Inductive star : X -> X -> Prop := | starR x : star x x | starT x y z : R x y -> star y z -> star x z. (*** Exercise 7.3 ***) Lemma starTR : forall x y z, star x y -> R y z -> star x z. Proof. intros x y z A B. induction A ; eauto using star. Qed. (* apply starT with (y:=x). now constructor. assumption. apply starT with (y:=y0) ; assumption. Qed. *) (*** Exercise 7.4 ***) Check star_ind. (*** star_ind : forall P : X -> X -> Prop, (forall x : X, P x x) -> (forall x y z : X, R x y -> star y z -> P y z -> P x z) -> forall x y : X, star x y -> P x y ***) Goal forall x y z, star x y -> star y z -> star x z. Proof. intros x y z A B. induction A ; eauto using star. Qed. Goal forall x y, R x y -> star x y. Proof. eauto using star. Qed. Inductive star1 (x : X) : X -> Prop := | star1R : star1 x x | star1T : forall y z, star1 x y -> R y z -> star1 x z. Check star1_ind. (*** star1_ind : forall (x : X) (P : X -> Prop), P x -> (forall y z : X, star1 x y -> P y -> R y z -> P z) -> forall y : X, star1 x y -> P y ***) Lemma star1TL : forall x y z, R x y -> star1 y z -> star1 x z. Proof. intros x y z A B. induction B ; eauto using star1. Qed. Goal forall x y, R x y -> star1 x y. Proof. eauto using star1. Qed. (*** Exercise 7.5 ***) Goal forall x, star1 x x. Proof. eauto using star1. Qed. (*** Exercise 7.5 ***) Goal forall x y z, star1 x y -> star1 y z -> star1 x z. Proof. intros x y z A B. induction B ; eauto using star1. Qed. (*** Exercise 7.5 ***) Goal forall x y, star x y <-> star1 x y. Proof. split. intros A. induction A ; eauto using star1, star1TL. intros A. induction A ; eauto using star, starTR. Qed. End Star. Implicit Arguments star [X]. Definition invariant {X : Type} (p : X -> Prop) (R : X -> X -> Prop) : Prop := forall x y, R x y -> p x -> p y. (*** Exercise 7.6 ***) Goal forall (X : Type) (R : X -> X -> Prop) (p : X -> Prop), invariant p R -> invariant p (star R). Proof. intros X r p A x y C D. induction C ; firstorder. Qed. Fixpoint iter (n : nat) {X : Type} (f : X -> X) (x : X) : X := match n with | O => x | S n' => f (iter n' f x) end. Definition comp {X : Type} (R S : X -> X -> Prop) (x z : X) : Prop := exists y, R x y /\ S y z. Definition stari {X : Type} (R : X -> X -> Prop) (x y : X) := exists n, iter n (comp R) (fun x y => x=y) x y. (*** Exercise 7.7 ***) Goal forall (X : Type) (R : X -> X-> Prop) (x y : X), star R x y <-> stari R x y. Proof. split. intros A. induction A. exists 0. reflexivity. destruct IHA as [n B]. exists (S n). simpl. exists y. tauto. intros [n A]. revert x y A. induction n ;simpl. intros x y A. rewrite A. now constructor. intros x y [x' [A B]]. apply (starT X R x x') ; now auto. Qed. 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 rel : Type := state -> state -> Prop. Definition functional (r : rel) : Prop := forall s s' s'', r s s' -> r s s'' -> s'=s''. (* *** Equivalence *) Definition rap (r r' : rel) : Prop := forall s s', r s s' -> r' s s'. Definition req (r r' : rel) : Prop := rap r r' /\ rap r' r. (*** Exercise 7.8 a - use firstorder ***) Goal forall r r' : rel, rap r r' -> functional r' -> functional r. Proof. firstorder. Qed. (*** Exercise 7.8 b - use eauto ***) Goal forall r r' : rel, rap r r' -> functional r' -> functional r. Proof. intros r r' A B s s' s'' C D. eauto. Qed. (*** Exercise 7.8 c - use eapply and eassumption ***) Goal forall r r' : rel, rap r r' -> functional r' -> functional r. Proof. intros r r' A B s s' s'' C D. eapply B; eapply A; eassumption. Qed. End abstract_Imp. (*** For Exercise 7.9, see the Coq code from the lecture on Nov 30. ***) Inductive even : nat -> Prop := | evenO : even 0 | evenS : forall n, even n -> even (S (S n)). (*** Exercise 7.10 ***) Goal forall n, even n -> even (S n) -> False. apply (even_ind (fun n => even (S n) -> False)). intros A. now inversion A. intros n A IHA B. inversion B. auto. Qed.