Set Implicit Arguments.

Require Import ATrs.
Require Import List.
Require Import SN.
Require Import ARelation.
Require Import RelUtil.
Require Import ACompat.

Section S.

Variable Sig : Signature.

Notation term := (term Sig).
Notation rule := (rule Sig).
Notation rules := (list rule).

Ltac WF_incl succ := apply WF_incl with (S := succ); [idtac | WFtac].

Section manna_ness.

Variables (R : rules) (succ : relation term).

Lemma manna_ness : reduction_ordering succ -> compat succ R -> WF (red R).

Proof.
intros. WF_incl succ. incl_red.
Qed.

End manna_ness.

Section manna_ness_mod.

Variables R E : rules.

Lemma manna_ness_mod : forall rp : Reduction_pair Sig,
  compat (rp_succ_eq rp) E -> compat (rp_succ rp) R -> WF (red_mod E R).

Proof.
intros. WF_incl (rp_succ rp). incl_red.
Qed.

End manna_ness_mod.

Section manna_ness_hd_mod.

Variables R E : rules.

Lemma manna_ness_hd_mod : forall wp : Weak_reduction_pair Sig,
  compat (wp_succ_eq wp) E -> compat (wp_succ wp) R -> WF (hd_red_mod E R).

Proof.
intros. WF_incl (wp_succ wp). incl_red.
Qed.

End manna_ness_hd_mod.

Section rule_elimination.

Variables R R' : rules.

Section mod.

Variables E E' : rules.

Require Import Lexico.

Lemma rule_elimination_mod : forall rp : Reduction_pair Sig,
  compat (rp_succ_eq rp) E -> compat (rp_succ rp) E' ->
  compat (rp_succ_eq rp) R -> compat (rp_succ rp) R' ->
  WF (red_mod E R) -> WF (red_mod (E ++ E') (R ++ R')).

Proof.
intros. set (succ := rp_succ rp). set (succ_eq := rp_succ_eq rp).
set (er := red_mod E R). set (F := E ++ E').
assert (h0 : er << succ_eq!). unfold er, succ_eq. incl_red.
assert (h1 : red F # << succ # @ red E #).
trans ((red E U red E')#). apply incl_rtc. unfold F. apply red_union.
trans (red_mod E E' # @ red E #). unfold red_mod. apply rtc_union.
comp. apply incl_rtc. unfold succ. incl_red.
assert (h2 : red_mod F (R ++ R') << succ# @ er U succ!).
trans (red_mod F R U red_mod F R'). apply red_mod_union. union.
unfold red_mod. trans ((succ # @ red E #) @ red R). comp. exact h1. assoc.
trans ((succ # @ red E #) @ red R'). unfold red_mod. comp. exact h1. assoc.
trans (succ # @ succ). comp.
trans (red_mod E R'). unfold succ. incl_red. apply rtc_step_incl_tc.
set (gt := succ! @ succ_eq#). assert (h3 : red_mod F (R ++ R') << er U gt).
trans (succ# @ er U succ!). exact h2.
trans ((er U succ! @ er) U succ!). union. apply rtc_comp.
trans (er U (succ! @ er U succ!)). apply union_assoc. union.
trans (succ! @ er%). apply union_fact2. unfold gt. comp.
apply incl_rc_rtc. exact h0.
assert (h4 : succ_eq# @ succ! << succ!).
apply comp_incl_tc. apply comp_rtc_incl. rptac.
eapply WF_incl with (S := lex' gt (er!)).
trans (er U gt). exact h3. trans (er! U gt). union.
apply tc_incl. trans (gt U er!). apply union_commut.
apply lex'_intro. apply WF_lex'.
unfold gt. apply WF_compat_inv. exact h4. apply WF_tc. WFtac.
apply WF_tc. exact H3.
apply tc_trans.
apply comp_tc_incl. trans (succ_eq! @ gt). comp. exact h0.
apply comp_tc_incl. unfold gt. assoc. comp. apply comp_incl_tc. rptac.
Qed.

Lemma weak_rule_elimination_mod : forall wp : Weak_reduction_pair Sig,
  compat (wp_succ_eq wp) E ->
  compat (wp_succ_eq wp) R -> compat (wp_succ wp) R' ->
  WF (hd_red_mod E R) -> WF (hd_red_mod E (R ++ R')).

Proof.
intros. set (succ := wp_succ wp). set (succ_eq := wp_succ_eq wp).
set (er := hd_red_mod E R). set (er' := hd_red_mod E R').
apply WF_incl with (S := lex' succ (er!)).
trans (er U succ). trans (er U er'). unfold er, er'. apply hd_red_mod_union.
union. unfold er', succ. incl_red.
trans (succ U er). apply union_commut.
trans (succ U er!). union. apply tc_incl.
apply lex'_intro. apply WF_lex'. WFtac. apply WF_tc. exact H2. apply tc_trans.
apply comp_tc_incl. trans (succ_eq! @ succ). comp. unfold er.
trans (red_mod E R). apply hd_red_mod_incl_red_mod. incl_red.
apply comp_tc_incl. rptac.
Qed.

Lemma weak_rule_elimination_mod_min : forall wp : Weak_reduction_pair Sig,
  compat (wp_succ_eq wp) E ->
  compat (wp_succ_eq wp) R -> compat (wp_succ wp) R' ->
  WF (hd_red_mod_min E R) -> WF (hd_red_mod_min E (R ++ R')).

Proof.
  intros. set (succ := wp_succ wp). set (succ_eq := wp_succ_eq wp).
  set (er := hd_red_mod_min E R). set (er' := hd_red_mod_min E R').
  apply WF_incl with (S := lex' succ (er!)).
  trans (er U succ). trans (er U er'). unfold er, er'. apply hd_red_mod_min_union.
  union. unfold er', succ. incl_red.
  trans (succ U er). apply union_commut.
  trans (succ U er!). union. apply tc_incl.
  apply lex'_intro. apply WF_lex'. WFtac. apply WF_tc. exact H2. apply tc_trans.
  apply comp_tc_incl. trans (succ_eq! @ succ). comp. unfold er.
  trans (red_mod E R). apply incl_trans with (hd_red_mod E R).
  apply hd_red_mod_min_incl. apply hd_red_mod_incl_red_mod. incl_red.
  apply comp_tc_incl. rptac.
Qed.

End mod.

Lemma rule_elimination : forall rp : Reduction_pair Sig,
  compat (rp_succ_eq rp) R -> compat (rp_succ rp) R' ->
  WF (red R) -> WF (red (R ++ R')).

Proof.
intros. eapply WF_incl. apply red_incl_red_mod.
change (WF (red_mod (nil++nil) (R++R'))). eapply rule_elimination_mod.
unfold compat. simpl. intuition.
unfold compat. simpl. intuition.
apply H. apply H0.
eapply WF_incl. apply red_mod_empty_incl_red. exact H1.
Qed.

Lemma weak_rule_elimination : forall wp : Weak_reduction_pair Sig,
  compat (wp_succ_eq wp) R -> compat (wp_succ wp) R' ->
  WF (hd_red R) -> WF (hd_red (R ++ R')).

Proof.
intros. eapply WF_incl. apply hd_red_incl_hd_red_mod.
change (WF (hd_red_mod (nil++nil) (R++R'))). eapply weak_rule_elimination_mod.
unfold compat. simpl. intuition.
unfold compat. simpl. intuition.
apply H0. eapply WF_incl. simpl. apply hd_red_mod_empty_incl_hd_red. exact H1.
Qed.

End rule_elimination.


End S.