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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive bound: nat → nat →cfp→ Prop :=
| BoundEps n k
  : bound n k CFPEps
| BoundVar1 n k m
  : m < n → bound n k(CFPVar m)
| BoundVar2 n k m
  : m ≥ n+k → bound n k (CFPVar m)
| BoundChoice n k s t
  : bound n k s → bound n k t → bound n k (CFPChoice s t)
| BoundSeq n k s t
  : bound n k s → bound n k t → bound n k (CFPSeq s t)
| BoundFix n k s
  : bound (S n) k s → bound n k (CFPFix s).

Lemma bound_zero n s
  : bound n 0 s.
Proof.
  general induction s; eauto using bound.
  - decide (x < n).
    + constructor. eauto.
    + constructor 3. omega.
Qed.

Lemma bound_step n k s l
  : bound n k s → l≤ k → bound n l s.
Proof.
  intros. general induction H; eauto using bound.
  constructor 3. omega.
Qed.

Lemma bound_shift_interval n k s i
  : bound n (k + i) s → bound (n+i) k s.
Proof.
  intros. general induction H; eauto using bound.
  - constructor. omega.
  - constructor 3. omega.
Qed.

Lemma bound_trans n k m s
  : bound n k s → bound (n+k) m s → bound n (k+m) s.
Proof.
  intros. general induction H; eauto using bound.
  - inv H0.
    + constructor. omega.
    + constructor 3. omega.
  - inv H1. eauto using bound.
  - inv H1. eauto using bound.
  - inv H0. eauto using bound.
Qed.

Lemma bound_ren s k n f
  : (∀ i, f i ≥ k+n ∨ f i < n) → bound n k s.[ren(f)].
Proof.
  general induction s; asimpl; eauto using bound.
  - constructor. apply IHs. intros. destruct i.
    + asimpl. right. omega.
    + asimpl. destruct (H i).
      × left. omega.
      × right. omega.
  - destruct (H x).
    + constructor 3. omega.
    + constructor. omega.
Qed.

Lemma bound_ren_preserve n m k l s f
  : bound n k s
    → (∀ x, x < n → f x < m)
    → (∀ x, n+k ≤ x → m + l ≤ f x)
    → bound m l s.[ren f].
Proof.
  intros. general induction H; eauto using bound.
  asimpl. constructor. apply IHbound.
  - intros. destruct x.
    + asimpl. omega.
    + asimpl. assert (f x < m).
      { apply H0. omega. }
      omega.
  - intros. destruct x.
    + inv H2.
    + asimpl. assert (m+l ≤ f x).
      { apply H1. omega. }
      omega.
Qed.

Lemma bound_lift n k s
  : bound n k s
    → bound (S n) k s.[ren(+1)].
Proof.
  intros.
  apply bound_ren_preserve with (n:= n) (k:= k); eauto.
  - intros. asimpl. omega.
  - intros. asimpl. omega.
Qed.

Lemma bound_shift n k t
  : bound n (S k) t
    → bound n k t.[ren shift].
Proof.
  intros. apply bound_ren_preserve with (n:= n) (k:= S k); eauto.
  - intros. destruct x.
    + asimpl. eauto.
    + asimpl. omega.
  - intros. destruct x.
    + exfalso. omega.
    + asimpl. omega.
Qed.

Lemma bound_subst s n k sigma f
  : bound n k s → simulatesI sigma (f >>> ids) n k → s.[sigma] = s.[ren(f)].
Proof.
  intros. general induction H; asimpl; eauto.
  - destruct H0 as [H1 H2]. eauto.
  - destruct H0 as [H1 H2]. eauto.
  - rewrite (IHbound1 sigma f H1).
    rewrite (IHbound2 sigma f H1). eauto.
  - rewrite (IHbound1 sigma f H1).
    rewrite (IHbound2 sigma f H1). eauto.
  - f_equal. apply IHbound. split.
    + destruct H0 as [H1 H2]. intros. destruct i.
      × asimpl. eauto.
      × asimpl. rewrite H1; eauto. omega.
    + destruct H0 as [H1 H2]. intros. destruct i.
      × asimpl. eauto.
      × asimpl. rewrite H2; eauto. omega.
Qed.

Lemma bound_subst_preserve n m k s sigma
  : bound n k s
    → (∀ i, i < n → bound m k (sigma i))
    → (∀ i, i≥ n+k → bound m k (sigma i))
    → bound m k (s.[sigma]).
Proof.
  intros.
  general induction H; asimpl; eauto using bound.
  constructor. apply IHbound.
  - intros. destruct i.
    + asimpl. constructor. omega.
    + asimpl. assert (i < n).
      { omega. }
      specialize (H0 i H3).
      apply bound_lift. eauto.
  - intros. destruct i.
    + asimpl. inv H2.
    + asimpl. assert (i ≥ n + k); try omega.
      specialize (H1 i H3).
      apply bound_lift. eauto.
Qed.

Lemma bound_boundT k s xi
  : bound 0 k s → TC s xi → boundT k xi.
Proof.
  intros. general induction H0; eauto using boundT.
  - inv H.
    + inv H3.
    + constructor; eauto using boundT.
  - inv H.
    + inv H3.
    + constructor; eauto using boundT.
  - inv H. apply boundT_concat_compose; eauto.
  - inv H. eauto.
  - inv H. eauto.
  - inv H. apply IHTC. apply bound_subst_preserve with (n:= 1); eauto.
    + intros. assert (i = 0); try omega.
      rewrite H2. asimpl. eauto.
    + intros. assert (∃ j, i = S j).
      { ∃ (i - 1). omega. }
      destruct H2 as [j A].
      rewrite A. asimpl. constructor 3. omega.
Qed.