Module Scope

Scopes: definition, validation and construction

Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import UtilBase.
Require Import RTLPaths.
Require Import Utf8.
Require Import DLib.
Require Import Bourdoncle.
Require Import Maps.

Definition path := rev_path.

Module Type SCOPE.
  Parameter t : Type.

  Parameter nodes : t -> list node.

  Parameter sons: t -> list t.

  Notation "n ∈ sc" := (In n (nodes sc)) (at level 10).
  Notation "sc1 ⊆ sc2" := (incl (nodes sc1) (nodes sc2)) (at level 10).

  Record family (f:function) := {
    scope : node -> t;
    header : t -> node;
    parent : t -> t;
    elements: list t;

    in_scope: forall n, f_In n f -> n ∈ (scope n);
    scope_least: forall n sc, In sc elements -> n ∈ sc -> (scope n) ⊆ sc;

    header_f_In: forall sc, In sc elements -> f_In (header sc) f;
    scope_header: forall sc, In sc elements -> scope (header sc) = sc;

    incl_in_parent: forall sc, In sc elements -> sc ⊆ (parent sc);
    parent_least: forall sc sc',
      In sc elements -> In sc' elements ->
      sc ⊆ sc' -> sc = sc' \/ (parent sc) ⊆ sc';
    sons_in_element: forall sc sc',
      In sc elements -> In sc' (sons sc) -> In sc' elements;
    parent_in_element: forall sc,
      In sc elements -> In (parent sc) elements;

    scope_in_elements: forall n, In (scope n) elements;
    enter_in_scope_at_header_only: forall n n',
      succ_node f n n' ->
      ~ n ∈ (scope n') ->
       n' = header (scope n') /\ parent (scope n') = scope n;

    cycle_at_not_header: forall rl n,
      f_In n f ->
      n <> header (scope n) ->
      path f n rl n -> rl <> nil -> In (header (scope n)) rl;

    cycle_at_header: forall rl n,
      f_In n f ->
      n = header (scope n) ->
      path f n rl n -> rl <> nil ->
      In (header (parent (scope n))) rl \/
        (forall n', In n' rl -> n' ∈ (scope n));

    in_scope_root: forall sc,
      In sc elements ->
      f.(fn_entrypoint) ∈ sc ->
      f.(fn_entrypoint) = header sc;

    parent_strict_subset: forall sc,
      In sc elements ->
      (header (parent sc)) ∈ sc -> f.(fn_entrypoint) = header sc;

    root_no_pred: forall n, ~ succ_node f n f.(fn_entrypoint)
  }.
  Implicit Arguments scope [f].
  Implicit Arguments header [f].
  Implicit Arguments parent [f].
  Implicit Arguments elements [f].

  Parameter build_family: forall (f:function), option (family f).

End SCOPE.


Untrusted OCaml code validated a posteriori.
Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).

Lemma succ_node_f_In: forall f n n', succ_node f n n' -> f_In n f.
Proof.
  destruct 1 as (x & X1 & X2).
  unfold f_In; congruence.
Qed.


Module ImplemScope.

  Definition t := (node * list bourdoncle)%type.

  Fixpoint bourdoncle_elements (l:list node) (b:bourdoncle) : list node :=
    match b with
      | I n => n :: l
      | L h lb => List.fold_left bourdoncle_elements lb (h::l)
    end.

  Definition nodes (sc:t) : list node :=
    let (h,l) := sc in
      List.fold_left bourdoncle_elements l (h::nil).

  Definition sons1 (l:list t) (b:bourdoncle) : list t :=
    match b with
      | I n => l
      | L h lb => (h,lb)::l
    end.

  Definition sons (sc:t) : list t :=
    fold_left sons1 (snd sc) nil.

  Module I.

  Definition scope_table := (PTree.t (node * list bourdoncle) * PTree.t node)%type.

  Fixpoint build_scope_table_aux (myscope:t) (st:scope_table*bool) (b:bourdoncle) :
    (scope_table * bool) :=
    let (m,distinct) := st in
    let (scope,parent) := m in
      match b with
        | I n => ((PTree.set n myscope scope, parent),negb (ptree_mem n scope) && distinct)
      | L h lb =>
        List.fold_left (build_scope_table_aux (h,lb)) lb
        ((PTree.set h (h,lb) scope, PTree.set h (fst myscope) parent),
          negb (ptree_mem h scope) && distinct)
    end.

  Fixpoint in_bourdoncle (n0:node) (b:bourdoncle) : bool :=
    match b with
      | I n => Peqb n0 n
      | L h lb => orb (Peqb n0 h) (List.existsb (in_bourdoncle n0) lb)
    end.

  Definition build_scope_table (sc:t) : res scope_table :=
    let (h,l) := sc in
    let (tab,distinct) :=
      List.fold_left (build_scope_table_aux sc) l
      ((PTree.set h (h,l) (PTree.empty _), (PTree.empty _)),true) in
      if distinct
        then OK tab
        else Error (MSG "bourdoncle contains dup" :: nil).

  Definition header_ (sc:t) : node := fst sc.

  Definition scope_ (tab:scope_table) (main:t) (n:node) :=
    match PTree.get n (fst tab) with
      | None => main
      | Some sc => sc
    end.

  Definition parent_ (tab:scope_table) (sc:t) : t :=
    match PTree.get (header_ sc) (snd tab) with
      | None => sc
      | Some h' =>
        match PTree.get h' (fst tab) with
          | None => sc
          | Some sc' => sc'
        end
    end.
    
  Definition cast_bourdoncle (b:bourdoncle) : res (node * list bourdoncle) :=
    match b with
      | I _ => Error (MSG "cast_bourdoncle error" :: nil)
      | L h lb => OK (h, lb)
    end.

  Open Scope error_monad_scope.


  Section Exists.
    Context {A:Type}.
    Variable (f:A->Prop).
    Fixpoint Exists (l:list A) : Prop :=
      match l with
        | nil => False
        | a::l => f a \/ Exists l
      end.
  End Exists.

  Fixpoint sc_In (h0:node) (l0:list bourdoncle) (b:bourdoncle) : Prop :=
    match b with
      | I n => False
      | L h lb => (h=h0 /\ lb=l0)
        \/ Exists (sc_In h0 l0) lb
    end.

  Notation "a ! b" := (PTree.get b a) (at level 1).


  Lemma fold_build_scope_false_aux:
    (forall b0 sc0 tab,
      snd (build_scope_table_aux sc0 (tab, false) b0) = false) ->
  forall lb0 sc0 tab,
    snd (fold_left (build_scope_table_aux sc0) lb0 (tab, false)) = false.
Proof.
    intros HP.
    fix IH 1; intros [|b0 lb0]; simpl in *; intros.
    > congruence.
    > case_eq (build_scope_table_aux sc0 (tab, false) b0); intros tab1 b1 Ht.
      generalize (HP b0 sc0 tab); rewrite Ht; simpl; intros HH; inv HH.
      exploit IH; eauto.
  Defined.

  Lemma fold_build_scope_false:
  forall b0 sc0 tab,
    snd (build_scope_table_aux sc0 (tab, false) b0) = false.
Proof.
    fix IH 1; intros [n|h0 lb0]; simpl; intros; try congruence.
    > destruct tab.
      rewrite andb_false_r in *; auto.
    > destruct tab.
      rewrite andb_false_r.
      exploit fold_build_scope_false_aux; eauto.
  Qed.

  Lemma fold_build_scope_false_elim: forall lb0 sc0 tab tab',
    fold_left (build_scope_table_aux sc0) lb0 (tab,false) <> (tab',true).
Proof.
    red; intros.
    generalize (fold_build_scope_false_aux fold_build_scope_false lb0 sc0 tab).
    rewrite H.
    simpl; congruence.
  Qed.

  Lemma old_map_build_scope_table_aux:
    (forall b0 sc0 tab n b tab1,
      (fst tab) ! n <> None ->
      build_scope_table_aux sc0 (tab, b) b0 = (tab1, true) ->
      (fst tab1) ! n = (fst tab) ! n) ->
  forall lb0 sc0 tab b tab',
    fold_left (build_scope_table_aux sc0) lb0 (tab, b) = (tab', true) ->
    forall n,
      PTree.get n (fst tab) <> None ->
      PTree.get n (fst tab') = PTree.get n (fst tab).
Proof.
    intros HP.
    fix 1; intros [|b0 lb0]; simpl in *; intros.
    > congruence.
    > case_eq (build_scope_table_aux sc0 (tab, b) b0); intros tab1 b1 Ht.
      rewrite Ht in *.
      destruct b1.
      > rewrite (old_map_build_scope_table_aux _ _ _ _ _ H); eauto.
        rewrite (HP _ _ _ _ _ _ H0 Ht); eauto.
      > generalize (fold_build_scope_false_aux fold_build_scope_false lb0 sc0 tab1).
        rewrite H.
        simpl; congruence.
  Defined.

  Lemma old_map_build_scope_table: forall b0 sc0 tab n b tab1,
      (fst tab) ! n <> None ->
      build_scope_table_aux sc0 (tab, b) b0 = (tab1, true) ->
      (fst tab1) ! n = (fst tab) ! n.
Proof.
    fix IH 1.
    intros [n|h0 lb0]; simpl in *; intros.
    > destruct tab; inv H0; simpl in *.
      rewrite PTree.gsspec; destruct peq; subst; auto.
      unfold ptree_mem in *.
      destruct (t0!n); simpl in *; congruence.
    > destruct tab; simpl in *.
      generalize (old_map_build_scope_table_aux IH _ _ _ _ _ H0).
      simpl; intros.
      rewrite H1; rewrite PTree.gsspec; destruct peq; try congruence.
      subst.
      unfold ptree_mem in *; destruct (t0!h0); try congruence.
      simpl in *.
      elim fold_build_scope_false_elim with (1:=H0).
  Qed.

  Lemma build_scope_table_same: forall b0 sc0 tab n b tab1 p,
      (fst tab) ! n = Some p ->
      build_scope_table_aux sc0 (tab, b) b0 = (tab1, true) ->
      (fst tab1) ! n = Some p.
Proof.
    intros.
    exploit old_map_build_scope_table; eauto.
    2: intros T; rewrite T; auto.
    congruence.
  Qed.

  Lemma fold_build_scope_table_same: forall lb0 sc0 tab n b tab' p,
      (fst tab) ! n = Some p ->
      fold_left (build_scope_table_aux sc0) lb0 (tab, b) = (tab', true) ->
      (fst tab') ! n = Some p.
Proof.
    intros.
    exploit (old_map_build_scope_table_aux old_map_build_scope_table); eauto.
    2: intros T; rewrite T; auto.
    congruence.
  Qed.

  Hint Resolve build_scope_table_same fold_build_scope_table_same.

  Lemma old_map_build_scope_table_snd_aux:
    (forall b0 sc0 tab n b tab1,
      (fst tab) ! n <> None ->
      build_scope_table_aux sc0 (tab, b) b0 = (tab1, true) ->
      (snd tab1) ! n = (snd tab) ! n) ->
  forall lb0 sc0 tab b tab',
    fold_left (build_scope_table_aux sc0) lb0 (tab, b) = (tab', true) ->
    forall n,
      PTree.get n (fst tab) <> None ->
      PTree.get n (snd tab') = PTree.get n (snd tab).
Proof.
    intros HP.
    fix 1; intros [|b0 lb0]; simpl in *; intros.
    > congruence.
    > case_eq (build_scope_table_aux sc0 (tab, b) b0); intros tab1 b1 Ht.
      rewrite Ht in *.
      destruct b1.
      > rewrite (old_map_build_scope_table_snd_aux _ _ _ _ _ H); eauto.
        generalize (old_map_build_scope_table _ _ _ _ _ _ H0 Ht); congruence.
      > elim fold_build_scope_false_elim with (1:=H).
  Defined.

  Lemma old_map_build_scope_table_snd: forall b0 sc0 tab n b tab1,
      (fst tab) ! n <> None ->
      build_scope_table_aux sc0 (tab, b) b0 = (tab1, true) ->
      (snd tab1) ! n = (snd tab) ! n.
Proof.
    fix IH 1.
    intros [n|h0 lb0]; simpl in *; intros.
    > destruct tab; inv H0; simpl in *; auto.
    > destruct tab; simpl in *.
      generalize (old_map_build_scope_table_snd_aux IH _ _ _ _ _ H0).
      simpl; intros.
      rewrite H1; rewrite PTree.gsspec; destruct peq; try congruence.
      subst.
      unfold ptree_mem in *; destruct (t0!h0); try congruence.
      simpl in *.
      elim fold_build_scope_false_elim with (1:=H0).
  Qed.

  Lemma sc_In_get_aux:
    (forall b0 sc0 tab b tab',
      build_scope_table_aux sc0 (tab,b) b0 = (tab',true) ->
      forall h n lb,
        In (I n) (I h :: lb) ->
        sc_In h lb b0 -> PTree.get n (fst tab') = Some (h, lb)) ->
    forall lb0 sc0 tab b tab',
      fold_left (build_scope_table_aux sc0) lb0 (tab, b) = (tab', true) ->
      forall h n lb, In (I n) (I h :: lb) ->
        Exists (sc_In h lb) lb0 -> (fst tab') ! n = Some (h, lb).
Proof.
    intros HP.
    fix IH 1; intros [|b0 lb0]; simpl; intros.
    > intuition.
    > destruct H1.
      > case_eq ((build_scope_table_aux sc0 (tab, b) b0)); intros.
        destruct b1.
        > exploit HP; eauto; intros.
          rewrite H2 in *.
          rewrite (old_map_build_scope_table_aux old_map_build_scope_table
            _ _ _ _ _ H); auto.
          congruence.
        > rewrite H2 in *.
          elim fold_build_scope_false_elim with (1:=H).
      > case_eq ((build_scope_table_aux sc0 (tab, b) b0)); intros.
        rewrite H2 in *.
        exploit IH; eauto; intros.
  Defined.

  Lemma sc_In_get_aux2:
    (forall b0 sc0 tab b tab',
      build_scope_table_aux sc0 (tab,b) b0 = (tab',true) ->
      forall h n lb,
        In (I n) (I h :: lb) ->
        sc_In h lb b0 -> PTree.get n (fst tab') = Some (h, lb)) ->
    forall lb0 h0 lb0' tab b tab',
      fold_left (build_scope_table_aux (h0,lb0'++lb0)) lb0 (tab, b) = (tab', true) ->
      forall n, In (I n) lb0 -> (fst tab') ! n = Some (h0, lb0'++lb0).
Proof.
    intros HP.
    fix IH 1; intros [|b0 lb0]; simpl; intros.
    > intuition.
    > destruct H0.
      > case_eq ((build_scope_table_aux (h0, lb0' ++ b0 :: lb0) (tab, b) b0)); intros.
        destruct b1.
        > rewrite H1 in *.
          rewrite (old_map_build_scope_table_aux old_map_build_scope_table
            _ _ _ _ _ H); auto.
          > inv H0.
            simpl in H1.
            destruct tab; inv H1.
            simpl.
            rewrite PTree.gss; auto.
          > inv H0; simpl in H1.
            destruct tab; inv H1.
            simpl.
            rewrite PTree.gss; congruence.
        > rewrite H1 in *.
          elim fold_build_scope_false_elim with (1:=H).
      > case_eq ((build_scope_table_aux (h0, lb0' ++ b0 :: lb0) (tab, b) b0)); intros.
        rewrite H1 in *.
        generalize (IH lb0 h0 (lb0'++b0::nil) s b1 tab').
        rewrite app_ass; simpl; eauto.
  Defined.
      
  Lemma sc_In_get : forall b0 sc0 tab b tab',
    build_scope_table_aux sc0 (tab,b) b0 = (tab',true) ->
    forall h n lb,
      In (I n) (I h :: lb) ->
      sc_In h lb b0 -> PTree.get n (fst tab') = Some (h, lb).
Proof.
    fix 1.
    intros [n|h0 lb0]; simpl in *.
    > intuition.
    > intros sc0 tab b tab' H h n lb H4 H0.
      destruct tab.
      destruct H0 as [(H1 & H2)|H0].
      > destruct H4.
        > generalize (old_map_build_scope_table_aux old_map_build_scope_table _ _ _ _ _ H n).
          simpl; subst.
          inv H0; rewrite PTree.gss.
          intros HP; apply HP; congruence.
        > subst.
          generalize (sc_In_get_aux2 sc_In_get lb h nil); simpl; eauto.
      > eapply sc_In_get_aux; eauto.
  Qed.

  Lemma sc_In_get_main : forall b lb0 tab',
    build_scope_table (b,lb0) = OK tab' ->
    forall h n lb,
      In (I n) (I h :: lb) ->
      sc_In h lb (L b lb0) -> PTree.get n (fst tab') = Some (h, lb).
Proof.
    unfold build_scope_table; intros.
    case_eq (fold_left (build_scope_table_aux (b, lb0)) lb0
             (PTree.set b (b, lb0) (PTree.empty (node * list bourdoncle)),
             (PTree.empty node), true)); intros.
    rewrite H2 in *.
    destruct b0; inv H.
    simpl in H1.
    destruct H1.
    > destruct H; subst.
      simpl in H0; destruct H0.
      > inv H.
        rewrite (old_map_build_scope_table_aux old_map_build_scope_table
          _ _ _ _ _ H2); simpl; auto.
        > rewrite PTree.gss; auto.
        > rewrite PTree.gss; congruence.
      > generalize (sc_In_get_aux2 sc_In_get lb h nil); simpl; intros T.
        apply (T _ _ _ H2 _ H).
    > apply (sc_In_get_aux sc_In_get _ _ _ _ _ H2 _ _ _ H0); auto.
  Qed.

  Definition In_scope (main:t) (n:node) (sc:t) : Prop :=
    let (h,lb) := sc in
    let (h0,lb0) := main in
      In (I n) (I h :: lb) /\ sc_In h lb (L h0 lb0).

  Lemma In_scope_get_fst : forall main tab,
    build_scope_table main = OK tab ->
    forall n sc, In_scope main n sc -> PTree.get n (fst tab) = Some sc.
Proof.
    intros.
    destruct main; destruct sc; simpl in H0; intros.
    destruct H0.
    exploit (sc_In_get_main); eauto.
  Qed.

  Lemma fold_sc_In_get_inv :
    (forall b0 h0 l0 tab b tab',
      build_scope_table_aux (h0,l0) (tab,b) b0 = (tab',true) ->
      forall h n lb,
        PTree.get n (fst tab') = Some (h, lb) ->
        PTree.get n (fst tab) = Some (h, lb) \/
        ((h,lb) = (h0,l0) /\ b0 = I n) \/
        (In (I n) (I h :: lb) /\ sc_In h lb b0)) ->
    forall lb0 sc0 n tab b tab' h lb,
      fold_left (build_scope_table_aux sc0) lb0 (tab, b) = (tab', true) ->
      (fst tab') ! n = Some (h, lb) ->
      (fst tab)! n = Some (h, lb) \/
      (sc0 = (h, lb) /\ In (I n) lb0) \/
      (In (I n) (I h :: lb) /\ Exists (sc_In h lb) lb0).
Proof.
    intros IH'; fix IH 1; intros [|b0 lb0]; simpl; intros.
    > inv H; auto.
    > case_eq (build_scope_table_aux sc0 (tab,b) b0); intros; rewrite H1 in *.
      destruct b1.
      > exploit IH; eauto.
        simpl; destruct 1; auto.
        > destruct sc0; exploit IH'; eauto.
          destruct 1; auto.
          intuition.
        > intuition.
      > elim fold_build_scope_false_elim with (1:=H).
  Defined.

  Lemma sc_In_get_inv : forall b0 h0 l0 tab b tab',
    build_scope_table_aux (h0,l0) (tab,b) b0 = (tab',true) ->
    forall h n lb,
      PTree.get n (fst tab') = Some (h, lb) ->
      PTree.get n (fst tab) = Some (h, lb) \/
      ((h,lb) = (h0,l0) /\ b0 = I n) \/
      (In (I n) (I h :: lb) /\ sc_In h lb b0).
Proof.
    fix 1.
    intros [n|h0 lb0]; simpl in *.
    > destruct tab; intros.
      inv H; simpl in *.
      rewrite PTree.gsspec in *; destruct peq.
      > inv H0; auto.
      > auto.
    > intros h1 l0 tab b tab' H h n lb H0.
      destruct tab; simpl in *.
      exploit (fold_sc_In_get_inv sc_In_get_inv); eauto; simpl; clear H.
      intuition.
      > rewrite PTree.gsspec in *; destruct peq; auto.
        inv H1; intuition.
      > inv H1; intuition.
  Qed.

  Lemma sc_In_get_main_inv : forall b lb0 tab',
    build_scope_table (b,lb0) = OK tab' ->
    forall h n lb, PTree.get n (fst tab') = Some (h, lb) ->
      In (I n) (I h :: lb) /\ sc_In h lb (L b lb0).
Proof.
    unfold build_scope_table; intros.
    case_eq (fold_left (build_scope_table_aux (b, lb0)) lb0
             (PTree.set b (b, lb0) (PTree.empty (node * list bourdoncle)),
             (PTree.empty node), true)); intros.
    rewrite H1 in *.
    destruct b0; inv H.
    exploit (fold_sc_In_get_inv sc_In_get_inv); eauto.
    simpl; destruct 1.
    > rewrite PTree.gsspec in *; destruct peq.
      > inv H; auto.
      > rewrite PTree.gempty in H; congruence.
    > intuition.
      > inv H; auto.
      > inv H; auto.
  Qed.

  Lemma In_scope_get_fst_inv : forall main tab,
    build_scope_table main = OK tab ->
    forall n sc, PTree.get n (fst tab) = Some sc -> In_scope main n sc.
Proof.
    intros.
    destruct main; destruct sc; simpl.
    exploit sc_In_get_main_inv; eauto.
  Qed.

  Lemma get_fst_In_scope_iff : forall main tab,
    build_scope_table main = OK tab ->
    forall n sc, In_scope main n sc <-> PTree.get n (fst tab) = Some sc.
Proof.
    split.
    > apply In_scope_get_fst; auto.
    > apply In_scope_get_fst_inv; auto.
  Qed.

  Lemma get_fst_of_my_header : forall main tab,
    build_scope_table main = OK tab ->
    forall n h l, PTree.get n (fst tab) = Some (h,l) ->
      PTree.get h (fst tab) = Some (h,l).

Proof.
    intros.
    exploit In_scope_get_fst_inv; eauto; intros.
    erewrite <- get_fst_In_scope_iff; eauto.
    clear H H0.
    destruct main; simpl in *; intuition.
  Qed.

  Lemma get_root_main : forall sc tab',
    build_scope_table sc = OK tab' ->
    (fst tab')!(fst sc) = Some sc.
Proof.
    unfold build_scope_table; intros.
    destruct sc.
    case_eq (fold_left (build_scope_table_aux (p, l)) l
             (PTree.set p (p, l) (PTree.empty (node * list bourdoncle)),
             (PTree.empty node), true)); intros.
    rewrite H0 in *.
    destruct b; inv H.
    simpl.
    rewrite (old_map_build_scope_table_aux old_map_build_scope_table
          _ _ _ _ _ H0); simpl; auto.
    > rewrite PTree.gss; auto.
    > rewrite PTree.gss; congruence.
  Qed.

  Lemma fold_in_parent :
    (forall b0 sc0 tab b tab',
      build_scope_table_aux sc0 (tab,b) b0 = (tab',true) ->
      (fst tab)!(fst sc0) = Some sc0 ->
      In b0 (snd sc0) ->
      forall p n,
        PTree.get n (snd tab') = Some p ->
        PTree.get n (snd tab) = Some p \/
        (exists sc, PTree.get p (fst tab') = Some (p,sc) /\
          exists l, In (L n l) sc)) ->
    forall lb0 n p sc0 tab b tab',
      fold_left (build_scope_table_aux sc0) lb0 (tab,b) = (tab', true) ->
      (fst tab)!(fst sc0) = Some sc0 ->
      (incl lb0 (snd sc0)) ->
      (snd tab') ! n = Some p ->
        PTree.get n (snd tab) = Some p \/
      (exists sc, PTree.get p (fst tab') = Some (p,sc) /\
          exists l, In (L n l) sc).
Proof.
    intros IH'; fix IH 1; intros [|b lb]; simpl; intros.
    > inv H; auto.
    > case_eq (build_scope_table_aux sc0 (tab,b0) b).
      intros tab1 b1 Hb.
      destruct b1.
      > rewrite Hb in *.
        exploit IH; eauto with datatypes.
        destruct 1; auto.
        exploit IH'; eauto.
        destruct 1; auto.
        destruct H4 as (sc & S1 & S2).
        right; exists sc; split; eauto.
      > rewrite Hb in *.
        elim fold_build_scope_false_elim with (1:=H).
  Defined.

  Lemma in_parent : forall b0 sc0 tab b tab',
    build_scope_table_aux sc0 (tab,b) b0 = (tab',true) ->
    (fst tab)!(fst sc0) = Some sc0 ->
    In b0 (snd sc0) ->
    forall p n,
      PTree.get n (snd tab') = Some p ->
      PTree.get n (snd tab) = Some p \/
      (exists sc, PTree.get p (fst tab') = Some (p,sc) /\
        exists l, In (L n l) sc).
Proof.
    fix 1.
    intros [n|h0 lb0]; simpl in *.
    > destruct tab; intros.
      inv H; simpl in *; auto.
    > intros sc0 tab b tab' H Hp1 Hp2 p n H0.
      destruct tab; simpl in *.
      exploit (fold_in_parent in_parent); eauto with datatypes; simpl.
      rewrite PTree.gss; auto.
      destruct 1; auto.
      rewrite PTree.gsspec in *; destruct peq; auto.
      inv H1; auto.
      destruct sc0; simpl in *.
      right; exists l; split; eauto.
      eapply fold_build_scope_table_same; eauto.
      simpl.
      rewrite PTree.gsspec in *; destruct peq; auto.
      assert (ptree_mem h0 t0=true).
        unfold ptree_mem.
        rewrite <- e; rewrite Hp1; auto.
      rewrite H1 in H; simpl in *.
      elim fold_build_scope_false_elim with (1:=H).
  Qed.

  Lemma in_parent_main : forall main tab,
    build_scope_table main = OK tab ->
    forall p n,
      (snd tab)!n = Some p ->
      (exists sc, (fst tab)!p = Some (p,sc) /\ exists l, In (L n l) sc).
Proof.
    unfold build_scope_table; intros.
    destruct main.
    case_eq (fold_left (build_scope_table_aux (p0,l)) l
      (PTree.set p0 (p0, l) (PTree.empty (node * list bourdoncle)),
              (PTree.empty node), true)); intros;
    rewrite H1 in *; try congruence.
    destruct b; try congruence.
    inv H.
    exploit (fold_in_parent in_parent); eauto with datatypes; simpl.
    rewrite PTree.gss; auto.
    destruct 1; auto.
    rewrite PTree.gempty in *; congruence.
  Qed.

  Section In_fold1.
    Variable n0: node.
    Variable f: list node -> bourdoncle -> list node.
    Variable P: forall b l, In n0 l -> In n0 (f l b).
    
    Lemma In_fold1: forall lb l, In n0 l -> In n0 (fold_left f lb l).
Proof.
      fix 1.
      intros [|b lb] l Hi; simpl.
      apply Hi.
      apply In_fold1.
      apply P.
      apply Hi.
    Defined.

  End In_fold1.

  Lemma in_acc_in_bourdoncle_elements : forall n0 b l,
    In n0 l -> In n0 (bourdoncle_elements l b).
Proof.
    intros n0.
    fix 1.
    intros [n|h lb]; simpl in *; auto.
    intros l Hl.
    apply In_fold1.
    apply in_acc_in_bourdoncle_elements.
    right; auto.
  Qed.

  Section In_fold2.
    Variable n0: node.
    Variable Q : bourdoncle -> Prop.
    Variable f: list node -> bourdoncle -> list node.
    Variable P1: forall b l, In n0 l -> In n0 (f l b).
    Variable P2: forall b l, Q b -> In n0 (f l b).

    Lemma In_fold2: forall lb l b,
      In b lb -> Q b ->
      In n0 (fold_left f lb l).
Proof.
      fix 1.
      intros [|b lb] l b0 H1 H2.
      elim H1.
      simpl in H1; destruct H1.
      simpl.
      apply In_fold1.
      apply P1.
      apply P2.
      subst; auto.
      simpl.
      apply (In_fold2 lb (f l b) b0); auto.
    Defined.
  End In_fold2.

  Lemma in_bourdoncle_in_bourdoncle_elements : forall n0 b l,
    in_bourdoncle n0 b = true -> In n0 (bourdoncle_elements l b).
Proof.
    intros n0.
    fix 1.
    intros [n|h lb] l Hi; simpl in *.
    rewrite Peqb_eq in *; auto.
    destruct (Bool.orb_true_elim _ _ Hi).
    apply In_fold1.
    apply in_acc_in_bourdoncle_elements.
    left; rewrite Peqb_eq in *; auto.
    rewrite existsb_exists in e.
    destruct e as (b & Hb1 & Hb2).
    apply (In_fold2 n0 (fun b => in_bourdoncle n0 b = true)) with (b:=b).
    apply in_acc_in_bourdoncle_elements.
    apply in_bourdoncle_in_bourdoncle_elements.
    apply Hb1.
    apply Hb2.
  Qed.

  Section In_fold3.
    Variable n0: node.
    Variable Q : bourdoncle -> Prop.
    Variable f: list node -> bourdoncle -> list node.
    Variable P: forall b l, In n0 (f l b) -> Q b \/ In n0 l.

    Lemma In_fold3: forall lb l,
      In n0 (fold_left f lb l) ->
      (exists b, In b lb /\ Q b) \/ In n0 l.
Proof.
      fix 1.
      intros [|h lb] l; simpl; intros Hi.
      auto.
      destruct (In_fold3 _ _ Hi).
      destruct H as (b & B1 & B2); left; eauto.
      destruct (P _ _ H); eauto.
    Defined.
  End In_fold3.

  Lemma in_bourdoncle_elements_in_bourdoncle : forall n0 b l,
    In n0 (bourdoncle_elements l b) -> in_bourdoncle n0 b = true \/ In n0 l.
Proof.
    intros n0.
    fix 1.
    intros [n|h lb] l Hi; simpl in *.
    rewrite Peqb_eq in *; intuition.
    rewrite Bool.orb_true_iff.
    destruct (In_fold3 n0 (fun b => in_bourdoncle n0 b = true) bourdoncle_elements
      in_bourdoncle_elements_in_bourdoncle _ _ Hi).
    destruct H as (b & B1 & B2).
    left; right.
    rewrite existsb_exists; eauto.
    simpl in H; destruct H; auto.
    left; left.
    rewrite Peqb_eq in *; auto.
  Qed.

  Lemma in_bourdoncle_elements_sc_In_aux:
    (forall b n l,
      In n (bourdoncle_elements l b) ->
      In n l \/ b = I n \/
      exists h, exists lb,
        In (I n) (I h :: lb) /\ sc_In h lb b) ->
    (forall l n l0 h',
      In n (fold_left bourdoncle_elements l l0) ->
      In n l0 \/ In (I n) l \/
      exists h, exists lb,
        In (I n) (I h :: lb) /\ sc_In h lb (L h' l)).
Proof.
    intros HP.
    fix IH 1; intros [|n0 l0]; simpl; auto.
    intros n l1 h' Hi.
    destruct (IH _ _ _ h' Hi) as [H1|[H1|H1]]; clear IH.
    > destruct (HP _ _ _ H1); clear HP; auto.
      destruct H; subst; auto.
      destruct H as (h & lb & L1 & L2).
      right; right.
      exists h; exists lb; split; auto.
    > auto.
    > destruct H1 as (h & lb & L1 & L2).
      right; right.
      simpl in L2; destruct L2.
      > destruct H; subst.
        exists h; exists (n0::lb); split; auto.
        simpl in *; destruct L1; subst; auto.
      > exists h; exists lb; auto.
  Defined.

  Lemma in_bourdoncle_elements_sc_In: forall b n l,
    In n (bourdoncle_elements l b) ->
    In n l \/ b = I n \/
    exists h, exists lb,
      In (I n) (I h :: lb) /\ sc_In h lb b.
Proof.
    fix IH 1; intros [n0|h0 lb0]; simpl.
    > destruct 1; auto.
      subst; auto.
    > intros.
      destruct (in_bourdoncle_elements_sc_In_aux IH _ _ _ h0 H); clear H.
      > simpl in H0; destruct H0; auto.
        right; right; subst.
        exists n; exists lb0; auto.
      > right; right.
        destruct H0.
        > exists h0; exists lb0; split; auto.
        > destruct H as (h & lb & L1 & L2).
          simpl in L2.
          eauto.
  Qed.

  Lemma in_nodes: forall n sc,
    In n (nodes sc) -> exists sc_n, In_scope sc n sc_n.
Proof.
    intros n (b,l) Hi; simpl in *.
    unfold In_scope.
    destruct (in_bourdoncle_elements_sc_In_aux in_bourdoncle_elements_sc_In _ _ _ b Hi);
      clear Hi.
    simpl in H; intuition; subst.
    > exists (n,l); simpl; auto.
    > destruct H.
      > exists (b,l); simpl; auto.
      > destruct H as (h & lb & L1 & L2).
        exists (h, lb); split; auto.
  Qed.

  Lemma fold_sc_In_in_bourdoncle_elements:
    (forall b h lb l,
      sc_In h lb b ->
      In h (bourdoncle_elements l b)) ->
    forall l h lb l0,
      Exists (sc_In h lb) l ->
      In h (fold_left bourdoncle_elements l l0).
Proof.
    intros IH'.
    fix IH 1; intros [|n l]; simpl; intuition.
    > apply In_fold1; eauto.
      apply in_acc_in_bourdoncle_elements.
    > eauto.
  Defined.

  Lemma sc_In_in_bourdoncle_elements: forall b h lb l,
    sc_In h lb b ->
    In h (bourdoncle_elements l b).
Proof.
    fix IH 1; intros [n|h l]; simpl; intuition.
    > subst.
      apply In_fold1; auto with datatypes.
      apply in_acc_in_bourdoncle_elements.
    > eapply (fold_sc_In_in_bourdoncle_elements IH); eauto.
  Qed.

  Lemma Exists_exists : forall A P (l:list A),
    Exists P l <-> exists x, In x l /\ P x.
Proof.
    induction l; simpl; intuition eauto.
    destruct H as (x & H1 & H2); eauto.
    destruct H1 as (x & H3 & H4); eauto.
    destruct H1 as (x & H3 & H4); intuition eauto.
    subst; auto.
  Qed.

  Lemma sc_In_in_bourdoncle_elements2: forall b h lb l n,
    In (I n) lb ->
    sc_In h lb b ->
    In n (bourdoncle_elements l b).
Proof.
    fix IH 1; intros [n|h l]; simpl; intuition.
    > subst.
      apply In_fold2 with (b:=I n) (Q:=fun b => b=I n); auto with datatypes.
      apply in_acc_in_bourdoncle_elements.
      intros.
      apply in_bourdoncle_in_bourdoncle_elements.
      subst; simpl.
      rewrite Peqb_eq; auto.
    > rewrite Exists_exists in H1.
      destruct H1 as (b & B1 & B2).
      apply In_fold2 with (b:=b) (Q:=fun b => exists h0, exists lb, sc_In h0 lb b /\
        In (I n) lb); auto with datatypes.
      apply in_acc_in_bourdoncle_elements.
      intros.
      destruct H0 as (h1 & lb1 & L1 & L2).
      eauto.
      eauto.
  Qed.

  Lemma in_nodes_inv: forall n sc sc_n,
    In_scope sc n sc_n ->
    In n (nodes sc).
Proof.
    intros n (b,l) (b_n,l_n) Hi; simpl in *.
    intuition.
    > inv H1.
      apply In_fold1; auto with datatypes.
      apply in_acc_in_bourdoncle_elements.
    > inv H1.
      eapply (fold_sc_In_in_bourdoncle_elements sc_In_in_bourdoncle_elements); eauto.
    > subst.
      eapply In_fold2; eauto with datatypes.
      apply in_acc_in_bourdoncle_elements.
      eapply in_bourdoncle_in_bourdoncle_elements; eauto.
      simpl.
      rewrite Peqb_eq; auto.
    > rewrite Exists_exists in H.
      destruct H as (b' & B1 & B2).
      apply In_fold2 with (b:=b') (Q:=fun b =>
        exists l_n,
          exists b_n, In (I n) l_n /\ sc_In b_n l_n b) ; eauto with datatypes.
      apply in_acc_in_bourdoncle_elements.
      clear H1 B2 B1 b' b_n l_n b l.
      intros b l (l_n & b_n & B1 & B2).
      eapply sc_In_in_bourdoncle_elements2; eauto.
  Qed.


  Lemma list_sc_In_trans:
    (forall b0 n1 l1 n2 l2,
      sc_In n1 l1 b0 ->
      sc_In n2 l2 (L n1 l1) ->
      sc_In n2 l2 b0) ->
    forall l0 n1 l1 n2 l2,
      Exists (sc_In n1 l1) l0 ->
      Exists (sc_In n2 l2) l1 ->
      Exists (sc_In n2 l2) l0.
Proof.
    intros HP.
      fix IH' 1; intros [|n l]; intros; simpl in *; intuition.
      > exploit (HP n); eauto.
      > exploit (IH' l); eauto.
  Defined.

  Lemma sc_In_trans: forall b0 n1 l1 n2 l2,
    sc_In n1 l1 b0 ->
    sc_In n2 l2 (L n1 l1) ->
    sc_In n2 l2 b0.
Proof.
    fix IH 1; intros [n0|n0 l0]; intros; simpl in *.
    intuition.
    intuition; subst; auto.
    right.
    eapply list_sc_In_trans; eauto.
  Qed.

  Lemma In_scope_trans: forall sc0 n1 sc1 n2 sc2,
    In_scope sc0 n1 sc1 ->
    In_scope sc1 n2 sc2 ->
    In_scope sc0 n2 sc2.
Proof.
    destruct sc0; destruct sc1; destruct sc2; simpl.
    intuition try congruence.
    > inv H0; inv H2.
      right; eapply (list_sc_In_trans sc_In_trans); eauto.
    > inv H0.
      right; eapply (list_sc_In_trans sc_In_trans); eauto.
    > inv H2.
      right; eapply (list_sc_In_trans sc_In_trans); eauto.
    > right; eapply (list_sc_In_trans sc_In_trans); eauto.
  Qed.

  Notation "sc1 ⊆ sc2" := (incl (nodes sc1) (nodes sc2)) (at level 10).


  Lemma In_scope_incl: forall (sc:t) (n:node) (sc_n:t),
    In_scope sc n sc_n ->
    sc_n ⊆ sc.
Proof.
    intros sc n sc_n H x Hx.
    apply in_nodes in Hx.
    destruct Hx as (sc_x & Hx).
    eapply in_nodes_inv; eauto.
    eapply In_scope_trans; eauto.
  Qed.

  Definition in_scope_test (n:node) (s:t) : bool :=
    let (h,l) := s in
      Peqb n h ||
        List.existsb (in_bourdoncle n) l.

  Lemma in_scope_test_correct : forall sc n, in_scope_test n sc = true <-> In n (nodes sc).
Proof.
    unfold in_scope_test.
    destruct sc; split; intros.
    rewrite orb_true_iff in H; destruct H.
    rewrite Peqb_eq in H.
    subst.
    simpl.
    apply In_fold1.
    apply in_acc_in_bourdoncle_elements.
    simpl; auto.
    rewrite existsb_exists in H.
    destruct H as (b & Hb1 & Hb2).
    apply (In_fold2 n (fun b => in_bourdoncle n b = true)) with (b:=b); auto.
    apply in_acc_in_bourdoncle_elements.
    apply in_bourdoncle_in_bourdoncle_elements.
    simpl in H.
    rewrite orb_true_iff.
    destruct (In_fold3 n (fun b => in_bourdoncle n b = true) bourdoncle_elements
      (in_bourdoncle_elements_in_bourdoncle n) _ _ H); auto.
    right.
    rewrite existsb_exists; auto.
    rewrite Peqb_eq; left.
    simpl in H0; intuition.
  Qed.

  Definition incl_scope_test (s1 s2:t) : bool :=
    List.forallb (fun n => in_scope_test n s2) (nodes s1).

  Lemma incl_scope_test_correct : forall sc1 sc2,
    incl_scope_test sc1 sc2 = true <-> sc1 ⊆ sc2.
Proof.
    unfold incl_scope_test; intros sc1 sc2.
    rewrite forallb_forall.
    split; intros.
    intros n Hn.
    rewrite <- in_scope_test_correct; auto.
    rewrite in_scope_test_correct; auto.
  Qed.

  Section scope_properties.
  Variable f : function.
  Variable main : t.
  Variable tab:scope_table.
  Variable headers:list node.
  Let elements:list t := map (scope_ tab main) headers.

  Hypothesis get_fst_In_scope_iff :
    forall n sc, In_scope main n sc <-> PTree.get n (fst tab) = Some sc.
  Hypothesis f_In_In_scope : forall n,
    f_In n f -> PTree.get n (fst tab) <> None.
  Hypothesis in_headers1: forall h,
    In h headers -> exists l, PTree.get h (fst tab) = Some (h,l).
  Hypothesis in_headers2: forall h,
    In h headers -> f_In h f.
  Hypothesis root_In_headers: In f.(fn_entrypoint) headers.
  Hypothesis snd_root: PTree.get f.(fn_entrypoint) (snd tab) = None.
  Hypothesis scope_root: (fst tab)!(f.(fn_entrypoint)) = Some main.
  Hypothesis in_headers3: forall h l,
    PTree.get h (fst tab) = Some (h,l) -> In h headers.
  Hypothesis get_fst_of_my_header : forall n h l, PTree.get n (fst tab) = Some (h,l) ->
      PTree.get h (fst tab) = Some (h,l).
  Hypothesis parent_is_header : forall h p,
    PTree.get h (snd tab) = Some p -> In p headers.
  Hypothesis parent_tab:
    forall p n,
      (snd tab)!n = Some p ->
      (exists sc, (fst tab)!p = Some sc /\ exists l, In (L n l) (snd sc)).
  Hypothesis check_root: forall h,
    In h headers -> h=f.(fn_entrypoint) \/
    in_scope_test f.(fn_entrypoint) (scope_ tab main h) = false.
  Hypothesis headers_snd_some: forall h,
    In h headers -> h = f.(fn_entrypoint) \/
    exists p, (snd tab)!h = Some p /\
      in_scope_test p (scope_ tab main h) = false.
  Hypothesis parent_least_check: forall h h',
    In h headers -> In h' headers -> h<>h' ->
    In h (nodes (scope_ tab main h')) ->
    match (snd tab)!h with
      | None => True
      | Some p => In p (nodes (scope_ tab main h'))
    end.


  Lemma in_scope: forall n, f_In n f -> In n (nodes (scope_ tab main n)).
Proof.
    unfold scope_; intros.
    case_eq ((fst tab)!n); intros.
    > rewrite <- get_fst_In_scope_iff in H0.
      destruct main as [b0 l0].
      destruct p as [b l].
      destruct H0.
      simpl.
      simpl in H0; destruct H0.
      > inv H0.
        apply In_fold1; auto.
        intros; apply in_acc_in_bourdoncle_elements; auto.
      > apply (In_fold2 n (fun b => in_bourdoncle n b = true)) with (b:=I n); auto.
        > intros; apply in_acc_in_bourdoncle_elements; auto.
        > intros; apply in_bourdoncle_in_bourdoncle_elements; auto.
        > simpl.
          rewrite Peqb_refl; auto.
    > eelim f_In_In_scope; eauto.
  Qed.

  Lemma scope_least: forall n sc,
    In sc elements ->
    In n (nodes sc) -> (scope_ tab main n) ⊆ sc.
Proof.
    unfold elements, scope_; intros.
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    apply in_headers1 in T2.
    destruct T2 as (l & T2).
    rewrite T2 in *.
    rewrite <- get_fst_In_scope_iff in *.
    rewrite T1 in *.
    apply in_nodes in H0.
    destruct H0 as (sc_n & S0).
    assert (In_scope main n sc_n) by (eapply In_scope_trans; eauto).
    rewrite get_fst_In_scope_iff in H.
    rewrite H.
    eapply In_scope_incl; eauto.
  Qed.

  Lemma header_scope_: forall h,
    In h headers ->
    header_ (scope_ tab main h) = h.
Proof.
    unfold scope_, header_; intros h.
    intros; destruct in_headers1 with h as (l & L); auto.
    rewrite L; auto.
  Qed.

  Lemma header_f_In: forall sc, In sc elements -> f_In (header_ sc) f.
Proof.
    unfold elements; intros.
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    subst; rewrite header_scope_; auto.
  Qed.

  Lemma scope_header: forall sc, In sc elements -> scope_ tab main (header_ sc) = sc.
Proof.
    unfold elements, scope_; intros.
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    apply in_headers1 in T2.
    destruct T2 as (l & T2).
    rewrite T2 in *.
    subst; simpl in *.
    rewrite T2; auto.
  Qed.

    
  Lemma scope_main_or_in_header: forall n,
    exists h, In h headers /\ scope_ tab main n = scope_ tab main h.
Proof.
    intros; unfold scope_.
    case_eq ((fst tab)!n); intros.
    destruct p as (h & l).
    assert ((fst tab)!h = Some (h,l)) by (eauto).
    exists h; rewrite H0.
    split; eauto.
    exists (f.(fn_entrypoint)); split; auto.
    rewrite scope_root; auto.
  Qed.

  Lemma scope_in_elements: forall n, In (scope_ tab main n) elements.
Proof.
    unfold elements; intros.
    destruct (scope_main_or_in_header n) as (h & H1 & H2).
    rewrite H2.
    apply in_map; auto.
  Qed.

  Lemma incl_in_parent: forall sc, In sc elements -> sc ⊆ (parent_ tab sc).
Proof.
    unfold elements, parent_; intros.
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    subst; rewrite header_scope_; auto.
    apply scope_least.
    > case_eq ((snd tab)!h); intros.
      > case_eq ((fst tab)!p); intros.
        > assert (In p headers) by eauto.
          assert (scope_ tab main p=p0).
            unfold scope_.
            rewrite H0; auto.
          rewrite <- H2; apply scope_in_elements.
        > apply scope_in_elements.
      > apply scope_in_elements.
    > case_eq ((snd tab)!h); intros.
      > exploit parent_tab; eauto.
        intros (sc & S1 & l & S2).
        rewrite S1.
        destruct sc; unfold nodes; simpl in *.
        eapply In_fold2 with (b:=L h l) (Q:=fun b => exists l, b = L h l); eauto.
        apply in_acc_in_bourdoncle_elements.
        intros.
        apply in_bourdoncle_in_bourdoncle_elements.
        destruct H0; subst; simpl.
        rewrite Peqb_refl; simpl; auto.
      > unfold scope_.
        exploit in_headers1; eauto.
        destruct 1 as (l & L).
        rewrite L; simpl.
        apply In_fold1.
        apply in_acc_in_bourdoncle_elements.
        simpl; auto.
  Qed.

  Lemma parent_least: forall sc sc',
      In sc elements -> In sc' elements ->
      sc ⊆ sc' -> sc = sc' \/ (parent_ tab sc) ⊆ sc'.
Proof.
    unfold elements, parent_; intros.
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    rewrite in_map_iff in H0.
    destruct H0 as (h0 & T10 & T20).
    subst.
    assert (In h (nodes (scope_ tab main h0))).
      apply H1.
      apply in_scope; auto.
    destruct (peq h h0).
    > subst; auto.
    > exploit (parent_least_check h h0); eauto.
      elim headers_snd_some with h; auto.
      > intros T _.
        elim in_headers1 with f.(fn_entrypoint); auto.
        intros l0 T0.
        replace (header_ (scope_ tab main h)) with f.(fn_entrypoint).
        rewrite snd_root; auto.
        unfold scope_.
        rewrite T; rewrite T0; auto.
      > intros (p & P1 & P2).
        rewrite P1.
        replace (header_ (scope_ tab main h)) with h.
        rewrite P1.
        intros P.
        assert ((scope_ tab main p) ⊆ (scope_ tab main h0)).
          apply scope_least; auto.
          apply scope_in_elements.
          right.
          elim in_headers1 with p; eauto.
          intros lp Hp.
          unfold scope_ in *; rewrite Hp in *; auto.
        elim in_headers1 with h; eauto.
        intros lh Hh.
        unfold scope_; rewrite Hh; auto.
  Qed.

  Lemma In_sons_aux: forall b0 lb0 lb l,
    In (b0,lb0) (fold_left sons1 lb l) -> In (L b0 lb0) lb \/ In (b0,lb0) l.
Proof.
    induction lb; simpl; auto.
    intros.
    elim IHlb with (1:=H); auto.
    destruct a; simpl; intuition.
    left; left; congruence.
  Qed.

  Lemma sons_in_element: forall sc sc',
    In sc elements -> In sc' (sons sc) -> In sc' elements.
Proof.
    unfold sons, elements; intros.
    destruct sc' as (b' & lb').
    apply In_sons_aux in H0.
    destruct H0; try (intuition; fail).
    rewrite in_map_iff in H.
    destruct H as (h & T1 & T2).
    elim in_headers1 with (1:=T2); intros l L1.
    assert (sc = (h,l)).
      generalize T1; unfold scope_; rewrite L1; congruence.
    rewrite <- get_fst_In_scope_iff in L1.
    clear T1.
    subst sc; simpl in H0.
    assert (In_scope (h,l) b' (b',lb')).
      simpl; intuition.
      right; rewrite Exists_exists.
      exists (L b' lb'); simpl; auto.
    assert (In_scope main b' (b',lb')) by (eapply In_scope_trans; eauto).
    rewrite get_fst_In_scope_iff in H1.
    replace (b',lb') with (scope_ tab main b').
    apply in_map; eauto.
    unfold scope_; rewrite H1; auto.
  Qed.

  Lemma parent_in_element: forall sc,
    In sc elements -> In (parent_ tab sc) elements.
Proof.
    unfold elements, parent_; intros.
    destruct sc as (h & l); simpl.
    case_eq ((snd tab)!h); intros; auto.
    elim parent_tab with (1:=H0); intros sc (S1 & lh & S2).
    rewrite S1.
    replace sc with (scope_ tab main p).
    apply scope_in_elements.
    unfold scope_; rewrite S1; auto.
  Qed.

  Lemma in_scope_root: forall sc,
      In sc elements ->
      In f.(fn_entrypoint) (nodes sc) ->
      f.(fn_entrypoint) = header_ sc.
Proof.
    unfold elements; intros.
    rewrite in_map_iff in H.
    destruct H as (h & H1 & H2).
    destruct (check_root h); auto.
    > subst.
      rewrite header_scope_; auto.
    > rewrite <- in_scope_test_correct in H0.
      congruence.
  Qed.

  Lemma parent_strict_subset: forall sc,
    In sc elements ->
    In (header_ (parent_ tab sc)) (nodes sc) -> f.(fn_entrypoint) = header_ sc.
Proof.
    unfold parent_, elements; intros.
    rewrite in_map_iff in H.
    destruct H as (h & H1 & H2).
    elim in_headers1 with h; auto; intros l Hl.
    generalize H1; unfold scope_.
    rewrite Hl; simpl; intros; subst.
    rewrite <- H3; simpl.
    elim headers_snd_some with h; auto.
    intros (p & P1 & P2).
    rewrite <- H3 in H0; simpl in H0.
    rewrite P1 in H0.
    assert (In p (nodes (scope_ tab main h))).
      rewrite <- H3; simpl.
      elim in_headers1 with p; eauto.
      intros lp L.
      rewrite L in H0; auto.
    rewrite <- in_scope_test_correct in H.
    congruence.
  Qed.

  Variable order: node -> N.
  Notation scope := (scope_ tab main).
  Notation parent := (parent_ tab).
  Hypothesis succ_order: forall n s,
    succ_node f n s -> (order n < order s)%N \/ s = header_ (scope n).
  Hypothesis
    enter_in_scope_at_header_only: forall n n',
      succ_node f n n' ->
      ~ In n (nodes (scope n')) ->
       n' = header_ (scope n') /\ parent (scope n') = scope n.

  Lemma enter_in_scope_at_header_only1: forall n n' sc,
    succ_node f n n' -> In sc elements ->
    ~ In n (nodes sc) -> In n' (nodes sc) -> n' = header_ sc.
Proof.
    intros.
    exploit (enter_in_scope_at_header_only); eauto.
    > intro; destruct H1.
      assert ((scope n') ⊆ sc).
        apply scope_least; auto.
      apply H1; auto.
    > destruct 1.
      assert (HS:(scope n') ⊆ sc).
        apply scope_least; auto.
      destruct (parent_least (scope n') sc); auto.
      > apply scope_in_elements.
      > congruence.
      > rewrite H4 in *.
        destruct H1.
        apply H5.
        apply in_scope.
        apply succ_node_f_In with n'; auto.
   Qed.

   
   Lemma path_inv0 : forall n1 tr n2,
    path f n1 tr n2 ->
    incl (n1::tr) (nodes (scope n2)) ->
    forall sc, In sc elements -> ~ In n2 (nodes sc) -> In n1 (nodes sc) ->
      In (header_ sc) (n1::tr).
Proof.
     induction 1; auto.
     intuition.
     intros H1 sc Hs1 Hs2 Hs3.
     destruct (List.In_dec peq n' (nodes sc)).
     > right; eauto with datatypes.
     > exploit enter_in_scope_at_header_only1; simpl; eauto.
   Qed.

   Lemma path_inv1 : forall n1 tr n2,
     f_In n1 f ->
     path f n1 tr n2 ->
     incl (n1::tr) (nodes (scope n2)) ->
     ~ In n2 (nodes (scope n1)) ->
     In (header_ (scope n1)) (n1::tr).
Proof.
     intros; eapply path_inv0; eauto.
     apply scope_in_elements.
     apply in_scope; auto.
   Qed.


   Lemma path_in_other_path: forall n1 tr n2,
     path f n1 tr n2 -> forall n3,
     In n3 (n1::tr) ->
     exists tr', path f n3 tr' n2 /\ incl tr' tr /\ (length tr' <= length tr)%nat.
Proof.
     induction 1; simpl; intros.
     > intuition; subst.
       exists nil; repeat constructor; auto with datatypes.
     > destruct H1.
       > subst.
         exists (n'::rl); split; auto.
         > econstructor; eauto.
         > split; auto with datatypes.
       > elim IHrev_path with n3; auto; intros tr' (T1 & T2 & T3).
         exists tr'; split; auto.
         split; auto with datatypes.
   Qed.

   Lemma header_in_scope: forall sc,
     In sc elements ->
     In (header_ sc) (nodes sc).
Proof.
     intros.
     replace (nodes sc) with (nodes (scope (header_ sc))).
     apply in_scope.
     apply header_f_In; auto.
     rewrite scope_header; auto.
   Qed.

   Lemma sim_in_scope: forall n1 n2,
     In n1 (nodes (scope n2)) ->
     In n2 (nodes (scope n1)) ->
     header_ (scope n1) = header_ (scope n2).
Proof.
     intros.
     assert ((scope n1) ⊆ (scope n2)).
       apply scope_least; auto.
       apply scope_in_elements.
     assert ((scope n2) ⊆ (scope n1)).
       apply scope_least; auto.
       apply scope_in_elements.
     exploit parent_least; eauto.
       apply scope_in_elements.
       apply scope_in_elements.
     destruct 1; try congruence.
     revert H1; intros.
     exploit parent_least; eauto.
       apply scope_in_elements.
       apply scope_in_elements.
     destruct 1; try congruence.
     assert (f.(fn_entrypoint) = header_ (scope n1)).
       apply parent_strict_subset.
       apply scope_in_elements.
       apply H2.
       apply H4.
       apply header_in_scope.
       apply parent_in_element.
       apply scope_in_elements.
     assert (f.(fn_entrypoint) = header_ (scope n2)).
       apply parent_strict_subset.
       apply scope_in_elements.
       apply H1.
       apply H3.
       apply header_in_scope.
       apply parent_in_element.
       apply scope_in_elements.
     congruence.
   Qed.

  Lemma path_inv2: forall N n1 tr n2,
    length tr = N ->
    path f n1 tr n2 ->
    incl (n1::tr) (nodes (scope n2)) ->
    (order n2 < order n1)%N \/ In (header_ (scope n2)) (n1::tr) \/ tr=nil.
Proof.
    intros N; pattern N; apply lt_wf_rec.
    clear N; intros N HI n1 tr n2 Hl Hp Hi.
    inv Hp; auto.
    destruct (List.In_dec peq n' (nodes (scope n2))).
    > exploit HI; eauto.
      > simpl; omega.
      > eauto with datatypes.
      > destruct 1 as [HI'|[HI'|HI']].
        > elim succ_order with (1:=H0); intros Ho.
          > left.
            eapply Nlt_trans; eauto.
          > destruct (List.In_dec peq n2 (nodes (scope n'))).
            assert (header_ (scope n2) = header_ (scope n')) by (apply sim_in_scope; auto).
            rewrite H1; simpl; auto.
            assert (In (header_ (scope n')) (n'::rl)).
              eapply path_inv1; eauto.
              eapply succ_f_In; eauto.
              eauto with datatypes.
            rewrite <- Ho in *.
            assert (exists tr', path f n1 tr' n2 /\ incl tr' rl /\ (length tr' <= length rl)%nat) by (eapply path_in_other_path; eauto).
            destruct H2 as (tr' & T1 & T2 & T3).
            eelim HI with (3:=T1); eauto.
            > destruct 1.
              > right; left.
                simpl in H2; destruct H2; eauto with datatypes.
                simpl; auto.
              > subst; inv T1; elim n.
                replace (nodes (scope n')) with (nodes (scope (header_ (scope n')))).
                apply in_scope.
                apply header_f_In.
                apply scope_in_elements.
                rewrite scope_header; auto.
                apply scope_in_elements.
            > rewrite <- plus_n_O.
              simpl; omega.
            > eauto with datatypes.
            > right; left; eauto with datatypes.
        > subst; inv H.
          elim succ_order with (1:=H0); intros Ho; auto.
          subst; auto with datatypes.
    > assert (~ In n' (nodes (scope n1))).
        intro; destruct n.
        assert ((scope n1) ⊆ (scope n2)).
          apply scope_least; auto.
          apply scope_in_elements.
        apply H2; auto.
      assert (n1 = header_ (scope n2)).
        eapply enter_in_scope_at_header_only1; eauto.
        apply scope_in_elements.
      simpl; auto.
   Qed.

   Lemma path_incl_case: forall n1 rl n,
     path f n1 rl n ->
     In n1 (nodes (scope n)) ->
     incl rl (nodes (scope n)) \/ In (header_ (scope n)) (n1::rl).
Proof.
     induction 1.
     > left; intro; intuition.
     > destruct (List.In_dec peq n' (nodes (scope n))); intros.
       destruct IHrev_path; eauto with datatypes.
       exploit enter_in_scope_at_header_only1; eauto.
       apply scope_in_elements.
       simpl; auto.
   Qed.

   Lemma cycle_at_not_header: forall rl n,
     f_In n f ->
     n <> header_ (scope n) ->
     path f n rl n -> rl <> nil -> In (header_ (scope n)) rl.
Proof.
     intros.
     elim path_incl_case with (1:=H1); auto; intros.
     exploit path_inv2; eauto.
     assert (In n (nodes (scope n))).
       apply in_scope; auto.
     auto with datatypes.
     intuition.
     eelim Nlt_irrefl; eauto.
     simpl in H4; intuition.
     simpl in H3; intuition.
     apply in_scope; auto.
   Qed.

   Lemma path_header_aux: forall n1 rl n,
     path f n1 rl n ->
     n = header_ (scope n) ->
     incl (n1::rl) (nodes (scope n)) \/
     ~ In n1 (nodes (scope n)) \/
     exists rl', exists n',
       incl (n'::rl') rl /\
       path f n (n'::rl') n /\
       ~ In n' (nodes (scope n)).
Proof.
     induction 1.
     > left; intro; simpl; intuition.
       subst; apply in_scope; auto.
     > destruct (List.In_dec peq n'' (nodes (scope n))); intros; auto.
       destruct IHrev_path; eauto with datatypes.
       destruct H2.
       > exploit enter_in_scope_at_header_only1; eauto.
         apply scope_in_elements.
         intros.
         right; right; exists rl; exists n'; repeat split; auto with datatypes.
         constructor; auto.
         congruence.
       > destruct H2 as (rl' & n0 & N1 & N2 & N3).
         right; right; exists rl'; exists n0; repeat split; auto with datatypes.
   Qed.

   Lemma path_header: forall rl n,
     f_In n f ->
     path f n rl n ->
     n = header_ (scope n) ->
     incl rl (nodes (scope n)) \/
     exists rl', exists n',
       incl (n'::rl') rl /\
       path f n (n'::rl') n /\
       parent (scope n) = scope n'.
Proof.
     intros.
     edestruct path_header_aux; eauto with datatypes.
     destruct H2.
     > destruct H2.
       apply in_scope; auto.
     > destruct H2 as (rl' & n' & N1 & N2 & N3).
       right; exists rl'; exists n'; repeat split; auto.
       exploit enter_in_scope_at_header_only; eauto.
       inversion N2; auto.
       intuition.
   Qed.

   Lemma rotate_path: forall n' rl n,
       path f n' rl n -> forall n'',
       f_In n'' f ->
       succ_node f n'' n ->
       path f n' (rl++n''::nil) n''.
Proof.
     induction 1; simpl.
     > constructor; auto.
       constructor; auto.
     > intros.
       exploit IHrev_path; eauto; clear IHrev_path; intros IH.
       constructor; auto.
   Qed.

   Lemma cycle_at_header: forall rl n,
     f_In n f ->
      n = header_ (scope n) ->
      path f n rl n -> rl <> nil ->
      In (header_ (parent_ tab (scope n))) rl \/
        (forall n', In n' rl -> In n' (nodes (scope n))).
Proof.
     intros.
     exploit path_header; eauto.
     destruct 1; auto.
     destruct H3 as (rl' & n' & N1 & N2 & N3); left.
     clear H1 H2.
     revert H0; inv N2; intuition.
     assert (path f n' (rl'++n'::nil) n').
       eapply rotate_path; eauto.
       eapply succ_f_In; eauto.
     rewrite N3 in *.
     destruct (peq n' (header_ (scope n'))); auto.
     apply N1; simpl; left; congruence.
     exploit (cycle_at_not_header (rl' ++ n' :: nil) n'); eauto.
     eapply succ_f_In; eauto.
     destruct rl'; simpl; congruence.
     rewrite in_app; intros.
     apply N1.
     simpl; intuition.
     simpl in H4; intuition.
   Qed.

End scope_properties.

End I.

  Notation "n ∈ sc" := (In n (nodes sc)) (at level 10).
  Notation "sc1 ⊆ sc2" := (incl (nodes sc1) (nodes sc2)) (at level 10).

  Record family (f:function) := {
    scope : node -> t;
    header : t -> node;
    parent : t -> t;
    elements: list t;

    in_scope: forall n, f_In n f -> n ∈ (scope n);
    scope_least: forall n sc, In sc elements -> n ∈ sc -> (scope n) ⊆ sc;

    header_f_In: forall sc, In sc elements -> f_In (header sc) f;
    scope_header: forall sc, In sc elements -> scope (header sc) = sc;

    incl_in_parent: forall sc, In sc elements -> sc ⊆ (parent sc);
    parent_least: forall sc sc',
      In sc elements -> In sc' elements ->
      sc ⊆ sc' -> sc = sc' \/ (parent sc) ⊆ sc';
    sons_in_element: forall sc sc',
      In sc elements -> In sc' (sons sc) -> In sc' elements;
    parent_in_element: forall sc,
      In sc elements -> In (parent sc) elements;

    scope_in_elements: forall n, In (scope n) elements;
    enter_in_scope_at_header_only: forall n n',
      succ_node f n n' ->
      ~ n ∈ (scope n') ->
       n' = header (scope n') /\ parent (scope n') = scope n;

    cycle_at_not_header: forall rl n,
      f_In n f ->
      n <> header (scope n) ->
      path f n rl n -> rl <> nil -> In (header (scope n)) rl;

    cycle_at_header: forall rl n,
      f_In n f ->
      n = header (scope n) ->
      path f n rl n -> rl <> nil ->
      In (header (parent (scope n))) rl \/
        (forall n', In n' rl -> n' ∈ (scope n));

    in_scope_root: forall sc,
      In sc elements ->
      f.(fn_entrypoint) ∈ sc ->
      f.(fn_entrypoint) = header sc;

    parent_strict_subset: forall sc,
      In sc elements ->
      (header (parent sc)) ∈ sc -> f.(fn_entrypoint) = header sc;

    root_no_pred: forall n, ~ succ_node f n f.(fn_entrypoint)
  }.
  Implicit Arguments scope [f].
  Implicit Arguments header [f].
  Implicit Arguments parent [f].
  Implicit Arguments elements [f].

Lemma po1: forall f (tab:I.scope_table),
  ptree_forall (fn_code f)
  (fun (n : node) (_ : instruction) =>
    ptree_mem n (fst tab)) = true ->
  forall n0 : RTL.node, f_In n0 f -> (fst tab) ! n0 <> None.
Proof.
  unfold f_In; intros.
  case_eq ((fn_code f)!n0); intros; try congruence.
  exploit (ptree_forall_correct1 _ (fun n _ => ptree_mem n (fst tab)) (fn_code f) );
    eauto.
  unfold ptree_mem.
  case_eq ((fst tab)!n0); congruence.
Qed.

Definition headers {A} (tab:PTree.t (node*A)) : list node :=
  PTree.fold (fun l p a => if peq p (fst a) then p::l else l) tab nil.

Lemma in_headers1 : forall A tab h,
  In h (@headers A tab) -> exists a, tab!h = Some (h,a).
Proof.
  intros A tab h; unfold headers.
  apply PTree_Properties.fold_rec
    with (P:=fun m l => In h l ->exists a, m!h = Some (h,a)); intros.
  rewrite <- H; auto.
  intuition.
  destruct peq.
  simpl in H2; destruct H2; subst.
  rewrite H2; rewrite PTree.gss; auto.
  destruct v; simpl in *.
  subst; eauto.
  rewrite PTree.gsspec; destruct peq.
  destruct v; simpl in *.
  subst; eauto.
  eauto.
  rewrite PTree.gsspec; destruct peq.
  subst.
  elim H1; auto; intros; congruence.
  eauto.
Qed.

Lemma in_headers2 : forall A tab a h,
  tab!h = Some (h,a) -> In h (@headers A tab).
Proof.
  intros A tab a h; unfold headers.
  apply PTree_Properties.fold_rec
    with (P:=fun m l => m!h = Some (h,a) -> In h l); intros.
  apply H0; rewrite H; auto.
  rewrite PTree.gempty in H; congruence.
  destruct peq; auto.
  rewrite PTree.gsspec in H2; destruct peq; simpl; auto.
  rewrite PTree.gsspec in H2; destruct peq; simpl; auto.
  inv H2; simpl in *; congruence.
Qed.

Definition forall_cfg_edge (f:function) (test:node->node->bool) : bool :=
  ptree_forall (fn_code f)
  (fun n ins =>
    forallb (fun n' => test n n') (successors_instr ins)).

Lemma forall_cfg_edge_correct : forall f test,
  forall_cfg_edge f test = true ->
  forall n n', succ_node f n n' -> test n n' = true.
Proof.
  unfold forall_cfg_edge; intros.
  destruct H0 as (ins & T1 & T2).
  exploit ptree_forall_correct1; eauto.
  simpl.
  rewrite forallb_forall; eauto.
Qed.


Definition build_family (f:function) : option (family f).
Proof.
destruct (build_bourdoncle f) as (b & order).
case_eq (I.cast_bourdoncle b); [intros (h,l) Hb|intros; exact None].
case_eq (I.build_scope_table (h,l)); [intros tab Htab|intros; exact None].
destruct (peq h f.(fn_entrypoint)); [|exact None].
case_eq (ptree_forall (fn_code f) (fun n _ => ptree_mem n (fst tab))); intros Hp1; [|exact None].
set (headers := headers (fst tab)).
set (elements:= map (I.scope_ tab (h,l)) headers).
case_eq (forallb (fun h => ptree_mem h (fn_code f)) headers); intros Hf1; [|exact None].
assert(get_fst_In_scope_iff :
    forall n sc, I.In_scope (h,l) n sc <-> PTree.get n (fst tab) = Some sc).
  eapply I.get_fst_In_scope_iff; eauto.
assert (f_In_In_scope : forall n,
    f_In n f -> PTree.get n (fst tab) <> None).
  eapply po1; eauto.
assert (in_headers1: forall h,
    In h headers -> exists l, PTree.get h (fst tab) = Some (h,l)).
  apply in_headers1.
assert (root_In_headers: In f.(fn_entrypoint) headers).
  exploit I.get_root_main; eauto.
  simpl; rewrite <- e.
  intros; eapply in_headers2; eauto.
assert (in_headers3: forall h l,
    PTree.get h (fst tab) = Some (h,l) -> In h headers).
  intros; eapply in_headers2; eauto.
assert (in_headers2: forall h, In h headers -> f_In h f).
  rewrite forallb_forall in Hf1.
  intros; exploit Hf1; eauto.
  unfold f_In, ptree_mem.
  destruct ((fn_code f)!h0); congruence.
case_eq (PTree.get f.(fn_entrypoint) (snd tab)); [intros; exact None|intros snd_root].
assert (scope_root: (fst tab)!(f.(fn_entrypoint)) = Some (h,l)).
  exploit I.get_root_main; eauto.
  rewrite <- e; auto.
assert (get_fst_of_my_header : forall n h l, PTree.get n (fst tab) = Some (h,l) ->
      PTree.get h (fst tab) = Some (h,l)).
  intros; eapply I.get_fst_of_my_header; eauto.
assert (parent_is_header : forall h p,
    PTree.get h (snd tab) = Some p -> In p headers).
  intros.
  exploit I.in_parent_main; eauto.
  intros (ll & H1 & l0 & H2).
  eauto.
assert (parent_tab:
    forall p n,
      (snd tab)!n = Some p ->
      (exists sc, (fst tab)!p = Some sc /\ exists l, In (L n l) (snd sc))).
  intros.
  exploit I.in_parent_main; eauto.
  intros (ll & H1 & l0 & H2).
  eauto.
case_eq (forallb (fun h0 => if peq h0 f.(fn_entrypoint) then true else
  negb (I.in_scope_test f.(fn_entrypoint) (I.scope_ tab (h,l) h0))) headers); intros Hf2; [|exact None].
assert (check_root: forall h0,
    In h0 headers -> h0=f.(fn_entrypoint) \/
    I.in_scope_test f.(fn_entrypoint) (I.scope_ tab (h,l) h0) = false).
  rewrite forallb_forall in Hf2.
  intros; exploit Hf2; eauto.
  destruct peq; auto; right.
  destruct I.in_scope_test; simpl in *; congruence.
case_eq (forallb (fun h0 => if peq h0 f.(fn_entrypoint) then true else
  match (snd tab)!h0 with
    | None => false
    | Some p => negb (I.in_scope_test p (I.scope_ tab (h,l) h0))
  end) headers); intros Hf3; [|exact None].
assert (headers_snd_some: forall h0,
    In h0 headers -> h0 = f.(fn_entrypoint) \/
    exists p, (snd tab)!h0 = Some p /\
      I.in_scope_test p (I.scope_ tab (h,l) h0) = false).
  rewrite forallb_forall in Hf3.
  intros; exploit Hf3; eauto.
  destruct peq; auto; right.
  case_eq ((snd tab)!h0); intros; rewrite H1 in *; try congruence.
  exists p; split; auto.
  destruct I.in_scope_test; simpl in *; congruence.
case_eq (forallb (fun h0 =>
   forallb (fun h' =>
    if peq h0 h' then true else
      if I.in_scope_test h0 (I.scope_ tab (h,l) h') then
        match (snd tab)!h0 with
          | None => true
          | Some p => I.in_scope_test p (I.scope_ tab (h,l) h')
        end
        else true) headers) headers); intros Hf4; [|exact None].
assert (parent_least_check: forall h0 h',
    In h0 headers -> In h' headers -> h0<>h' ->
    In h0 (nodes (I.scope_ tab (h,l) h')) ->
    match (snd tab)!h0 with
      | None => True
      | Some p => In p (nodes (I.scope_ tab (h,l) h'))
    end).
  intros.
  rewrite forallb_forall in Hf4.
  apply Hf4 in H; clear Hf4.
  rewrite forallb_forall in H.
  apply H in H0; clear H.
  destruct peq; try (elim H1; assumption).
  rewrite <- I.in_scope_test_correct in H2.
  rewrite H2 in *.
  case_eq ((snd tab)!h0); intros; rewrite H in *; auto.
  rewrite <- I.in_scope_test_correct; auto.
case_eq (forall_cfg_edge f
  (fun n n' =>
    if I.in_scope_test n (I.scope_ tab (h, l) n') then true
      else (peq n' (I.header_ (I.scope_ tab (h, l) n')))
        && (peq (I.header_ (I.parent_ tab (I.scope_ tab (h, l) n')))
                (I.header_ (I.scope_ tab (h, l) n))))); intros Hf5; [|exact None].
case_eq (forall_cfg_edge f
  (fun n s => nlt (PMap.get n order) (PMap.get s order)
    || peq s (I.header_ (I.scope_ tab (h,l) n)))); intros Hf6; [|exact None].
assert (succ_order: forall n s,
    succ_node f n s -> ((PMap.get n order) < (PMap.get s order))%N \/ s = I.header_ (I.scope_ tab (h,l) n)).
  intros.
  exploit forall_cfg_edge_correct; eauto; simpl.
  simpl.
  rewrite orb_true_iff; destruct 1.
  destruct nlt; auto.
  inv H0.
  destruct peq; auto.
  inv H0.
assert (
    enter_in_scope_at_header_only: forall n n',
      succ_node f n n' ->
      ~ In n (nodes (I.scope_ tab (h,l) n')) ->
       n' = I.header_ (I.scope_ tab (h,l) n') /\ I.parent_ tab (I.scope_ tab (h,l) n') = I.scope_ tab (h,l) n).
  intros.
  clear Hf6.
  exploit forall_cfg_edge_correct; eauto; clear Hf5; simpl.
  rewrite <- I.in_scope_test_correct in H0.
  destruct I.in_scope_test; try congruence.
  destruct (peq n' (I.header_ (I.scope_ tab (h, l) n'))); simpl; try congruence.
  destruct (peq (I.header_ (I.parent_ tab (I.scope_ tab (h, l) n')))
     (I.header_ (I.scope_ tab (h, l) n))); simpl; try congruence.
  intros _.
  split; auto.
  assert (I.scope_ tab (h,l) (I.header_ (I.parent_ tab (I.scope_ tab (h, l) n'))) =
          I.scope_ tab (h,l) (I.header_ (I.scope_ tab (h, l) n))) by congruence.
  erewrite I.scope_header in H1; eauto.
  erewrite I.scope_header in H1; eauto.
  eapply I.scope_in_elements; eauto.
  eapply I.parent_in_element; eauto.
  eapply I.scope_in_elements; eauto.
case_eq (forall_cfg_edge f
  (fun n n' => negb (peq n' f.(fn_entrypoint)))); intros Hf7; [|exact None].
apply Some.
apply (Build_family _
                      (I.scope_ tab (h,l))
                      I.header_
                      (I.parent_ tab)
                      (elements)).
  eapply I.in_scope; eauto.
  intros n sc H1 H2; eapply I.scope_least; eauto.
  unfold elements; intros; eapply I.header_f_In; eauto.
  unfold elements; intros; eapply I.scope_header; eauto.
  unfold elements; intros; eapply I.incl_in_parent; eauto.
  unfold elements; intros; eapply I.parent_least; eauto.
  unfold elements; intros; eapply I.sons_in_element; eauto.
  unfold elements; intros; eapply I.parent_in_element; eauto.
  unfold elements; intros; eapply I.scope_in_elements; eauto.
  assumption.
  intros; eapply I.cycle_at_not_header with (order:=fun n => PMap.get n order); eauto.
  intros; eapply I.cycle_at_header with (order:=fun n => PMap.get n order); eauto.
  unfold elements; intros; eapply I.in_scope_root; eauto.
  unfold elements; intros; eapply I.parent_strict_subset; eauto.
  red; intros.
  exploit forall_cfg_edge_correct; eauto.
  simpl.
  destruct peq; intuition.
Qed.

End ImplemScope.

Module Scope:SCOPE := ImplemScope.

Section transf_family.
  Variable f tf: function.
  Variable fsc: Scope.family f.
  Variable same_dom: forall n, f_In n f <-> f_In n tf.
  Variable same_cfg: forall n s, succ_node f n s <-> succ_node tf n s.
  Variable same_fn_entrypoint: f.(fn_entrypoint) = tf.(fn_entrypoint).


  Lemma same_path: forall rl n n',
    path tf n rl n' <-> path f n rl n'.
Proof.
    unfold path.
    induction rl; split; try constructor.
    intros T; inv T; constructor.
    rewrite same_dom; auto.
    intros T; inv T; constructor.
    rewrite <- same_dom; auto.
    inv H.
    rewrite <- same_cfg in *; rewrite IHrl in *; eauto.
    inv H.
    rewrite same_cfg in *; rewrite IHrl in *; eauto.
    inv H.
    rewrite same_cfg in *; rewrite IHrl in *; eauto.
    inv H.
    rewrite same_cfg in *; auto.
  Qed.

  Definition transf_family : Scope.family tf.
Proof.
  apply (Scope.Build_family _
                      (Scope.scope fsc)
                      (Scope.header fsc)
                      (Scope.parent fsc)
                      (Scope.elements fsc));
  intros;
    try rewrite <- same_dom in *;
      try rewrite <- same_cfg in *;
        try rewrite <- same_fn_entrypoint in *;
          try rewrite same_path in *;
            try (destruct fsc; eauto; fail).
  Defined.

End transf_family.


Notation "n ∈ sc" := (In n (Scope.nodes sc)) (at level 10).
Notation "sc1 ⊆ sc2" := (incl (Scope.nodes sc1) (Scope.nodes sc2)) (at level 10).
Definition In_dec (n:node) (sc:Scope.t): { n ∈ sc } + {~ n ∈ sc} :=
  List.In_dec peq n (Scope.nodes sc).

Hint Resolve Scope.in_scope Scope.scope_least.

Definition exited_scopes {f} (fsc:Scope.family f) (n n':node) : list node :=
  flat_map
    (fun s => if In_dec n s && negb (In_dec n' s) then Scope.nodes s else nil)
    (Scope.elements fsc).

Definition is_header {f} (fsc:Scope.family f) (n:node) : Prop :=
  f_In n f /\ Scope.header fsc (Scope.scope fsc n) = n.


Lemma incl_in : forall sc1 sc2 n,
  n ∈ sc1 -> sc1 ⊆ sc2 -> n ∈ sc2.
Proof.
  unfold incl; intros; eauto.
Qed.

Section properties.
Variable f: function.
Variable fsc: Scope.family f.
Notation header := (Scope.header fsc).
Notation scope := (Scope.scope fsc).
Notation parent := (Scope.parent fsc).
Notation elements := (Scope.elements fsc).

Lemma contains_header: forall sc, In sc elements -> header sc ∈ sc.
Proof.
  intros.
  exploit (Scope.in_scope _ fsc (header sc)).
  apply Scope.header_f_In; auto.
  rewrite (Scope.scope_header _ fsc sc); auto.
Qed.

Lemma in_scope_header_in_scope: forall n sc,
  In sc elements ->
  f_In n f ->
  (header (scope n)) ∈ sc -> n ∈ sc.
Proof.
  intros.
  apply incl_in with (Scope.scope fsc n); auto.
  generalize (Scope.scope_least f fsc _ _ H H1).
  rewrite Scope.scope_header; auto.
  apply Scope.scope_in_elements.
Qed.

Lemma enter_in_scope_at_header_only1: forall n n' sc,
  succ_node f n n' -> In sc elements ->
  ~ n ∈ sc -> n' ∈ sc -> n' = header sc.
Proof.
  intros.
  exploit (Scope.enter_in_scope_at_header_only f fsc); eauto.
  > intro; destruct H1.
    apply incl_in with (Scope.scope fsc n'); auto.
  > destruct 1.
    assert (HS:=Scope.scope_least f fsc n' sc H0 H2).
    destruct (Scope.parent_least _ fsc (scope n') sc); auto.
    > apply Scope.scope_in_elements.
    > congruence.
    > rewrite H4 in *.
      destruct H1.
      apply incl_in with (2:=H5).
      apply Scope.in_scope.
      apply succ_node_f_In with n'; auto.
Qed.

Lemma in_scope_get_scope_trans: forall n n' sc,
  In sc elements ->
  n ∈ (scope n') -> n' ∈ sc -> n ∈ sc.
Proof.
  intros.
  exploit Scope.scope_least; eauto.
Qed.


Lemma in_exited_trans:
  forall n n' n'',
    f_In n f ->
    n' ∈ (scope n) ->
    ~ n'' ∈ (scope n) ->
    In n (exited_scopes fsc n' n'').
Proof.
  intros; unfold exited_scopes.
  rewrite in_flat_map.
  exists (scope n); split; auto.
  > apply Scope.scope_in_elements.
  > destruct In_dec; simpl; intuition.
    destruct In_dec; simpl; intuition.
Qed.

End properties.

Generated by coq2html