Library ARS
Require Export Base.
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).
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.
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.
-
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 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).
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.
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.
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, _).
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.
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.