Module RTLReachesproof

Lemmas related to RTLReaches.

Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Smallstep.
Require Import RTL.
Require Import RTLutils.
Require Import Kildall.
Require Import Conventions.
Require Import Integers.
Require Import Floats.
Require Import Utils.
Require Import RTLReaches.
Require Import Events.


Utility lemmas

Section dfs.
Variable entry:node.
Variable code:code.

Definition cardinal {A} (m:PTree.t A) :=
  List.length (List.map (@fst _ _) (PTree.elements m)).

Lemma not_seen_sons_aux0 : forall l0 l1 l2 seen_set seen_set',
  fold_left
  (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
    let (new, seen) := ns in
      match seen ! j with
        | Some _ => ns
        | None => (j :: new, PTree.set j tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
  forall x, In x l1 -> In x l2.
Proof.
  induction l0; simpl; intros.
  inv H; auto.
  destruct (seen_set!a); inv H; eauto.
Qed.

Lemma not_seen_sons_prop1 : forall i j seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  cfg code i j -> In j l \/ seen_set ! j = Some tt.
Proof.
  unfold not_seen_sons; intros.
  inv H0.
  rewrite HCFG_ins in *.
  assert (
   forall l0 l1 l2 seen_set seen_set',
   fold_left
     (fun (ns : prod (list node) (PTree.t unit)) (j0 : positive) =>
      let (new, seen) := ns in
      match seen ! j0 with
      | Some _ => ns
      | None => (j0 :: new, PTree.set j0 tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
   In j l0 -> In j l2 \/ seen_set ! j = Some tt).
  induction l0; simpl; intros.
  intuition.
  destruct (peq a j).
  subst.
  case_eq (seen_set0!j); intros.
  destruct u; auto.
  rewrite H2 in *.
  left; eapply not_seen_sons_aux0; eauto.
  destruct H1.
  intuition.
  destruct (seen_set0!a); eauto.
  elim IHl0 with (1:=H0); auto.
  rewrite PTree.gso; auto.
  eauto.
Qed.

Lemma not_seen_sons_prop8 : forall i j seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  In j l -> cfg code i j.
Proof.
  unfold not_seen_sons; intros.
  assert (
   forall l0 l1 l2 seen_set seen_set',
   fold_left
     (fun (ns : prod (list node) (PTree.t unit)) (j0 : positive) =>
      let (new, seen) := ns in
      match seen ! j0 with
      | Some _ => ns
      | None => (j0 :: new, PTree.set j0 tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
   In j l2 -> In j l0 \/ In j l1).
  induction l0; simpl; intros.
  inv H1; auto.
  case_eq (seen_set0!a); intros; rewrite H3 in *.
  elim IHl0 with (1:=H1); auto.
  elim IHl0 with (1:=H1); auto.
  simpl; destruct 1; auto.
  case_eq (code!i); intros; rewrite H2 in H.
  apply H1 in H; auto; clear H1.
  destruct H as [H|H]; try (elim H; fail).
  econstructor; eauto.
  inv H; elim H0.
Qed.

Lemma not_seen_sons_prop2 : forall i j seen_set,
  In j (fst (not_seen_sons code i seen_set)) ->
  seen_set ! j = None.
Proof.
  unfold not_seen_sons; intros.
  case_eq (code!i); [intros ins Hi|intros Hi]; rewrite Hi in *.
  assert (forall l l0 seen_set,
    In j
        (fst
           (fold_left
              (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
               let (new, seen) := ns in
               match seen ! j with
               | Some _ => ns
               | None => (j :: new, PTree.set j tt seen)
               end) l (l0, seen_set))) ->
        In j l0\/ seen_set ! j = None).
  induction l; simpl; auto.
  intros.
  case_eq (seen_set0 ! a); intros; rewrite H1 in *; eauto.
  elim IHl with (1:=H0); auto.
  simpl; destruct 1; subst; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  intros; congruence.
  elim H0 with (1:=H); auto.
  simpl; intuition.
  simpl in H; intuition.
Qed.

Lemma not_seen_sons_prop5 : forall i seen_set,
  list_norepet (fst (not_seen_sons code i seen_set)).
Proof.
  unfold not_seen_sons; intros.
  destruct (code ! i); simpl; try constructor.
  assert (forall l l0 seen_set l1 seen_set',
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    (forall x, In x l0 -> seen_set!x = Some tt) ->
    list_norepet l0 ->
    (forall x, In x l1 -> seen_set'!x = Some tt) /\ list_norepet l1).
  induction l; simpl; intros.
  inv H ;auto.
  case_eq (seen_set0!a); intros; rewrite H2 in *; auto.
  elim IHl with (1:=H); auto.
  elim IHl with (1:=H); auto.
  simpl; destruct 1; auto.
  subst; rewrite PTree.gss; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  constructor; auto.
  intro; rewrite (H0 a) in H2; auto; congruence.
  generalize (H (successors_instr i0) nil seen_set).
  destruct (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) (successors_instr i0) (nil, seen_set)); intuition.
  eelim H0; eauto.
  simpl; intuition.
  constructor.
Qed.

Lemma not_seen_sons_prop3_aux : forall l i l0 seen_set l1 seen_set',
    seen_set!i = Some tt ->
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt.
Proof.
 induction l; simpl; intros.
 inv H0; auto.
 destruct (seen_set!a).
 rewrite (IHl _ _ _ _ _ H H0); auto.
 assert ((PTree.set a tt seen_set)! i = Some tt).
 rewrite PTree.gsspec; destruct peq; auto.
 rewrite (IHl _ _ _ _ _ H1 H0); auto.
Qed.

Lemma not_seen_sons_prop3 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, seen_set!i = Some tt -> seen_set'!i = Some tt.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  apply not_seen_sons_prop3_aux with (2:=H2); auto.
Qed.


Lemma not_seen_sons_prop4 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, In i l -> seen_set'!i = Some tt.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  assert (forall l i l0 seen_set l1 seen_set',
    In i l1 ->
    (forall i, In i l0 -> seen_set !i = Some tt) ->
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt).
  induction l0; simpl; intros.
  inv H3; auto.
  case_eq (seen_set0 ! a); intros; rewrite H4 in *; inv H3.
  apply IHl0 with (3:= H6); auto.
  apply IHl0 with (3:= H6); auto.
  simpl; destruct 1; subst.
  rewrite PTree.gss; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  apply H with (3:=H2); auto.
  simpl; intuition.
  elim H0.
Qed.

Lemma not_seen_sons_prop6 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, seen_set'!i = Some tt -> seen_set!i = Some tt \/ In i l.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  assert (forall l i l0 seen_set l1 seen_set',
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt ->
    seen_set !i = Some tt \/ In i l1).
  induction l0; simpl; intros.
  inv H; auto.
  case_eq (seen_set0 ! a); intros; rewrite H3 in *; inv H.
  apply IHl0 with (1:= H5); auto.
  elim IHl0 with (1:= H5) (i:=i2); auto; intros.
  rewrite PTree.gsspec in H; destruct peq; auto.
  subst.
  right.
  eapply not_seen_sons_aux0; eauto.
  apply H with (1:=H2); auto.
Qed.

Lemma iter_hh7 : forall seen_list stack
  (HH7: forall i j, In i seen_list -> cfg code i j -> In j seen_list \/ In j stack),
  forall i j, (cfg code)** i j -> In i seen_list -> In j seen_list \/
    exists k, (cfg code)** i k /\ (cfg code)** k j /\ In k stack.
Proof.
  induction 2; intros; auto.
  edestruct HH7; eauto.
  right; exists y; repeat split; auto.
  edestruct IHclos_refl_trans1; eauto.
  edestruct IHclos_refl_trans2; eauto.
  destruct H3 as [k [T1 [T2 T3]]].
  right; exists k; repeat split; eauto.
  destruct H2 as [k [T1 [T2 T3]]].
  right; exists k; repeat split; eauto.
Qed.

Lemma acc_succ_prop : forall workl seen_set seen_list stack seen code'
  (HH1: In entry seen_list)
  (HH2: list_norepet stack)
  (HH3: forall i, In i stack -> seen_set ! i = Some tt)
  (HH4: forall i, In i seen_list -> seen_set ! i = Some tt)
  (HH5: forall i, In i seen_list -> In i stack -> False)
  (HH6: forall i, seen_set ! i = Some tt -> In i seen_list \/ In i stack)
  (HH7: forall i j, In i seen_list -> cfg code i j -> In j seen_list \/ In j stack)
  (HH8: forall i, In i seen_list -> (cfg code)** entry i)
  (HH11: forall i, In i stack -> (cfg code)** entry i)
  (HH9: acc_succ code workl (OK (seen_set,seen_list,stack)) = OK (seen, code'))
  (HH10: list_norepet seen_list),
  (forall j, (cfg code)** entry j -> In j seen /\ code ! j = code' !j)
  /\ (forall j ins, code'!j = Some ins -> In j seen)
  /\ list_norepet seen
  /\ (forall j, In j seen -> code!j = code'!j)
  /\ (forall i j, In i seen -> cfg code i j -> In j seen)
  /\ (forall j, In j seen -> (cfg code)** entry j).
Proof.
  induction workl; simpl; intros until 11.
  destruct stack; inv HH9.
  assert (forall j : node, (cfg code **) entry j -> In j seen); intros.
  elim (iter_hh7 seen nil HH7 entry j); auto.
  destruct 1; intuition.
  split; auto.
  intros.
  rewrite gcombine; auto.
  rewrite HH4; auto.
  split; intros.
  rewrite gcombine in H0; auto.
  unfold remove_dead in *.
  case_eq (seen_set!j); intros; rewrite H1 in *; try congruence.
  elim HH6 with j; intros; auto.
  destruct u; auto.
  split; auto.
  split; auto.
  intros.
  rewrite gcombine; simpl; auto.
  rewrite HH4; auto.
  split.
  intros; exploit HH7; eauto; destruct 1; simpl; auto.
  assumption.

  destruct stack; inv HH9.
  assert (forall j : node, (cfg code **) entry j -> In j seen); intros.
  elim (iter_hh7 seen nil HH7 entry j); auto.
  destruct 1; intuition.
  split; auto.
  intros.
  rewrite gcombine; auto.
  rewrite HH4; auto.
  split; intros.
  rewrite gcombine in H0; unfold remove_dead in *.
  case_eq (seen_set!j); intros; rewrite H1 in *; try congruence.
  elim HH6 with j; intros; auto.
  destruct u; auto.
  auto.
  split; auto.
  split; auto.
  intros; rewrite gcombine; auto.
  rewrite HH4; auto.
  split.
  intros; exploit HH7; eauto; destruct 1; auto.
  assumption.

  case_eq (not_seen_sons code p (PTree.set p tt seen_set)); intros new seen_set' Hn.
  rewrite Hn in *.

  apply IHworkl with (10:=H0); auto; clear H0.

  apply list_norepet_append; auto.
  generalize (not_seen_sons_prop5 p (PTree.set p tt seen_set)); rewrite Hn; auto.
  inv HH2; auto.
  unfold list_disjoint; red; intros; subst.
  assert (seen_set!y=None).
  generalize (not_seen_sons_prop2 p y (PTree.set p tt seen_set)); rewrite Hn; simpl; intros.
  apply H1 in H.
  rewrite PTree.gsspec in H; destruct peq; try congruence.
  rewrite HH3 in H1; auto; congruence.

  simpl; intros i Hi.
  rewrite in_app in Hi; destruct Hi; auto.
  eapply not_seen_sons_prop4; eauto.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gsspec; destruct peq; auto.

simpl; intros i Hi.
  destruct Hi; subst.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gss; auto.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gsspec; destruct peq; auto.
  
simpl; intros i Hi1 Hi2.
  rewrite in_app in Hi2.
  destruct Hi2.
  generalize (not_seen_sons_prop2 p i (PTree.set p tt seen_set)); rewrite Hn; simpl; intros.
  apply H0 in H; clear H0.
  rewrite PTree.gsspec in H; destruct peq; try congruence.
  destruct Hi1; subst; try congruence.
  rewrite HH4 in H; congruence.
  destruct Hi1; subst.
  inv HH2; intuition.
  elim HH5 with i; auto.
  
intros i Hi.
  elim not_seen_sons_prop6 with (1:=Hn) (2:=Hi); intros.
  rewrite PTree.gsspec in H; destruct peq; auto.
  left; left; auto.
  elim HH6 with i; auto with datatypes.
  simpl; destruct 1; auto.
  right; rewrite in_app; auto.
  right; rewrite in_app; auto.

intros i j Hi1 Hi2.
  simpl in Hi1; destruct Hi1; subst.
  elim not_seen_sons_prop1 with i j (PTree.set i tt seen_set) seen_set' new; auto; intros.
  right; eauto with datatypes.
  rewrite PTree.gsspec in H; destruct peq; auto.
  left; left; auto.
  elim HH6 with j; auto.
  simpl; destruct 1; auto with datatypes.
  elim HH7 with i j; auto.
  simpl; destruct 1; auto with datatypes.

simpl; intros i Hi.
  destruct Hi; auto.
  subst; auto.

simpl; intros i Hi.
  rewrite in_app in Hi.
  destruct Hi; auto.
  exploit not_seen_sons_prop8; eauto.

  constructor; auto.
  intro HI; elim HH5 with p; auto with arith.
Qed.
  
End dfs.

Proof of the well-formedness of generated functions

Lemma dfs_prop_aux : forall tf seen code',
  dfs tf = OK (seen, code') ->
  (forall j, (cfg (RTL.fn_code tf))** (RTL.fn_entrypoint tf) j ->
    In j seen /\ (RTL.fn_code tf) ! j = code' ! j)
  /\ (forall j ins, code'!j = Some ins -> In j seen)
  /\ list_norepet seen
  /\ (forall j, In j seen -> (RTL.fn_code tf)!j = code'!j)
  /\ (forall i j, In i seen -> cfg (fn_code tf) i j -> In j seen)
  /\ (forall i, In i seen -> (cfg (RTL.fn_code tf))** (RTL.fn_entrypoint tf) i).
Proof.
  unfold dfs; intros tf seen.
  destruct (map (@fst node instruction) (PTree.elements (RTL.fn_code tf))); simpl.
  intros; congruence.
  case_eq (not_seen_sons (RTL.fn_code tf) (RTL.fn_entrypoint tf)
           (PTree.set (RTL.fn_entrypoint tf) tt (PTree.empty unit)));
  intros new seen_set TT.
  intros code' T; monadInv T.
  assert (
 (forall j : node,
    (cfg (RTL.fn_code tf) **) (RTL.fn_entrypoint tf) j ->
    In j x /\ (RTL.fn_code tf) ! j = code' ! j) /\
   (forall (j : positive) (ins : instruction),
    code' ! j = Some ins -> In j x) /\ list_norepet x /\
   (forall j, In j x -> (RTL.fn_code tf)!j = code'!j) /\
   (forall i j, In i x -> cfg (fn_code tf) i j -> In j x) /\
   (forall j : positive, In j x -> (cfg (fn_code tf) **) (fn_entrypoint tf) j)
   ).
  apply acc_succ_prop with (entry:=(RTL.fn_entrypoint tf)) (10:=EQ); auto.

  apply list_norepet_append; auto.
  generalize (not_seen_sons_prop5 (RTL.fn_code tf) (RTL.fn_entrypoint tf)
         (PTree.set (RTL.fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; auto.
  constructor.
  intro; simpl; intuition.

  intros.
  rewrite in_app in H; destruct H.
  generalize (not_seen_sons_prop4 (RTL.fn_code tf) (RTL.fn_entrypoint tf)
         (PTree.set (RTL.fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; eauto.
  elim H.

  simpl; intuition.
  subst.
  generalize (not_seen_sons_prop3 (RTL.fn_code tf) (RTL.fn_entrypoint tf)
         (PTree.set (RTL.fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; intros.
  eapply H; eauto.
  rewrite PTree.gss; auto.

  simpl; intuition; subst.
  rewrite in_app in H0; destruct H0.
  generalize (not_seen_sons_prop2 (RTL.fn_code tf) (RTL.fn_entrypoint tf)
    (RTL.fn_entrypoint tf)
    (PTree.set (RTL.fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl.
  rewrite PTree.gss; intros.
  apply H0 in H; congruence.
  elim H.
  
  intros.
  elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes.
  rewrite PTree.gsspec; destruct peq; subst; intros; auto.
  rewrite PTree.gempty in H0; congruence.
  
  simpl; intuition.
  elim not_seen_sons_prop1 with (j:=j) (1:=TT); auto with datatypes.
  rewrite PTree.gsspec; destruct peq; subst; intros; auto.
  rewrite PTree.gempty in H; congruence.
  rewrite H1; auto.

  simpl; destruct 1; subst.
  constructor 2.
  elim H.

  intros i; rewrite in_app; destruct 1.
  exploit not_seen_sons_prop8; eauto.
  elim H.

  repeat constructor.
  intro H; elim H.

  destruct H.
  destruct H0.
  destruct H1.
  destruct H2.
  destruct H3 as [H3 H5].
  repeat split; intros.
  rewrite <- rev_alt; rewrite <- In_rev; eauto.
  elim H with j; auto.
  elim H with j; auto.
  rewrite <- rev_alt; rewrite <- In_rev; eauto.
  rewrite <- rev_alt; auto.
  apply list_norepet_rev; auto.
  rewrite <- rev_alt in H4; rewrite <- In_rev in H4; eauto.
  rewrite <- rev_alt in *; rewrite <- In_rev in *; eauto.
  rewrite <- rev_alt in *; rewrite <- In_rev in *; eauto.
Qed.

Lemmas derived from the main lemma.
Lemma transf_function_ppoints1 : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  (forall j, (cfg (fn_code f))** (fn_entrypoint f) j ->
    In j seen /\ (fn_code f) ! j = (fn_code tf) ! j).
Proof.
  intros.
  monadInv H.
  eapply dfs_prop_aux ; eauto.
Qed.

Lemma transf_function_fn_entrypoint : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  fn_entrypoint tf = fn_entrypoint f.
Proof.
  intros.
  unfold transf_function in H.
  destruct (dfs f); simpl in H; try congruence.
  destruct p; inv H.
  reflexivity.
Qed.

Lemma transf_function_ppoints1' : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  (forall j, (cfg (fn_code f))** (fn_entrypoint f) j ->
    (cfg (fn_code tf))** (fn_entrypoint tf) j).
Proof.
  intros.
  rewrite <- cfg_star_same.
  assert (fn_entrypoint tf = fn_entrypoint f).
    eapply transf_function_fn_entrypoint; eauto.
  apply cfg_star_same_code with (fn_code f).
  intros.
  rewrite cfg_star_same in *.
  clear H0.
  rewrite H1 in H2.
  exploit transf_function_ppoints1; eauto.
  intuition.
  rewrite cfg_star_same; rewrite H1; auto.
Qed.

Lemma transf_function_ppoints2:
  forall f seen tf,
    transf_function f = OK (seen, tf) ->
    (forall j ins, (fn_code tf)!j = Some ins -> In j seen).
Proof.
  intros.
  monadInv H; simpl in *.
  exploit dfs_prop_aux ; eauto; intuition eauto.
Qed.

Lemma transf_function_ppoints4 : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  (forall j, In j seen -> (fn_code f)!j = (fn_code tf) ! j).
Proof.
  intros.
  monadInv H.
  eapply dfs_prop_aux ; eauto.
Qed.

Lemma transf_function_ppoints5 : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  (forall i j, In i seen -> cfg (fn_code f) i j -> In j seen).
Proof.
  intros.
  monadInv H.
  eapply dfs_prop_aux ; eauto.
Qed.

Lemma transf_function_ppoints6 : forall f tf seen,
  transf_function f = OK (seen, tf) ->
  (forall i, In i seen -> (cfg (fn_code tf))** (fn_entrypoint tf) i).
Proof.
  intros.
  eapply transf_function_ppoints1'; eauto.
  monadInv H.
  eapply dfs_prop_aux ; eauto.
Qed.

Lemma transf_function_cfg: forall f tf,
  forall i ins, (fn_code tf) ! i = Some ins -> (fn_code f) ! i = Some ins ->
  forall j,
    cfg (fn_code tf) i j -> cfg (fn_code f) i j.
Proof.
  intros.
  inv H1.
  rewrite H in HCFG_ins. inv HCFG_ins.
  apply CFG with (ins := ins0); auto.
Qed.

Lemma transf_function_cfg_star_aux:
  forall f tf seen
  (TRANSF: transf_function f = OK (seen, tf))
  (ALLSEEN: forall i ins, (fn_code f) ! i = Some ins -> In i seen),
  forall j,
    cfg_star (fn_code tf) (fn_entrypoint tf) j ->
    forall ins',
    (fn_code f) ! j = Some ins' ->
    cfg_star (fn_code f) (fn_entrypoint f) j.
Proof.
  induction 3; intros.
  erewrite <- transf_function_fn_entrypoint; eauto.
  constructor.
  generalize TRANSF; intros H'.
  inv H0.
  assert ((fn_code f) ! j = Some ins).
    case_eq ((fn_code f) ! j); intros.
    generalize H0; intros INS.
    apply ALLSEEN in H0.
    eapply transf_function_ppoints4 in H0; eauto.
    rewrite HCFG_ins in H0. rewrite H0 in INS; auto.
    generalize HCFG_ins; intros INS.
    eapply transf_function_ppoints2 in HCFG_ins; eauto.
    eapply transf_function_ppoints4 in HCFG_ins; eauto.
    rewrite <- HCFG_ins in INS.
    rewrite H0 in INS. inv INS.
  apply cfg_star1 with (j := j); auto.
  apply IHcfg_star with (ins' := ins); auto.
  eapply transf_function_cfg; eauto.
Qed.

Lemma transf_function_cfg_star:
  forall f tf seen
  (TRANSF: transf_function f = OK (seen, tf))
  (ALLSEEN: forall i ins, (fn_code f) ! i = Some ins -> In i seen),
  forall j ins',
    (fn_code f) ! j = Some ins' ->
    cfg_star (fn_code f) (fn_entrypoint f) j.
Proof.
  intros.
  generalize H; intros INS.
  apply ALLSEEN in H.
  eapply transf_function_ppoints6 in H; eauto.
  apply cfg_star_same in H.
  eapply transf_function_cfg_star_aux in H; eauto.
Qed.
Generated by coq2html