Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base Congruence FreeVariables.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fact decomposed_subst s t u
  : bound 0 1 s
    → bound 0 1 t
    → (part s t).[u /] =T CFPChoice s.[ren(shift)] (CFPSeq t.[ren(shift)] u).
Proof.
  intros. split; intros.
  - asimpl in H1. inv H1; eauto using TC.
     + constructor.
       rewrite bound_subst with (n:= 0) (k:= 1) (f:= shift) in H5; eauto using simulatesI_shift.
     + constructor 7. inv H5; eauto using TC.
       constructor; eauto.
       rewrite bound_subst with (n:= 0) (k:= 1) (f:= shift) in H4; eauto using simulatesI_shift.
  - inv H1; eauto using TC.
    + asimpl. constructor.
      rewrite bound_subst with (n:= 0) (k:= 1) (f:= shift); eauto using simulatesI_shift.
    + asimpl. constructor 7. inv H5; eauto using TC.
      constructor; eauto.
      rewrite bound_subst with (n:= 0) (k:= 1) (f:= shift); eauto using simulatesI_shift.
Qed.

Fact decomposed_unfold s t n
  : bound 0 1 s
    → bound 0 1 t
    → unfold (part s t) (S n)
       =T CFPChoice (s.[ren(shift)]) (CFPSeq t.[ren(shift)] (unfold (part s t) n)).
Proof.
  intros.
  change ( (part s t).[unfold (part s t) n /] =T
                                                 CFPChoice s.[ren shift] (CFPSeq t.[ren shift] (unfold (part s t) n))).
  apply decomposed_subst; eauto.
Qed.

Lemma decomposed_unfold_distribute s t u n
  : bound 0 1 s
    → bound 0 1 t
    → bound 0 1 u
    → (unfold (part (CFPSeq s u) t) n)
       =T CFPSeq (unfold (part s t) n) u.[ren(shift)].
Proof.
  intros. general induction n.
  - symmetry. asimpl. apply Seq_Null_absorb_left.
  - rewrite decomposed_unfold; eauto.
    + rewrite IHn; eauto.
      assert ((CFPSeq s u).[ren shift] =T CFPSeq s.[ren(shift)] u.[ren(shift)]).
      { asimpl. reflexivity. }
      rewrite H2.
      rewrite <- Seq_assoc.
      rewrite <- Seq_Choice_distribute2.
      rewrite <- decomposed_unfold; eauto. reflexivity.
    + constructor; eauto.
Qed.

Lemma decomposed_unfold_distribute_lift s t u n
  : bound 0 1 s
    → bound 0 1 t
    → (unfold (part (CFPSeq s u.[ren(+1)]) t) n)
       =T CFPSeq (unfold (part s t) n) u.
Proof.
  intros. rewrite decomposed_unfold_distribute; eauto.
  - asimpl. rewrite shift_id. asimpl. reflexivity.
  - apply bound_ren. intros. left. simpl. omega.
Qed.

Lemma decompose_Fix_distribute s t u
  : bound 0 1 s
    → bound 0 1 t
    → bound 0 1 u
    → (CFPFix (part (CFPSeq s u) t))
       =T (CFPSeq (CFPFix (part s t)) u.[ren(shift)]).
Proof.
  intros. split; intros.
  - apply Fix_unfold_subsume in H2. destruct H2 as [n H2].
    apply decomposed_unfold_distribute in H2; eauto.
    inv H2; eauto using TC.
    constructor; eauto. apply unfold_Fix_subsume with (n:= n).
    eauto.
  - inv H2; eauto using TC. apply Fix_unfold_subsume in H5.
    destruct H5 as [n H5]. apply unfold_Fix_subsume with (n:= n).
    apply decomposed_unfold_distribute; eauto. constructor; eauto.
Qed.

Lemma decomposed_Fix_distribute_lift s t u
  : bound 0 1 s
    → bound 0 1 t
    → (CFPFix (part (CFPSeq s u.[ren(+1)]) t))
       =T (CFPSeq (CFPFix (part s t)) u).
Proof.
  intros. rewrite decompose_Fix_distribute; eauto.
  - assert (u.[ren ((+1) >>> shift)] = u.[ids]).
    { apply extens. intros. destruct n; eauto. }
    asimpl. rewrite H1. asimpl. reflexivity.
  - apply bound_ren. left. simpl. omega.
Qed.

Lemma decomposed_Star s t
  : bound 0 1 s
     → bound 0 1 t
     → CFPFix (part s t)
        =T CFPSeq (Star t) s.[ren(shift)].
Proof.
  intros.
  unfold Star.
  rewrite <- decompose_Fix_distribute; eauto using bound.
  unfold part. rewrite Seq_Eps_iden_left.
  reflexivity.
Qed.

Lemma decomposed_Star_lift s t
  : bound 0 1 s
     → bound 0 1 t
     → CFPFix (part s.[ren(+1)] t)
        =T CFPSeq (Star t) s.
Proof.
  intros.
  unfold Star.
  rewrite <- decomposed_Fix_distribute_lift; eauto using bound.
  unfold part. rewrite Seq_Eps_iden_left. reflexivity.
Qed.