Library sn_commute
Global Generalizable All Variables.
Global Set Automatic Introduction.
Require Import Utf8 Setoid.
Reserved Infix "∪" (at level 50).
Reserved Notation "A *" (at level 10).
Inductive rtc `(A : relation T) : relation T :=
| rtc_refl t : A* t t
| rtc_step t₁ t₂ t₃ : A t₁ t₂ → A* t₂ t₃ → A* t₁ t₃
where "A *" := (@rtc _ A).
Hint Constructors rtc : trs.
Lemma rtc_trans `(A : relation T) t₁ t₂ t₃ : A* t₁ t₂ → A* t₂ t₃ → A* t₁ t₃.
Proof. induction 1; eauto with trs. Qed.
Hint Resolve rtc_trans : trs.
Inductive SN `(A : relation T) : T → Prop :=
| sn_make t : (∀ t', A t t' → SN A t') → SN A t.
Hint Constructors SN : trs.
Section sn.
Context `(A : relation T).
Lemma sn_step t₁ t₂ : SN A t₁ → A t₁ t₂ → SN A t₂.
Proof. induction 1. eauto. Qed.
Lemma sn_rtc t₁ t₂ : SN A t₁ → A* t₁ t₂ → SN A t₂.
Proof. induction 2; eauto using sn_step with trs. Qed.
End sn.
Hint Resolve sn_step sn_rtc : trs.
Inductive union `(A : relation T) (B : relation T) : relation T :=
| union_right t₁ t₂ : A t₁ t₂ → (A∪B) t₁ t₂
| union_left t₁ t₂ : B t₁ t₂ → (A∪B) t₁ t₂
where "A ∪ B" := (@union _ A B).
Hint Constructors union : trs.
Section sn_commute.
Context `(A : relation T) (B : relation T) (sn_B : ∀ t, SN B t).
Context (commute : ∀ t₁ t₂ t₃, B t₁ t₂ → A t₂ t₃ → ∃ t₄, A t₁ t₄ ∧ (A∪B)* t₄ t₃).
Lemma sn_make_union t₁ : (∀ t₂ t₃, B* t₁ t₂ → A t₂ t₃ → SN (A∪B) t₃) → SN (A∪B) t₁.
Proof.
intros Hsn. induction (sn_B t₁) as [t₁ _ IH].
apply sn_make. intros t₂ Ht₁t₂. destruct Ht₁t₂; eauto with trs.
Qed.
Lemma commute_trc t₁ t₂ t₃ : B* t₁ t₂ → A t₂ t₃ → ∃ t₄, A t₁ t₄ ∧ (A∪B)* t₄ t₃.
Proof.
intros Ht₁t₂ Ht₂t₃. induction Ht₁t₂ as [|t₁ t₂ t₂' Ht₁t₂ Ht₂t₂' IH].
eauto with trs.
destruct (IH Ht₂t₃) as [t₄ [Ht₂t₄ Ht₄t₃]].
destruct (commute _ _ _ Ht₁t₂ Ht₂t₄) as [t₁' [Ht₁t₁' Ht₁'t₄]].
eauto with trs.
Qed.
Lemma commute_sn t : SN A t → SN (A∪B) t.
Proof.
induction 1. apply sn_make_union; auto. intros.
edestruct commute_trc as [?[??]]; eauto with trs.
Qed.
End sn_commute.
Global Set Automatic Introduction.
Require Import Utf8 Setoid.
Reserved Infix "∪" (at level 50).
Reserved Notation "A *" (at level 10).
Inductive rtc `(A : relation T) : relation T :=
| rtc_refl t : A* t t
| rtc_step t₁ t₂ t₃ : A t₁ t₂ → A* t₂ t₃ → A* t₁ t₃
where "A *" := (@rtc _ A).
Hint Constructors rtc : trs.
Lemma rtc_trans `(A : relation T) t₁ t₂ t₃ : A* t₁ t₂ → A* t₂ t₃ → A* t₁ t₃.
Proof. induction 1; eauto with trs. Qed.
Hint Resolve rtc_trans : trs.
Inductive SN `(A : relation T) : T → Prop :=
| sn_make t : (∀ t', A t t' → SN A t') → SN A t.
Hint Constructors SN : trs.
Section sn.
Context `(A : relation T).
Lemma sn_step t₁ t₂ : SN A t₁ → A t₁ t₂ → SN A t₂.
Proof. induction 1. eauto. Qed.
Lemma sn_rtc t₁ t₂ : SN A t₁ → A* t₁ t₂ → SN A t₂.
Proof. induction 2; eauto using sn_step with trs. Qed.
End sn.
Hint Resolve sn_step sn_rtc : trs.
Inductive union `(A : relation T) (B : relation T) : relation T :=
| union_right t₁ t₂ : A t₁ t₂ → (A∪B) t₁ t₂
| union_left t₁ t₂ : B t₁ t₂ → (A∪B) t₁ t₂
where "A ∪ B" := (@union _ A B).
Hint Constructors union : trs.
Section sn_commute.
Context `(A : relation T) (B : relation T) (sn_B : ∀ t, SN B t).
Context (commute : ∀ t₁ t₂ t₃, B t₁ t₂ → A t₂ t₃ → ∃ t₄, A t₁ t₄ ∧ (A∪B)* t₄ t₃).
Lemma sn_make_union t₁ : (∀ t₂ t₃, B* t₁ t₂ → A t₂ t₃ → SN (A∪B) t₃) → SN (A∪B) t₁.
Proof.
intros Hsn. induction (sn_B t₁) as [t₁ _ IH].
apply sn_make. intros t₂ Ht₁t₂. destruct Ht₁t₂; eauto with trs.
Qed.
Lemma commute_trc t₁ t₂ t₃ : B* t₁ t₂ → A t₂ t₃ → ∃ t₄, A t₁ t₄ ∧ (A∪B)* t₄ t₃.
Proof.
intros Ht₁t₂ Ht₂t₃. induction Ht₁t₂ as [|t₁ t₂ t₂' Ht₁t₂ Ht₂t₂' IH].
eauto with trs.
destruct (IH Ht₂t₃) as [t₄ [Ht₂t₄ Ht₄t₃]].
destruct (commute _ _ _ Ht₁t₂ Ht₂t₄) as [t₁' [Ht₁t₁' Ht₁'t₄]].
eauto with trs.
Qed.
Lemma commute_sn t : SN A t → SN (A∪B) t.
Proof.
induction 1. apply sn_make_union; auto. intros.
edestruct commute_trc as [?[??]]; eauto with trs.
Qed.
End sn_commute.