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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive lin: nat → cfp → Prop :=
| LinEps n
  : lin n CFPEps
| LinVar n x
  : lin n (CFPVar x)
| LinSeq n x t
  : n ≤ x → lin n t → lin n (CFPSeq (CFPVar x) t)
| LinChoice n s t
  : lin n s → lin n t → lin n (CFPChoice s t)
| LinFix n s
  : lin (S n) s → lin n (CFPFix s).

Fact lin_step n m s
  : lin n s → m ≤ n → lin m s.
Proof.
  intros. general induction H; eauto using lin.
  - constructor; eauto. omega.
  - constructor; eauto. apply IHlin. omega.
Qed.

Fact lin_tailrec n s
  : lin n s → tailrec n s.
Proof.
  intros. general induction H; eauto using tailrec.
  constructor; eauto; eauto using tailrec.
  constructor 3. omega.
Qed.

Fact lin_ren_preserve s n m f
  : (∀ x, n ≤ x → m ≤ f x)
    → lin n s → lin m s.[ren(f)].
Proof.
  intros. general induction H0; eauto using lin.
  constructor. asimpl. apply IHlin.
  intros. destruct x; try omega.
  asimpl. assert (m ≤ f x).
  { apply H. omega. }
  omega.
Qed.

Fact bound_lin n k s
  : lin n s → bound n k s → lin (n+k) s.
Proof.
  intros. general induction H; eauto using lin.
  - inv H1. inv H6.
    + constructor; eauto. omega.
    + constructor; eauto.
  - inv H1. constructor; eauto.
  - inv H0. constructor. eauto.
Qed.