Library rewriting_with_some_implicits_rules
Section Relation_Definition.
Variable A : Type.
Definition relation := A ⇒ A ⇒ Prop.
Variable R : relation.
Variable S : relation.
Section General_Properties_of_Relations.
Definition reflexive : Prop := forall x:A, R x x.
Definition transitive : Prop := forall x y z:A, R x y ⇒ R y z ⇒ R x z.
Definition symmetric : Prop := forall x y:A, R x y ⇒ R y x.
Definition antisymmetric : Prop := forall x y:A, R x y ⇒ R y x ⇒ x = y.
Definition equiv := reflexive /\ transitive /\ symmetric.
Definition composition : relation ⇒ relation ⇒ relation :=
fun R1 R2 : relation => fun x y : A => exists z : A, R1 x z /\ R2 z y.
Definition union : relation ⇒ relation ⇒ relation :=
fun R1 R2 : relation => fun x y : A => R1 x y \/ R2 x y.
Definition commutation : Prop := forall x y z:A, R x y ⇒ S y z ⇒ exists w, S x w /\ R w z.
Definition commutation_bis :Prop := forall x y z:A, R x y ⇒ S x z ⇒ exists w, S y w /\ R z w.
Definition Rlr := fun R:relation => fun x y => R x y \/ R y x.
Inductive Rstar : A⇒A⇒Prop :=
|Rstar_cont_eq : forall x y, x=y->(Rstar x y)
|Rstar_cont_ind : forall x y z, (R x y)->(Rstar y z)-> (Rstar x z).
Definition Rlrstar := fun R:relation => fun x y => Rstar x y \/ R y x.
Definition Roreq :=fun R:relation => fun x y => x=y \/ R x y.
Definition joinable := fun R:relation => fun x y => exists z, (Rstar x z) /\ (Rstar y z).
Definition weak_commutation_in (x:A) :=
forall y z:A, R x y ⇒ S x z ⇒ exists t, S y t /\ R z t.
Definition confluence_in (x:A) :=
forall y z:A, Rstar x y ⇒ Rstar x z ⇒ joinable R y z.
Definition local_confluence_in (x:A) :=
forall y z:A, R x y ⇒ R x z ⇒ joinable R y z.
Definition strong_confluence_in (x:A) :=
forall y z:A, R x y ⇒ R x z ⇒ exists t, Roreq R y t /\ Rstar z t.
Definition semi_confluence_in (x:A) :=
forall y z:A, R x y ⇒ Rstar x z ⇒ joinable R y z.
Definition diamond_property_in (x:A) :=
forall y z:A, R x y ⇒ R x z ⇒ exists t, R y t /\ R z t.
Definition confluence := forall x, confluence_in x.
Definition local_confluence := forall x, local_confluence_in x.
Definition semi_confluence := forall x, semi_confluence_in x.
Definition strong_confluence := forall x, strong_confluence_in x.
Definition diamond_property := forall x,diamond_property_in x.
Definition noetherian :=
forall (P:A ⇒ Prop),
(forall y:A, (forall z:A, R y z ⇒ P z) ⇒ P y) ⇒ forall x:A, P x.
End General_Properties_of_Relations.
End Relation_Definition.
Implicit Arguments composition [A].
Implicit Arguments transitive [A].
Implicit Arguments commutation [A].
Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
Hint Unfold composition commutation joinable confluence local_confluence.
Variable S : Type.
Ltac conclusion_aux t :=
match t with
| ?P1 ⇒ ?P2 => conclusion_aux P2
| _ => t
end.
Ltac decompose_and_clear id :=
progress (decompose [or and ex] id);clear id.
Ltac apply_decompose H :=
let t := type of H in
let conc := conclusion_aux t in
let id:= fresh in
(assert (id:conc);[auto|try decompose_and_clear id]).
Ltac unfold_all := unfold reflexive, transitive, antisymmetric, symmetric,
confluence, confluence_in,
composition, commutation, commutation_bis,
joinable,
local_confluence, local_confluence_in,
strong_confluence, strong_confluence_in,
semi_confluence, semi_confluence_in
in *.
Ltac apply_diagram H :=
let id:=fresh in
(assert (id:=H);apply_decompose id;clear id);unfold_all.
Ltac conclusion := eauto.
Ltac substitute x := subst x.
Ltac debut := unfold_all;intros.
Ltac treat_equality :=
match goal with
| H:(?X1 = ?X2) |- _ => substitute X2
end.
Ltac my_induction_1 H := induction H;[treat_equality|idtac].
Ltac Rconclusion := eauto with Rules.
Ltac Rapply_diagram H := apply_diagram H;[idtac|eauto with Rules].
Section one_relation.
Variable R: relation S.
Infix "→" := R (at level 50, no associativity).
Notation "x →* y" := (Rstar S R x y) (at level 50, no associativity).
Notation "x →=? y" := (Roreq S R x y) (at level 50, no associativity).
Lemma Rstar_equality : forall x , x →* x.
Proof.
debut.
apply_diagram (Rstar_cont_eq S R x x).
conclusion.
Qed.
Hint Resolve Rstar_equality : Rules.
Lemma Rstar_cont_R : forall x y, (x → y)-> x →* y.
Proof.
debut.
apply_diagram (Rstar_equality y).
apply_diagram (Rstar_cont_ind S R x y y).
conclusion.
Qed.
Hint Resolve Rstar_cont_R : Rules.
Lemma Rstar_transitivity : forall x y z : S, x →* y ⇒ y →* z ⇒ x →* z.
Proof.
debut.
my_induction_1 H.
conclusion.
apply_diagram IHRstar.
apply_diagram (Rstar_cont_ind S R x y z).
conclusion.
Qed.
Hint Resolve Rstar_transitivity : Rules.
Lemma Rstar_cases : forall x y, x →* y ⇒ x=y \/ exists y', x → y' /\ y' →* y.
Proof.
debut.
destruct H.
conclusion.
conclusion.
Qed.
Theorem newman :
local_confluence S R ⇒ noetherian S R ⇒ confluence S R.
Proof.
intros.
assert (ind:=H0 (confluence_in S R));clear H0.
unfold confluence.
apply ind;clear ind.
unfold confluence_in.
debut.
rename y into x.
rename y0 into y.
apply_diagram (Rstar_cases x y).
substitute y.
Rconclusion.
apply_diagram (Rstar_cases x z).
substitute z.
Rconclusion.
apply_diagram (H x x0 x1).
apply_diagram (H0 x0).
apply_diagram (H4 y x2).
apply_diagram (Rstar_transitivity x1 x2 x3).
apply_diagram (H0 x1).
apply_diagram (H12 x3 z).
apply_diagram (Rstar_transitivity y x3 x4).
Rconclusion.
Qed.
Lemma l3 : semi_confluence S R ⇒ confluence S R.
Proof.
unfold semi_confluence, semi_confluence_in, confluence, confluence_in, joinable.
intros H x y z H1.
generalize z.
my_induction_1 H1.
debut.
Rconclusion.
debut.
apply_diagram (H x y z1).
apply_diagram (IHRstar x0).
Rconclusion.
Qed.
Lemma Roreq_cases : forall x y, Roreq S R x y ⇒ x = y \/ x → y.
Proof.
debut.
conclusion.
Qed.
Lemma l4 : strong_confluence S R ⇒ semi_confluence S R.
Proof.
intros.
unfold semi_confluence, semi_confluence_in.
cut (forall x z : S, x →* z ⇒ forall y, x → y ⇒ joinable S R R y z);[eauto|idtac].
intros x z H1.
my_induction_1 H1.
debut.
Rconclusion.
rename y into x'.
debut.
apply_diagram (H x x' y).
apply_diagram (Roreq_cases x' x0).
substitute x0.
Rconclusion.
apply_diagram (IHRstar x0).
Rconclusion.
Qed.
Theorem th4 : strong_confluence S R ⇒ confluence S R.
Proof.
debut.
apply_diagram l4.
apply_diagram l3.
conclusion.
Qed.
End one_relation.
Hint Resolve Rstar_transitivity Rstar_equality Rstar_cont_R : Rules.
Section two_relations.
Variable R1: relation S.
Variable R2: relation S.
Infix "°" := composition (at level 60, no associativity).
Notation "x →₁ y" := (R1 x y) (at level 50, no associativity).
Notation "x →₂ y" := (R2 x y) (at level 50, no associativity).
Notation "x →₁* y" := (Rstar S R1 x y) (at level 50, no associativity).
Notation "x →₂* y" := (Rstar S R2 x y) (at level 50, no associativity).
Notation "x →₁₂* y" := (Rstar S (union S R1 R2) x y) (at level 50, no associativity).
Notation "x →₁₂ y" := (union S R1 R2 x y) (at level 50, no associativity).
Theorem example1 :
transitive R1 ⇒ transitive R2 ⇒ commutation R2 R1 ⇒ transitive (R1 ° R2).
Proof.
debut.
apply_diagram H2;clear H2.
apply_diagram H3;clear H3.
apply_diagram (H1 x0 y x1).
apply_diagram (H x x0 x2).
apply_diagram (H0 x2 x1 z).
conclusion.
Qed.
Lemma union_R : forall x y, x →₁ y ⇒x →₁₂ y.
Proof.
debut.
apply_diagram H.
unfold union;conclusion.
Qed.
Lemma union_R_rev : forall x y, x →₂ y ⇒x →₁₂ y.
Proof.
intros.
apply_diagram H.
unfold union;conclusion.
Qed.
Hint Resolve union_R union_R_rev : Rules.
Lemma cases_union : forall x y, x →₁₂ y ⇒ x →₁ y \/ x →₂ y.
Proof.
debut.
conclusion.
Qed.
Lemma union_Rstar : forall x y, x →₁* y ⇒x →₁₂* y.
Proof.
debut.
my_induction_1 H.
Rconclusion.
Rconclusion.
Qed.
Lemma union_Rstar_rev : forall x y, x →₂* y ⇒x →₁₂* y.
Proof.
debut.
my_induction_1 H.
Rconclusion.
Rconclusion.
Qed.
Hint Resolve union_Rstar_rev union_Rstar : Rules.
Lemma commutation_union_aux :
confluence S R1 ⇒
commutation_bis S (Rstar S R1) (Rstar S R2) ⇒
forall x y z, x →₁* y ⇒x →₁₂* z ⇒ exists t, y →₁₂* t /\ z →₁₂* t.
Proof.
intros H1 H2.
cut (forall x z : S, x →₁₂* z ⇒ forall y, x →₁* y ⇒ exists t, y →₁₂* t /\ z →₁₂* t).
eauto.
intros x z H3.
my_induction_1 H3.
debut.
Rconclusion.
rename y into z'.
debut.
apply_diagram (cases_union x z').
apply_diagram (Rstar_cont_R R1 x z').
apply_diagram (H1 x y z').
apply_diagram (IHRstar x0).
Rconclusion.
apply_diagram (Rstar_cont_R R2 x z').
apply_diagram (H2 x y z').
apply_diagram (IHRstar x0).
Rconclusion.
Qed.
End two_relations.