(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 8 ***) (*** Solution ***) Section Relation. Variable X : Type. Definition rel : Type := X -> X -> Prop. Definition reflexive (r : rel) : Prop := forall x, r x x. Definition transitive (r : rel) : Prop := forall x y z, r x y -> r y z -> r x z. Definition functional (r : rel) : Prop := forall x y z, r x y -> r x z -> y=z. Definition normal (r : rel) (x : X) : Prop := ~ exists y, r x y. Definition rap (r r' : rel) : Prop := forall x y, r x y -> r' x y. Definition req (r r' : rel) : Prop := rap r r' /\ rap r' r. (*** Exercise 8.2a ***) Goal forall r, reflexive r -> ~ exists x, normal r x. Proof. intros r A [x B]. apply B. exists x. apply A. Qed. (* Composition *) Definition comp (r s : rel) : rel := fun x z => exists y, r x y /\ s y z. (*** Exercise 8.2b ***) Goal forall r s, functional r -> functional s -> functional (comp r s). Proof. intros r s A B x y y' [z [C1 C2]] [z' [D1 DS2]]. assert (z=z') by eauto. subst. eauto. Qed. (*** Exercise 8.2c: do not use firstorder or eauto ***) Goal forall r s, reflexive r -> reflexive s -> reflexive (comp r s). Proof. intros r s A B x. exists x. split. apply A. apply B. Qed. (*** Exercise 8.2d: do not use firstorder ***) Lemma transitive_rap r s : rap r s -> transitive s -> rap (comp r s) s. Proof. intros A B x y [z [C D]]. eauto. Qed. (*** Exercise 8.2e: do not use firstorder. You may use hnf. ***) Lemma reflexive_rap r s : rap r s -> reflexive s -> rap r (comp r s). Proof. intros A B x y C. hnf. eauto. Qed. (* Star *) Inductive star (r : rel) : rel := | starR x : star r x x | starS x y z : r x y -> star r y z -> star r x z. Lemma star_reflexive r : reflexive (star r). Proof. intros x. constructor. Qed. Lemma star_transitive r : transitive (star r). Proof. intros x y z A B. induction A ; eauto using star. Qed. Goal forall r, req (comp (star r) (star r) ) (star r). Proof. split. apply transitive_rap. hnf ; trivial. apply star_transitive. apply reflexive_rap. hnf ; trivial. apply star_reflexive. Qed. (** Exercise 8.3a **) Lemma star_expansive r : rap r (star r). Proof. hnf. eauto using star. Qed. Lemma star_right r x y z : star r x y -> r y z -> star r x z. Proof. intros A B. induction A ; eauto using star. Qed. Lemma star_ind' (r : rel) (x y : X) (p : X -> Prop) : p y -> ( forall x x', r x x' -> star r x' y -> p x' -> p x) -> star r x y -> p x. Proof. intros A B C. induction C ; eauto. Qed. Definition normal_form (r : rel) : rel := fun x y => star r x y /\ normal r y. (** Exercise 8.3b **) Lemma normal_form_functional (r : rel) : functional r -> functional (normal_form r). Proof. intros A x y z [B C] [D E]. induction B ; destruct D ; trivial. exfalso. apply C. now eauto. exfalso. apply E. now eauto. assert (y=y0) by eauto. subst. auto. Qed. (** Exercise 8.3c **) Lemma star_least r s : reflexive s -> transitive s -> rap r s -> rap (star r) s. Proof. intros R T A x y B. induction B ; eauto. Qed. (** Exercise 8.3d **) Lemma star_idempotent r : req (star (star r)) (star r). Proof. split. apply star_least. apply star_reflexive. apply star_transitive. hnf. trivial. apply star_expansive. Qed. (* Confluence *) Definition joinable (r : rel) (x y : X) : Prop := exists z, r x z /\ r y z. Definition diamond (r : rel) : Prop := forall x y z, r x y -> r x z -> joinable r y z. Definition confluent (r : rel) : Prop := diamond (star r). Definition locally_confluent (r : rel) : Prop := forall x y z, r x y -> r x z -> joinable (star r) y z. (** Exercise 8.4 **) Lemma diamond_confluence' (r : rel) x y z : diamond r -> r x y -> star r x z -> joinable (star r) y z. Proof. intros D A B. revert y A. induction B as [x | x z' z] ; intros y A. now exists y ; eauto using star. assert (C : joinable r y z') by eauto. (* diamond used *) destruct C as [u [C1 C2]]. assert (E : joinable (star r) u z) by eauto. (* IH used *) destruct E as [w [E1 E2]]. exists w. eauto using star. Qed. Theorem diamond_confluence (r : rel) : diamond r -> confluent r. (* star preserves diamond *) Proof. intros D x y z A. revert z ; induction A as [x | x y' y] ; intros z B. now exists z ; eauto using star. assert (C : joinable (star r) y' z) by eauto using diamond_confluence'. destruct C as [u [C1 C2]]. assert (F : joinable (star r) y u) by eauto. (* IH used *) destruct F as [w [F1 F2]]. exists w. intuition. eapply star_transitive ; eauto. Qed. (* Exercise 8.5 *) Lemma joinable_sym (r : rel) x y : joinable r x y -> joinable r y x. Proof. firstorder. Qed. Lemma joinable_1 (r : rel) x y z : r x y -> joinable (star r) y z -> joinable (star r) x z. Proof. intros A [s [B C]]. exists s ; eauto using star. Qed. Lemma joinable_star (r : rel) x y z : star r x y -> joinable (star r) y z -> joinable (star r) x z. Proof. intros A [s [B C]]. exists s. intuition. eapply star_transitive ; eauto. Qed. End Relation.