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

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.

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 ×.
  - isabsurd.
  - 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.

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. rewrite compileF_length; eauto.
  - rewrite Len; intros; hnf in H; dcr; subst; inv_get.
    rewrite compileF_length; eauto.
    rewrite take_app_lt; 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_lt, <- 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 sim_I RL r L L' V s (a:ann bool) (Ann:getAnn a)
 (RCH: reachability 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.
  - 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_lt, <- 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 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.

  Require Import SimF.

  Instance SR : ProofRelationF bool := {
   ParamRelF G Z Z' := Z' = Z;
   ArgRelF 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_lt; 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_lt, <- 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 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.
  - 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_lt, <- 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 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.

Lemma UCE_paramsMatch PL RL s lv
  : reachability 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.
  - specialize (H NOTCOND0). specialize (H0 NOTCOND). subst. simpl in ×.
    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; eauto.
    rewrite filter_by_app in H4; eauto with len.
    rewrite filter_by_nil in H4; 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 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 H0; eauto.
    + rewrite H2; eauto.
  - cases.
    + rewrite IHLS; eauto.
    + rewrite Heq. simpl; eauto.
Qed.

Lemma UCE_live i ZL LV RL s uc lv
  : reachability 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.
    intros. eapply H. destruct H1; eauto.
    left. eapply compile_live_incl; eauto.
  - repeat cases; eauto. econstructor; eauto; intros.
    + rewrite compile_live_incl; eauto.
    + rewrite compile_live_incl; eauto.
  - repeat get_functional. 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.
           ++ repeat rewrite filter_by_length; eauto 20 with len.
        -- rewrite compileF_length; eauto. rewrite filter_by_length, map_id; eauto 20 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.
             ** rewrite map_length.
                repeat rewrite filter_by_length; eauto 20 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 Sound (getAnn ⊝ als ++ RL) s slv
    → getAnn slv
    → trueIsCalled 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 SoundAndComplete RL (snd Zs) lv →
       trueIsCalled (snd Zs) (LabI n) →
       getAnn lv →
       trueIsCalled (compile RL (snd Zs) lv)
                (LabI (countTrue (take n RL))))
  (UC:reachability 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 SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
  (Ann: getAnn alt)
  (IC: trueIsCalled t (LabI l'))
  (CC: callChain trueIsCalled F (LabI l') (LabI k))
  (GetF: get F k ZsEnd)
  (ICEnd: trueIsCalled (snd ZsEnd) (LabI (❬F❭ + n)))
  (GetAls: get als k aEnd)
: callChain trueIsCalled
            (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_lt; eauto 20 with len.
    rewrite <- map_take. eauto. 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; eauto.
    econstructor 2; [ | | ].
    rewrite take_app_lt; eauto 20 with len.
    rewrite <- map_take. eauto.
    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 SoundAndComplete RL (snd Zs) lv →
       trueIsCalled (snd Zs) (LabI n) →
       getAnn lv →
       trueIsCalled (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 SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
  (Ann: get (getAnn ⊝ als ++ RL) l' true)
  (CC: callChain trueIsCalled F (LabI l') (LabI k))
: callChain trueIsCalled
            (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_lt; eauto 20 with len.
    rewrite <- map_take. eauto.
    simpl.
    eapply IH in H0; eauto.
    subst. eauto.
Qed.

Lemma UCE_trueIsCalled RL s lv n
  : reachability SoundAndComplete RL s lv
    → trueIsCalled s (LabI n)
    → getAnn lv
    → trueIsCalled (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 trueIsCalled;
    simpl in *; eauto using trueIsCalled.
  - repeat cases; eauto using trueIsCalled.
  - repeat cases; eauto using trueIsCalled.
  - 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 SoundAndComplete (getAnn ⊝ als ++ RL) (snd Zs) a)
    → reachability SoundAndComplete (getAnn ⊝ als ++ RL) t alt
    → getAnn alt
    → isCalledFrom trueIsCalled F t (LabI n)
    → n < ❬F❭
    → isCalledFrom trueIsCalled (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_lt in H3 at 2.
  setoid_rewrite <- map_take in H3. eauto.
  eauto with len.
Qed.

Lemma UCE_noUnreachableCode RL s lv
  : reachability SoundAndComplete RL s lv
    → getAnn lv
    → noUnreachableCode trueIsCalled (compile RL s lv).
Proof.
  intros Live GetAnn.
  induction Live; simpl in *; repeat cases; eauto using noUnreachableCode.
  - specialize (H NOTCOND0). specialize (H0 NOTCOND). 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.