Set Implicit Arguments.

Require Import Relations.
Require Import LogicUtil.
Require Export SContext.
Require Import RelUtil.

Section definition.

Variable Sig : Signature.

Notation string := (list Sig).

Record rule : Type := mkRule { lhs : string; rhs : string }.

Definition red R : relation string := fun s1 s2 ⇒
  ∃ l, ∃ r, ∃ c,
    In (mkRule l r) R ∧ s1 = fill c l ∧ s2 = fill c r.

Definition red_mod E R := red E # @ red R.

End definition.

Implicit Arguments mkRule [Sig].

Ltac redtac := repeat
  match goal with
    | H : red _ ?t ?u |- _ ⇒
      let l := fresh "l" in let r := fresh "r" in let c := fresh "c" in
      let h1 := fresh in
      (unfold red in H; destruct H as [l]; destruct H as [r];
        destruct H as [c]; destruct H as [H h1]; destruct h1)
    | H : red_mod _ _ _ _ |- _ ⇒ do 2 destruct H; redtac
  end.

Section S.

Variable Sig : Signature.

Notation string := (list Sig).
Notation rule := (rule Sig).

Variable R : list rule.

Lemma red_rule : ∀ l r c, In (mkRule l r) R → red R (fill c l) (fill c r).

Proof.
intros. unfold red. ∃ l. ∃ r. ∃ c. auto.
Qed.

Lemma red_fill : ∀ c t u, red R t u → red R (fill c t) (fill c u).

Proof.
intros. redtac. unfold red.
∃ l. ∃ r. ∃ (comp c c0). split. assumption.
subst t. subst u. do 2 rewrite fill_comp. auto.
Qed.

Lemma red_nil : ∀ x y : string, red nil x y → x = y.

Proof.
unfold red. intros. decomp H. destruct H1.
Qed.

Lemma red_nil_rtc : ∀ x y : string, red nil # x y → x = y.

Proof.
induction 1. apply red_nil. exact H. refl. transitivity y; assumption.
Qed.

Lemma red_mod_empty_incl_red : red_mod nil R << red R.

Proof.
unfold inclusion. intros. redtac. ded (red_nil_rtc H). subst x0.
subst x. subst y. apply red_rule. exact H0.
Qed.

Lemma red_incl_red_mod_empty : red R << red_mod nil R.

Proof.
unfold inclusion. intros. ∃ x. split. apply rt_refl. exact H.
Qed.

Lemma red_mod_empty : red_mod nil R == red R.

Proof.
split. apply red_mod_empty_incl_red. apply red_incl_red_mod_empty.
Qed.

End S.

Require Import SN.

Ltac no_relative_rules :=
  match goal with
    |- WF (@red_mod ?S ?E _) ⇒
      norm E; eapply WF_incl; [apply (@red_mod_empty_incl_red S) | idtac]
    | _ ⇒ idtac
  end.