Library doc.html.Rel
This file provides some proofs of properties on relations (notably
combination for confluence and well-foundedness) formalized in the
Coq proof assistant (version 8.2-1).
Version: August 2009
Inductive union {A} (R1 R2: relation A) (x y: A): Prop :=
| Left : R1 x y → union R1 R2 x y
| Right : R2 x y → union R1 R2 x y.
Definition concat {A} (R1 R2: relation A) x y :=
∃ z, R1 x z ∧ R2 z y.
Definition sub_rel {A} (R S: relation A) := ∀ x y, R x y → S x y.
Definition eq_rel {A} (R S: relation A) := ∀ x y, R x y ↔ S x y.
Notation "R ; S" := (concat R S) (at level 65, right associativity) : rel_scope.
Notation "R ∪ S" := (union R S) (at level 65, right associativity) : rel_scope.
Notation "R '⋆'" := (clos_refl_trans R) (at level 29) : rel_scope.
Notation "R '⁺'" := (clos_trans R) (at level 29) : rel_scope.
Notation "R '⁻¹'" := (transp R) (at level 29) : rel_scope.
Notation "R '?'" := (union (@eq _) R) (at level 29) : rel_scope.
Notation "R ⊆ S" := (sub_rel R S) (at level 66) : rel_scope.
Notation "R ≡ S" := (eq_rel R S) (at level 66) : rel_scope.
Definition diamond {A} (R: relation A) := (R; R⁻¹) ⊆ (R⁻¹; R).
Definition confluent {A} (R: relation A) := diamond (R ⋆).
Definition weakly_confluent {A} (R: relation A) := (R; R⁻¹) ⊆ (R ⋆ ⁻¹; R ⋆).
Definition commute {A} (R1 R2: relation A) := (R2 ; R1⁻¹) ⊆ (R1⁻¹ ; R2).
| Left : R1 x y → union R1 R2 x y
| Right : R2 x y → union R1 R2 x y.
Definition concat {A} (R1 R2: relation A) x y :=
∃ z, R1 x z ∧ R2 z y.
Definition sub_rel {A} (R S: relation A) := ∀ x y, R x y → S x y.
Definition eq_rel {A} (R S: relation A) := ∀ x y, R x y ↔ S x y.
Notation "R ; S" := (concat R S) (at level 65, right associativity) : rel_scope.
Notation "R ∪ S" := (union R S) (at level 65, right associativity) : rel_scope.
Notation "R '⋆'" := (clos_refl_trans R) (at level 29) : rel_scope.
Notation "R '⁺'" := (clos_trans R) (at level 29) : rel_scope.
Notation "R '⁻¹'" := (transp R) (at level 29) : rel_scope.
Notation "R '?'" := (union (@eq _) R) (at level 29) : rel_scope.
Notation "R ⊆ S" := (sub_rel R S) (at level 66) : rel_scope.
Notation "R ≡ S" := (eq_rel R S) (at level 66) : rel_scope.
Definition diamond {A} (R: relation A) := (R; R⁻¹) ⊆ (R⁻¹; R).
Definition confluent {A} (R: relation A) := diamond (R ⋆).
Definition weakly_confluent {A} (R: relation A) := (R; R⁻¹) ⊆ (R ⋆ ⁻¹; R ⋆).
Definition commute {A} (R1 R2: relation A) := (R2 ; R1⁻¹) ⊆ (R1⁻¹ ; R2).
Lemma eq_rel_refl A (R: relation A): R ≡ R.
Lemma eq_rel_sym A (R1 R2: relation A): R1 ≡ R2 → R2 ≡ R1.
Lemma eq_rel_trans A (R1 R2 R3: relation A): R1 ≡ R2 → R2 ≡ R3 → R1 ≡ R3.
Add Parametric Relation A : (relation A) (@eq_rel A)
reflexivity proved by (eq_rel_refl A)
symmetry proved by (eq_rel_sym A)
transitivity proved by (eq_rel_trans A)
as eq_rel_setoid.
Lemma eq_rel_sym A (R1 R2: relation A): R1 ≡ R2 → R2 ≡ R1.
Lemma eq_rel_trans A (R1 R2 R3: relation A): R1 ≡ R2 → R2 ≡ R3 → R1 ≡ R3.
Add Parametric Relation A : (relation A) (@eq_rel A)
reflexivity proved by (eq_rel_refl A)
symmetry proved by (eq_rel_sym A)
transitivity proved by (eq_rel_trans A)
as eq_rel_setoid.
Morphisms for relation application
Add Parametric Morphism A : (@id (relation A)) with
signature (@eq_rel A) ==> pointwise_relation A (pointwise_relation A iff) as rel_apply_mor.
Add Parametric Morphism A : (fun (R: relation A) (x y: A) ⇒ R x y) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as rel_apply2_mor.
signature (@eq_rel A) ==> pointwise_relation A (pointwise_relation A iff) as rel_apply_mor.
Add Parametric Morphism A : (fun (R: relation A) (x y: A) ⇒ R x y) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as rel_apply2_mor.
Morphisms for sub_rel
Add Parametric Morphism A : (@sub_rel A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> iff as sub_rel_mor.
signature (@eq_rel A) ==> (@eq_rel A) ==> iff as sub_rel_mor.
Morphisms for union
Add Parametric Morphism A : (@union A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq_rel A) as union_mor.
Add Parametric Morphism A : (@union A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as union_ext_mor.
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq_rel A) as union_mor.
Add Parametric Morphism A : (@union A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as union_ext_mor.
Morphisms for concat
Add Parametric Morphism A : (@concat A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq_rel A) as concat_mor.
Add Parametric Morphism A : (@concat A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as concat_ext_mor.
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq_rel A) as concat_mor.
Add Parametric Morphism A : (@concat A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as concat_ext_mor.
Morphisms for clos_refl_trans
Add Parametric Morphism A : (@clos_refl_trans A) with
signature (@eq_rel A) ==> (@eq_rel A) as clos_refl_trans_mor.
Add Parametric Morphism A : (@clos_refl_trans A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as clos_refl_trans_ext_mor.
signature (@eq_rel A) ==> (@eq_rel A) as clos_refl_trans_mor.
Add Parametric Morphism A : (@clos_refl_trans A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as clos_refl_trans_ext_mor.
Morphisms for clos_trans
Add Parametric Morphism A : (@clos_trans A) with
signature (@eq_rel A) ==> (@eq_rel A) as clos_trans_mor.
Add Parametric Morphism A : (@clos_trans A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as clos_trans_ext_mor.
signature (@eq_rel A) ==> (@eq_rel A) as clos_trans_mor.
Add Parametric Morphism A : (@clos_trans A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as clos_trans_ext_mor.
Morphisms for transp
Add Parametric Morphism A : (@transp A) with
signature (@eq_rel A) ==> (@eq_rel A) as transp_mor.
Add Parametric Morphism A : (@transp A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as transp_ext_mor.
signature (@eq_rel A) ==> (@eq_rel A) as transp_mor.
Add Parametric Morphism A : (@transp A) with
signature (@eq_rel A) ==> (@eq A) ==> (@eq A) ==> iff as transp_ext_mor.
Morphisms for Acc
Add Parametric Morphism A : (@Acc A) with
signature (@eq_rel A) ==> (@eq A) ==> iff as acc_mor.
signature (@eq_rel A) ==> (@eq A) ==> iff as acc_mor.
Morphisms for well_founded
Add Parametric Morphism A : (@well_founded A) with
signature (@eq_rel A) ==> iff as wf_mor.
signature (@eq_rel A) ==> iff as wf_mor.
Morphisms for commute
Add Parametric Morphism A : (@commute A) with
signature (@eq_rel A) ==> (@eq_rel A) ==> iff as commute_mor.
signature (@eq_rel A) ==> (@eq_rel A) ==> iff as commute_mor.
Lemma star_idempotent A (R: relation A):
R ⋆⋆ ≡ R ⋆.
Lemma plus_idempotent A (R: relation A):
R ⁺⁺ ≡ R ⁺.
Lemma plus_star_equiv A (R: relation A):
R ⋆⁺ ≡ R⁺ ⋆.
Lemma star_plus_star_equiv A (R: relation A):
R ⋆⁺ ≡ R ⋆.
Lemma plus_star_star_equiv A (R: relation A):
R⁺ ⋆ ≡ R ⋆.
Lemma plus_star_concat_equiv A (R: relation A):
R⁺ ≡ R ⋆; R.
Lemma plus_star_included A (R: relation A):
R⁺ ⊆ R ⋆.
Lemma concat_assoc A (R1 R2 R3: relation A):
(R1; R2); R3 ≡ R1; (R2; R3).
Lemma star_equiv A (R: relation A):
R ⋆ ≡ R ⋆ ; R ⋆.
Lemma transp_involutive A (R: relation A):
R⁻¹⁻¹ ≡ R.
Lemma transp_concat_commute A (R1 R2: relation A):
(R1; R2)⁻¹ ≡ (R2⁻¹; R1⁻¹).
Lemma transp_star_commute A (R: relation A):
R⁻¹ ⋆ ≡ R ⋆ ⁻¹.
Lemma transp_plus_commute A (R: relation A):
R⁻¹⁺ ≡ R⁺ ⁻¹.
Lemma union_star_equiv A (R1 R2: relation A):
(R1 ∪ R2)⋆ ≡ (R1 ⋆; R2 ⋆)⋆.
Lemma concat_star_included1 A (R1 R2: relation A):
R1 ⋆ ⊆ (R1; R2 ⋆)⋆.
Lemma concat_star_included2 A (R1 R2: relation A):
R2 ⋆ ⊆ (R1 ⋆; R2)⋆.
Lemma union_star_included1 A (R1 R2: relation A):
R1 ⋆ ⊆ (R1 ∪ R2)⋆.
Lemma union_star_included2 A (R1 R2: relation A):
R2 ⋆ ⊆ (R1 ∪ R2)⋆.
Lemma union_star_equiv2 A (R1 R2: relation A):
(R1 ∪ R2)⋆ ≡ (R1 ⋆ ∪ R2 ⋆)⋆.
Lemma union_plus_included1 A (R1 R2: relation A):
R1⁺ ⊆ (R1 ∪ R2)⁺.
Lemma union_plus_included2 A (R1 R2: relation A):
R2⁺ ⊆ (R1 ∪ R2)⁺.
Lemma union_plus_equiv2 A (R1 R2: relation A):
(R1 ∪ R2)⁺ ≡ (R1⁺ ∪ R2⁺)⁺.
Lemma concat_star_equiv A (R1 R2: relation A):
(R1; R2 ⋆) ≡ (R1; R2 ⋆) ; R2 ⋆.
Inductive t_length_clos A (R: relation A) : nat → A → A → Prop :=
| t_length_step : ∀ x y, R x y → t_length_clos A R 1 x y
| t_length_trans : ∀ x y z n,
t_length_clos A R n x y → R y z → t_length_clos A R (1+n) x z.
Lemma t_length_clos_equiv A (R: relation A) :
R ⁺ ≡ (fun x y ⇒ exists n, t_length_clos R n x y).
Lemma t_length_clos_transitivity A (R: relation A) : ∀ n m x y z,
t_length_clos R n x y →
t_length_clos R m y z →
t_length_clos R (n+m) x z.
Lemma t_length_clos_1_step A (R: relation A) :
∀ x y, t_length_clos R 1 x y → R x y.
R ⋆⋆ ≡ R ⋆.
Lemma plus_idempotent A (R: relation A):
R ⁺⁺ ≡ R ⁺.
Lemma plus_star_equiv A (R: relation A):
R ⋆⁺ ≡ R⁺ ⋆.
Lemma star_plus_star_equiv A (R: relation A):
R ⋆⁺ ≡ R ⋆.
Lemma plus_star_star_equiv A (R: relation A):
R⁺ ⋆ ≡ R ⋆.
Lemma plus_star_concat_equiv A (R: relation A):
R⁺ ≡ R ⋆; R.
Lemma plus_star_included A (R: relation A):
R⁺ ⊆ R ⋆.
Lemma concat_assoc A (R1 R2 R3: relation A):
(R1; R2); R3 ≡ R1; (R2; R3).
Lemma star_equiv A (R: relation A):
R ⋆ ≡ R ⋆ ; R ⋆.
Lemma transp_involutive A (R: relation A):
R⁻¹⁻¹ ≡ R.
Lemma transp_concat_commute A (R1 R2: relation A):
(R1; R2)⁻¹ ≡ (R2⁻¹; R1⁻¹).
Lemma transp_star_commute A (R: relation A):
R⁻¹ ⋆ ≡ R ⋆ ⁻¹.
Lemma transp_plus_commute A (R: relation A):
R⁻¹⁺ ≡ R⁺ ⁻¹.
Lemma union_star_equiv A (R1 R2: relation A):
(R1 ∪ R2)⋆ ≡ (R1 ⋆; R2 ⋆)⋆.
Lemma concat_star_included1 A (R1 R2: relation A):
R1 ⋆ ⊆ (R1; R2 ⋆)⋆.
Lemma concat_star_included2 A (R1 R2: relation A):
R2 ⋆ ⊆ (R1 ⋆; R2)⋆.
Lemma union_star_included1 A (R1 R2: relation A):
R1 ⋆ ⊆ (R1 ∪ R2)⋆.
Lemma union_star_included2 A (R1 R2: relation A):
R2 ⋆ ⊆ (R1 ∪ R2)⋆.
Lemma union_star_equiv2 A (R1 R2: relation A):
(R1 ∪ R2)⋆ ≡ (R1 ⋆ ∪ R2 ⋆)⋆.
Lemma union_plus_included1 A (R1 R2: relation A):
R1⁺ ⊆ (R1 ∪ R2)⁺.
Lemma union_plus_included2 A (R1 R2: relation A):
R2⁺ ⊆ (R1 ∪ R2)⁺.
Lemma union_plus_equiv2 A (R1 R2: relation A):
(R1 ∪ R2)⁺ ≡ (R1⁺ ∪ R2⁺)⁺.
Lemma concat_star_equiv A (R1 R2: relation A):
(R1; R2 ⋆) ≡ (R1; R2 ⋆) ; R2 ⋆.
Inductive t_length_clos A (R: relation A) : nat → A → A → Prop :=
| t_length_step : ∀ x y, R x y → t_length_clos A R 1 x y
| t_length_trans : ∀ x y z n,
t_length_clos A R n x y → R y z → t_length_clos A R (1+n) x z.
Lemma t_length_clos_equiv A (R: relation A) :
R ⁺ ≡ (fun x y ⇒ exists n, t_length_clos R n x y).
Lemma t_length_clos_transitivity A (R: relation A) : ∀ n m x y z,
t_length_clos R n x y →
t_length_clos R m y z →
t_length_clos R (n+m) x z.
Lemma t_length_clos_1_step A (R: relation A) :
∀ x y, t_length_clos R 1 x y → R x y.
Lemma commute_sym A (R1 R2: relation A):
commute R1 R2 → commute R2 R1.
Lemma commute_star1 A (R1 R2:relation A):
commute R1 R2 → commute (R1 ⋆) R2.
Lemma commute_star2 A (R1 R2:relation A):
commute R1 R2 → commute R1 (R2 ⋆).
Lemma commute_star A (R1 R2:relation A):
commute R1 R2 → commute (R1 ⋆) (R2 ⋆).
Lemma commute_plus_star A (R1 R2: relation A):
commute (R1⁺) R2 → commute (R1 ⋆) R2.
Lemma commute_union A (R1 R2 R3: relation A):
commute R1 R2 →
commute R1 R3 →
commute R1 (R2 ∪ R3).
Lemma commutation_condition A (R1 R2: relation A):
(R1; R2⁻¹) ⊆ (R2 ⋆ ⁻¹; R1?) →
commute (R1 ⋆) (R2 ⋆).
commute R1 R2 → commute R2 R1.
Lemma commute_star1 A (R1 R2:relation A):
commute R1 R2 → commute (R1 ⋆) R2.
Lemma commute_star2 A (R1 R2:relation A):
commute R1 R2 → commute R1 (R2 ⋆).
Lemma commute_star A (R1 R2:relation A):
commute R1 R2 → commute (R1 ⋆) (R2 ⋆).
Lemma commute_plus_star A (R1 R2: relation A):
commute (R1⁺) R2 → commute (R1 ⋆) R2.
Lemma commute_union A (R1 R2 R3: relation A):
commute R1 R2 →
commute R1 R3 →
commute R1 (R2 ∪ R3).
Lemma commutation_condition A (R1 R2: relation A):
(R1; R2⁻¹) ⊆ (R2 ⋆ ⁻¹; R1?) →
commute (R1 ⋆) (R2 ⋆).
Lemma confluent_commute_star_refl_equiv A (R: relation A):
confluent R ↔ commute (R ⋆) (R ⋆).
Lemma concat_wf_equiv A (R1 R2: relation A):
well_founded (R1 ; R2) → well_founded (R2 ; R1).
Lemma diamond_union A (R1 R2: relation A):
commute R1 R2 →
diamond R1 →
diamond R2 →
diamond (R1 ∪ R2).
Lemma diamond_t_length A (R: relation A) :
diamond R →
∀ n m x y z, t_length_clos R m x z →
t_length_clos R n y z →
exists t, t_length_clos R n t x ∧ t_length_clos R m t y.
Lemma diamond_plus A (R: relation A) :
diamond R → diamond (R⁺).
Lemma diamond_confluent A (R: relation A) :
diamond R → confluent R.
confluent R ↔ commute (R ⋆) (R ⋆).
Lemma concat_wf_equiv A (R1 R2: relation A):
well_founded (R1 ; R2) → well_founded (R2 ; R1).
Lemma diamond_union A (R1 R2: relation A):
commute R1 R2 →
diamond R1 →
diamond R2 →
diamond (R1 ∪ R2).
Lemma diamond_t_length A (R: relation A) :
diamond R →
∀ n m x y z, t_length_clos R m x z →
t_length_clos R n y z →
exists t, t_length_clos R n t x ∧ t_length_clos R m t y.
Lemma diamond_plus A (R: relation A) :
diamond R → diamond (R⁺).
Lemma diamond_confluent A (R: relation A) :
diamond R → confluent R.
Hindley-Rosen lemma, from 'The λ-calculus, its Syntax and
Semantics', H.P. Barendregt, Ch. 3 § 3
Lemma hindley_rosen1 A (R1 R2: relation A):
commute R1 R2 →
diamond R1 →
diamond R2 →
confluent (R1 ∪ R2).
Lemma hindley_rosen2 A (R1 R2: relation A):
commute (R1 ⋆) (R2 ⋆) →
confluent R1 →
confluent R2 →
confluent (R1 ∪ R2).
Lemma newman A (R: relation A):
well_founded R →
weakly_confluent R →
confluent R.
commute R1 R2 →
diamond R1 →
diamond R2 →
confluent (R1 ∪ R2).
Lemma hindley_rosen2 A (R1 R2: relation A):
commute (R1 ⋆) (R2 ⋆) →
confluent R1 →
confluent R2 →
confluent (R1 ∪ R2).
Lemma newman A (R: relation A):
well_founded R →
weakly_confluent R →
confluent R.
Definition nf A (R: relation A) (x: A) :=
∀ y, ~(R y x).
∀ y, ~(R y x).
x is a normal form of y
Definition is_nf_of A (R: relation A) (x y: A) :=
nf R x ∧ (R ⋆) x y.
Definition nf_unique A (R: relation A) :=
∀ x y z, is_nf_of R y x → is_nf_of R z x →
y = z.
nf R x ∧ (R ⋆) x y.
Definition nf_unique A (R: relation A) :=
∀ x y z, is_nf_of R y x → is_nf_of R z x →
y = z.
R1 commutes with R2' normal forms
Definition nf_commute A (R1 R2: relation A) :=
∀ x y x' y',
is_nf_of R2 x' x → is_nf_of R2 y' y →
R1 x y →
(R1⁺) x' y'.
∀ x y x' y',
is_nf_of R2 x' x → is_nf_of R2 y' y →
R1 x y →
(R1⁺) x' y'.
R1 preserves R2's normal forms
Definition preserves_nf A (R1 R2: relation A) :=
∀ x y, nf R2 y → R1 x y → nf R2 x.
∀ x y, nf R2 y → R1 x y → nf R2 x.
Lemma nf_star_eq A (R: relation A):
∀ x y, nf R x → (R ⋆) y x → y = x.
Lemma confluent_nf_unique A (R: relation A):
confluent R → nf_unique R.
∀ x y, nf R x → (R ⋆) y x → y = x.
Lemma confluent_nf_unique A (R: relation A):
confluent R → nf_unique R.
This lemma requires classical logic.
Lemma well_founded_nf_exists A (R: relation A) (x: A) :
well_founded R → exists y, is_nf_of R y x.
Lemma preserves_nf_plus A (R1 R2: relation A):
preserves_nf R1 R2 → preserves_nf (R1⁺) R2.
Lemma preserves_nf_star A (R1 R2: relation A):
preserves_nf R1 R2 → preserves_nf (R1 ⋆) R2.
Lemma nf_commute_plus A (R1 R2: relation A):
confluent R2 → well_founded R2 →
nf_commute R1 R2 →
∀ x y z t, is_nf_of R2 z x → is_nf_of R2 t y → ((R1 ∪ R2)⁺) y x →
(R1 ⋆) t z.
Lemma nf_commute_star A (R1 R2: relation A):
confluent R2 → well_founded R2 →
nf_commute R1 R2 →
∀ x y z t, is_nf_of R2 z x → is_nf_of R2 t y → ((R1 ∪ R2)⋆) y x →
(R1 ⋆) t z.
well_founded R → exists y, is_nf_of R y x.
Lemma preserves_nf_plus A (R1 R2: relation A):
preserves_nf R1 R2 → preserves_nf (R1⁺) R2.
Lemma preserves_nf_star A (R1 R2: relation A):
preserves_nf R1 R2 → preserves_nf (R1 ⋆) R2.
Lemma nf_commute_plus A (R1 R2: relation A):
confluent R2 → well_founded R2 →
nf_commute R1 R2 →
∀ x y z t, is_nf_of R2 z x → is_nf_of R2 t y → ((R1 ∪ R2)⁺) y x →
(R1 ⋆) t z.
Lemma nf_commute_star A (R1 R2: relation A):
confluent R2 → well_founded R2 →
nf_commute R1 R2 →
∀ x y z t, is_nf_of R2 z x → is_nf_of R2 t y → ((R1 ∪ R2)⋆) y x →
(R1 ⋆) t z.
Lemma wf_plus_equiv A (R: relation A):
well_founded (R⁺) ↔ well_founded R.
Lemma union_wf A (R1 R2: relation A):
well_founded (R1 ⋆ ; R2) →
well_founded (R2 ⋆ ; R1) →
well_founded (R1 ∪ R2).
well_founded (R⁺) ↔ well_founded R.
Lemma union_wf A (R1 R2: relation A):
well_founded (R1 ⋆ ; R2) →
well_founded (R2 ⋆ ; R1) →
well_founded (R1 ∪ R2).
Akama's lemmas, from 'On Mints' Reduction for ccc-Calculus', Yohji Akama, TLCA '93
Lemma akama_well_founded A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
nf_commute R1 R2 →
well_founded (R1 ∪ R2).
Lemma akama_confluence A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
nf_commute R1 R2 →
confluent (R1 ∪ R2).
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
nf_commute R1 R2 →
well_founded (R1 ∪ R2).
Lemma akama_confluence A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
nf_commute R1 R2 →
confluent (R1 ∪ R2).
from 'On the Power of Simple Diagrams', Roberto Di Cosmo, RTA '96
Definition of DPG and some lemmas about it
Definition DPG A (R1 R2: relation A) :=
(R2;R1⁻¹) ⊆ (R1⁺ ⁻¹;R2 ⋆).
Lemma commutation_condition_DPG_plus A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
commute (R1⁺) (R2 ⋆).
Lemma commutation_condition_DPG A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
commute (R1 ⋆) (R2 ⋆).
Lemma DPG_diagram1 A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
preserves_nf R1 R2 →
∀ y z, (R2 ⋆; R1 ⋆ ⁻¹) y z → nf R2 y →
exists t, (R1 ⋆) t y ∧ (R2 ⋆) t z ∧ nf R2 t.
Lemma DPG_diagram2 A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
nf_unique R2 → preserves_nf R1 R2 →
nf_commute R1 R2.
(R2;R1⁻¹) ⊆ (R1⁺ ⁻¹;R2 ⋆).
Lemma commutation_condition_DPG_plus A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
commute (R1⁺) (R2 ⋆).
Lemma commutation_condition_DPG A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
commute (R1 ⋆) (R2 ⋆).
Lemma DPG_diagram1 A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
preserves_nf R1 R2 →
∀ y z, (R2 ⋆; R1 ⋆ ⁻¹) y z → nf R2 y →
exists t, (R1 ⋆) t y ∧ (R2 ⋆) t z ∧ nf R2 t.
Lemma DPG_diagram2 A (R1 R2: relation A):
well_founded R1 → DPG R1 R2 →
nf_unique R2 → preserves_nf R1 R2 →
nf_commute R1 R2.
DPG versions of Hindley-Rosen's ans Akama's lemmas
Lemma DPG_hindley_rosen A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → DPG R1 R2 →
confluent (R1 ∪ R2).
Lemma DPG_akama_well_founded A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
DPG R1 R2 → preserves_nf R1 R2 →
well_founded (R1 ∪ R2).
Lemma DPG_akama_confluence A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
DPG R1 R2 → preserves_nf R1 R2 →
confluent (R1 ∪ R2).
confluent R1 → confluent R2 →
well_founded R1 → DPG R1 R2 →
confluent (R1 ∪ R2).
Lemma DPG_akama_well_founded A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
DPG R1 R2 → preserves_nf R1 R2 →
well_founded (R1 ∪ R2).
Lemma DPG_akama_confluence A (R1 R2: relation A):
confluent R1 → confluent R2 →
well_founded R1 → well_founded R2 →
DPG R1 R2 → preserves_nf R1 R2 →
confluent (R1 ∪ R2).
This page has been generated by coqdoc