Set Implicit Arguments.

Require Import LogicUtil.
Require Export ADP.
Require Import ATrs.
Require Import ListUtil.
Require Import RelUtil.
Require Import RelSub.
Require Import Path.
Require Import ARelation.
Require Import SN.
Require Import ListOccur.
Require Import ListRepeatFree.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (Vector.t term).
Notation rule := (rule Sig). Notation rules := (list rule).
Notation lhs := (@lhs Sig). Notation rhs := (@rhs Sig).

Variable R : rules.

Variable hyp : rules_preserv_vars R.

Notation DP := (dp R).
Notation Chain := (chain R).

Lemma hyp' : rules_preserv_vars DP.

Proof.
apply dp_preserv_vars. exact hyp.
Qed.

Require Import ARename.
Require Import ASubstitution.

Definition dp_graph a1 a2 := In a1 DP ∧ In a2 DP
  ∧ ∃ p, ∃ s,
    int_red R # (sub s (rhs a1)) (sub s (shift p (lhs a2))).

Lemma restricted_dp_graph : is_restricted dp_graph DP.

Proof.
unfold is_restricted, dp_graph, inclusion. intros. intuition.
Qed.

Definition chain_dp a t u := In a DP ∧
  ∃ s, int_red R # t (sub s (lhs a)) ∧ u = sub s (rhs a).

Lemma chain_dp_chain : ∀ a, chain_dp a << Chain.

Proof.
unfold inclusion. intros. destruct H. do 2 destruct H0.
∃ (sub x0 (lhs a)). intuition.
subst y. destruct a. simpl. apply hd_red_rule. exact H.
Qed.

Lemma chain_chain_dp : ∀ t u, Chain t u → ∃ a, chain_dp a t u.

Proof.
intros. do 2 destruct H. redtac. subst x. subst u. ∃ (mkRule l r).
unfold chain_dp. simpl. intuition. ∃ s. intuition.
Qed.

Fixpoint chain_dps (a : rule) (l : rules) {struct l} : relation term :=
  match l with
    | nil ⇒ chain_dp a
    | b :: m ⇒ chain_dp a @ chain_dps b m
  end.

Lemma chain_dps_app : ∀ l a b m,
  chain_dps a (l ++ b :: m) << chain_dps a l @ chain_dps b m.

Proof.
induction l; simpl; intros. apply inclusion_refl. assoc. comp. apply IHl.
Qed.

Implicit Arguments chain_dps_app [l a b m].

Lemma chain_dps_app' : ∀ a l m b p, a :: l = m ++ b :: p →
  chain_dps a l << chain_dps a (tail m) % @ chain_dps b p.

Proof.
intros. destruct m; simpl in H; injection H; unfold inclusion; intros.
subst p. subst b. ∃ x. unfold clos_refl. intuition.
subst r. subst l. simpl. ded (chain_dps_app _ _ H2). do 2 destruct H0.
∃ x0. unfold clos_refl. intuition.
Qed.

Implicit Arguments chain_dps_app' [a l m b p x y].

Require Import Iter.

Lemma chain_dps_iter_chain :
  ∀ l a, chain_dps a l << iter Chain (length l).

Proof.
induction l; simpl; intros. apply chain_dp_chain.
comp. apply chain_dp_chain. apply IHl.
Qed.

Lemma iter_chain_chain_dps : ∀ n t u, iter Chain n t u →
  ∃ a, ∃ l, length l = n ∧ chain_dps a l t u.

Proof.
induction n; simpl; intros. ded (chain_chain_dp H). destruct H0.
∃ x. ∃ (@nil rule). intuition.
do 2 destruct H. ded (chain_chain_dp H). destruct H1. ∃ x0.
ded (IHn _ _ H0). do 3 destruct H2. ∃ (x1 :: x2). simpl. intuition.
∃ x. intuition.
Qed.

Implicit Arguments iter_chain_chain_dps [n t u].

Lemma chain_dp2_dp_graph : ∀ a1 a2 t u v,
  chain_dp a1 t u → chain_dp a2 u v → dp_graph a1 a2.

Proof.
intros. destruct a1 as [l0 r0]. destruct a2 as [l1 r1].
destruct H. simpl in H1. do 2 destruct H1. subst u. rename x into s0.
destruct H0. simpl in H2. do 2 destruct H2. subst v. rename x into s1.
unfold dp_graph. intuition. simpl. set (p := maxvar l0 + 1). ∃ p.
set (s0' := restrict s0 (vars l0)).
set (s1' := restrict (comp s1 (shift_inv_sub p l1)) (vars (shift p l1))).
set (s := ASubstitution.union s0' s1'). ∃ s.
assert (compat s0' s1' (vars l0) (vars (shift p l1))). unfold compat. intros.
ded (vars_max H3). ded (in_vars_shift_min H4). unfold p in H6.
absurd (x ≤ maxvar l0). omega. assumption.
assert (dom_incl s0' (vars l0)). unfold s0'. apply dom_incl_restrict.
assert (dom_incl s1' (vars (shift p l1))). unfold s1'. apply dom_incl_restrict.
assert (sub s r0 = sub s0' r0). unfold s. eapply sub_union1. apply H5.
apply H3. apply hyp'. assumption. rewrite H6.
assert (sub s0' r0 = sub s0 r0). unfold s0'. symmetry.
apply sub_restrict_incl. apply hyp'. assumption. rewrite H7.
assert (sub s (shift p l1) = sub s1' (shift p l1)).
unfold s. eapply sub_union2. apply H4. apply H3. apply List.incl_refl.
rewrite H8.
assert (sub s1' (shift p l1) = sub s1 l1). unfold s1'.
rewrite <- sub_restrict. rewrite <- sub_shift.
refl. rewrite H9. assumption.
Qed.

Lemma chain_dps_path_dp_graph : ∀ l a b t u,
  chain_dps a (l ++ b :: nil) t u → is_path dp_graph a b l.

Proof.
induction l; simpl; intros; do 2 destruct H.
eapply chain_dp2_dp_graph. apply H. apply H0.
ded (IHl _ _ _ _ H0). intuition.
destruct l; simpl in H0; do 2 destruct H0.
eapply chain_dp2_dp_graph. apply H. apply H0.
eapply chain_dp2_dp_graph. apply H. apply H0.
Qed.

Implicit Arguments chain_dps_path_dp_graph [l a b t u].

Require Import ACompat.
Require Import Cycle.

Variables (succ succ_eq : relation term)
  (Hredord : weak_rewrite_ordering succ succ_eq)
  (Hreword : rewrite_ordering succ_eq)
  (Habsorb : absorb succ succ_eq)
  (HcompR : compat succ_eq R)
  (HcompDP : compat succ_eq (dp R))
  (Hwf : WF succ)
  (Hcycle : ∀ a l, length l < length DP → cycle_min dp_graph a l →
    ∃ b, In b (a :: l) ∧ succ (lhs b) (rhs b)).

Notation eq_dec := (@eq_rule_dec Sig).
Notation occur := (occur eq_dec).

Lemma chain_dp_hd_red_mod : ∀ a, chain_dp a << hd_red_mod R (a::nil).

Proof.
unfold inclusion. intros. destruct H. do 2 destruct H0. subst y.
destruct a. simpl. simpl in H0. ∃ (sub x0 lhs). split.
apply incl_elim with (R := int_red R #). apply incl_rtc.
apply int_red_incl_red. exact H0. apply hd_red_rule. simpl. auto.
Qed.

Lemma compat_chain_dp : ∀ a, chain_dp a << succ_eq#.

Proof.
intros. trans (red_mod R DP). trans (Chain). apply chain_dp_chain.
trans (hd_red_mod R DP). apply chain_hd_red_mod. apply hd_red_mod_incl_red_mod.
trans (succ_eq!). apply compat_red_mod_tc; assumption. apply tc_incl_rtc.
Qed.

Lemma compat_chain_dps : ∀ l a, chain_dps a l << succ_eq#.

Proof.
induction l; simpl; intros. apply compat_chain_dp. trans (succ_eq# @ succ_eq#).
comp. apply compat_chain_dp. apply IHl. apply rtc_idem.
Qed.

Lemma compat_chain_dp_strict : ∀ a,
  succ (lhs a) (rhs a) → chain_dp a << succ.

Proof.
unfold inclusion. intros. destruct H0. do 2 destruct H1. subst y.
apply (comp_rtc_incl Habsorb). ∃ (sub x0 (lhs a)). split.
apply incl_elim with (R := int_red R #). 2: exact H1. apply incl_rtc.
trans (red R). apply int_red_incl_red. apply compat_red; assumption.
destruct Hredord. apply H2. exact H.
Qed.

Lemma WF_cycles : WF (chain R).

Proof.
set (n := length DP). apply WF_iter with (S n). intro.
assert (Hwf' : WF (succ @ succ_eq#)). apply absorb_WF_modulo_r; assumption.
generalize (Hwf' x). induction 1. apply SN_intro; intros. apply H0.
ded (iter_chain_chain_dps H1). do 3 destruct H2.
assert (length x1 > 0). omega. ded (last_intro H4). do 3 destruct H5.
clear H4. rewrite H5 in H3. ded (chain_dps_path_dp_graph H3).
set (l' := x0 :: x2 ++ x3 :: nil). assert (∃ z, occur z l' ≥ 2).
unfold l'. eapply long_path_occur. apply restricted_dp_graph. apply H4.
rewrite H6. rewrite H2. unfold n. omega.
assert (∃ l, ∃ a, ∃ m,
  l' = l ++ a :: m ∧ succ (lhs a) (rhs a)).
destruct H7. set (p := occur x4 l' - 2). assert (occur x4 l' = S (S p)).
unfold p. omega. ded (occur_S eq_dec H8). do 3 destruct H9. destruct H10.
clear H8. rewrite H9. ded (occur_S eq_dec H11). do 3 destruct H8.
destruct H12. clear H11. clear H13. clear p. rewrite H8. rewrite H8 in H9.
clear H8. clear H10.
assert (cycle dp_graph x4 x7). unfold cycle. eapply sub_path. unfold l' in H9.
apply H9. exact H4. ded (cycle_min_intro eq_dec H8). decomp H10.
assert (length l' = n+2). unfold l'. simpl. rewrite <- H5. omega.
rewrite H9 in H10. change (length (x5++(x4::x7)++x4::x8) = n+2) in H10.
rewrite H11 in H10. repeat (rewrite length_app in H10; simpl in H10).
unfold n in H10. assert (h : length x11 < length DP).
unfold cycle_min in H14. destruct H14. assert (length (x10::x11) ≤ length DP).
apply repeat_free_dec_incl_length. apply eq_dec. exact H14.
apply incl_appr_incl with (x10::nil). simpl. eapply restricted_path_incl.
apply restricted_dp_graph. exact H13. simpl in H15. omega. clear H10.
ded (Hcycle h H14). do 2 destruct H10. ded (in_elim H10).
do 2 destruct H15. ∃ (x5++x9++x14). ∃ x13. ∃ (x15++x12++x4::x8).
intuition. repeat rewrite app_ass. transitivity (x5++(x4::x7)++x4::x8). refl.
rewrite H11. rewrite app_ass. transitivity (x5++x9++(x10::x11)++x12++x4::x8).
simpl. rewrite app_ass. refl. rewrite H15. rewrite app_ass. refl.
do 4 destruct H8. unfold l' in H8. ded (chain_dps_app' H8 H3).
do 2 destruct H10.
assert (succ_eq# x x7). destruct H10. subst x7. intuition.
eapply incl_elim. apply compat_chain_dps. apply H10.
assert ((succ @ succ_eq#) x7 y). destruct x6; simpl in H11.
ded (compat_chain_dp_strict H9 H11). ∃ y. intuition.
do 2 destruct H11. ∃ x8. split. eapply incl_elim.
apply (compat_chain_dp_strict H9). exact H11.
eapply incl_elim. apply compat_chain_dps. apply H13.
do 2 destruct H13. ∃ x8. intuition.
eapply incl_elim with (R := succ_eq# @ succ). apply comp_rtc_incl. intuition.
∃ x7. intuition.
Qed.

End S.