Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base CFP Regularity Equivalences Linearity Congruence DistributeFix.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Fixpoint lini s u :=
  match s with
  | CFPEps ⇒ u
  | (CFPVar x) ⇒ CFPSeq (CFPVar x) u
  | (CFPChoice s t) ⇒ CFPChoice (lini s u) (lini t u)
  | (CFPSeq s t) ⇒ lini s (lini t u)
  | (CFPFix (CFPChoice CFPEps (CFPSeq s (CFPVar 0)))) ⇒ CFPFix (CFPChoice u.[ren(+1)] (lini s (CFPVar 0)))
  | (CFPFix s) ⇒ CFPFix s
  end.

Lemma lini_lin n s u
  : reg n s → lin n u → lin n (lini s u).
Proof.
  intros. general induction H; simpl; eauto using lin.
  constructor. constructor; eauto using lin.
  apply reg_bound in H. apply lin_ren_preserve with (n:= n); eauto.
  intros. simpl. omega.
Qed.

Lemma lini_correct s u
  : regi s → lini s u =T CFPSeq s u.
Proof.
  intros. general induction H; simpl.
  - rewrite Seq_Eps_iden_left. reflexivity.
  - reflexivity.
  - rewrite Seq_assoc. rewrite <- (IHregi2 u).
    rewrite <- (IHregi1 (lini t u)). reflexivity.
  - rewrite Seq_Choice_distribute2.
     rewrite (IHregi1). rewrite IHregi2. reflexivity.
  - rewrite Seq_Null_absorb_left. unfold Null. reflexivity.
  - rewrite (IHregi (CFPVar 0)).
    change (CFPFix (part u.[ren(+1)] s) =T CFPSeq (Star s) u).
    rewrite decomposed_Star; eauto.
    + rewrite <- id_shift. reflexivity.
    + apply bound_ren. intros. left. simpl. omega.
Qed.

Theorem lini_correct_final n s u
  : reg n s → lin n u → lin n (lini s u) ∧ lini s u =T CFPSeq s u.
Proof.
  intros. split; eauto using lini_lin, lini_correct, reg_regi.
Qed.