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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive reg: nat → cfp → Prop :=
| RegEps n
  : reg n CFPEps
| RegVar n x
  : n ≤ x → reg n (CFPVar x)
| RegSeq n s t
  : reg n s → reg n t → reg n (CFPSeq s t)
| RegChoice n s t
  : reg n s → reg n t → reg n (CFPChoice s t)
| RegStar n s
  : reg (S n) s → reg n (Star s)
| RegNull n
  : reg n Null.

Fact reg_bound n s
  : reg n s → bound 0 n s.
Proof.
  intros. general induction H; eauto using bound.
  constructor. constructor; eauto using bound.
  constructor; eauto using bound.
  assert (1 = 0+1); try omega. rewrite H0.
  apply bound_shift_interval. asimpl.
  eauto.
Qed.

Fact reg_tailrec n s
  : reg n s → tailrec n s.
Proof.
  intros. general induction H; eauto using tailrec, reg_bound.
Qed.

Fact reg_step n m s
  : reg n s → m ≤ n → reg m s.
Proof.
  intros. general induction H; eauto using reg.
  - constructor. omega.
  - constructor. apply IHreg. omega.
Qed.

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

Fact reg_shift s n
  : reg (S n) s → reg n s.[ren(shift)].
Proof.
  intros.
  apply reg_name_preserve with (n:= S n); eauto.
  intros. destruct x; asimpl; try omega.
Qed.

Fact bound_reg n k s
  : reg n s → bound n k s → reg (n+k) s.
Proof.
  intros. general induction H; eauto using reg.
  - inv H0; constructor; omega.
  - inv H1. eauto using reg.
  - inv H1. eauto using reg.
  - inv H0. constructor. apply IHreg.
    inv H4. inv H7. eauto.
Qed.

Inductive regi: cfp → Prop :=
| RegiEps
  : regi CFPEps
| RegiVar x
  : regi (CFPVar x)
| RegiSeq s t
  : regi s → regi t → regi (CFPSeq s t)
| RegiChoice s t
  : regi s → regi t → regi (CFPChoice s t)
| RegiNull
  : regi Null
| RegiStar s
  : bound 0 1 s → regi s → regi (Star s).

Fact reg_regi n s
  : reg n s → regi s.
Proof.
  intros. general induction H; eauto using regi.
  constructor; eauto.
  apply reg_bound in H. apply bound_step with (k:= S n); eauto.
  omega.
Qed.

Fact regi_reg s
  : regi s → reg 0 s.
Proof.
  intros. general induction H; eauto using reg.
  - constructor. omega.
  - constructor. assert (1 = 0 +1); try omega.
    rewrite H1. apply bound_reg; eauto.
Qed.

Fact reg_correct n s
  : reg n s ↔ regi s ∧ bound 0 n s.
Proof.
  split; intros.
  - split; eauto using reg_regi, reg_bound.
  - destruct H. apply regi_reg in H.
    assert (n = 0 + n); try omega.
    rewrite H1.
    eauto using bound_reg.
Qed.