Set Implicit Arguments.

Require Import ATrs.
Require Import ListUtil.
Require Import VecUtil.
Require Import LogicUtil.
Require Import RelUtil.
Require Import SN.

Section S.

Variable Sig : Signature.

Notation symb := (symbol Sig).
Notation rule := (rule Sig). Notation rules := (list rule).

Inductive dup_symb : Type :=
| hd_symb : symb → dup_symb
| int_symb : symb → dup_symb.

Definition dup_ar s :=
  match s with
    | hd_symb s' ⇒ arity s'
    | int_symb s' ⇒ arity s'
  end.

Lemma eq_dup_symb_dec : ∀ f g : dup_symb, {f=g}+{¬f=g}.

Proof.
decide equality; apply eq_symbol_dec.
Defined.

Definition dup_sig := mkSignature dup_ar eq_dup_symb_dec.

Notation Sig' := dup_sig. Notation Fun' := (@Fun Sig').

Fixpoint dup_int_term t :=
  match t with
    | Var x ⇒ Var x
    | Fun f v ⇒ Fun' (int_symb f) (Vmap dup_int_term v)
  end.

Lemma dup_int_term_fun : ∀ f v,
  dup_int_term (Fun f v) = Fun' (int_symb f) (Vmap dup_int_term v).

Proof.
intros. trivial.
Qed.

Definition dup_hd_term t :=
  match t with
    | Var x ⇒ Var x
    | Fun f v ⇒ Fun' (hd_symb f) (Vmap dup_int_term v)
  end.

Lemma dup_hd_term_fun : ∀ f v,
  dup_hd_term (Fun f v) = Fun' (hd_symb f) (Vmap dup_int_term v).

Proof.
intros. trivial.
Qed.

Definition dup_int_subst (s : substitution Sig) n := dup_int_term (s n).

Lemma dup_int_subst_spec : ∀ s t,
  sub (dup_int_subst s) (dup_int_term t) = dup_int_term (sub s t).

Proof.
intros.
pattern t.
set (Q := Vforall (fun t0 ⇒
  sub (dup_int_subst s) (dup_int_term t0) = dup_int_term (sub s t0))).
apply term_ind with (Q:=Q).
intro; unfold dup_int_subst; simpl. apply refl_equal.
intros. rewrite dup_int_term_fun.
do 2 rewrite sub_fun. rewrite dup_int_term_fun.
unfold Q in H.
cut (Vmap (sub (dup_int_subst s)) (Vmap dup_int_term v) =
  Vmap dup_int_term (Vmap (sub s) v)).
intros. rewrite <- H0. auto.
do 2 rewrite Vmap_map.
apply Vmap_eq. apply H.
unfold Q; simpl; auto.
unfold Q; simpl; auto.
Qed.

Lemma dup_int_subst_hd_dup : ∀ s f v,
  sub (dup_int_subst s) (dup_hd_term (Fun f v))
  = dup_hd_term (sub s (Fun f v)).

Proof.
intros.
rewrite dup_hd_term_fun. do 2 rewrite sub_fun. rewrite dup_hd_term_fun.
cut ((Vmap (sub (dup_int_subst s)) (Vmap dup_int_term v)) =
 (Vmap dup_int_term (Vmap (sub s) v)) ).
intro. rewrite <- H. apply refl_equal.
do 2 rewrite Vmap_map.
apply Vmap_eq_ext.
apply dup_int_subst_spec.
Qed.

Notation Cont' := (@Cont Sig').

Fixpoint dup_int_context c :=
  match c with
    | Hole ⇒ Hole
    | Cont f _ _ H v c' w ⇒ Cont' (int_symb f) H
      (Vmap dup_int_term v) (dup_int_context c') (Vmap dup_int_term w)
  end.

Lemma dup_int_context_spec : ∀ c s l,
  dup_int_term (fill c (sub s l)) =
  fill (dup_int_context c) (sub (dup_int_subst s) (dup_int_term l)).

Proof.
induction c; intros.
simpl.
rewrite dup_int_subst_spec. apply refl_equal.
simpl.
cut (Vmap dup_int_term (Vcast (Vapp t (Vector.cons (fill c (sub s l)) t0)) e) =
  (Vcast (Vapp (Vmap dup_int_term t)
    (Vector.cons
      (fill (dup_int_context c) (sub (dup_int_subst s) (dup_int_term l)))
      (Vmap dup_int_term t0))) e)).
intro. rewrite H; auto.
rewrite Vmap_cast.
rewrite Vmap_app.
simpl.
rewrite IHc.
auto.
Qed.

Definition dup_hd_context c :=
  match c with
    | Hole ⇒ Hole
    | Cont f _ _ H v c' w ⇒ Cont' (hd_symb f) H
      (Vmap dup_int_term v) (dup_int_context c') (Vmap dup_int_term w)
  end.

Definition dup_int_rule r :=
  mkRule (dup_int_term (lhs r)) (dup_int_term (rhs r)).

Definition dup_hd_rule r :=
  mkRule (dup_hd_term (lhs r)) (dup_hd_term (rhs r)).

Definition dup_int_rules := map dup_int_rule.

Definition dup_hd_rules := map dup_hd_rule.

Section red.

Variable R : rules.

Variable hyp : forallb (@is_notvar_lhs Sig) R = true.
Variable hyp' : forallb (@is_notvar_rhs Sig) R = true.

Lemma hd_red_dup_hd_red : ∀ t u, hd_red R t u →
  hd_red (dup_hd_rules R) (dup_hd_term t) (dup_hd_term u).

Proof.
intros. redtac. subst. unfold hd_red.
∃ (dup_hd_term l). ∃ (dup_hd_term r). ∃ (dup_int_subst s).
ded (is_notvar_lhs_elim hyp H). decomp H0.
ded (is_notvar_rhs_elim hyp' H). decomp H0. subst.
do 2 rewrite dup_int_subst_hd_dup. intuition. unfold dup_hd_rules.
change (In (dup_hd_rule (mkRule (Fun x x0) (Fun x1 x2))) (map dup_hd_rule R)).
apply in_map. hyp.
Qed.

Lemma red_dup_int_red : ∀ t u,
  red R t u → red (dup_int_rules R) (dup_int_term t) (dup_int_term u).

Proof.
intros. redtac.
∃ (dup_int_term l). ∃ (dup_int_term r).
∃ (dup_int_context c). ∃ (dup_int_subst s).
split.
change (In (dup_int_rule (mkRule l r)) (map dup_int_rule R)).
apply in_map. auto.
do 2 rewrite <- dup_int_context_spec.
split; subst; refl.
Qed.

Lemma int_red_dup_int_red : ∀ t u,
  int_red R t u → red (dup_int_rules R) (dup_hd_term t) (dup_hd_term u).

Proof.
intros. redtac.
∃ (dup_int_term l). ∃ (dup_int_term r).
∃ (dup_hd_context c). ∃ (dup_int_subst s).
destruct c. tauto.
split.
change (In (dup_int_rule (mkRule l r)) (map dup_int_rule R)).
apply in_map. auto.
subst; simpl.
split; rewrite Vmap_cast; rewrite Vmap_app;
simpl; rewrite <- dup_int_context_spec; auto.
Qed.

End red.

Section WF.

Variables E R : rules.

Variable no_lhs_var : forallb (@is_notvar_lhs Sig) R = true.
Variable no_rhs_var : forallb (@is_notvar_rhs Sig) R = true.

Lemma WF_duplicate_hd_int_red :
  WF (hd_red_mod (dup_int_rules E) (dup_hd_rules R))
  → WF (hd_red_Mod (int_red E #) R).

Proof.
intros. set (rel := hd_red_mod (dup_int_rules E) (dup_hd_rules R)).
set (rel' := Rof rel (dup_hd_term)).
apply (@WF_incl _ (hd_red_Mod (int_red E #) R) rel').
unfold rel', rel, hd_red_Mod, hd_red_mod. unfold inclusion; intros.
destruct H0 as [z]; ∃ (dup_hd_term z). destruct H0; split.
clear H1. induction H0. apply rt_step. apply int_red_dup_int_red. hyp.
apply rt_refl. eapply rt_trans. apply IHclos_refl_trans1. hyp.
apply hd_red_dup_hd_red; auto. subst rel rel'. apply WF_inverse; auto.
Qed.

End WF.

Notation term' := (term Sig').
Notation rule' := (ATrs.rule Sig').

Definition is_int_symb (t : term') :=
  match t with
    | Fun (int_symb _) _ ⇒ true
    | _ ⇒ false
  end.

Definition is_int_symb_lhs (a : rule') := is_int_symb (lhs a).
Definition is_int_symb_rhs (a : rule') := is_int_symb (rhs a).

Definition is_hd_symb (t : term') :=
  match t with
    | Fun (hd_symb _) _ ⇒ true
    | _ ⇒ false
  end.

Definition is_hd_symb_lhs (a : rule') := is_hd_symb (lhs a).
Definition is_hd_symb_rhs (a : rule') := is_hd_symb (rhs a).

Section int_red.

Notation rules' := (list rule').

Variable R : rules'.

Variable int_hyp : forallb is_int_symb_lhs R = true.

Lemma dup_int_rules_int_red : ∀ f v t,
  red R (Fun' (hd_symb f) v) t → int_red R (Fun' (hd_symb f) v) t.

Proof.
intros. redtac. ∃ l. ∃ r. ∃ c. ∃ s. split.
destruct c. simpl in ×. rewrite forallb_forall in int_hyp. ded (int_hyp _ H).
gen H2. compute. case_eq l. discr. gen H3. gen H2. gen t0. case_eq f0. discr.
subst l. rewrite sub_fun in H0. discr. congruence. tauto.
Qed.

Lemma dup_int_rules_int_red_rtc_aux : ∀ u t, red R # u t →
  ∀ f v, u = Fun' (hd_symb f) v →
    int_red R # u t ∧ ∃ w, t = Fun' (hd_symb f) w.

Proof.
intros u t H.
induction H; intros.
assert (int_red R # x y).
apply rt_step.
rewrite H0.
apply dup_int_rules_int_red. subst;auto.
split. auto.
clear H.
ded (int_red_rtc_preserv_hd H1).
destruct H.
∃ v. subst. rewrite H; auto.
do 3 destruct H; subst.
destruct H. inversion H. subst.
∃ x2. apply refl_equal.

split. apply rt_refl.
∃ v; auto.
ded (IHclos_refl_trans1 _ _ H1).
clear IHclos_refl_trans1.
destruct H2.
destruct H3 as [w].
ded (IHclos_refl_trans2 _ _ H3).
destruct H4. destruct H5.
split.
eapply rt_trans; eauto.
∃ x0. auto.
Qed.

Lemma dup_int_rules_int_red_rtc : ∀ f v t,
  red R # (Fun' (hd_symb f) v) t → int_red R # (Fun' (hd_symb f) v) t.

Proof.
intros. ded (dup_int_rules_int_red_rtc_aux H (refl_equal _)). tauto.
Qed.

End int_red.

Section red_dup.

Variable R : rules.

Notation R' := (dup_int_rules R).

Variable hyp : forallb (@is_notvar_lhs Sig') R' = true.

Lemma red_dup_int_hd_symb : ∀ f us v,
  red R' (Fun' (hd_symb f) us) v → ∃ vs, v = Fun' (hd_symb f) vs.

Proof.
intros. redtac. destruct (in_map_elim H). destruct H2. destruct x.
inversion H3. subst. destruct c; simpl in ×.
rewrite forallb_forall in hyp. ded (hyp _ H). destruct lhs. discr.
simpl dup_int_term in H0. rewrite sub_fun in H0. Funeqtac. discr.
Funeqtac.
∃ (Vcast (Vapp t (Vector.cons (fill c (sub s (dup_int_term rhs))) t0)) e).
refl.
Qed.

Lemma rtc_red_dup_int_hd_symb_aux : ∀ f u v, red R' # u v →
  ∀ us, u = Fun' (hd_symb f) us → ∃ vs, v = Fun' (hd_symb f) vs.

Proof.
induction 1; intros. eapply red_dup_int_hd_symb. subst. apply H. eauto.
destruct (IHclos_refl_trans1 _ H1). eapply IHclos_refl_trans2. apply H2.
Qed.

Lemma rtc_red_dup_int_hd_symb : ∀ f us v,
  red R' # (Fun' (hd_symb f) us) v → ∃ vs, v = Fun' (hd_symb f) vs.

Proof.
intros. eapply rtc_red_dup_int_hd_symb_aux. apply H. refl.
Qed.

End red_dup.

End S.

Implicit Arguments rtc_red_dup_int_hd_symb [Sig R f us v].

Ltac mark := apply WF_duplicate_hd_int_red; [refl | refl | idtac].