Library rewriting
Julien Narboux
A diagrammatic formalization of abstract rewriting
Section Relation_Definition.
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.
Composition of two relations
Definition composition : relation ⇒ relation ⇒ relation :=
fun R1 R2 : relation => fun x y : A => exists z : A, R1 x z /\ R2 z y.
Union of two relations
Definition union : relation ⇒ relation ⇒ relation :=
fun R1 R2 : relation => fun x y : A => R1 x y \/ R2 x y.
Definition of swappable and commutation
The two definitions appear under the name of "commutation" in the literature
Definition swappable : Prop := forall x y z:A, R x y ⇒ S y z ⇒ exists w, S x w /\ R w z.
Definition commutation :Prop := forall x y z:A, R x y ⇒ S x z ⇒ exists w, S y w /\ R z w.
Reflexive closure
Definition Roreq :=fun R:relation => fun x y => x=y \/ R x y.
Symmetric closure
Definition Rlr := fun R:relation => fun x y => R x y \/ R y x.
Symmetric transitive closure
Inductive Rstar : A⇒A⇒Prop :=
|Rstar_cont_eq : forall x, Rstar x x
|Rstar_induction : forall x y z, R x y⇒ Rstar y z⇒ Rstar x z.
Transitive closure
Inductive Rplus : A⇒A⇒Prop :=
|Rplus_cont_R : forall x y, R x y ⇒ Rplus x y
|Rplus_induction : forall x y z, R x y⇒ Rplus y z⇒ Rplus x z.
Reflexive, transitive, symmetric closure
Inductive Rlrstar : A⇒A⇒Prop :=
|Rlrstar_cont_R : forall x y, R x y ⇒ Rlrstar x y
|Rlrstar_cont_R_rev : forall x y, R y x ⇒ Rlrstar x y
|Rlrstar_cont_eq : forall x, Rlrstar x x
|Rlrstar_induction : forall x y z, Rlrstar x y⇒ Rlrstar y z⇒ Rlrstar x z.
Definition joinable := fun R:relation => fun x y => exists z, (Rstar x z) /\ (Rstar y z).
Definition church_rosser := forall x y, Rlrstar x y ⇒ joinable R x y.
Path of length n
Inductive Rn : nat ⇒ A ⇒ A ⇒ Prop :=
|Rn_0 : forall x, Rn 0 x x
|Rn_1 : forall x y, R x y ⇒ Rn 1 x y
|Rn_induction : forall x y z n, R x y⇒ Rn n y z⇒ Rn (n+1) x 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 isNF := fun x => ~ (exists y, R x y).
Definition isWN := fun x => exists y, Rstar x y /\ isNF y.
Definition reduces_to_normal_form := fun x y => Rstar x y /\ isNF y.
Definition WN := fun R:relation => forall x, isWN x.
Inductive isSN : A ⇒ Prop :=
|SN_base : forall x, isNF x ⇒ isSN x
|SN_induction : forall x, (forall y, R x y ⇒ isSN y) ⇒ isSN x.
Definition SN := forall x, isSN 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.
Definition convergent := confluence /\ SN.
Lemma SN_implies_noetherian : SN ⇒ noetherian.
Proof.
unfold noetherian.
intros H.
unfold SN in H.
cut (forall x, forall P : A ⇒ Prop,
(forall y : A, (forall z : A, R y z ⇒ P z) ⇒ P y) ⇒ P x).
intros.
apply H0.
apply H1.
intro x;assert (isSN x).
apply H.
induction H0.
intros.
apply H1.
intros.
assert (exists y : A, R x y).
exists z;auto.
unfold isNF in H0;intuition.
intros.
apply H2.
intros.
apply H1.
auto.
assumption.
Qed.
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.
Tactics for diagrammatic-like proofs
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, swappable, commutation,
church_rosser, reduces_to_normal_form,
local_confluence, local_confluence_in,
strong_confluence, strong_confluence_in,
semi_confluence, semi_confluence_in, joinable
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 treat_equality :=
match goal with
| H:(?X1 = ?X2) |- _ => substitute X2
end.
Ltac my_induction_1 H := induction H.
Ltac start := unfold_all;intros.
These tactics uses the implicit rules contained in the Rules hints base.
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" := (Rplus S R x y) (at level 50, no associativity).
Notation "x →=? y" := (Roreq S R x y) (at level 50, no associativity).
Lemma Rstar_cont_R : forall x y, (x → y)-> x →* y.
Proof.
start.
apply_diagram (Rstar_cont_eq S R y).
apply_diagram (Rstar_induction S R x y y).
conclusion.
Qed.
Lemma Rstar_transitivity : forall x y z : S, x →* y ⇒ y →* z ⇒ x →* z.
Proof.
start.
my_induction_1 H.
conclusion.
apply_diagram IHRstar.
apply_diagram (Rstar_induction S R x y z).
conclusion.
Qed.
Lemma Rstar_cases : forall x y, x →* y ⇒ x=y \/ exists y', x → y' /\ y' →* y.
Proof.
start.
destruct H.
conclusion.
conclusion.
Qed.
Lemma Rplus_transitivity : forall x y z : S, x →+ y ⇒ y →+ z ⇒ x →+ z.
Proof.
start.
my_induction_1 H.
apply_diagram (Rplus_induction S R x y z).
conclusion.
apply_diagram IHRstar.
apply_diagram (Rplus_induction S R x y z).
conclusion.
Qed.
Lemma Rstar_cont_Rplus : forall x y : S, x →+ y ⇒ x →* y.
Proof.
start.
my_induction_1 H.
apply_diagram (Rstar_cont_R x y).
conclusion.
apply_diagram (Rstar_induction S R x y z).
conclusion.
Qed.
Lemma Rplus_cases : forall x y, x →+ y ⇒ x → y \/ exists y', x → y' /\ y' →+ y.
Proof.
start.
destruct H.
conclusion.
conclusion.
Qed.
Lemma Rstar_R_Rstar : forall x y z, x →* y ⇒ y → z ⇒ x →* z.
Proof.
start.
apply_diagram (Rstar_cont_R y z).
apply_diagram (Rstar_transitivity x y z).
conclusion.
Qed.
Lemma Rplus_R_Rplus : forall x y z, x →+ y ⇒ y → z ⇒ x →+ z.
Proof.
start.
apply_diagram (Rplus_cont_R S R y z).
apply_diagram (Rplus_transitivity x y z).
conclusion.
Qed.
Lemma Rplus_Rstar_Rplus : forall x y z, x →+ y ⇒ y →* z ⇒ x →+ z.
Proof.
start.
my_induction_1 H0.
conclusion.
apply_diagram (Rplus_R_Rplus x x0 y).
apply_diagram IHRstar.
conclusion.
Qed.
Lemma R_Rstar_Rplus : forall x y z, x → y ⇒ y →* z ⇒ x →+ z.
Proof.
start.
apply_diagram (Rplus_cont_R S R x y).
apply_diagram (Rplus_Rstar_Rplus x y z).
conclusion.
Qed.
Lemma Rstar_cases_2 : forall x y, x →* y ⇒ x=y \/ x →+ y.
Proof.
start.
apply_diagram (Rstar_cases x y).
conclusion.
apply_diagram (R_Rstar_Rplus x x0 y).
conclusion.
Qed.
Lemma Rstar_finite_path : forall x y, x →* y ⇒ exists n, Rn S R n x y.
Proof.
start.
my_induction_1 H.
exists 0.
apply Rn_0.
elim IHRstar;intros.
exists (x0+1).
eapply Rn_induction;eauto.
Qed.
Require Import Ring.
Require Import Arith.
Lemma aux : forall x:nat, x+1 > 0.
Proof.
intros.
assert (~ Datatypes.S x <= 0).
apply le_Sn_O.
intuition.
Qed.
Lemma aux2 : forall x:nat, x+1 <> 0.
Proof.
intros.
assert (x+1 > 0).
apply aux;auto.
unfold gt in H.
unfold lt in H.
unfold not;intro.
rewrite H0 in H.
assert (0 <= 1).
auto.
assert (1=0).
apply le_antisym;auto.
discriminate.
Qed.
Lemma Rplus_finite_path_non_null : forall x y, x →+ y ⇒ exists n, n<>0 /\ Rn S R n x y.
Proof.
start.
my_induction_1 H.
exists 1.
split; try apply Rn_1;auto.
elim IHRplus;intros.
exists (x0+1).
split.
apply aux2.
intuition.
eapply Rn_induction;eauto.
Qed.
Lemma SN_Rplus_R : SN S (Rplus S R) ⇒ SN S R.
unfold SN.
intros.
assert (isSN S (Rplus S R) x);auto.
induction H0.
apply SN_base.
unfold isNF in *.
unfold not;intro.
decompose [ex] H1.
assert (exists y : S, x →+ y).
exists x0.
apply Rplus_cont_R.
auto.
intuition.
apply SN_induction.
intros.
apply H1.
apply Rplus_cont_R.
auto.
Qed.
Theorem newman :
local_confluence S R ⇒ noetherian S R ⇒ confluence S R.
Proof.
intros.
induction
assert (ind:=H0 (confluence_in S R));clear H0.
unfold confluence.
apply ind;clear ind.
unfold confluence_in.
start.
rename y into x.
rename y0 into y.
First degenerated case
apply_diagram (Rstar_cases x y).
substitute y.
apply_diagram (Rstar_cont_eq S R z).
conclusion.
Second degenrated case
apply_diagram (Rstar_cases x z).
substitute z.
apply_diagram (Rstar_cont_eq S R y).
conclusion.
General case
start.
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).
conclusion.
Qed.
A second version of the Newman's lemma using implicit star_transitivity...
Hint Resolve Rstar_cont_R Rstar_cont_eq Rstar_transitivity : Rules.
Theorem newman_shorter :
local_confluence S R ⇒ noetherian S R ⇒ confluence S R.
Proof.
intros.
induction
assert (ind:=H0 (confluence_in S R));clear H0.
unfold confluence;apply ind;clear ind;unfold confluence_in.
start.
rename y into x.
rename y0 into y.
First degenerated case
apply_diagram (Rstar_cases x y).
substitute y.
Rconclusion.
Second degenrated case
apply_diagram (Rstar_cases x z).
substitute z.
Rconclusion.
General case
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).
Rconclusion.
Qed.
Lemma Rlrstar_cont_Rstar : forall x y, x →* y ⇒ Rlrstar S R x y.
Proof.
intros.
induction H.
apply Rlrstar_cont_eq.
apply_diagram (Rlrstar_cont_R S R x y).
eapply Rlrstar_induction.
apply H2.
auto.
Qed.
Lemma Rlrstar_symmetry : forall x y, Rlrstar S R x y ⇒ Rlrstar S R y x.
Proof.
intros.
induction H.
apply Rlrstar_cont_R_rev;auto.
apply Rlrstar_cont_R;auto.
apply Rlrstar_cont_eq;auto.
eapply Rlrstar_induction.
apply IHRlrstar2.
apply IHRlrstar1.
Qed.
Lemma R_R_Rlrstar : forall x y z, x →* y ⇒ x →* z ⇒ Rlrstar S R y z.
Proof.
intros.
apply_diagram (Rlrstar_cont_Rstar x y).
apply_diagram (Rlrstar_cont_Rstar x z).
eapply Rlrstar_induction.
apply_diagram (Rlrstar_symmetry x y).
apply H4.
apply H3.
Qed.
Lemma church_rosser_confluence : church_rosser S R ⇒ confluence S R.
start.
apply_diagram (R_R_Rlrstar x y z).
apply_diagram (H y z).
conclusion.
Qed.
Lemma confluence_church_rosser : confluence S R ⇒ church_rosser S R.
Proof.
start.
my_induction_1 H0.
apply_diagram (Rstar_cont_R x y).
apply_diagram (Rstar_cont_eq S R y).
conclusion.
apply_diagram (Rstar_cont_R y x).
apply_diagram (Rstar_cont_eq S R x).
conclusion.
apply_diagram (Rstar_cont_eq S R x).
conclusion.
apply_diagram IHRlrstar1.
apply_diagram IHRlrstar2.
apply_diagram (H y x0 x1).
apply_diagram (Rstar_transitivity x x0 x2).
apply_diagram (Rstar_transitivity z x1 x2).
conclusion.
Qed.
Lemma confluence_semi_confluence : confluence S R ⇒ semi_confluence S R.
Proof.
start.
apply_diagram (Rstar_cont_R x y).
apply_diagram (H x y z).
conclusion.
Qed.
Lemma semi_confluence_confluence : 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.
start.
apply_diagram (Rstar_cont_eq S R z0).
conclusion.
start.
apply_diagram (H x y z1).
apply_diagram (IHRstar x0).
apply_diagram (Rstar_transitivity z1 x0 x1).
apply_diagram (Rstar_induction S R x y z0).
apply_diagram (Rstar_transitivity x z0 x1).
conclusion.
Qed.
Lemma Roreq_cases : forall x y, Roreq S R x y ⇒ x = y \/ x → y.
Proof.
start.
conclusion.
Qed.
Lemma strong_confluence_semi_confluence : 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.
start.
apply_diagram (Rstar_cont_R x y).
apply_diagram (Rstar_cont_eq S R y).
conclusion.
rename y into x'.
start.
apply_diagram (H x x' y).
apply_diagram (Roreq_cases x' x0).
substitute x0.
apply_diagram (Rstar_transitivity y x' z).
apply_diagram (Rstar_cont_eq S R z).
conclusion.
apply_diagram (IHRstar x0).
apply_diagram (Rstar_transitivity y x0 x1).
conclusion.
Qed.
Theorem strong_confluence_confluence : strong_confluence S R ⇒ confluence S R.
Proof.
start.
apply_diagram strong_confluence_semi_confluence.
apply_diagram semi_confluence_confluence.
conclusion.
Qed.
Lemma confluence_normal_form_1 :
confluence S R ⇒ forall x y, Rlrstar S R x y ⇒ isNF S R y ⇒ x→* y.
Proof.
start.
apply_diagram (confluence_church_rosser).
apply_diagram (H3 x y).
apply_diagram (Rstar_cases y x0).
substitute x0.
conclusion.
unfold isNF in H1.
assert (exists y0, y→ y0).
conclusion.
intuition.
Qed.
Lemma confluence_normal_form_2 :
confluence S R ⇒ forall x y, Rlrstar S R x y ⇒ isNF S R x ⇒ isNF S R y ⇒
x = y.
Proof.
start.
apply_diagram (confluence_church_rosser).
apply_diagram (H4 x y).
apply_diagram (Rstar_cases y x0).
substitute x0.
apply_diagram (Rstar_cases x y).
auto.
assert (exists y0, x→ y0).
conclusion.
unfold isNF in *.
intuition.
assert (exists y0, y→ y0).
conclusion.
unfold isNF in *.
intuition.
Qed.
Lemma confluence_normal_form_unicity : confluence S R ⇒ forall x y y',
reduces_to_normal_form S R x y ⇒ reduces_to_normal_form S R x y' ⇒ y=y'.
Proof.
start.
intuition.
apply_diagram (R_R_Rlrstar x y y').
apply_diagram (confluence_normal_form_2 H y y').
conclusion.
Qed.
End one_relation.
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 ⇒ swappable S R2 R1 ⇒ transitive (R1 ° R2).
Proof.
start.
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.
start.
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.
Lemma union_Rstar : forall x y, x →₁* y ⇒x →₁₂* y.
Proof.
start.
my_induction_1 H.
apply_diagram (Rstar_cont_eq S (union S R1 R2) x).
conclusion.
apply_diagram (union_R x y).
apply_diagram (Rstar_induction S (union S R1 R2) x y z).
conclusion.
Qed.
Lemma cases_union : forall x y, x →₁₂ y ⇒ x →₁ y \/ x →₂ y.
Proof.
start.
conclusion.
Qed.
Lemma union_Rstar_rev : forall x y, x →₂* y ⇒x →₁₂* y.
Proof.
start.
my_induction_1 H.
apply_diagram (Rstar_cont_eq S (union S R1 R2) x).
conclusion.
apply_diagram (union_R_rev x y).
apply_diagram (Rstar_induction S (union S R1 R2) x y z).
conclusion.
Qed.
Lemma union_star_star_union :
forall x y, Rstar S (union S R1 R2) x y ⇒ Rstar S (union S (Rstar S R1) (Rstar S R2)) x y.
Proof.
start.
induction H.
apply_diagram (Rstar_cont_eq S (union S (Rstar S R1) (Rstar S R2)) x).
conclusion.
apply_diagram (cases_union x y).
apply_diagram (Rstar_cont_R R1 x y).
assert ((union S (Rstar S R1) (Rstar S R2)) x y).
left;auto.
eapply Rstar_induction.
apply H1.
auto.
apply_diagram (Rstar_cont_R R2 x y).
assert ((union S (Rstar S R1) (Rstar S R2)) x y).
right;auto.
eapply Rstar_induction.
apply H1.
auto.
Qed.
Lemma commutation_union_simple :
confluence S R1 ⇒
commutation (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.
start.
apply_diagram (Rstar_cont_eq S (union S R1 R2) y).
apply_diagram (union_Rstar x y).
conclusion.
rename y into z'.
start.
apply_diagram (cases_union x z').
apply_diagram (Rstar_cont_R R1 x z').
apply_diagram (H1 x y z').
apply_diagram (IHRstar x0).
apply_diagram (union_Rstar y x0).
apply_diagram (Rstar_transitivity (union S R1 R2) y x0 x1).
conclusion.
apply_diagram (Rstar_cont_R R2 x z').
apply_diagram (H2 x y z').
apply_diagram (IHRstar x0).
apply_diagram (union_Rstar_rev y x0).
apply_diagram (Rstar_transitivity (union S R1 R2) y x0 x1).
conclusion.
Qed.
Lemma confluence_star_eq_confluence :
confluence S R1 ⇒
(forall x y, x →₁* y ⇒ x →₂* y) ⇒
(forall x y, x →₂* y ⇒ x →₁* y) ⇒
confluence S R2.
Proof.
start.
apply_diagram (H1 x y).
apply_diagram (H1 x z).
apply_diagram (H x y z).
apply_diagram (H0 y x0).
apply_diagram (H0 z x0).
conclusion.
Qed.
Lemma inclusion_start_eq :
(forall x y, x →₁ y ⇒ x →₂ y) ⇒
(forall x y, x →₂ y ⇒ x →₁* y) ⇒
(forall x y, x →₁* y ⇒ x →₂* y) /\
(forall x y, x →₂* y ⇒ x →₁* y).
Proof.
start.
split.
start.
induction H1.
apply_diagram (Rstar_cont_eq S R2 x).
conclusion.
apply_diagram (H x y).
apply_diagram (Rstar_cont_R R2 x y).
apply_diagram (Rstar_transitivity R2 x y z).
conclusion.
start.
induction H1.
apply_diagram (Rstar_cont_eq S R1 x).
conclusion.
apply_diagram (H0 x y).
apply_diagram (Rstar_transitivity R1 x y z).
conclusion.
Qed.
End two_relations.