Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base CFP Traces.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive TC : cfp → trace → Prop :=
| TCPartial s
  : TC s P
| TCTotal
  : TC CFPEps T
| TCVarPartial x
  : TC (CFPVar x) (V x P)
| TCVarTotal x
  : TC (CFPVar x) (V x T)
| TSeq s t xi1 xi2
  : TC s xi1 → TC t xi2 → TC (CFPSeq s t) (concat xi1 xi2)
| TChoiceLeft s t xi
  : TC s xi → TC (CFPChoice s t) xi
| TCChoiceRight s t xi
  : TC t xi → TC (CFPChoice s t) xi
| TCFix s xi
  : TC (s.[CFPFix s /]) xi → TC (CFPFix s) xi.

Definition eqTC s t := ∀ xi, TC s xi ↔ TC t xi.
Notation "s =T t" := (eqTC s t) (at level 70).

Instance eqTC_Equivalence: Equivalence (eqTC).
Proof.
  constructor; firstorder.
Qed.

Fact P_trivialtrace s
  : TC s P.
Proof.
  constructor.
Qed.

Fact trace_concat_P s xi
  : TC s xi → TC s (concat xi P).
Proof.
  intros. general induction H; eauto using TC.
  rewrite concat_assoc. constructor; eauto.
Qed.

Fact trace_concat_partial_left s xi1 xi2
  : TC s (concat xi1 xi2) → partial xi1 → TC s xi1.
Proof.
  intros. rewrite concat_partial_absorb_right in H; eauto.
Qed.

Fact trace_partial_Seq_left s t xi
  : TC s xi → partial xi → TC (CFPSeq s t) xi.
Proof.
  intros.
  rewrite <- concat_partial_absorb_right with (xi2:= P); eauto.
  constructor; eauto using TC.
Qed.

Fact trace_partial_prefix s xi
  : TC s xi → TC s (concat (butLast xi) P).
Proof.
  intros. general induction H; simpl; eauto using TC.
  decide (partial xi1).
  - setoid_rewrite concat_partial_absorb_right at 2; eauto.
    rewrite <- concat_partial_absorb_right with (xi2:= P).
    + constructor; eauto using TC.
    + apply concat_P_partial_right.
  - apply not_partial_total in n.
    destruct xi2.
    + constructor; eauto using TC. rewrite butLast_P_distribute. eauto.
    + rewrite <- concat_T_iden_right.
      setoid_rewrite concat_T_iden_right at 1.
      constructor; eauto.
    + rewrite butLast_concat_distribute; eauto.
      × rewrite concat_assoc.
        constructor; eauto.
      × eauto using composed.
Qed.

Fact trace_partial_prefix2 s xi
  : TC s xi → partial xi → TC s (butLast xi).
Proof.
  intros. apply trace_partial_prefix in H.
  rewrite <- concat_P_iden_right in H; eauto.
  apply butLast_partial_preserve. eauto.
Qed.

Fixpoint iterate (X: Type) (n: nat) (f: X → X) (x: X): X :=
  match n with
  | 0 ⇒ x
  | (S n) ⇒ f (iterate n f x)
  end.

Fact prefix_closed s xi n
  : TC s xi → TC s (concat (iterate n butLast xi) P).
Proof.
  general induction n.
  - simpl. eauto using trace_concat_P.
  - simpl. rewrite <- butLast_P_distribute.
    rewrite <- concat_partial_absorb_right with (xi2:= P).
    + apply trace_partial_prefix. eauto.
    + rewrite butLast_P_distribute. apply concat_P_partial_right.
Qed.

Lemma ren_trace_ren s xi f
  : TC s xi → TC s.[ren f] (ren_trace f xi).
Proof.
  intros. general induction H; simpl; eauto using TC.
  - rewrite ren_concat_distribute. eauto using TC.
  - asimpl. constructor.
    specialize (IHTC f). asimpl in IHTC.
    assert (s.[CFPFix s.[up (ren f)] .: ren f] = s.[ren (0 .: f >>> (+1))].[CFPFix s.[ren (0 .: f >>> (+1))]/]).
    { asimpl. eauto. }
    setoid_rewrite H0 in IHTC. eauto.
Qed.

Lemma Null_trace xi
  : TC (CFPFix (CFPVar 0)) xi → xi = P.
Proof.
  intros. general induction H.
  - eauto.
  - asimpl in H. asimpl in IHTC. apply IHTC. eauto.
Qed.