Require Import CSet Util LengthEq Take MoreList Filter OUnion AllInRel.
Require Import IL Annotation LabelsDefined Sawtooth InRel.
Require Import Liveness.Liveness TrueLiveness Reachability.
Require Import Sim SimTactics.
Require SimI SimF.

Set Implicit Arguments.
Unset Printing Records.

Definition compileF (compile : ∀ (RL:list bool) (s:stmt) (a:ann bool), stmt)
(RL:list bool) :=
  fix f (F:〔params × stmt〕) (ans:list (ann bool)) :=
    match F, ans with
    | (Z,s)::F, a::ans ⇒
      if getAnn a then (Z, compile RL s a) :: f F ans
      else f F ans
    | _, _ ⇒ nil
    end.

Fixpoint compile (RL:list bool) (s:stmt) (a:ann bool) {struct s} :=
  match s, a with
    | stmtLet x e s, ann1 _ an ⇒
      stmtLet x e (compile RL s an)
    | stmtIf e s t, ann2 _ ans ant ⇒
      if [op2bool e = Some true] then
        (compile RL s ans)
      else if [ op2bool e = Some false ] then
             (compile RL t ant)
           else
             stmtIf e (compile RL s ans) (compile RL t ant)
    | stmtApp f Y, ann0 _ ⇒
      stmtApp (LabI (countTrue (take (counted f) RL))) Y
    | stmtReturn x, ann0 _ ⇒ stmtReturn x
    | stmtFun F t, annF lv ans ant ⇒
      let LV' := getAnn ⊝ ans ++ RL in
      let F' := compileF compile LV' F ans in
      match F' with
      | nil ⇒ compile LV' t ant
      | _ ⇒ stmtFun F' (compile LV' t ant)
      end
    | s, _ ⇒ s
  end.

Lemma compileF_filter RL F als
  : compileF compile RL F als
    = map (fun p ⇒ (fst (fst p), compile RL (snd (fst p)) (snd p)))
          (filter (fun b ⇒ getAnn (snd b)) (zip pair F als)).
Proof.
  length_equify. general induction F; destruct als; simpl; eauto.
  - destruct a; eauto.
  - destruct a as [Z s]; cases; simpl; f_equal; eauto.
Qed.

Lemma compileF_Z_filter_by RL F als (LEN: ❬F❭ = ❬als❭)
  : fst ⊝ compileF compile RL F als
    = filter_by (fun b ⇒ b) (getAnn ⊝ als) (fst ⊝ F).
Proof.
  length_equify. general induction LEN; simpl; eauto.
  destruct x as [Z s]; cases; simpl; f_equal; eauto.
Qed.

Lemma compileF_get RL F n ans Zs a
  : get F n Zs
    → get ans n a
    → getAnn a = true
    → get (compileF compile RL F ans) (countTrue (getAnn ⊝ (take n ans)))
          (fst Zs, compile RL (snd Zs) a).
Proof.
  intros GetF GetAns EQ.
  general induction ans; destruct F as [|[Z s] ?]; isabsurd.
  - inv GetF; inv GetAns.
    + simpl. rewrite EQ; eauto using get.
    + simpl. cases; simpl; eauto using get.
Qed.

Lemma compileF_get_inv RL F ans Z' s' n'
  : get (compileF compile RL F ans) n' (Z', s')
    → ∃ Zs a n, get F n Zs
      ∧ get ans n a
      ∧ getAnn a = true
      ∧ Z' = fst Zs
      ∧ s' = compile RL (snd Zs) a
      ∧ n' = countTrue (getAnn ⊝ (take n ans)).
Proof.
  intros Get.
  general induction ans; destruct F as [|[Z s] ?]; simpl in *; isabsurd.
  - cases in Get.
    + inv Get.
      × eauto 20 using get.
      × clear Get. edestruct IHans as [Zs [a' [n' [lv ?]]]]; eauto; dcr; subst.
        ∃ Zs, a', (S n'). simpl; rewrite <- Heq; eauto 20 using get.
    + edestruct IHans as [Zs [a' [n [lv ?]]]]; eauto; dcr; subst.
      ∃ Zs, a', (S n). simpl; rewrite <- Heq; eauto 20 using get.
Qed.

Lemma compile_occurVars RL s uc
  : occurVars (compile RL s uc) ⊆ occurVars s.
Proof.
  revert RL uc.
  sind s; destruct s; intros RL uc; destruct uc; simpl; eauto.
  - rewrite IH; eauto.
  - repeat cases; simpl; repeat rewrite IH; eauto with cset.
  - cases.
    + rewrite IH; eauto.
    + rewrite Heq; clear Heq; simpl.
      eapply incl_union_lr; eauto.
      eapply list_union_incl; eauto with cset.
      intros; inv_get. destruct x as [Z s'].
      edestruct compileF_get_inv; eauto; dcr; subst.
      eapply incl_list_union. eauto using map_get_1.
      simpl. rewrite IH; eauto.
Qed.

Lemma compile_freeVars RL s uc
  : freeVars (compile RL s uc) ⊆ freeVars s.
Proof.
  revert RL uc.
  sind s; destruct s; intros RL uc; destruct uc; simpl; eauto.
  - rewrite IH; eauto.
  - repeat cases; simpl; repeat rewrite IH; eauto with cset.
  - cases.
    + rewrite IH; eauto.
    + rewrite Heq; clear Heq; simpl.
      eapply incl_union_lr; eauto.
      eapply list_union_incl; eauto with cset.
      intros; inv_get. destruct x as [Z s'].
      edestruct compileF_get_inv; eauto; dcr; subst.
      eapply incl_list_union. eauto using map_get_1.
      simpl. rewrite IH; eauto.
Qed.

Lemma compileF_length LV F ans
  : length F = length ans
    → length (compileF compile LV F ans) = countTrue (getAnn ⊝ ans).
Proof.
  intros. length_equify.
  general induction H; simpl; eauto.
  cases; subst. cases; simpl; eauto.
Qed.

Smpl Add
     match goal with
     | [ H: ❬?B❭ = ❬?C❭ |- context [ ❬compileF compile ?A ?B ?C❭ ] ] ⇒
       rewrite (@compileF_length A B C H)
     end : len.

Local Hint Extern 0 ⇒
match goal with
| [ H : op2bool ?e ≠ Some ?t , H' : op2bool ?e ≠ Some ?t → _ |- _ ] ⇒
  specialize (H' H); subst
| [ H : op2bool ?e = Some true , H' : op2bool ?e ≠ Some false → _ |- _ ] ⇒
  let H'' := fresh "H" in
  assert (H'':op2bool e ≠ Some false) by congruence;
    specialize (H' H''); subst
end.

Lemma compileF_nil_als_false RL F als (LEN:❬F❭ = ❬als❭)
  : nil = compileF compile RL F als
    → ∀ n a, get als n a → getAnn a = false.
Proof.
  length_equify.
  general induction LEN; simpl in ×.
  - destruct x as [Z s]; simpl in ×.

    cases in H.
    + inv H.
    + inv H0; eauto.
Qed.

Lemma compileF_not_nil_exists_true RL F als (LEN:❬F❭ = ❬als❭)
  : nil ≠ compileF compile RL F als
    → ∃ n a, get als n a ∧ getAnn a.
Proof.
  length_equify.
  general induction LEN; simpl in ×.
  - isabsurd.
  - destruct x as [Z s]; simpl in ×.
    cases in H.
    + eexists 0, y; split; eauto using get.
    + edestruct IHLEN; dcr; eauto 20 using get.
Qed.

Lemma impb_elim (a b:bool)
  : impb a b → a → b.
Proof.
  intros. rewrite <- H. eauto.
Qed.

Hint Resolve impb_elim.

Module I.

  Import SimI.

Instance SR : ProofRelationI bool := {
   ParamRelI G Z Z' := Z' = Z;
   ArgRelI V V' G VL VL' := VL' = VL ∧ V = V';
   Image AL := countTrue AL;
   IndexRelI AL n n' :=
     n' = countTrue (take n AL) ∧ get AL n true
}.
- intros AL' AL n n' [H H']; subst.
  split.
  + clear H' H.
    general induction AL'; simpl.
    × orewrite (n - 0 = n). omega.
    × destruct n; simpl; eauto. cases; simpl; eauto.
  + rewrite get_app_ge in H'; eauto.
Defined.

Lemma compileF_separates RL F als (Len:❬F❭ = ❬als❭)
  : separates SR (getAnn ⊝ als) RL F (compileF compile (getAnn ⊝ als ++ RL) F als).
Proof.
  hnf; intros; split; [| split; [| split]].
  - eauto with len.
  - simpl. eauto with len.
  - rewrite Len; intros; hnf in H; dcr; subst; inv_get.
    len_simpl.
    rewrite take_app_le; eauto with len.
    erewrite (take_eta n (getAnn ⊝ als)) at 2.
    rewrite countTrue_app.
    erewrite <- get_eq_drop; eauto using map_get_1.
    rewrite EQ. simpl. omega.
  - rewrite Len; intros; simpl in *; dcr; subst.
    rewrite compileF_length; eauto.
    rewrite take_app_ge; eauto with len.
    rewrite countTrue_app. omega.
Qed.

Lemma compileF_indexwise_paramrel RL F als (Len:❬F❭ = ❬als❭)
  : indexwise_paramrel SR F (compileF compile (getAnn ⊝ als ++ RL) F als) (getAnn ⊝ als) RL.
Proof.
  hnf; intros.
  simpl in *; dcr; subst.
  rewrite get_app_lt in H4; eauto with len.
  inv_get; simpl.
  exploit (compileF_get (getAnn ⊝ als ++ RL)); try eapply H2; eauto.
  simpl in ×.
  erewrite take_app_le, <- map_take in H1; eauto with len.
  get_functional. eauto.
Qed.

Lemma sim_compile_fun_cases r RL L V s L' F als alt
  : sim r Bisim (mapi I.mkBlock F ++ L, V, s)
   (mapi I.mkBlock (compileF compile (getAnn ⊝ als ++ RL) F als) ++ L', V,
    compile (getAnn ⊝ als ++ RL) s alt)
→ sim r Bisim (L, V, stmtFun F s)
        (L', V,
         match compileF compile (getAnn ⊝ als ++ RL) F als with
         | nil ⇒ compile (getAnn ⊝ als ++ RL) s alt
         | _ :: _ ⇒
           stmtFun (compileF compile (getAnn ⊝ als ++ RL) F als) (compile (getAnn ⊝ als ++ RL) s alt)
         end).
Proof.
  intros. cases.
  - simpl in ×. pone_step_left. eauto.
  - rewrite Heq in *; clear Heq.
    pone_step. left. eauto.
Qed.

Lemma poLe_impl_use (a b:bool)
  : poLe a b
    → a
    → b.
Proof.
  destruct a, b; firstorder.
Qed.

Opaque poLe.

Local Hint Resolve poLe_impl_use.

Lemma sim_I RL r L L' V s (a:ann bool) (Ann:getAnn a)
 (RCH: reachability cop2bool Sound RL s a)
 (LSIM:labenv_sim Bisim (sim r) SR RL L L')
  : sim r Bisim (L,V, s) (L',V, compile RL s a).
Proof.
  unfold sim. revert_except s.
  sind s; destruct s; simpl in *; intros; invt reachability; simpl in × |- ×.
  - destruct e.
    + eapply (sim_let_op il_statetype_I); eauto.
    + eapply (sim_let_call il_statetype_I); eauto.
  - eapply (sim_if_elim il_statetype_I); intros; eauto 20 using op2bool_cop2bool_not_some.
  - assert (b=true). destruct a0, b; isabsurd; eauto. subst.
    eapply labenv_sim_app; eauto.
    + hnf; simpl. split; eauto using zip_get.
    + intros; simpl in *; subst. eauto 20.
  - pno_step.
  - eapply sim_compile_fun_cases.
    eapply (IH s); eauto with len.
    eapply labenv_sim_extension; eauto.
    + intros. hnf; intros; simpl in *; dcr; subst; inv_get.
      exploit (compileF_get (getAnn ⊝ als ++ RL)); try eapply H5; eauto.
      erewrite take_app_le, <- map_take in H7; eauto with len.
      simpl in ×. get_functional.
      exploit H4; eauto.
    + eapply compileF_indexwise_paramrel; eauto.
    + eapply compileF_separates; eauto.
Qed.

Lemma sim_UCE V s a
  : reachability cop2bool Sound nil s a
    → getAnn a
    → @sim I.state _ I.state _ bot3 Bisim (nil,V, s) (nil,V, compile nil s a).
Proof.
  intros.
  eapply (@sim_I nil); eauto; isabsurd.
Qed.

End I.

Module F.

  Import SimF.

  Instance SR : ProofRelationF bool := {
   ParamRelF G Z Z' := Z' = Z;
   ArgRelF E E' G VL VL' := VL' = VL;
   IndexRelF AL n n' :=
     n' = countTrue (take n AL) ∧ get AL n true;
   Image AL := countTrue AL
}.
- intros AL' AL n n' [H H']; subst.
  split.
  + clear H' H.
    general induction AL'; simpl.
    × orewrite (n - 0 = n). omega.
    × destruct n; simpl; eauto. cases; simpl; eauto.
  + rewrite get_app_ge in H'; eauto.
Defined.

Lemma compileF_separates RL F als (Len:❬F❭ = ❬als❭)
  : separates SR (getAnn ⊝ als) RL F (compileF compile (getAnn ⊝ als ++ RL) F als).
Proof.
  hnf; intros; split; [| split; [| split]].
  - eauto with len.
  - simpl. rewrite compileF_length; eauto.
  - rewrite Len; intros; hnf in H; dcr; subst; inv_get.
    rewrite compileF_length; eauto.
    rewrite take_app_le; eauto with len.
    erewrite (take_eta n (getAnn ⊝ als)) at 2.
    rewrite countTrue_app.
    erewrite <- get_eq_drop; eauto using map_get_1.
    rewrite EQ. simpl. omega.
  - rewrite Len; intros; simpl in *; dcr; subst.
    rewrite compileF_length; eauto.
    rewrite take_app_ge; eauto with len.
    rewrite countTrue_app. omega.
Qed.

Lemma compileF_indexwise_paramrel RL F als (Len:❬F❭ = ❬als❭)
  : indexwise_paramrel SR F (compileF compile (getAnn ⊝ als ++ RL) F als) (getAnn ⊝ als) RL.
Proof.
  hnf; intros.
  simpl in *; dcr; subst.
  rewrite get_app_lt in H4; eauto with len.
  inv_get; simpl.
  exploit (compileF_get (getAnn ⊝ als ++ RL)); try eapply H2; eauto.
  simpl in ×.
  erewrite take_app_le, <- map_take in H1; eauto with len.
  get_functional. eauto.
Qed.

Lemma sim_compile_fun_cases r RL L V s L' F als alt
  : sim r Bisim (mapi (F.mkBlock V) F ++ L, V, s)
   (mapi (F.mkBlock V) (compileF compile (getAnn ⊝ als ++ RL) F als) ++ L', V,
    compile (getAnn ⊝ als ++ RL) s alt)
→ sim r Bisim (L, V, stmtFun F s)
        (L', V,
         match compileF compile (getAnn ⊝ als ++ RL) F als with
         | nil ⇒ compile (getAnn ⊝ als ++ RL) s alt
         | _ :: _ ⇒
           stmtFun (compileF compile (getAnn ⊝ als ++ RL) F als) (compile (getAnn ⊝ als ++ RL) s alt)
         end).
Proof.
  intros. cases.
  - simpl in ×. pone_step_left. eauto.
  - rewrite Heq in *; clear Heq.
    pone_step. left. eauto.
Qed.

Lemma sim_F RL r L L' V s (a:ann bool) (Ann:getAnn a)
 (UC: reachability cop2bool Sound RL s a)
 (LSIM:labenv_sim Bisim (sim r) SR RL L L')
  : sim r Bisim (L,V, s) (L',V, compile RL s a).
Proof.
  unfold sim. revert_except s.
  sind s; destruct s; simpl in *; intros; invt reachability; simpl in × |- ×.
  - destruct e.
    + eapply (sim_let_op il_statetype_F); eauto.
    + eapply (sim_let_call il_statetype_F); eauto.
  - eapply (sim_if_elim il_statetype_F); intros; eauto.
    + eapply IH; eauto. rewrite <- H2; eauto using op2bool_cop2bool_not_some.
    + eapply IH; eauto. rewrite <- H3; eauto using op2bool_cop2bool_not_some.
  - assert (b=true). destruct a0, b; isabsurd; eauto. subst.
    eapply labenv_sim_app; eauto.
    + hnf; simpl. split; eauto using zip_get.
    + intros; simpl in *; subst. eauto 20.
  - pno_step.
  - eapply sim_compile_fun_cases.
    eapply (IH s); eauto with len.
    eapply labenv_sim_extension; eauto.
    + intros. hnf; intros; simpl in *; dcr; subst; inv_get.
      exploit (compileF_get (getAnn ⊝ als ++ RL)); try eapply H5; eauto.
      erewrite take_app_le, <- map_take in H7; eauto with len.
      simpl in ×. get_functional.
      exploit H4; eauto.
    + eapply compileF_indexwise_paramrel; eauto.
    + eapply compileF_separates; eauto.
Qed.

Lemma sim_UCE V s a
  : reachability cop2bool Sound nil s a
    → getAnn a
    → @sim F.state _ F.state _ bot3 Bisim (nil,V, s) (nil,V, compile nil s a).
Proof.
  intros.
  eapply (@sim_F nil); eauto; isabsurd.
Qed.

End F.

Opaque poLe.

Lemma UCE_paramsMatch PL RL s lv
  : reachability cop2bool Sound RL s lv
    → getAnn lv
    → paramsMatch s PL
    → paramsMatch (compile RL s lv) (filter_by (fun b ⇒ b) RL PL).
Proof.
  intros UC Ann PM.
  general induction UC; inv PM; simpl in × |- *; repeat cases; eauto using paramsMatch.
  - rewrite op2bool_cop2bool in COND.
    eapply IHUC1; eauto. exploit H; eauto.
    rewrite COND. intro. clear_trivial_eqs.
  - rewrite op2bool_cop2bool in COND.
    eapply IHUC2; eauto. exploit H0; eauto.
  - exploit H; eauto. exploit H0; eauto.
    econstructor; eauto.
  - simpl in ×.
    exploit (get_filter_by (fun b ⇒ b) H H3). destruct a,b; isabsurd; eauto.
    rewrite map_id in H1.
    econstructor; eauto.
  - exploit IHUC as IH; eauto.
    rewrite filter_by_app in IH; eauto with len.
    rewrite filter_by_nil in IH; eauto.
    intros; inv_get; eauto using compileF_nil_als_false.
  - rewrite Heq; clear Heq p b0.
    econstructor.
    + intros ? [Z s] Get.
      eapply compileF_get_inv in Get; destruct Get; dcr; subst; simpl; eauto.
      exploit H2; eauto.
      rewrite compileF_Z_filter_by, map_filter_by, <- filter_by_app; eauto with len.
    + rewrite compileF_Z_filter_by, map_filter_by, <- filter_by_app; eauto with len.
Qed.

Fixpoint compile_live (s:stmt) (a:ann (set var)) (b:ann bool) : ann (set var) :=
  match s, a, b with
    | stmtLet x e s, ann1 lv an, ann1 _ bn ⇒
      ann1 lv (compile_live s an bn)
    | stmtIf e s t, ann2 lv ans ant, ann2 _ bns bnt ⇒
      if [op2bool e = Some true] then
        compile_live s ans bns
      else if [op2bool e = Some false ] then
        compile_live t ant bnt
      else
        ann2 lv (compile_live s ans bns) (compile_live t ant bnt)
    | stmtApp f Y, ann0 lv, _ ⇒ ann0 lv
    | stmtReturn x, ann0 lv, _ ⇒ ann0 lv
    | stmtFun F t, annF lv anF ant, annF _ bnF bnt ⇒
      let anF'' := zip (fun (Zs:params × stmt) ab ⇒
                         compile_live (snd Zs) (fst ab) (snd ab)) F (pair ⊜ anF bnF) in
      let anF' := filter_by (fun b ⇒ b) (getAnn ⊝ bnF) anF'' in
      match anF' with
      | nil ⇒ (compile_live t ant bnt)
      | _ ⇒ annF lv anF' (compile_live t ant bnt)
      end
    | _, a, _ ⇒ a
  end.

Lemma compile_live_incl i uci ZL LV RL s lv uc
  : true_live_sound i ZL LV s lv
    → reachability cop2bool uci RL s uc
    → getAnn (compile_live s lv uc) ⊆ getAnn lv.
Proof.
  intros LS UC.
  general induction LS; inv UC; simpl; eauto.
  - repeat cases; simpl; eauto.
    + rewrite IHLS1; eauto.
    + rewrite IHLS2; eauto.
  - cases.
    + rewrite IHLS; eauto.
    + rewrite Heq. simpl; eauto.
Qed.

Lemma UCE_live i ZL LV RL s uc lv
  : reachability cop2bool Sound RL s uc
    → getAnn uc
    → true_live_sound i ZL LV s lv
    → true_live_sound i (filter_by (fun b ⇒ b) RL ZL)
                      (filter_by (fun b ⇒ b) RL LV)
                      (compile RL s uc)
                      (compile_live s lv uc).
Proof.
  intros UC Ann LS.
  general induction LS; inv UC; simpl in *; eauto using true_live_sound.
  - econstructor; eauto using compile_live_incl with cset.
    rewrite compile_live_incl in *; eauto.
  - repeat cases.
    + eapply IHLS1; [eauto| ].
      rewrite <- H5; [eauto|].
      rewrite op2bool_cop2bool in COND; eauto.
      rewrite COND. intro. clear_trivial_eqs.
    + eapply op2bool_cop2bool_not_some in NOTCOND.
      eapply IHLS2; eauto.
      exploit H6; eauto.
    + exploit H5; eauto using op2bool_cop2bool_not_some.
      exploit H6; eauto using op2bool_cop2bool_not_some.
      econstructor; intros; eauto; try congruence.
      rewrite compile_live_incl; eauto.
      rewrite compile_live_incl; eauto.
  - simpl in ×.
    assert (❬take (labN l) RL❭ = ❬take (labN l) ZL❭).
    eapply get_range in H. eapply get_range in H7.
    repeat rewrite take_length_le; eauto. omega. omega.
    econstructor; eauto.
    exploit (get_filter_by (fun b ⇒ b) H7 H); eauto.
    destruct a, b; isabsurd; eauto.
    simpl. rewrite map_id in H5. eauto.
    exploit (get_filter_by (fun b ⇒ b) H7 H0); eauto.
    destruct a, b; isabsurd; eauto.
    simpl. rewrite map_id in H5. eauto.
  - cases.
    + exploit IHLS; eauto.
      assert (∀ (n : nat) (b : bool), get (getAnn ⊝ als0) n b → b = false). {
        intros; inv_get; eauto using compileF_nil_als_false.
      }
      rewrite !filter_by_app in H4; eauto with len.
      rewrite filter_by_nil in H4; eauto.
      setoid_rewrite filter_by_nil in H4 at 3; eauto.
      setoid_rewrite filter_by_nil at 3; eauto.
    + rewrite Heq. exploit compileF_not_nil_exists_true; eauto.
      rewrite <- Heq; congruence. clear Heq; dcr.
      cases.
      × exfalso. refine (filter_by_not_nil _ _ _ _ _ (eq_sym Heq));
                        eauto 20 using Is_true_eq_true with len.
      × rewrite Heq; clear Heq.
        econstructor; eauto.
        -- rewrite compileF_Z_filter_by; eauto with len.
           rewrite map_filter_by. rewrite <- !filter_by_app; eauto 20 with len.
           eapply true_live_sound_monotone.
           eapply IHLS; eauto 20 with len.
           rewrite !filter_by_app; eauto 20 with len.
           eapply PIR2_app; [ | reflexivity ].
           eapply PIR2_get; intros; inv_get.
           ++ simpl. eapply compile_live_incl; eauto.
           ++ eauto with len.
        -- eauto with len.
        -- intros; inv_get.
           destruct Zs as [Z s].
           edestruct compileF_get_inv; eauto; dcr; subst. simpl.
           rewrite compileF_Z_filter_by; eauto with len.
           inv_get. rewrite <- filter_by_app; eauto with len.
           eapply true_live_sound_monotone.
           ++ eapply H1; eauto 20 with len.
           ++ rewrite !filter_by_app; eauto 20 with len. eapply PIR2_app; [ | reflexivity ].
             eapply PIR2_get; intros; inv_get; simpl.
             ** eapply compile_live_incl; eauto.
             ** eauto with len.
        -- intros. inv_get.
           destruct Zs as [Z s].
           edestruct compileF_get_inv; eauto; dcr; subst. simpl.
           inv_get. cases; eauto.
           rewrite compile_live_incl; eauto.
        -- rewrite compile_live_incl; eauto.
Qed.

Lemma trueIsCalled_compileF_not_nil
      (s : stmt) (slv : ann bool) k F als RL x
  : reachability cop2bool Sound (getAnn ⊝ als ++ RL) s slv
    → getAnn slv
    → isCalled true s (LabI k)
    → get als k x
    → ❬F❭ = ❬als❭
    → nil = compileF compile (getAnn ⊝ als ++ RL) F als
    → False.
Proof.
  intros UC Ann IC Get Len.
  assert (LenNEq:length (compileF compile (getAnn ⊝ als ++ RL) F als)
                 ≠ 0). {
    rewrite compileF_length; eauto.
    edestruct (reachability_trueIsCalled UC IC); eauto; simpl in *; dcr.
    inv_get.
    eapply countTrue_exists. eapply map_get_eq; eauto.
  }
  intros EQ. eapply LenNEq. rewrite <- EQ. reflexivity.
Qed.

Hint Resolve Is_true_eq_true.

Lemma UCE_callChain RL F als t alt l' k ZsEnd aEnd n
      (IH : ∀ k Zs,
          get F k Zs →
       ∀ (RL : 〔bool〕) (lv : ann bool) (n : nat),
       reachability cop2bool SoundAndComplete RL (snd Zs) lv →
       (isCalled true) (snd Zs) (LabI n) →
       getAnn lv →
       (isCalled true) (compile RL (snd Zs) lv)
                (LabI (countTrue (take n RL))))
  (UC:reachability cop2bool SoundAndComplete (getAnn ⊝ als ++ RL) t alt)
  (LEN: ❬F❭ = ❬als❭)
  (UCF:∀ (n : nat) (Zs : params × stmt) (a : ann bool),
       get F n Zs →
       get als n a →
       reachability cop2bool SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
  (Ann: getAnn alt)
  (IC: isCalled true t (LabI l'))
  (CC: callChain (isCalled true) F (LabI l') (LabI k))
  (GetF: get F k ZsEnd)
  (ICEnd: (isCalled true) (snd ZsEnd) (LabI (❬F❭ + n)))
  (GetAls: get als k aEnd)
: callChain (isCalled true)
            (compileF compile (getAnn ⊝ als ++ RL) F als)
            (LabI (countTrue (take l' (getAnn ⊝ als ++ RL))))
            (LabI (countTrue (getAnn ⊝ als) +
                   countTrue (take n RL))).
Proof.
  general induction CC.
  - exploit reachability_trueIsCalled as IMPL; try eapply IC; eauto.
    simpl in *; dcr; inv_get. rewrite H1 in Ann.
    exploit compileF_get; eauto.
    econstructor 2; [ | | econstructor 1 ].
    + rewrite take_app_le; eauto 20 with len.
    + simpl.
      eapply IH in ICEnd; eauto.
      rewrite take_app_ge in ICEnd; eauto 20 with len.
      rewrite map_length in ICEnd.
      orewrite (❬F❭ + n - ❬als❭ = n) in ICEnd. simpl.
      rewrite countTrue_app in ICEnd. eauto.
  - exploit reachability_trueIsCalled; try eapply IC; eauto.
    simpl in *; dcr; inv_get.
    assert (getAnn x0). {
      rewrite <- H4. eauto.
    }
    exploit compileF_get; try eapply H1; eauto.
    econstructor 2; [ | | ].
    rewrite take_app_le; eauto 20 with len.
    simpl.
    eapply IH in H0; eauto.
    eapply IHCC in H0; eauto.
Qed.

Lemma UCE_callChain' RL F als l' k
      (IH : ∀ k Zs,
          get F k Zs →
       ∀ (RL : 〔bool〕) (lv : ann bool) (n : nat),
       reachability cop2bool SoundAndComplete RL (snd Zs) lv →
       (isCalled true) (snd Zs) (LabI n) →
       getAnn lv →
       (isCalled true) (compile RL (snd Zs) lv)
                (LabI (countTrue (take n RL))))
  (LEN: ❬F❭ = ❬als❭)
  (UCF:∀ (n : nat) (Zs : params × stmt) (a : ann bool),
       get F n Zs →
       get als n a →
       reachability cop2bool SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
  (Ann: get (getAnn ⊝ als ++ RL) l' true)
  (CC: callChain (isCalled true) F (LabI l') (LabI k))
: callChain (isCalled true)
            (compileF compile (getAnn ⊝ als ++ RL) F als)
            (LabI (countTrue (take l' (getAnn ⊝ als ++ RL))))
            (LabI (countTrue (take k (getAnn ⊝ als ++ RL)))).
Proof.
  general induction CC.
  - econstructor.
  - inv_get.
    exploit reachability_trueIsCalled; try eapply H0; eauto.
    simpl in *; dcr; inv_get. assert (x0 = true).
    destruct (getAnn x), x0; isabsurd; eauto.
    exploit compileF_get; eauto.
    econstructor 2; [ | | ].
    rewrite take_app_le; eauto 20 with len.
    eapply IH in H0; eauto.
    subst. eauto.
Qed.

Lemma UCE_trueIsCalled RL s lv n
  : reachability cop2bool SoundAndComplete RL s lv
    → isCalled true s (LabI n)
    → getAnn lv
    → isCalled true (compile RL s lv) (LabI (countTrue (take n RL))).
Proof.
  intros Live IC.
  revert RL lv n Live IC.
  sind s; simpl; intros; invt reachability; invt isCalled;
    simpl in *; eauto using isCalled.
  - repeat cases; eauto using isCalled.
    + eapply IH; eauto.
      rewrite <- H0; eauto using op2bool_cop2bool_not_some.
    + econstructor; eauto. eapply IH; eauto.
      rewrite <- H0; eauto using op2bool_cop2bool_not_some.
  - repeat cases; eauto using isCalled.
    + eapply IH; eauto.
      rewrite <- H1; eauto using op2bool_cop2bool_not_some.
    + econstructor 3; eauto. eapply IH ; eauto.
      rewrite <- H1; eauto using op2bool_cop2bool_not_some.
  - eapply callChain_cases in H8. destruct H8; subst.
    + cases.
      × exploit (IH t) as IHt; eauto.
        rewrite take_app_ge in IHt; eauto 20 with len.
        rewrite map_length in IHt.
        orewrite (❬F❭ + n - ❬als❭ = n) in IHt. simpl.
        rewrite countTrue_app in IHt.
        erewrite <- compileF_length in IHt; eauto.
        erewrite <- Heq in IHt. eauto.
      × rewrite Heq. econstructor. econstructor 1.
        exploit (IH t) as IHt; eauto.
        rewrite compileF_length; eauto. simpl.
        rewrite take_app_ge in IHt; eauto 20 with len.
        rewrite map_length in IHt.
        orewrite (❬F❭ + n - ❬als❭ = n) in IHt. simpl.
        rewrite countTrue_app in IHt. eauto.
    + destruct H6 as [? [? [? ?]]]; dcr.
      destruct l' as [l'].
      cases.
      × exfalso. inv_get.
        eapply get_in_range in H2. destruct H2. inv_get.
        eapply (@trueIsCalled_compileF_not_nil t); eauto.
      × rewrite Heq; clear Heq p b. inv_get.
        econstructor; eauto. simpl.
        rewrite compileF_length; eauto.
        eapply UCE_callChain; eauto.
Qed.

Lemma UCE_isCalledFrom RL F als t alt n (Len:❬F❭ = ❬als❭)
  : (∀ (n : nat) (Zs : params × stmt) (a : ann bool),
       get F n Zs →
       get als n a →
       reachability cop2bool SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
    → reachability cop2bool SoundAndComplete (getAnn ⊝ als ++ RL) t alt
    → getAnn alt
    → isCalledFrom (isCalled true) F t (LabI n)
    → n < ❬F❭
    → isCalledFrom (isCalled true) (compileF compile (getAnn ⊝ als ++ RL) F als)
                   (compile (getAnn ⊝ als ++ RL) t alt) (LabI (countTrue (getAnn ⊝ take n als))).
Proof.
  intros UCF UCt gAt ICF.
  destruct ICF as [[l'] [? ?]].
  exploit UCE_trueIsCalled; eauto.
  eexists; split; eauto.
  exploit UCE_callChain'; eauto using UCE_trueIsCalled.
  exploit reachability_trueIsCalled; eauto.
  dcr; subst; simpl in ×. rewrite H6 in gAt.
  destruct x; isabsurd; eauto.
  setoid_rewrite take_app_le in H3 at 2.
  setoid_rewrite <- map_take in H3. eauto.
  rewrite map_length. omega.
Qed.

Lemma UCE_noUnreachableCode RL s lv
  : reachability cop2bool SoundAndComplete RL s lv
    → getAnn lv
    → noUnreachableCode (isCalled true) (compile RL s lv).
Proof.
  intros Live GetAnn.
  induction Live; simpl in *; repeat cases; eauto using noUnreachableCode.
  - rewrite op2bool_cop2bool in COND. rewrite H in GetAnn; eauto.
    rewrite COND; eauto. intro. clear_trivial_eqs.
  - eapply op2bool_cop2bool_not_some in NOTCOND. rewrite H0 in GetAnn; eauto.
  - exploit H; eauto using op2bool_cop2bool_not_some.
    exploit H0; eauto using op2bool_cop2bool_not_some. subst.
    simpl in ×. econstructor; eauto.
  - rewrite Heq; clear Heq.
    econstructor; eauto using noUnreachableCode.
    + intros. destruct Zs as [Z' s'].
      edestruct compileF_get_inv as [Zs' [a [n' ?]]]; eauto; dcr; subst; simpl.
      simpl in ×.
      eapply H2; eauto.
    + intros. simpl in ×.
      edestruct get_in_range as [Zs ?]; eauto. destruct Zs as [Z' s'].
      edestruct compileF_get_inv as [Zs' [a [n' [lv' ?]]]]; eauto.
      dcr; subst; simpl.
      exploit H3 as ICF; eauto.
      eapply UCE_isCalledFrom; eauto with len.
Qed.

Require Import AppExpFree.

Lemma UCE_app_expfree LVZL s lv
: app_expfree s
  → app_expfree (compile LVZL s lv).
Proof.
  intros AEF.
  general induction AEF; destruct lv; simpl;
    repeat let_pair_case_eq; repeat simpl_pair_eqs; subst; simpl;
      repeat cases; eauto using app_expfree.
  - rewrite Heq. econstructor; intros; inv_get; eauto.
    destruct Zs; edestruct compileF_get_inv; eauto; dcr; subst.
    eapply H0; eauto.
Qed.

Require Import RenamedApart PE.

Fixpoint compile_renamedApart (s:stmt) (a:ann (set var × set var)) (b:ann bool)
  : ann (set var × set var) :=
  match s, a, b with
  | stmtLet x e s, ann1 (D, _) an, ann1 _ bn ⇒
    let an' := compile_renamedApart s an bn in
    ann1 (D, {x; snd (getAnn an')}) an'
  | stmtIf e s t, ann2 (D, _) ans ant, ann2 _ bns bnt ⇒
    let ans' := compile_renamedApart s ans bns in
    let ant' := compile_renamedApart t ant bnt in
    if [op2bool e = Some true] then ans'
    else if [op2bool e = Some false ] then ant'
         else ann2 (D, snd (getAnn ans') ∪ snd (getAnn ant')) ans' ant'
  | stmtApp f Y, ann0 lv, _ ⇒ ann0 lv
  | stmtReturn x, ann0 lv, _ ⇒ ann0 lv
  | stmtFun F t, annF (D, _) anF ant, annF _ bnF bnt ⇒
    let anF'' := zip (fun (Zs:params × stmt) ab ⇒
                       compile_renamedApart (snd Zs) (fst ab) (snd ab)) F (pair ⊜ anF bnF) in
    let anF' := filter_by (fun b ⇒ b) (getAnn ⊝ bnF) anF'' in
    let bnt' := compile_renamedApart t ant bnt in
    match anF' with
    | nil ⇒ bnt'
    | _ ⇒ annF (D, list_union (defVars ⊜ (filter_by (fun b ⇒ b) (getAnn ⊝ bnF) F) anF') ∪ snd (getAnn bnt')) anF' bnt'
    end
  | _, a, _ ⇒ a
  end.

Lemma compile_renamedApart_pes RL s an al
  : renamedApart s an
    → reachability cop2bool Sound RL s al
    → prod_eq Equal Subset (getAnn (compile_renamedApart s an al)) (getAnn an).
Proof.
  intros RA RCH.
  time (general induction RA; inv RCH; simpl in *; repeat cases; simpl; eauto).
  - econstructor; eauto.
    rewrite IHRA; eauto. rewrite H1, H2; eauto.
  - rewrite IHRA1, H2; eauto.
    econstructor; eauto. rewrite <- H1; eauto.
  - rewrite IHRA2, H3; eauto. econstructor; eauto.
    rewrite <- H1. eauto.
  - econstructor; eauto.
    rewrite IHRA1, IHRA2; eauto. rewrite <- H1, H2, H3; eauto.
  - rewrite IHRA; eauto. rewrite H4. econstructor; eauto.
    rewrite <- H5; eauto.
  - econstructor; eauto.
    rewrite Heq. clear Heq. rewrite IHRA, H4, <- H5; eauto. simpl.
    eapply incl_union_lr; eauto.
    eapply list_union_incl; intros; eauto with cset.
    inv_get.
    eapply incl_list_union.
    instantiate (2:=posOfTrue n (getAnn ⊝ als)).
    eauto using zip_get.
    unfold defVars; simpl.
    rewrite H1; eauto; eauto.
Qed.

Lemma UCE_renamedApart RL s lv G
  : renamedApart s G
    → reachability cop2bool Sound RL s lv
    → renamedApart (compile RL s lv) (compile_renamedApart s G lv).
Proof.
  intros RA RCH.
  general induction RCH; inv RA; simpl; eauto using renamedApart.
  - econstructor; eauto. reflexivity.
    eapply pe_eta_split. econstructor; eauto.
    rewrite compile_renamedApart_pes; eauto.
    eapply (prod_eq_proj1 H8); eauto.
  - repeat cases; eauto using renamedApart.
    simpl in ×.
    econstructor; try reflexivity; eauto.
    eapply disj_incl; eauto.
    rewrite compile_renamedApart_pes, H12; eauto.
    rewrite compile_renamedApart_pes, H13; eauto.
    eapply pe_eta_split; econstructor; eauto.
    rewrite compile_renamedApart_pes, H12; eauto.
    eapply pe_eta_split; econstructor; eauto.
    rewrite compile_renamedApart_pes, H13; eauto.
  - cases.
    rewrite filter_by_nil; eauto.
    intros; inv_get; eauto using compileF_nil_als_false.
    rewrite Heq.
    cases.
    + exfalso. symmetry in Heq0.
      edestruct compileF_not_nil_exists_true; eauto; dcr.
      rewrite <- Heq. congruence.
      eapply filter_by_not_nil in Heq0; eauto 20 with len.
    + rewrite Heq0.
      eapply renamedApartLet with (Dt:=snd (getAnn (compile_renamedApart t ant alt)));
        eauto 20 with len.
      × intros; inv_get; eauto. destruct Zs.
        edestruct (compileF_get_inv _ _ _ H5); eauto; dcr; subst.
        rewrite map_take in ×.
        rewrite posOfTrue_countTrue in *; eauto using map_get_eq. repeat get_functional.
        eapply H2; eauto.
      × hnf; intros; inv_get. destruct a0.
        edestruct (compileF_get_inv _ _ _ H5); eauto; dcr; subst.
        rewrite map_take in ×.
        rewrite posOfTrue_countTrue in *; eauto using map_get_eq. repeat get_functional.
        edestruct H9; dcr; eauto.
        hnf; simpl in ×.
        split. rewrite compile_renamedApart_pes; eauto.
        split; eauto. split; eauto.
        rewrite !compile_renamedApart_pes, H12; eauto.
      × hnf; intros; inv_get. destruct x, x1.
        edestruct (compileF_get_inv _ _ _ H15); eauto; dcr; subst.
        edestruct (compileF_get_inv _ _ _ H16); eauto; dcr; subst.
        rewrite map_take in ×.
        assert (GET:get (getAnn ⊝ als) x10 true) by eauto using map_get_eq.
        rewrite (posOfTrue_countTrue GET) in ×.
        assert (GET2:get (getAnn ⊝ als) x3 true) by eauto using map_get_eq.
        rewrite (posOfTrue_countTrue GET2) in ×.
        repeat get_functional. simpl.
        exploit (H10 x10 x3); only 2-3: eauto using zip_get.
        intro; subst. rewrite map_take in ×. congruence.
        unfold defVars in *; simpl.
        rewrite !compile_renamedApart_pes; eauto.
      × eapply pe_eta_split; econstructor.
        rewrite compile_renamedApart_pes, H12; eauto.
        reflexivity.
      × eapply eq_union_lr; eauto.
        eapply list_union_eq; eauto with len.
        intros; inv_get. unfold defVars; simpl. destruct x1.
        edestruct (compileF_get_inv _ _ _ H15); eauto; dcr; subst.
        rewrite map_take in ×.
        rewrite posOfTrue_countTrue in *; eauto using map_get_eq.
        repeat get_functional. simpl. eauto.
Qed.

Require Import VarP.

Lemma UCE_var_P (P:var → Prop) RL (s:stmt) a
      (VP:var_P P s)
      (RCH: reachability cop2bool Sound RL s a)
  : var_P P (compile RL s a).
Proof.
  general induction VP; invt reachability; simpl;
    repeat cases; eauto 10 using var_P.
  - rewrite Heq; clear Heq p b1.
    econstructor; eauto.
    + intros; inv_get; simpl; eauto.
      destruct Zs as [Z s].
      eapply compileF_get_inv in H2; destruct H2; dcr;
        subst; simpl; eauto.
    + intros; inv_get; simpl.
      destruct Zs as [Z s].
      eapply compileF_get_inv in H2; destruct H2; dcr;
        subst; simpl; eauto.
Qed.