(*** Semantics, Coq part of Assignment 5 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/sem-ws13-forum ***) Set Implicit Arguments. Unset Strict Implicit. (** * Definitions *) Notation "R '<=2' S" := (forall x y, R x y -> S x y) (at level 70). Notation "R '=2' S" := (R <=2 S /\ S <=2 R) (at level 70). Section Fix_X. Variable X : Type. Implicit Types R S : X -> X -> Prop. Implicit Types x y z : X. Definition reflexive R := forall x, R x x. Definition symmetric R := forall x y, R x y -> R y x. Definition transitive R := forall x y z, R x y -> R y z -> R x z. Definition functional R := forall x y z, R x y -> R x z -> y = z. (** * Reflexive Transitive Closure *) Inductive star R : X -> X -> Prop := | starR x : star R x x | starC x y z : R x y -> star R y z -> star R x z. Lemma star_trans R : transitive (star R). Proof. induction 1; eauto using star. Qed. Lemma star_step R : R <=2 star R. Proof. eauto using star. Qed. Lemma star_min R S : R <=2 S -> reflexive S -> transitive S -> star R <=2 S. Proof. induction 4; eauto. Qed. Lemma star_pidempotent R : star (star R) <=2 star R. Proof. apply star_min; eauto using star_trans. constructor. Qed. Lemma star_idempotent R : star (star R) =2 star R. Proof. split. apply star_pidempotent. apply star_step. Qed. Lemma star_mono R S : R <=2 S -> star R <=2 star S. Proof. induction 2; eauto using star. Qed. (** Equivalence closure *) Inductive ecl R : X -> X -> Prop := | eclR x : ecl R x x | eclC x y z : R x y -> ecl R y z -> ecl R x z | eclS x y z : R y x -> ecl R y z -> ecl R x z. Lemma ecl_trans R : transitive (ecl R). Proof. induction 1; eauto using ecl. Qed. Lemma ecl_sym R : symmetric (ecl R). Proof. induction 1; eauto using ecl, (@ecl_trans R). Qed. (** Commutation *) Definition com R S := forall x y z, R x y -> S x z -> exists u, S y u /\ R z u. Definition diamond R := com R R. Definition confluent R := diamond (star R). (** Church-Rosser property *) Definition joinable R x y := exists z, R x z /\ R y z. Definition semi_confluent R := forall x y z, R x y -> star R x z -> joinable (star R) y z. Definition church_rosser R := ecl R <=2 joinable (star R). End Fix_X. (*** Exercise 5.1 ***) Section Ex51. (*** FILL IN HERE ***) End Ex51. (*** Exercise 5.2 ***) Section Ex52. Variable X : Type. Implicit Types R S : X -> X -> Prop. Lemma ecl_mono R S : R <=2 S -> ecl R <=2 ecl S. Proof. (*** FILL IN HERE ***) Admitted. Lemma ecl_min R S : R <=2 S -> reflexive S -> symmetric S -> transitive S -> ecl R <=2 S. Proof. (*** FILL IN HERE ***) Admitted. (* Needs quite a bit of preparation, but the development mirrors star. *) Lemma ecl_idempotent R : ecl (ecl R) =2 ecl R. Proof. (*** FILL IN HERE ***) Admitted. End Ex52. (*** Exercise 5.3 ***) (*** Don't forget to do the second part outside of coq. ***) Section Ex53. Variable X : Type. Implicit Types R S : X -> X -> Prop. Lemma diamond_ext R S : R =2 S -> diamond R -> diamond S. Proof. (*** FILL IN HERE ***) Admitted. Lemma confluent_ext R S : R =2 S -> confluent R -> confluent S. Proof. (*** FILL IN HERE ***) Admitted. Lemma church_rosser_ext R S : R =2 S -> church_rosser R -> church_rosser S. Proof. (*** FILL IN HERE ***) Admitted. End Ex53. (*** Exercise 5.4 ***) Section Ex54. Variable X : Type. Implicit Types R : X -> X -> Prop. Lemma semi_confluent_to_cr R : semi_confluent R -> church_rosser R. Proof. (*** FILL IN HERE ***) Admitted. End Ex54. (*** Exercise 5.5 ***) Section Ex55_p1. Variable X : Type. Variable rho : (X -> X -> Prop) -> X -> X -> Prop. Implicit Types R S : X -> X -> Prop. Hypothesis rho_mono : forall R S, R <=2 S -> rho R <=2 rho S. Hypothesis rho_idem : forall R, rho (rho R) <=2 rho R. Lemma interpolation R S : R <=2 S -> S <=2 rho R -> rho S =2 rho R. Proof. (*** FILL IN HERE ***) Admitted. End Ex55_p1. Section Ex55_p2. Variable X : Type. Implicit Types R S : X -> X -> Prop. Lemma star_interpolation R S : R <=2 S -> S <=2 star R -> star S =2 star R. Proof. (*** FILL IN HERE ***) Admitted. Lemma ecl_interpolation R S : R <=2 S -> S <=2 ecl R -> ecl S =2 ecl R. Proof. (*** FILL IN HERE ***) Admitted. End Ex55_p2. (*** Exercise 5.6 ***) (*** Commutative Union Lemma ***) Section Ex56. Variable X : Type. Implicit Types R S T : X -> X -> Prop. Lemma com_lift_r R S : com R S -> com S (star R). Proof. (*** FILL IN HERE ***) Admitted. Lemma com_lift R S : com R S -> com (star R) (star S). Proof. (*** FILL IN HERE ***) Admitted. Lemma commutative_union R S : confluent R -> confluent S -> com (star R) (star S) -> confluent (fun x y => R x y \/ S x y). Proof. (*** FILL IN HERE ***) Admitted. End Ex56. (**** Don't forget to do Exercise 5.7! ****)