Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base Congruence FreeVariables Regularity TailRecursion DistributeFix.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fixpoint decomp (s: cfp) :=
  match s with
  | CFPEps ⇒ (CFPEps, Null)
  | (CFPVar 0) ⇒ (Null, CFPEps)
  | (CFPVar x) ⇒ (CFPVar x, Null)
  | (CFPSeq s t) ⇒ (match (decomp t) with
                     | (t1, t2) ⇒ (CFPSeq s t1, CFPSeq s t2)
                     end)
  | (CFPChoice s t) ⇒ (match (decomp s, decomp t) with
                        | ((s1,s2),(t1,t2)) ⇒ (CFPChoice s1 t1, CFPChoice s2 t2)
                        end)
  | (CFPFix s) ⇒ (CFPFix s, Null)
  end.

Fact decomp_total s
  : ∃ s1 s2, (s1, s2) = decomp s.
Proof.
  general induction s.
  - simpl. ∃ CFPEps, Null; eauto.
  - destruct IHs1 as [sa [sb A]].
    destruct IHs2 as [t1 [t2 B]].
    simpl. ∃ (CFPSeq s1 t1), (CFPSeq s1 t2).
    rewrite <- B. eauto.
  - destruct IHs1 as [sa [sb A]].
    destruct IHs2 as [t1 [t2 B]].
    simpl. ∃ (CFPChoice sa t1), (CFPChoice sb t2).
    rewrite <- A. rewrite <- B. eauto.
  - destruct IHs as [t1 [t2 A]]. simpl.
    ∃ (CFPFix s) , Null. eauto.
  - simpl. destruct x.
    + ∃ Null, CFPEps. eauto.
    + ∃ (CFPVar (S x)), Null. eauto.
Qed.

Lemma decomp_correct n s s1 s2
  : tailrec n s → (s1, s2) = decomp s → s =T part s1 s2.
Proof.
  intros. general induction H.
  - simpl in H0. unfold part.
    rewrite Seq_Null_absorb_left.
    rewrite Choice_Null_iden_right. reflexivity.
  - simpl in H0. destruct m.
    + unfold part. inv H0.
      rewrite Choice_Null_iden_left.
      rewrite Seq_Eps_iden_left. reflexivity.
    + unfold part. inv H0.
      rewrite Seq_Null_absorb_left.
      rewrite Choice_Null_iden_right. reflexivity.
  - unfold part. simpl in H1.
    destruct (decomp s) as [sa sb].
    destruct (decomp t) as [t1 t2].
    inv H1. rewrite IHtailrec1; eauto.
    rewrite IHtailrec2; eauto.
    unfold part. rewrite Choice_assoc.
    rewrite Seq_Choice_distribute2.
    setoid_rewrite Choice_assoc at 1.
    setoid_rewrite Choice_commute at 2.
    setoid_rewrite Choice_assoc at 1.
    setoid_rewrite Choice_commute at 3.
    reflexivity.
  - simpl in H2. unfold part.
    destruct (decomp t) as [t1 t2]. inv H2.
    rewrite IHtailrec2; eauto.
    unfold part.
    rewrite Seq_Choice_distribute1.
    setoid_rewrite Seq_assoc. reflexivity.
  - simpl in H0. unfold part.
    rewrite Seq_Null_absorb_left.
    rewrite Choice_Null_iden_right.
    reflexivity.
Qed.

Lemma reg_decomp n k s s1 s2
  : trec (S n) k s
    → reg 0 s
    → (s1, s2) = decomp s
    → reg 1 s1 ∧ trec (S n) k s1 ∧ reg (S n + k) s2.
Proof.
  intros. general induction H; split; eauto using reg, trec.
  - simpl in H1. destruct x.
    + inv H1. eauto using reg.
    + inv H1. constructor. omega.
  - simpl in H1. destruct x.
    + inv H1. split; eauto using trec, reg.
    + inv H1. split; eauto using trec, reg.
  - simpl in H1. destruct x.
    + inv H1. eauto using reg.
    + inv H1. constructor. omega.
  - simpl in H1. destruct x.
    + inv H1. split; eauto using trec, reg.
      constructor. constructor. omega.
    + inv H1. split; eauto using trec, reg.
  - inv H1. simpl in H2. destruct (decomp s) as [sa sb].
    destruct (decomp t) as [t1 t2]. inv H2.
    destruct (IHtrec1 n0 sa sb) as [A [B C]]; eauto.
    destruct (IHtrec2 n0 t1 t2) as [D [E F]]; eauto.
    constructor; eauto.
  - simpl in H2. inv H1.
    destruct (decomp s) as [sa sb].
    destruct (decomp t) as [t1 t2]. inv H2.
    destruct (IHtrec1 n0 sa sb) as [A [B C]]; eauto.
    destruct (IHtrec2 n0 t1 t2) as [D [E F]]; eauto.
    split; eauto using trec, reg.
  - simpl in H2. inv H1.
    destruct (decomp t) as [t1 t2]. inv H2.
    destruct (IHtrec2 n0 t1 t2) as [D [E F]]; eauto.
    constructor; eauto. assert (1 = 0 +1); try omega.
    rewrite H3.
    apply bound_reg; eauto.
    apply trec_tailrec in H. destruct H as [H H'].
    apply bound_step with (k:= (S n0 + k)); eauto.
    omega.
  - simpl in H2. inv H1.
    destruct (decomp t) as [t1 t2]. inv H2.
    destruct (IHtrec2 n0 t1 t2) as [D [E F]]; eauto.
    split; eauto using trec, reg.
    constructor; eauto.
    assert (S n0 + k = 0 + (S n0 + k)); try omega.
    rewrite H3.
    apply bound_reg; eauto.
    apply trec_tailrec in H. destruct H.
    eauto.
  - inv H0.
    + constructor. simpl in H1. inv H.
      inv H8. apply trec_tailrec in H9.
      destruct H9. assert (2 = 1 + 1); try omega.
      rewrite H5. apply bound_reg; eauto.
      assert (1= 0 + 1); try omega.
      rewrite H6.
      apply bound_shift_interval. simpl.
      apply bound_step with (k:= (S (S n0) + k)); eauto.
      omega.
    + constructor.
Qed.

Theorem decompose_correct n k s s1 s2
  : trec (S n) k s
    → reg 0 s
    → (s1, s2) = decomp s
    → CFPFix s =T (CFPSeq (Star s2) s1.[ren shift])
       ∧ trec n k (CFPSeq (Star s2) s1.[ren shift])
       ∧ reg 0 (CFPSeq (Star s2) s1.[ren shift]).
Proof.
  intros. destruct (reg_decomp H H0 H1) as [H2 [H3 H4]].
  destruct (trec_tailrec H) as [H5 H6].
  simpl in H5. apply decomp_correct with (s1:= s1) (s2:= s2) in H5; eauto.
  split.
  - rewrite H5. rewrite decomposed_Star.
    + reflexivity.
    + apply reg_bound. eauto.
    + apply reg_bound. apply reg_step with (n:= S n + k); eauto.
      omega.
  - split.
    { constructor.
      + constructor.
        constructor; eauto using trec.
        constructor; eauto using trec.
        simpl. apply tailrec_trec.
        × apply reg_tailrec. apply reg_step with (n:= S n + k); eauto. omega.
        × apply reg_bound. simpl in H4. eauto.
      + assert (n = 0 + n); try omega.
        rewrite H7. apply trec_bound_ren with (i:= 1).
        × apply reg_bound. eauto.
        × intros. inv H8.
        × intros. destruct x.
          { inv H8. }
          { simpl. omega. }
        × simpl. eauto. }
    { constructor.
      - constructor. eauto. apply reg_step with (n:= S n + k); eauto. omega.
      - apply reg_shift. eauto. }
Qed.

Fixpoint regularize s :=
  match s with
  | CFPEps ⇒ CFPEps
  | (CFPVar x) ⇒ CFPVar x
  | (CFPChoice s t) ⇒ CFPChoice (regularize s) (regularize t)
  | (CFPSeq s t) ⇒ CFPSeq (regularize s) (regularize t)
  | (CFPFix s) ⇒ (match (decomp (regularize s)) with
                   | (s1, s2) ⇒ CFPSeq (Star s2) s1.[ren(shift)]
                   end)
  end.

Lemma reg_regularize n k s
  : trec n k s → reg 0 (regularize s) ∧ trec n k (regularize s).
Proof.
  intros. general induction H; split; simpl; eauto using reg, trec.
  - constructor. omega.
  - constructor. omega.
  - destruct IHtrec1, IHtrec2. eauto using reg.
  - destruct IHtrec1, IHtrec2. eauto using trec.
  - destruct IHtrec1, IHtrec2. eauto using reg.
  - destruct IHtrec1, IHtrec2. eauto using trec.
  - destruct IHtrec. destruct (decomp_total (regularize s)) as [s1 [s2 H2]]. rewrite <- H2.
    destruct (@decompose_correct n k (regularize s) s1 s2 H1 H0 H2) as [H3 [H4 H5]]. eauto.
  - destruct IHtrec. destruct (decomp_total (regularize s)) as [s1 [s2 H2]]. rewrite <- H2.
    destruct (@decompose_correct n k (regularize s) s1 s2 H1 H0 H2) as [H3 [H4 H5]]. eauto.
Qed.

Lemma regularize_correct n s
  : tailrec n s → regularize s =T s.
Proof.
  intros. general induction H.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite IHtailrec1.
    rewrite IHtailrec2.
    reflexivity.
  - simpl. rewrite IHtailrec1.
    rewrite IHtailrec2.
    reflexivity.
  - simpl. destruct (decomp_total (regularize s)) as [s1[s2 A]].
    rewrite <- A.
    rewrite <- decomposed_Star.
    + rewrite <- IHtailrec.
      assert (part s1 s2 =T regularize s).
      { symmetry in IHtailrec.
        apply tailrec_trec with (k:= 0) in H.
        - apply reg_regularize in H. destruct H.
          apply trec_tailrec in H0. destruct H0.
          simpl in H0.
          assert (regularize s =T part s1 s2).
          { apply decomp_correct with (n:= S (n+0)); eauto. }
          rewrite H2. reflexivity.
        - apply bound_zero. }
      rewrite H0. reflexivity.
    + apply tailrec_trec with (k:= 0) in H.
      × apply reg_regularize in H. destruct H.
        apply reg_decomp with (s1:= s1) (s2:= s2) in H0; eauto.
        destruct H0 as [H1 [H2 H3]]. apply trec_tailrec in H2.
        destruct H2. apply reg_bound. eauto.
      × apply bound_zero.
    + apply tailrec_trec with (k:= 0) in H.
      × apply reg_regularize in H. destruct H.
        apply reg_decomp with (s1:= s1) (s2:= s2) in H0; eauto.
        destruct H0 as [H1 [H2 H3]]. apply trec_tailrec in H2.
        destruct H2. apply reg_bound. apply reg_step with (n:= S n + 0); eauto.
        omega.
      × apply bound_zero.
Qed.

Theorem regularize_correct_final s n
  : tailrec n s → tailrec n (regularize s)
                   ∧ regi (regularize s)
                   ∧ s =T (regularize s).
Proof.
  intros. apply tailrec_trec with (k:= 0) in H; eauto using bound_zero. destruct (reg_regularize H) as [A B].
  split.
  - apply trec_tailrec in B. destruct B. simpl in H.
    apply tailrec_step with (n:= n+0); eauto. omega.
  - split.
    + apply reg_regi with (n:= 0). eauto.
    + apply trec_tailrec in H. destruct H.
      apply regularize_correct in H. rewrite H. reflexivity.
Qed.