Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base CFP TraceSemantics Equivalences Substitutivity.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fixpoint unfold s n :=
  match n with
  | 0 ⇒ Null
  | (S n) ⇒ s.[(unfold s n)/]
  end.

Fact unfold_step s n m xi
  : TC (unfold s n) xi → n≤m → TC (unfold s m) xi.
Proof.
  general induction n.
  - asimpl in H. rewrite Null_trace; eauto using TC.
  - destruct m.
    + inv H0.
    + asimpl. asimpl in H.
      apply subst_subsumption_transfer with (sigma1:= unfold s n .: ids); eauto.
      intros. destruct x; asimpl; asimpl in H1; eauto.
      apply IHn; eauto. omega.
Qed.

Fact unfold_subst s n sigma
  : (unfold s n).[sigma] = unfold s.[up sigma] n.
Proof.
  general induction n; asimpl; eauto.
  rewrite IHn. eauto.
Qed.

Lemma subst_Fix_unfold_subsume s t xi
  : TC s.[CFPFix t/] xi → ∃ n, TC s.[(unfold t n) /] xi.
Proof.
  intros. general induction H.
  - ∃ 0. constructor.
  - symmetry in Heqc. apply inv_subst_Eps in Heqc. destruct Heqc as [[x [H1 H2]]| H3].
    + rewrite H1. simpl. destruct x.
      × asimpl in H2. inv H2.
      × asimpl in H2. inv H2.
    + rewrite H3. asimpl. ∃ 0. constructor.
  - symmetry in Heqc. apply inv_subst_Var in Heqc. destruct Heqc as [y [H1 H2]].
    destruct y.
    + asimpl in H2. inv H2.
    + asimpl in H2. inv H2.
      ∃ 1. simpl. constructor.
  - symmetry in Heqc. apply inv_subst_Var in Heqc. destruct Heqc as [y [H1 H2]].
    destruct y.
    + asimpl in H2. inv H2.
    + asimpl in H2. inv H2.
      ∃ 1. simpl. constructor.
  - symmetry in Heqc. apply inv_subst_Seq in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2[H3 [H4 H5]]]]].
    + rewrite H1. asimpl. destruct x; asimpl in H2; inv H2.
    + specialize (IHTC1 s1 t0). destruct IHTC1 as [n1 A]; eauto.
      specialize (IHTC2 s2 t0). destruct IHTC2 as [n2 B]; eauto.
      rewrite H5. ∃ (n1+n2).
      asimpl. constructor.
      × apply subst_subsumption_transfer with (sigma1:= unfold t0 n1.:ids).
        { intros. destruct x.
          - asimpl. asimpl in H1. apply unfold_step with (n:= n1); eauto.
            omega.
          - asimpl. asimpl in H1. eauto. }
        { eauto. }
      × apply subst_subsumption_transfer with (sigma1:= unfold t0 n2.:ids).
        { intros. destruct x.
          - asimpl. asimpl in H1. apply unfold_step with (n:= n2); eauto.
            omega.
          - asimpl. asimpl in H1. eauto. }
        { eauto. }
  - symmetry in Heqc. apply inv_subst_Choice in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2[H3 [H4 H5]]]]].
    + destruct x; asimpl in H2; inv H2.
    + specialize (IHTC s1 t0). destruct IHTC as [n1 A]; eauto.
      ∃ n1. rewrite H5. asimpl. eauto using TC.
  - symmetry in Heqc. apply inv_subst_Choice in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2[H3 [H4 H5]]]]].
    + destruct x; asimpl in H2; inv H2.
    + specialize (IHTC s2 t0). destruct IHTC as [n2 A]; eauto.
      ∃ n2. rewrite H5. asimpl. eauto using TC.
  - symmetry in Heqc. apply inv_subst_Fix in Heqc.
    destruct Heqc as [[x [H1 H2]]|[s' [H3 H4]]].
    + destruct x.
      × asimpl in H2. inv H2. asimpl.
        specialize (IHTC s s). destruct IHTC as [n A]; eauto.
        ∃ (S n). eauto.
      × ∃ 0. asimpl in H2. inv H2.
    + rewrite H4. asimpl.
      specialize (IHTC (s'.[CFPFix s' .: ids]) t). destruct IHTC.
      × asimpl. rewrite H3.
        rewrite up_change. eauto.
      × asimpl in H0. ∃ x.
        constructor. rewrite up_change. eauto.
Qed.

Lemma Fix_unfold_subsume s xi
  : TC (CFPFix s) xi → ∃ n, TC (unfold s n) xi.
Proof.
  intros. inv H.
  - ∃ 0. eauto using TC.
  - apply subst_Fix_unfold_subsume in H1.
    destruct H1 as [n A].
    ∃ (S n). simpl. eauto.
Qed.

Lemma unfold_Fix_subsume s n xi
  : TC (unfold s n) xi → TC (CFPFix s) xi.
Proof.
  intros. general induction n.
  - simpl in H. rewrite Null_trace; eauto. constructor.
  - simpl in H. constructor.
    apply subst_subsumption_transfer with (sigma1:= (unfold s n).: ids); eauto.
    intros. destruct x; asimpl in H0; asimpl; eauto.
Qed.