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

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Inductive tailrec: nat → cfp → Prop :=
| TailRecEps n
  : tailrec n CFPEps
| TailRecVar n m
  : tailrec n (CFPVar m)
| TailRecChoice n s t
  : tailrec n s → tailrec n t → tailrec n (CFPChoice s t)
| TailRecSeq n s t
  : bound 0 n s → tailrec n s → tailrec n t → tailrec n (CFPSeq s t)
| TailRecFix n s
  : tailrec (S n) s → tailrec n (CFPFix s).

Fact tailrec_step n m s
  : tailrec n s → m ≤ n → tailrec m s.
Proof.
  intros. general induction H; eauto using tailrec, bound_step.
  constructor. apply IHtailrec. omega.
Qed.

Fact tailrec_bound_lift n s k
  : tailrec n s → bound n k s → tailrec (n+ k) s.
Proof.
  intros. general induction H; eauto using tailrec.
  - inv H1; eauto using tailrec.
  - inv H2. eauto using tailrec, bound_trans.
  - inv H0. eauto using tailrec.
Qed.

Fact tailrec_ren_preserve n m s f
  : tailrec n s
    → (∀ x, x < n → f x < m)
    → (∀ x, n ≤ x → m ≤ f x)
    → tailrec m s.[ren f].
Proof.
  intros. general induction H; eauto using tailrec; asimpl.
  - constructor; eauto.
    apply bound_ren_preserve with (n:= 0) (k:= n); eauto.
    intros. inv H4.
  - constructor. apply IHtailrec.
    + intros. destruct x; asimpl; try omega.
      assert (f x < m).
      { apply H0. omega. }
      omega.
    + intros. destruct x; try omega.
      asimpl. assert (m ≤ f x).
      { apply H1. omega. }
      omega.
Qed.

Fact tailrec_lift n s
  : tailrec n s
    → tailrec (S n) s.[ren(+1)].
Proof.
  intros.
  apply tailrec_ren_preserve with (n:= n); eauto; intros; asimpl; omega.
Qed.

Fact tailrec_subst_preserve k s n t
  : tailrec (S n) s
    → tailrec n t
    → k ≤ n
    → tailrec n (s.[substPos k t]).
Proof.
  intros. general induction H; eauto using tailrec.
  - decide (m = k).
    + asimpl. rewrite e. rewrite substPos_eq. eauto.
    + decide (m < k).
      × asimpl. rewrite substPos_lt; try omega.
        constructor.
      × asimpl. rewrite substPos_gt; try omega.
        constructor. assert (k ≤ m); try omega.
        assert (k < m); try omega. destruct (le_lt_or_eq k m); eauto.
        exfalso. apply n. eauto.
  - asimpl. constructor; eauto.
    rewrite bound_subst with (n:= 0) (k:= S n0) (f:= shift); eauto.
    + apply bound_ren_preserve with (n:= 0) (k:= S n0); eauto; intros.
      { inv H4. }
      { destruct x; asimpl; try omega. }
    + split; intros.
      × inv H4.
      × asimpl. assert (k < i); try omega.
        rewrite substPos_gt; try omega.
        destruct i; asimpl; eauto.
        assert (i - 0 = i); try omega.
        rewrite H6. eauto.
  - asimpl. constructor. rewrite substPos_up.
    apply IHtailrec; try omega.
    apply tailrec_lift. eauto.
Qed.

Fact tailrec_terminal n s xi
  : tailrec n s → TC s xi → boundT n xi ∨ (∃ x, x < n ∧ terminal x xi ∧ boundT n (butLast xi)).
Proof.
  intros. general induction H0.
  - left; eauto using boundT.
  - left; eauto using boundT.
  - decide (x < n).
    + right. ∃ x. split; eauto using terminal, boundT.
    + left. constructor; eauto using boundT. omega.
  - decide (x< n).
    + right. ∃ x. split; eauto using terminal, boundT.
    + left. constructor; eauto using boundT. omega.
  - inv H. destruct (IHTC2 n) as [A2 | [x [B2 [C2 D2]]]]; eauto.
    + left. apply boundT_concat_compose; eauto.
      apply bound_boundT with (s:= s); eauto.
    + destruct (IHTC1 n H4) as [A1 | [x1 [B1 [C1 D1]]]].
      × decide (partial xi1).
        { left. rewrite concat_partial_absorb_right; eauto. }
        { apply not_partial_total in n0. right.
          ∃ x. split; eauto. split.
          - apply terminal_concat_compose with (n:= n); eauto.
          - rewrite butLast_concat_distribute; eauto.
            + apply boundT_concat_compose; eauto.
            + apply terminal_composed in C2. eauto. }
      × assert (boundT n xi1).
        { apply bound_boundT with (s:= s); eauto. }
        exfalso.
        apply terminal_boundT_contradict with (n:= n) (xi:= xi1) (x:= x1); eauto.
  - inv H. destruct (IHTC n H4) as [A | [x [B [C D]]]].
    + left. eauto.
    + right. ∃ x. split; eauto.
  - inv H. destruct (IHTC n H5) as [A | [x [B [C D]]]].
    + left. eauto.
    + right. ∃ x. split; eauto.
  - inv H. apply IHTC. rewrite substPos_zero_extens.
    apply tailrec_subst_preserve; eauto. omega.
Qed.

Fact tailrec_tailrec_trace n s xi
  : tailrec n s → TC s xi → tailrec_trace n xi.
Proof.
  intros. apply tailrec_terminal with (xi:= xi) in H; eauto.
  destruct H.
  - right. eauto.
  - left. eauto.
Qed.

Inductive trec: nat → nat → cfp → Prop:=
| TrecEps n k
  : trec n k CFPEps
| TrecVar1 n k x
  : x < n → trec n k (CFPVar x)
| TrecVar2 n k x
  : n+k ≤ x → trec n k (CFPVar x)
| TrecChoice n k s t
  : trec n k s → trec n k t → trec n k (CFPChoice s t)
| TrecSeq n k s t
  : trec 0 (n+k) s → trec n k t → trec n k (CFPSeq s t)
| TrecFix n k s
  : trec (S n) k s → trec n k (CFPFix s).

Fact trec_bound_lift n s k l
  : trec (n+k) l s → bound n k s → trec n (k+l) s.
Proof.
  intros. general induction H0; eauto using trec.
  - inv H0.
    + constructor. omega.
    + constructor 3. omega.
  - inv H. eauto using trec.
  - inv H. constructor; eauto.
    assert (n + (k + l) = n + k + l); try omega.
    rewrite H0. eauto.
  - inv H. eauto using trec.
Qed.

Fact trec_ren_preserve n m k l s f
  : trec n k s
    → (∀ x, x < n → f x < m)
    → (∀ x, n+k ≤ x → m + l ≤ f x)
    → trec m l s.[ren f].
Proof.
  intros. general induction H; eauto using trec.
  - asimpl. constructor; eauto.
    apply IHtrec1; intros; try omega.
    asimpl. apply H2. omega.
  - asimpl. constructor. apply IHtrec.
    + intros. destruct x; asimpl; try omega.
      assert (f x < m).
      { apply H0. omega. }
      omega.
    + intros. destruct x; asimpl; try omega.
      assert (m+l ≤ f x).
      { apply H1. omega. }
      omega.
Qed.

Fact trec_shift n k t
  : trec n (S k) t
    → trec n k t.[ren shift].
Proof.
  intros. apply trec_ren_preserve with (n:= n) (k:= S k); eauto.
  - intros. destruct x; asimpl; eauto; omega.
  - intros. destruct x; asimpl; omega.
Qed.

Fact trec_bound_ren m i n k f s
  : bound m i s
    → (∀ x, x < m → f x = x)
    → (∀ x, x ≥ m+i → f x = x - i)
    → trec (m + i + n) k s
    → trec (m+ n) k s.[ren f].
Proof.
  intros. general induction H; asimpl; eauto using trec.
  - inv H2.
    + constructor. rewrite H0; eauto.
      omega.
    + constructor. rewrite H0; try omega.
  - inv H2.
    + constructor. rewrite H1; try omega.
    + constructor 3. rewrite H1; try omega.
  - inv H3. constructor; eauto using trec.
  - inv H3. constructor; eauto using trec.
    apply trec_ren_preserve with (n:= 0)(k:= n + k + n0 + k0); eauto.
    + intros. inv H4.
    + intros. decide (x < n).
      × rewrite H1; eauto. omega.
      × decide (x ≥ n + k).
        { rewrite H2; auto. omega. }
        { exfalso. omega. }
  - constructor. assert (S (n+n0) = S n + n0); try omega.
    inv H2. apply IHbound; eauto.
    + intros. destruct x; simpl; eauto.
      rewrite H0; eauto. omega.
    + intros. destruct x; try omega.
      simpl. destruct k; rewrite H1; omega.
Qed.

Fact trec_tailrec n k s
  : trec n k s → tailrec (n + k) s ∧ bound n k s.
Proof.
  intros. general induction H; eauto using tailrec, bound.
  - destruct IHtrec1 as [A1 B1].
    destruct IHtrec2 as [A2 B2].
    split; eauto using tailrec, bound.
  - destruct IHtrec1 as [A1 B1].
    destruct IHtrec2 as [A2 B2].
    split; eauto using tailrec.
    constructor; eauto.
    assert (bound (0+n) k s).
    { apply bound_shift_interval.
      assert (n+k = k+n); try omega.
      rewrite <- H1. eauto. }
    simpl in H1. eauto.
  - destruct IHtrec as [A B].
    split; eauto using tailrec, bound.
Qed.

Fact tailrec_trec n k s
  : tailrec n s → bound n k s → trec n k s.
Proof.
  intros. general induction H; eauto using trec.
  - inv H0; eauto using trec.
  - inv H1; eauto using trec.
  - inv H2. constructor; eauto using trec_bound_lift.
  - inv H0. eauto using trec.
Qed.

Lemma trec_correct s
  : tailrec 0 s ↔ trec 0 0 s.
Proof.
  split.
  - intros. apply tailrec_trec; eauto.
    apply bound_zero.
  - intros. apply trec_tailrec in H.
    destruct H. eauto.
Qed.