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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive trace :=
| P
| T
| V (x: var) (xi: trace).

Inductive partial : trace → Prop :=
| PartialP
  : partial P
| PartialV x xi
  : partial xi → partial (V x xi).

Inductive total : trace → Prop :=
| TotalT
  : total T
| TotalV x xi
  : total xi → total (V x xi).

Inductive composed: trace → Prop :=
| ComposedV x xi
  : composed (V x xi).

Lemma partial_decision (xi: trace)
  : {partial xi} + {¬ partial xi}.
Proof.
  general induction xi.
  - left. constructor.
  - right. intros A. inv A.
  - destruct IHxi as [A | B].
    + left. eauto using partial.
    + right. intros A. apply B. inv A. eauto.
Qed.

Instance partial_dec (xi: trace): dec (partial xi).
Proof. unfold dec. apply partial_decision. Qed.

Lemma not_partial_total xi
  : ¬ partial xi → total xi.
Proof.
  general induction xi; eauto using total.
  - exfalso. apply H. eauto using partial.
  - constructor. apply IHxi. intros A.
    apply H. eauto using partial.
Qed.

Fixpoint concat xi1 xi2 :=
  match xi1 with
  | P ⇒ P
  | T ⇒ xi2
  | V x xi ⇒ V x (concat xi xi2)
  end.

Lemma inv_concat_P xi1 xi2
  : concat xi1 xi2 = P → xi1 = P ∨ xi1 = T ∧ xi2 = P.
Proof.
  general induction xi1; eauto.
Qed.

Lemma inv_concat_T xi1 xi2
  : concat xi1 xi2 = T → xi1 = T ∧ xi2 = T.
Proof.
  general induction xi1; eauto.
Qed.

Lemma inv_concat_V xi1 xi2 x xi
  : concat xi1 xi2 = V x xi → (∃ xi', xi1 = V x xi' ∧ xi = concat xi' xi2) ∨ (xi1 = T ∧ xi2 = V x xi).
Proof.
  general induction xi1; eauto.
Qed.

Lemma concat_assoc xi1 xi2 xi3
  : concat (concat xi1 xi2) xi3 = concat xi1 (concat xi2 xi3).
Proof.
  general induction xi1; simpl; eauto.
  rewrite (IHxi1 xi2 xi3). eauto.
Qed.

Lemma concat_T_iden_right xi:
  xi = concat xi T.
Proof.
  general induction xi; simpl; eauto.
  rewrite <- IHxi. eauto.
Qed.

Lemma concat_T_iden_left xi:
  xi = concat T xi.
Proof.
  general induction xi; simpl; eauto.
Qed.

Lemma concat_P_iden_right xi:
  partial xi → xi = concat xi P.
Proof.
  intros H. general induction H; simpl; eauto.
  rewrite <- IHpartial. eauto.
Qed.

Lemma concat_partial_absorb_right xi1 xi2:
  partial xi1 → concat xi1 xi2 = xi1.
Proof.
  intros. general induction H; simpl; eauto.
  rewrite (IHpartial xi2). eauto.
Qed.

Lemma concat_partial_preserve_right xi1 xi2:
  partial xi2 → partial (concat xi1 xi2).
Proof.
  intros. general induction xi1; simpl; eauto using partial.
Qed.

Lemma concat_total_compose xi1 xi2
  : total xi1 → total xi2 → total (concat xi1 xi2).
Proof.
  intros. general induction H.
  - rewrite <- concat_T_iden_left. eauto.
  - simpl. constructor. eauto.
Qed .

Lemma concat_P_partial_right xi
  : partial (concat xi P).
Proof.
  general induction xi; simpl; eauto using partial.
Qed.

Lemma concat_partial_compose xi1 xi2
  : partial (concat xi1 xi2) → total xi1 → partial xi2.
Proof.
  intros. general induction H0.
  - rewrite <- concat_T_iden_left in H. eauto.
  - simpl in H. inv H. apply IHtotal. eauto.
Qed.

Lemma concat_total_decompose xi1 xi2
  : total (concat xi1 xi2) → total xi1 ∧ total xi2.
Proof.
  intros. general induction xi1.
  - rewrite concat_partial_absorb_right in H; eauto using partial.
    inv H.
  - rewrite <- concat_T_iden_left in H. split; eauto using total.
  - simpl in H. inv H. destruct (IHxi1 xi2) as [A B]; eauto.
    split; eauto using total.
Qed.

Lemma concat_composed_compose xi1 xi2
  : total xi1 → composed xi2 → composed (concat xi1 xi2).
Proof.
  intros. general induction H; simpl; eauto using composed.
Qed.

Fixpoint butLast xi :=
  match xi with
  | P ⇒ P
  | T ⇒ T
  | V x P ⇒ P
  | V x T ⇒ T
  | V x xi ⇒ V x (butLast xi)
  end.

Lemma butLast_V_distribute x xi
  : composed xi
    → butLast (V x xi) = V x (butLast xi).
Proof.
  intros. destruct H. destruct xi; simpl; eauto.
Qed.

Lemma butLast_P_distribute xi
  : butLast (concat xi P)
    = concat (butLast xi) P.
Proof.
  destruct xi; simpl; eauto.
  general induction xi; simpl; eauto.
  f_equal. eauto.
Qed.

Lemma butLast_concat_distribute xi1 xi2
  : composed xi2
    → total xi1
    → butLast (concat xi1 xi2)
       = concat xi1 (butLast xi2).
Proof.
  intros. general induction xi1; asimpl; eauto.
  inv H0.
  change (butLast (V x (concat xi1 xi2)) = (V x (concat xi1 (butLast xi2)))).
  rewrite <- IHxi1; eauto.
  rewrite butLast_V_distribute; eauto.
  apply concat_composed_compose; eauto.
Qed.

Lemma butLast_partial_preserve xi
  : partial xi → partial (butLast xi).
Proof.
  intros. general induction H.
  - asimpl. eauto using partial.
  - asimpl. destruct xi; eauto using partial.
Qed.

Lemma butLast_total_preserve xi
  : total xi → total (butLast xi).
Proof.
  intros. general induction H.
  - asimpl. eauto using total.
  - asimpl. destruct xi; eauto using total.
Qed.

Fixpoint ren_trace f xi :=
  match xi with
  | P ⇒ P
  | T ⇒ T
  | (V x xi) ⇒ V (f x) (ren_trace f xi)
  end.

Lemma ren_concat_distribute f xi1 xi2
  : ren_trace f (concat xi1 xi2) = concat (ren_trace f xi1) (ren_trace f xi2).
Proof.
  intros. general induction xi1; simpl; eauto.
  rewrite IHxi1. eauto.
Qed.

Lemma ren_trace_id_inc_shift xi
  : xi= ren_trace shift (ren_trace (+1) xi).
Proof.
  general induction xi; simpl; eauto.
  rewrite <- IHxi. eauto.
Qed.

Lemma ren_total_preserve f xi
  : total xi → total (ren_trace f xi).
Proof.
  intros. general induction H; simpl; eauto using total.
Qed.

Lemma ren_partial_preserve f xi
  : partial xi → partial (ren_trace f xi).
Proof.
  intros. general induction H; simpl; eauto using partial.
Qed.

Lemma ren_partial_origin f xi
  : partial (ren_trace f xi) → partial xi.
Proof.
  intros. general induction xi; simpl; eauto using partial.
  simpl in H. inv H. constructor. eauto.
Qed.

Lemma ren_total_origin f xi
  : total (ren_trace f xi) → total xi.
Proof.
  intros. general induction xi; simpl; eauto using total.
  simpl in H. inv H. constructor. eauto.
Qed.

Lemma ren_composed_preserve f xi
  : composed xi → composed (ren_trace f xi).
Proof.
  intros. inv H. simpl. eauto using composed.
Qed.

Lemma ren_butLast_distribute f xi
  : butLast (ren_trace f xi) = ren_trace f (butLast xi).
Proof.
  destruct xi; simpl; eauto.
  general induction xi; asimpl; eauto.
  f_equal. eauto.
Qed.

Inductive boundT: nat → trace → Prop :=
| BoundTP n
  : boundT n P
| BoundTT n
  : boundT n T
| BoundTV n xi x
  : (n ≤ x) → boundT n xi → boundT n (V x xi).

Lemma boundT_concat_compose n xi1 xi2
  : boundT n xi1 → boundT n xi2 → boundT n (concat xi1 xi2).
Proof.
  intros. general induction H; eauto using boundT.
Qed.

Lemma boundT_concat_decompose_left n xi1 xi2
  : boundT n (concat xi1 xi2)
    → boundT n xi1.
Proof.
  intros. general induction xi1; simpl in H; eauto using boundT.
  inv H. eauto using boundT.
Qed.

Lemma boundT_concat_decompose_right n xi1 xi2
  : boundT n (concat xi1 xi2)
    → total xi1
    → boundT n xi2.
Proof.
  intros. general induction H0; simpl in H; eauto.
  inv H. eauto.
Qed.

Lemma boundT_zero xi
  : boundT 0 xi.
Proof.
  general induction xi; eauto using boundT.
  constructor; eauto. omega.
Qed.

Lemma boundT_ren_shift_preserve n xi
  : boundT (S n) xi
    → boundT n (ren_trace shift xi).
Proof.
  intros. general induction H; simpl; eauto using boundT.
  constructor; eauto.
  destruct x; asimpl; try omega.
Qed.

Lemma boundT_ren_shift_reconstruct n xi
  : boundT n (ren_trace shift xi)
    → boundT 1 xi
    → boundT (S n) xi.
Proof.
  intros. general induction H0; simpl in H; eauto using boundT.
  inv H1. constructor; eauto.
  destruct x; simpl in H5; try omega.
Qed.

Lemma boundT_step n m xi
  : boundT n xi → m ≤ n → boundT m xi.
Proof.
  intros. general induction H; eauto using boundT.
  constructor; try omega. eauto.
Qed.

Lemma boundT_ren_lift n xi
  : boundT n (ren_trace (+n) xi).
Proof.
  general induction xi; simpl; eauto using boundT.
  constructor; eauto.
  omega.
Qed.

Lemma boundT_butLast_preserve n xi
  : boundT n xi → boundT n (butLast xi).
Proof.
  intros. general induction H; simpl; eauto using boundT.
  destruct xi; eauto using boundT.
Qed.

Inductive terminal : nat → trace → Prop :=
| TerminalT x
  : terminal x (V x T)
| TerminalP x
  : terminal x (V x P)
| TerminalV x y xi
  : x ≠ y → terminal x xi → terminal x (V y xi).

Lemma terminal_composed x xi
  : terminal x xi → composed xi.
Proof.
  intros. general induction H; eauto using composed.
Qed.

Lemma terminal_unique x y xi
  : terminal x xi
    → terminal y xi
    → x = y.
Proof.
  intros. general induction H.
  - inv H0; eauto. inv H4.
  - inv H0; eauto. inv H4.
  - inv H1.
    + inv H0.
    + inv H0.
    + apply IHterminal. eauto.
Qed.

Lemma terminal_concat_compose n x xi1 xi2
  : boundT n xi1
    → total xi1
    → x < n
    → terminal x xi2
    → terminal x (concat xi1 xi2).
Proof.
  intros. general induction H; eauto using terminal.
  - inv H0.
  - simpl. constructor; try omega.
    inv H1. eauto.
Qed.

Lemma terminal_concat_P_compose x xi
  : terminal x xi → terminal x (concat xi P).
Proof.
  intros. general induction H; simpl; eauto using terminal.
Qed.

Lemma boundT_terminal_compose n x xi
  : boundT n (butLast xi)
    → terminal x xi
    → n ≤ x
    → boundT n xi.
Proof.
  intros. general induction xi; eauto using boundT.
  inv H0; eauto using boundT.
  destruct xi.
  - inv H6.
  - inv H6.
  - rewrite butLast_V_distribute in H; eauto.
    + inv H. constructor; eauto.
    + apply terminal_composed in H6. eauto.
Qed.

Lemma terminal_boundT_contradict n xi x
  : boundT n xi → x < n → terminal x xi → False.
Proof.
  intros. general induction H1.
  - inv H. omega.
  - inv H. omega.
  - inv H0. apply IHterminal with (n:= n); eauto.
Qed.

Lemma terminal_ren_shift_preserve x xi
  : terminal (S x) xi
    → boundT 1 xi
    → terminal x (ren_trace shift xi).
Proof.
  intros. general induction H; simpl; eauto using terminal.
  constructor.
  - intros A. apply H. rewrite A. destruct y; asimpl; eauto.
    inv H1. exfalso. omega.
  - inv H1. eauto.
Qed.

Lemma terminal_ren_shift_reconstruct x xi
  : terminal x (ren_trace shift xi)
    → boundT 1 xi
    → terminal (S x) xi.
Proof.
  intros. general induction H0; simpl in H.
  - inv H.
  - inv H.
  - simpl in H1. destruct xi.
    + simpl in H1. inv H1.
      × assert (S (shift x) = x).
        { destruct x; asimpl; try omega. }
        rewrite H2. constructor.
      × inv H6.
    + simpl in H1. inv H1.
      × assert (S (shift x) = x).
        { destruct x; asimpl; try omega. }
        rewrite H2. constructor.
      × inv H6.
    + simpl in H1. inv H1.
      constructor.
      × destruct x; simpl in H5; try omega.
      × apply IHboundT; eauto.
Qed.

Lemma terminal_concat_decompose_right x n xiA xiB
  : terminal x (concat xiA xiB)
    → boundT n xiA
    → x < n
    → terminal x xiB.
Proof.
  intros. general induction H0; simpl in H; eauto.
  - inv H.
  - apply IHboundT; eauto.
    simpl in H1. inv H1; try omega; eauto.
Qed.

Lemma terminal_concat_decompose x xiA xiB
  : terminal x (concat xiA xiB)
    → ((partial xiA ∨ xiB = T ∨ xiB = P)/\ terminal x xiA)
       ∨ (total xiA ∧ terminal x xiB).
Proof.
  intros. general induction xiA; simpl in H; eauto.
  - inv H.
  - right. split; eauto using total.
  - inv H.
    + symmetry in H3. destruct (inv_concat_T H3).
      left. rewrite H0. rewrite H1. split; eauto using terminal.
    + symmetry in H3. destruct (inv_concat_P H3) as [H1 | [H2 H4]].
      × rewrite H1. left. split; eauto using terminal. left. eauto using partial.
      × rewrite H2. rewrite H4. left. split; eauto using terminal.
    + destruct (IHxiA x0 xiB H4) as [ [H1 H2] |[H1 H2]].
      × destruct H1 as [H5 | [H6 |H7]]; left; split; eauto using terminal.
        left. eauto using partial.
      × right. split; eauto using terminal, total.
Qed.

Definition tailrec_trace n xi := (∃ x, x < n ∧ terminal x xi ∧ boundT n (butLast xi)) ∨ boundT n xi.

Lemma tailrec_trace_butLast_boundT n xi
  : tailrec_trace n xi → (boundT n (butLast xi)).
Proof.
  intros. destruct H as [[x [H1 [H2 H3]]] | H3]; eauto.
  apply boundT_butLast_preserve. eauto.
Qed.