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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fact Seq_assoc s t u
  : CFPSeq (CFPSeq s t) u =T CFPSeq s (CFPSeq t u).
Proof.
  split; intros; inv H; eauto using TC.
  - inv H2; eauto using TC.
    rewrite concat_assoc. eauto using TC.
  - inv H4; eauto using TC.
    + rewrite <- concat_partial_absorb_right with (xi2 := P); eauto using TC.
      apply concat_partial_preserve_right; eauto using partial.
    + rewrite <- concat_assoc. eauto using TC.
Qed.

Fact Seq_Choice_distribute1 s t u
  : CFPSeq s (CFPChoice t u) =T CFPChoice (CFPSeq s t) (CFPSeq s u).
Proof.
  split; intros.
  - inv H; eauto using TC.
    inv H4; eauto using TC.
  - inv H; eauto using TC; inv H3; eauto using TC.
Qed.

Fact Seq_Choice_distribute2 s t u
  : CFPSeq (CFPChoice s t) u =T CFPChoice (CFPSeq s u) (CFPSeq t u).
Proof.
  split; intros.
  - inv H; eauto using TC.
    inv H2; eauto using TC.
  - inv H; eauto using TC; inv H3; eauto using TC.
Qed.

Fact Seq_Null_absorb_left s
  : CFPSeq Null s =T Null.
Proof.
  split; intros.
  - inv H; eauto using TC. apply Null_trace in H2.
    rewrite H2. rewrite concat_partial_absorb_right; eauto using TC, partial.
  - apply Null_trace in H. rewrite H. constructor.
Qed.

Fact Choice_Null_iden_right s
  : CFPChoice s Null =T s.
Proof.
  split; intros; eauto using TC.
  inv H; eauto using TC.
  apply Null_trace in H3. rewrite H3. constructor.
Qed.

Fact Choice_commute s t
  : CFPChoice s t =T CFPChoice t s.
Proof.
  split; intros; inv H; eauto using TC.
Qed.

Fact Choice_Null_iden_left s
  : CFPChoice Null s =T s.
Proof.
  rewrite Choice_commute. eauto using Choice_Null_iden_right.
Qed.

Fact Seq_Eps_iden_right s
  : CFPSeq s CFPEps =T s.
Proof.
  split; intros.
  - inv H; eauto using TC. inv H4.
    + apply trace_concat_P. eauto.
    + setoid_rewrite <- concat_T_iden_right.
      eauto.
  - rewrite concat_T_iden_right. constructor; eauto using TC.
Qed.

Fact Seq_Eps_iden_left s
  : CFPSeq CFPEps s =T s.
Proof.
  split; intros.
  - inv H; eauto using TC. inv H2.
    + rewrite concat_partial_absorb_right; eauto using TC, partial.
    + setoid_rewrite <- concat_T_iden_left. eauto.
  - rewrite concat_T_iden_left. constructor; eauto using TC.
Qed.

Fact Choice_assoc s t u
  : CFPChoice s (CFPChoice t u) =T CFPChoice (CFPChoice s t) u.
Proof.
  split; intros; inv H; eauto using TC; inv H3; eauto using TC.
Qed.

Fact Choice_idem s
  : CFPChoice s s =T s.
Proof.
  split; intros; eauto using TC.
  inv H; eauto using TC.
Qed.

Fact Fix_unfold s
  : CFPFix s =T s.[CFPFix s/].
Proof.
  intros xi. split; intros; eauto using TC.
  inv H; eauto using TC.
Qed.

Fact no_Null_annulate_right x
  : ¬ CFPSeq (CFPVar x) Null =T Null.
Proof.
  intros A. unfold eqTC in A.
  specialize (A (V x P)).
  assert (TC (CFPSeq (CFPVar x) Null) (V x P)).
  { rewrite <- concat_partial_absorb_right with (xi2:= P); eauto using partial.
    constructor; eauto using TC. }
  rewrite A in H. apply Null_trace in H. inv H.
Qed.