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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fact inv_subst_Eps s sigma
  : s.[sigma] = CFPEps → (∃ x, s = CFPVar x ∧ sigma x = CFPEps) ∨ s = CFPEps.
Proof.
  intros. general induction s.
  - right. reflexivity.
  - left. ∃ x. split; eauto.
Qed.

Fact inv_subst_Var s sigma y
  : s.[sigma] = CFPVar y
    → (∃ x, s = CFPVar x ∧ sigma x = CFPVar y).
Proof.
  intros. general induction s.
  ∃ x. split; eauto.
Qed.

Fact inv_subst_Seq s t1 t2 sigma
  : s.[sigma] = CFPSeq t1 t2
    → (∃ x, s = CFPVar x ∧ sigma x = CFPSeq t1 t2)
       ∨ (∃ s1 s2, t1 = s1.[sigma] ∧ t2 = s2.[sigma] ∧ s = CFPSeq s1 s2).
Proof.
  intros. general induction s.
  - right. ∃ s1, s2. repeat split; eauto.
  - left. ∃ x. split; eauto.
Qed.

Fact inv_subst_Choice s t1 t2 sigma
  : s.[sigma] = CFPChoice t1 t2
    → (∃ x, s = CFPVar x ∧ sigma x = CFPChoice t1 t2)
       ∨ (∃ s1 s2, t1 = s1.[sigma] ∧ t2 = s2.[sigma] ∧ s = CFPChoice s1 s2).
Proof.
  intros. general induction s.
  - right. ∃ s1, s2. repeat split; eauto.
  - left. ∃ x. split; eauto.
Qed.

Fact inv_subst_Fix s t sigma
  : s.[sigma] = CFPFix t
    → (∃ x, s = CFPVar x ∧ sigma x = CFPFix t)
       ∨ (∃ s', t = s'.[up sigma] ∧ s = CFPFix s').
Proof.
  intros. general induction s.
  - right. ∃ s. repeat split; eauto.
  - left. ∃ x. split; eauto.
Qed.

Inductive TCsubst : cfp → (var→ cfp) → trace → Prop :=
| TCsubstPartial s sigma
  : TCsubst s sigma P
| TCsubstTotal sigma
  : TCsubst CFPEps sigma T
| TCsubstVar x xi sigma
  : TC (sigma x) xi → TCsubst (CFPVar x) sigma xi
| TCsubstSeq s t xi1 xi2 sigma
  : TCsubst s sigma xi1 → TCsubst t sigma xi2 → TCsubst (CFPSeq s t) sigma (concat xi1 xi2)
| TCsubstChoiceLeft s t xi sigma
  : TCsubst s sigma xi → TCsubst (CFPChoice s t) sigma xi
| TCsubstChoiceRight s t xi sigma
  : TCsubst t sigma xi → TCsubst (CFPChoice s t) sigma xi
| TCsubstFix s xi sigma
  : TCsubst (s.[CFPFix s /]) sigma xi → TCsubst (CFPFix s) sigma xi.

Lemma TC_TCsubst s sigma xi
  : TC s.[sigma] xi → TCsubst s sigma xi.
Proof.
  intros. general induction H; eauto using TCsubst.
  - symmetry in Heqc. apply inv_subst_Eps in Heqc. destruct Heqc as [[x [H1 H2]] | H3].
    + rewrite H1. constructor. rewrite H2. constructor.
    + rewrite H3. constructor.
  - symmetry in Heqc. apply inv_subst_Var in Heqc. destruct Heqc as [y [H1 H2]].
    rewrite H1. constructor. rewrite H2. constructor.
  - symmetry in Heqc. apply inv_subst_Var in Heqc. destruct Heqc as [y [H1 H2]].
    rewrite H1. constructor. rewrite H2. constructor.
  - symmetry in Heqc. apply inv_subst_Seq in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2 [H3 [H4 H5]]]]].
    + rewrite H1. constructor. rewrite H2. constructor; eauto.
    + rewrite H5. constructor; eauto.
  - symmetry in Heqc. apply inv_subst_Choice in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2 [H3 [H4 H5]]]]].
    + rewrite H1. constructor. rewrite H2. constructor; eauto.
    + rewrite H5. constructor; eauto.
  - symmetry in Heqc. apply inv_subst_Choice in Heqc.
    destruct Heqc as [[x [H1 H2]] |[s1 [s2 [H3 [H4 H5]]]]].
    + rewrite H1. constructor. rewrite H2. constructor 7; eauto.
    + rewrite H5. eauto using TCsubst.
  - symmetry in Heqc. apply inv_subst_Fix in Heqc.
    destruct Heqc as [[x [H1 H2]]| [s' [H3 H4]]].
    + rewrite H1. constructor. rewrite H2. eauto using TC.
    + rewrite H4. constructor. apply IHTC.
      rewrite H3. asimpl. eauto.
Qed.

Lemma TCsubst_TC s sigma xi
  : TCsubst s sigma xi → TC s.[sigma] xi.
Proof.
  intros. general induction H; eauto using TC.
  asimpl in IHTCsubst. constructor. asimpl. eauto.
Qed.

Inductive substT : trace → (var → cfp) → trace → Prop :=
| SubstTT sigma
  : substT T sigma T
| SubstTP sigma
  : substT P sigma P
| SubstTV sigma x xi xi' my
  : TC (sigma x) xi'
    → substT xi sigma my
    → substT (V x xi) sigma (concat xi' my).

Fact substT_total xi sigma
  : ∃ my, substT xi sigma my.
Proof.
  general induction xi.
  - ∃ P. eauto using substT.
  - ∃ T. eauto using substT.
  - destruct (IHxi sigma) as [my A].
    ∃ (concat P my). constructor; eauto using TC.
Qed.

Fact substT_concat_compose xi1 xi2 my1 my2 sigma
  : substT xi1 sigma my1
    → substT xi2 sigma my2
    → substT (concat xi1 xi2) sigma (concat my1 my2).
Proof.
  intros. general induction H; simpl; eauto using substT.
  rewrite concat_assoc. constructor; eauto.
Qed.

Fact substT_concat_decompose xi1 xi2 my sigma
  : substT (concat xi1 xi2) sigma my
    → ∃ my1 my2, substT xi1 sigma my1
                       ∧ substT xi2 sigma my2
                       ∧ my = concat my1 my2.
Proof.
  general induction xi1; simpl in H.
  - ∃ P. inv H.
    destruct (substT_total xi2 sigma) as [my2 A].
    ∃ my2.
    repeat split; eauto using substT.
  - simpl in H. ∃ T, my.
    split; eauto using substT.
  - simpl in H. inv H.
    specialize (IHxi1 xi2 my0 sigma H5).
    destruct IHxi1 as [my1 [my2 [A [B C]]]].
    ∃ (concat xi' my1), my2.
    repeat split; eauto using substT.
    rewrite C. rewrite concat_assoc. eauto.
Qed.

Lemma subst_trace_construct s xi sigma my
  : TC s xi → substT xi sigma my → TC s.[sigma] my.
Proof.
  intros. general induction H; asimpl; eauto using TC.
  - inv H0. constructor.
  - inv H0. asimpl. constructor.
  - inv H0. asimpl. inv H5.
    apply trace_concat_P. eauto.
  - inv H0. asimpl. inv H5.
    rewrite <- concat_T_iden_right. eauto.
  - asimpl. apply substT_concat_decompose in H1.
    destruct H1 as [my1 [my2 [A [B C]]]].
    rewrite C. constructor; eauto.
  - asimpl. constructor. asimpl.
    rewrite <- subst_Fix_distribute. eauto.
Qed.

Lemma subst_trace_deconstruct s my sigma
  : TC s.[sigma] my → ∃ xi, TC s xi ∧ substT xi sigma my.
Proof.
  intros. apply TC_TCsubst in H. general induction H.
  - ∃ P. split; eauto using TC, substT.
  - ∃ T. split; eauto using TC, substT.
  - ∃ (V x T). split; eauto using TC.
    rewrite concat_T_iden_right.
    eauto using substT.
  - destruct IHTCsubst1 as [xiA [A1 A2]].
    destruct IHTCsubst2 as [xiB [B1 B2]].
    ∃ (concat xiA xiB). split; eauto using TC, substT_concat_compose.
  - destruct IHTCsubst as [xiA [A1 A2]].
    ∃ xiA. split; eauto using TC.
  - destruct IHTCsubst as [xiA [A1 A2]].
    ∃ xiA. split; eauto using TC.
  - destruct IHTCsubst as [xiA [A1 A2]].
    ∃ xiA. split; eauto using TC.
Qed.

Lemma subst_tracesubsumption_preserve s t xi sigma
  : (∀ xi, TC s xi → TC t xi) → TC s.[sigma] xi → TC t.[sigma] xi.
Proof.
  intros. apply subst_trace_deconstruct in H0.
  destruct H0 as [xi1 [A B]].
  apply H in A.
  apply subst_trace_construct with (xi:= xi1); eauto.
Qed.

Lemma substitutivity1 s t sigma
  : s =T t → s.[sigma] =T t.[sigma].
Proof.
  intros. split; intros.
  - apply subst_tracesubsumption_preserve with (s:= s); eauto.
    intros. apply H. eauto.
  - apply subst_tracesubsumption_preserve with (s:= t); eauto.
    intros. apply H. eauto.
Qed.

Lemma subst_subsumption_transfer s sigma1 sigma2 xi
  : (∀ x xi, TC (sigma1 x) xi → TC (sigma2 x) xi)
    → TC s.[sigma1] xi → TC s.[sigma2] xi.
Proof.
  intros. apply TC_TCsubst in H0. general induction H0; eauto using TC.
  constructor. asimpl.
  rewrite <- subst_Fix_distribute. eauto.
Qed.

Lemma substitutivity2 s sigma1 sigma2
  : (∀ x, sigma1 x =T sigma2 x) → s.[sigma1] =T s.[sigma2].
Proof.
  intros. split; intros.
  - apply subst_subsumption_transfer with (sigma1:= sigma1); eauto.
    intros. apply H. eauto.
  - apply subst_subsumption_transfer with (sigma1:= sigma2); eauto.
    intros. apply H. eauto.
Qed.

Theorem substitutivity sigma1 sigma2 s t
  : (∀ x, sigma1 x =T sigma2 x) → s =T t → s.[sigma1] =T t.[sigma2].
Proof.
  intros. rewrite substitutivity2; eauto.
  rewrite substitutivity1; eauto. reflexivity.
Qed.