(** * Abstract Reduction Systems *) Set Implicit Arguments. Unset Strict Implicit. Notation "p '<=1' q" := (forall x, p x -> q x) (at level 70). Notation "p '=1' q" := (p <=1 q /\ q <=1 p) (at level 70). 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). (* NB: Notations are not type-checked *) (** Relational composition *) Definition rcomp X Y Z (R : X -> Y -> Prop) (S : Y -> Z -> Prop) : X -> Z -> Prop := fun x z => exists y, R x y /\ S y z. (** Power predicates *) Require Import Arith. Definition it X f n x := @nat_iter n X f x. Definition pow X R n : X -> X -> Prop := it (rcomp R) n eq. Section FixX. 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. (* Making first argument a non-uniform parameter doesn't simplify the induction principle. *) Check star_ind. Lemma star_simpl_ind R (p : X -> Prop) y : p y -> (forall x x', R x x' -> star R x' y -> p x' -> p x) -> forall x, star R x y -> p x. Proof. intros A B. induction 1; eauto. Qed. Goal forall R, transitive (star R). Proof. intros R x y z A B. revert x A. refine (star_simpl_ind _ _). - exact B. - intros x x' C D IH. exact (starC C IH). Qed. Goal forall R, transitive (star R). Proof. intros R x y z A B. induction A as [|x x' y C D IH]. - exact B. - (* IH not simplified *) specialize (IH B). exact (starC C IH). Qed. Lemma star_trans R: transitive (star R). Proof. induction 1; eauto using star. Qed. Lemma star_step R : R <=2 star R. Proof. intros x y A. econstructor. exact A. econstructor. Qed. Goal forall R, star (star R) <=2 star R. Proof. intros R x y. revert x. refine (star_simpl_ind _ _). - apply starR. - intros x x' B C IH. exact (star_trans B IH). Qed. (** Right-to-left induction *) Lemma star_right_ind R (p : X -> Prop) x : p x -> (forall y y', star R x y' -> p y' -> R y' y -> p y) -> forall y, star R x y -> p y. Proof. (* intros A B. induction 1; eauto using star. *) intros A B y C. induction C as [|x x' y D _ IH]. - exact A. - apply IH; clear IH y. + apply (B x' x); auto using starR. + intros y y' E. apply B. eauto using starC. Qed. (** Binary definition *) Inductive rtc R : X -> X -> Prop := | rtcR x : rtc R x x | rtcT x y z : rtc R x y -> rtc R y z -> rtc R x z | rtcC x y : R x y -> rtc R x y. Lemma star_rtc R : star R =2 rtc R. Proof. split; intros x y A. - induction A as [|x x' y C _ IH]. + constructor. + apply rtcT with (y:=x'). * apply rtcC, C. * exact IH. - induction A as [|x x' y _ IHA _ IHB|x y A]. + constructor. + eapply star_trans; eassumption. + apply star_step, A. Qed. Goal forall R, star R =2 rtc R. Proof. split. - induction 1; eauto using rtc. - induction 1; eauto using star, (@star_trans R). (* NB: Instantiation of star_trans needed to unfold reflexive *) Qed. Goal forall R S, R =2 S -> star R =2 rtc S. Proof. intros R S [A B]. split. - induction 1; eauto using rtc. - induction 1; eauto using star, (@star_trans R). Qed. (** Power characterization *) Lemma star_pow R x y : star R x y <-> exists n, pow R n x y. Proof. split; intros A. - induction A as [|x x' y B _ [n IH]]. + exists 0. reflexivity. + exists (S n), x'. auto. - destruct A as [n A]. revert x A. induction n; intros x A. + destruct A. constructor. + destruct A as [x' [A B]]. econstructor; eauto. Qed. (** Normal forms *) Definition reducible R x := exists y, R x y. Definition normal R x := ~ reducible R x. Definition NF R x y := star R x y /\ normal R y. Definition WN R x := exists y, NF R x y. Lemma star_normal R x y : star R x y -> normal R x -> x = y. Proof. intros A B. destruct A as [|x x' y A C]. reflexivity. - exfalso. apply B. exists x'. exact A. 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. Lemma star_ecl R : star R <=2 ecl R. Proof. induction 1; eauto using ecl. Qed. (** Diamond, confluence, Church-Rosser *) Definition joinable R x y := exists z, R x z /\ R y z. Definition diamond R := forall x y z, R x y -> R x z -> joinable R y z. Definition confluent R := diamond (star R). 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). Goal forall R, diamond R -> semi_confluent R. Proof. intros R A x y z B C. revert x C y B. refine (star_simpl_ind _ _). - intros y C. exists y. eauto using star. - intros x x' C D IH y E. destruct (A _ _ _ C E) as [v [F G]]. destruct (IH _ F) as [u [H I]]. assert (J:= starC G H). exists u. eauto using star. Qed. Lemma diamond_to_semi_confluent R : diamond R -> semi_confluent R. Proof. intros A x y z B C. revert y B. induction C as [|x x' z D _ IH]; intros y B. - exists y. eauto using star. - destruct (A _ _ _ B D) as [v [E F]]. destruct (IH _ F) as [u [G H]]. exists u. eauto using star. Qed. Lemma semi_confluent_confluent R : semi_confluent R <-> confluent R. Proof. split; intros A x y z B C. - revert y B. induction C as [|x x' z D _ IH]; intros y B. + exists y. eauto using star. + destruct (A _ _ _ D B) as [v [E F]]. destruct (IH _ E) as [u [G H]]. exists u. eauto using (@star_trans R). - apply (A x y z); eauto using star. Qed. Lemma diamond_to_confluent R : diamond R -> confluent R. Proof. intros A. apply semi_confluent_confluent, diamond_to_semi_confluent, A. Qed. Lemma functional_to_semi_confluent R : functional R -> semi_confluent R. Proof. intros A x y z B C. destruct C as [|x x' z D E]. - exists y. eauto using star. - assert (F:= A _ _ _ B D). subst x'. exists z. eauto using star. Qed. (* NB: Functional does not imply diamond *) Lemma confluent_CR R : church_rosser R <-> confluent R. Proof. split; intros A. - intros x y z B C. apply A. eauto using (@ecl_trans R), star_ecl, (@ecl_sym R). - intros x y B. apply semi_confluent_confluent in A. induction B as [x|x x' y C B IH|x x' y C B IH]. + exists x. eauto using star. + destruct IH as [z [D E]]. exists z. eauto using star. + destruct IH as [u [D E]]. destruct (A _ _ _ C D) as [z [F G]]. exists z. eauto using (@star_trans R). Qed. Lemma confluent_functional_NF R : confluent R -> functional (NF R). Proof. intros A x y z [B C] [D E]. destruct (A _ _ _ B D) as [u [F G]]. apply (star_normal F) in C. apply (star_normal G) in E. congruence. Qed. Lemma CR_ecl_normal_NF R x y : church_rosser R -> ecl R x y -> normal R y -> NF R x y. Proof. intros A B C. apply A in B as [z [B D]]. assert (E := star_normal D C). subst z. hnf. auto. Qed. Lemma CR_ecl_normal_eq R x y : church_rosser R -> normal R x -> normal R y -> ecl R x y -> x = y. Proof. intros A B C D. apply A in D as [z [E F]]. apply (star_normal E) in B. apply (star_normal F) in C. congruence. Qed. (** Triangle Property *) Implicit Types rho : X -> X. Definition triangle R rho := forall x y, R x y -> R y (rho x). Lemma triangle_to_diamond R rho : triangle R rho -> diamond R. Proof. intros T x y z A B. exists (rho x). auto. Qed. (** * Strong Normalization *) Inductive SN R : X -> Prop := | SNI : forall x, R x <=1 SN R -> SN R x. Check SN_ind. Goal forall R x, SN R x <-> R x <=1 SN R. Proof. split. - intros A y B. destruct A. auto. - apply SNI. Qed. Goal forall R x, R x x -> SN R x -> False. Proof. intros R x A B. induction B as [x B IH]. eauto. Qed. Lemma SN_induction R (p : X -> Prop) : (forall x, R x <=1 SN R -> R x <=1 p -> p x) -> SN R <=1 p. Proof. exact (fun sigma => fix F x A := match A with | SNI x' f => sigma x' f (fun y B => F y (f y B)) end). Qed. Definition locally_confluent R := forall x y z, R x y -> R x z -> joinable (star R) y z. Lemma Newman R : (forall x, SN R x) -> locally_confluent R -> confluent R. Proof. intros A B x. specialize (A x). induction A as [x _ IH]. intros y z C D. destruct C as [|x y' y C1 C2]. { exists z. eauto using star. } destruct D as [|x z' z D1 D2]. { exists y. eauto using star. } destruct (B _ _ _ C1 D1) as [u [E F]]. destruct (IH z' D1 u z F D2) as [v [G H]]. destruct (IH y' C1 y v C2) as [w [K L]]. { eauto using (@star_trans R). } exists w. eauto using star, (@star_trans R). Qed. End FixX. Hint Constructors star. Hint Unfold reducible normal NF joinable. Hint Resolve star_step (star_trans : forall X R x, _). (** * Interpolation *) Section Interpolation. Variable X : Type. Implicit Types R S : X -> X -> Prop. Definition stable (p : (X -> X -> Prop) -> Prop) := forall R S, star R =2 star S -> p S -> p R. Lemma confluent_stable : stable (@confluent X). Proof. intros R S [A B] C x y z D E. apply A in D. apply A in E. destruct (C _ _ _ D E) as [u [F G]]. exists u. auto. Qed. Lemma star_mono R S : R <=2 S -> star R <=2 star S. Proof. intros A x y B. induction B ; eauto. Qed. Lemma star_least R S : R <=2 S -> reflexive S -> transitive S -> star R <=2 S. Proof. intros A B C. induction 1 ; eauto. Qed. Lemma star_idempotent R : star (star R) =2 star R. Proof. split. - apply (star_least (R := star R)); hnf; eauto. - auto. Qed. Lemma interpolation R S : R <=2 S -> S <=2 star R -> star R =2 star S. Proof. intros A B. split; intros x y C. - apply (star_mono A), C. - apply star_idempotent. apply (star_mono B), C. Qed. End Interpolation. (** * Evaluation *) Section Evaluation_Defs. Variable X : Type. Implicit Types R : X -> X -> Prop. Implicit Types rho : X -> X. Definition eval R rho x y := exists n, it rho n x = y /\ normal R y. Definition sound R rho := forall x, star R x (rho x). Definition cofinal R rho := forall x y, star R x y -> exists n, star R y (it rho n x). Definition FP rho n x := it rho (S n) x = it rho n x. Lemma sound_stable rho : stable (fun R => @sound R rho). Proof. intros R S [A B] C x. apply B, C. Qed. Lemma cofinal_stable rho : stable (fun R => @cofinal R rho). Proof. intros R S [A B] C x y D. apply A in D. apply C in D as [n D]. eauto. Qed. End Evaluation_Defs. Hint Unfold eval. Section Evaluation. Variable X : Type. Variable R : X -> X -> Prop. Variable rho : X -> X. Section Triangle. Variable T : triangle R rho. Lemma triangle_to_sound : reflexive R -> sound R rho. Proof. intros A x. specialize (A x). apply T in A. auto. Qed. Lemma triangle_rect x y : R x y -> R (rho x) (rho y). Proof. intros A. apply T. apply T. exact A. Qed. Lemma triangle_rect_it x y n : R x y -> R (it rho n x) (it rho n y). Proof. intros A. induction n. exact A. apply triangle_rect, IHn. Qed. Lemma triangle_to_cofinal : cofinal R rho. Proof. intros x y A. induction A as [y|x x' y B A IH]. - exists 0. constructor. - destruct IH as [n IH]. apply (triangle_rect_it n) in B. apply T in B. exists (S n). eauto. Qed. End Triangle. Lemma FP_stat x m n : FP rho m x -> m <= n -> it rho m x = it rho n x. Proof. intros A B. induction B as [|n _ IH]. - reflexivity. - hnf in A. rewrite <- A. change (rho (it rho m x) = rho (it rho n x)). congruence. Qed. Lemma FP_unique m n x : FP rho m x -> FP rho n x -> it rho m x = it rho n x. Proof. intros A B. destruct (le_ge_dec m n) as [C|C]. - apply FP_stat; assumption. - symmetry. apply FP_stat; assumption. Qed. Lemma it_plus m n x : it rho m (it rho n x) = it rho (m + n) x. Proof. revert n. induction m as [|m]; intros n. reflexivity. unfold it. simpl. f_equal. apply IHm. Qed. Variable Sound : sound R rho. Lemma it_sound x n : star R x (it rho n x). Proof. induction n. now constructor. change (star R x (rho (it rho n x))). generalize (Sound (it rho n x)). eauto. Qed. Lemma normal_FP x : normal R x -> rho x = x. Proof. intros A. assert (B := Sound x). symmetry. apply (star_normal B A). Qed. Lemma it_le m n x : m <= n -> star R (it rho m x) (it rho n x). Proof. intros A. induction A as [|n _ IH]. now constructor. apply (star_trans IH). exact (@it_sound _ 1). Qed. Lemma eval_functional : functional (eval R rho). Proof. intros x y y' [m [A' A]] [n [B' B]]. subst y y'. apply normal_FP in A. apply normal_FP in B. apply FP_unique; assumption. Qed. Variable Cofinal : cofinal R rho. Lemma eval_correct : eval R rho =2 NF R. Proof. split; intros x y. - intros [n [A B]]. subst y. split. + apply it_sound. + exact B. - intros [A B]. apply Cofinal in A as [n A]. apply star_normal in A. + subst y. eauto. + exact B. Qed. Lemma rho_to_confluent : confluent R. Proof. intros x y z B C. apply Cofinal in B as [m B]. apply Cofinal in C as [n C]. destruct (le_ge_dec m n) as [D|D]; apply (it_le x) in D; eauto. Qed. Lemma rho_to_not_WN x : rho x = x -> reducible R x -> ~ WN R x. Proof. intros A B [y C]. cut (x = y). { intros D; subst y. apply C. exact B. } apply eval_correct in C as [m [C D]]. subst y. apply normal_FP in D. exact (@FP_unique 0 m x A D). Qed. End Evaluation.