Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.

Instead of assuming name uniqueness for all definitions in the program,
these variants only assume uniqueness for a particular name.

Use this approach to weaken the hypotheses for match_program
and transf_program_partial_augment.

1 files changed, 122 insertions, 70 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index db212685..30f03654 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -321,20 +321,47 @@ Proof.
   apply IHgl; auto. 
 Qed.
 
+Lemma add_globals_unique_preserves:
+  forall id gl ge,
+  (forall ge id1 g, P ge -> In (id1, g) gl -> id1 <> id -> P (add_global ge (id1, g))) ->
+  ~In id (map fst gl) -> P ge -> P (add_globals ge gl).
+Proof.
+  induction gl; simpl; intros. 
+  auto.
+  destruct a. apply IHgl; auto. 
+Qed.
+
+Lemma add_globals_unique_ensures:
+  forall gl1 id g gl2 ge,
+  (forall ge id1 g1, P ge -> In (id1, g1) gl2 -> id1 <> id -> P (add_global ge (id1, g1))) ->
+  (forall ge, P (add_global ge (id, g))) ->
+  ~In id (map fst gl2) -> P (add_globals ge (gl1 ++ (id, g) :: gl2)).
+Proof.
+  intros. rewrite add_globals_app. simpl. apply add_globals_unique_preserves with id; auto.
+Qed.
+
+Remark in_norepet_unique:
+  forall id g (gl: list (ident * globdef F V)),
+  In (id, g) gl -> list_norepet (map fst gl) ->
+  exists gl1 gl2, gl = gl1 ++ (id, g) :: gl2 /\ ~In id (map fst gl2).
+Proof.
+  induction gl as [|[id1 g1] gl]; simpl; intros.
+  contradiction.
+  inv H0. destruct H. 
+  inv H. exists nil, gl. auto. 
+  exploit IHgl; eauto. intros (gl1 & gl2 & X & Y). 
+  exists ((id1, g1) :: gl1), gl2; split; auto. rewrite X; auto. 
+Qed.
+
 Lemma add_globals_norepet_ensures:
   forall id g gl ge,
   (forall ge id1 g1, P ge -> In (id1, g1) gl -> id1 <> id -> P (add_global ge (id1, g1))) ->
   (forall ge, P (add_global ge (id, g))) ->
   In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl).
 Proof.
-  induction gl; simpl; intros.
-  contradiction.
-  inv H2. 
-  destruct H1. subst a. simpl in H5. 
-  apply add_globals_preserves; auto.
-  intros. apply H. auto. auto. red; intros; subst id0. elim H5. 
-  change id with (fst (id, g0)). apply List.in_map; auto. 
-  apply IHgl; auto. 
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
+  subst gl. apply add_globals_unique_ensures; auto. intros. eapply H; eauto. 
+  apply in_or_app; simpl; auto.
 Qed.
 
 End GLOBALENV_PRINCIPLES.
@@ -387,15 +414,14 @@ Proof.
   intros. unfold find_symbol; simpl. rewrite PTree.gss. econstructor; eauto.
 Qed.
 
-Theorem find_funct_ptr_exists:
-  forall p id f,
-  list_norepet (prog_defs_names p) ->
-  In (id, Gfun f) (prog_defs p) ->
+Theorem find_funct_ptr_exists_2:
+  forall p gl1 id f gl2,
+  prog_defs p = gl1 ++ (id, Gfun f) :: gl2 -> ~In id (map fst gl2) ->
   exists b,
      find_symbol (globalenv p) id = Some b
   /\ find_funct_ptr (globalenv p) b = Some f.
 Proof.
-  intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+  intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto.
 (* preserves *)
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
   destruct H1 as [b [A B]]. exists b; split.
@@ -408,15 +434,26 @@ Proof.
   exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
 Qed.
 
-Theorem find_var_exists:
-  forall p id v,
+Corollary find_funct_ptr_exists:
+  forall p id f,
   list_norepet (prog_defs_names p) ->
-  In (id, Gvar v) (prog_defs p) ->
+  In (id, Gfun f) (prog_defs p) ->
+  exists b,
+     find_symbol (globalenv p) id = Some b
+  /\ find_funct_ptr (globalenv p) b = Some f.
+Proof.
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
+  eapply find_funct_ptr_exists_2; eauto. 
+Qed.
+
+Theorem find_var_exists_2:
+  forall p gl1 id v gl2,
+  prog_defs p = gl1 ++ (id, Gvar v) :: gl2 -> ~In id (map fst gl2) ->
   exists b,
      find_symbol (globalenv p) id = Some b
   /\ find_var_info (globalenv p) b = Some v.
 Proof.
-  intros; unfold globalenv. eapply add_globals_norepet_ensures; eauto.
+  intros; unfold globalenv. rewrite H. eapply add_globals_unique_ensures; eauto.
 (* preserves *)
   intros. unfold find_symbol, find_var_info in *; simpl.
   destruct H1 as [b [A B]]. exists b; split.
@@ -428,6 +465,18 @@ Proof.
   exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
 Qed.
 
+Corollary find_var_exists:
+  forall p id v,
+  list_norepet (prog_defs_names p) ->
+  In (id, Gvar v) (prog_defs p) ->
+  exists b,
+     find_symbol (globalenv p) id = Some b
+  /\ find_var_info (globalenv p) b = Some v.
+Proof.
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
+  eapply find_var_exists_2; eauto. 
+Qed.
+
 Lemma find_symbol_inversion : forall p x b,
   find_symbol (globalenv p) x = Some b ->
   In x (prog_defs_names p).
@@ -1728,9 +1777,10 @@ Proof.
   destruct progmatch as (P & Q & R). rewrite R. auto. 
 Qed. 
 
-Hypothesis new_ids_fresh : 
-  forall s', find_symbol (globalenv p) s' <> None  -> 
-             ~In s' (map fst new_globs).
+Hypothesis new_ids_fresh:
+  forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False.
+Hypothesis new_ids_unique:
+  list_norepet (map fst new_globs).
 
 Lemma store_init_data_list_match:
   forall idl m b ofs m',
@@ -1743,7 +1793,7 @@ Proof.
           store_init_data (globalenv p') m b ofs a = Some m').
    destruct a; simpl; auto. rewrite find_symbol_match. auto.
    simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate.
-   apply new_ids_fresh. congruence.
+   red; intros. exploit find_symbol_inversion; eauto. 
   case_eq (store_init_data (globalenv p) m b ofs a); intros. 
     rewrite H1 in H. 
     pose proof (H0 _ H1). rewrite H2. auto. 
@@ -1780,6 +1830,32 @@ Proof.
   eapply alloc_globals_match; eauto. 
 Qed.
 
+Theorem find_new_funct_ptr_match:
+  forall id f, In (id, Gfun f) new_globs ->
+  exists b,
+     find_symbol (globalenv p') id = Some b
+  /\ find_funct_ptr (globalenv p') b = Some f.
+Proof.
+  intros.
+  destruct progmatch as [[tglob [P Q]] R].
+  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). 
+  rewrite S in Q. rewrite <- app_ass in Q. 
+  eapply find_funct_ptr_exists_2; eauto. 
+Qed.
+
+Theorem find_new_var_match:
+  forall id v, In (id, Gvar v) new_globs ->
+  exists b,
+     find_symbol (globalenv p') id = Some b
+  /\ find_var_info (globalenv p') b = Some v.
+Proof.
+  intros.
+  destruct progmatch as [[tglob [P Q]] R].
+  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). 
+  rewrite S in Q. rewrite <- app_ass in Q. 
+  eapply find_var_exists_2; eauto. 
+Qed.
+
 End MATCH_PROGRAMS.
 
 Section TRANSF_PROGRAM_AUGMENT.
@@ -1797,7 +1873,7 @@ Variable p': program B W.
 Hypothesis transf_OK:
   transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK p'.
 
-Remark prog_match:
+Let prog_match:
   match_program
     (fun fd tfd => transf_fun fd = OK tfd)
     (fun info tinfo => transf_var info = OK tinfo)
@@ -1818,27 +1894,6 @@ Proof.
   intros [tf [X Y]]. exists tf; auto.
 Qed.
 
-Theorem find_new_funct_ptr_exists: 
-  list_norepet (List.map fst new_globs) ->
-  forall id f, In (id, Gfun f) new_globs -> 
-  exists b, find_symbol (globalenv p') id = Some b
-         /\ find_funct_ptr (globalenv p') b = Some f.
-Proof.
-  intros. destruct prog_match as [[tglob [P Q]] R]. 
-  unfold globalenv. rewrite Q. rewrite add_globals_app. 
-  eapply add_globals_norepet_ensures; eauto.
-(* preserves *)
-  intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  destruct H1 as [b [X Y]]. exists b; split.
-  rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. rewrite PTree.gso. auto.
-  apply Plt_ne. eapply genv_funs_range; eauto.
-  auto. 
-(* ensures *)
-  intros. unfold find_symbol, find_funct_ptr in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
-Qed.
-
 Theorem find_funct_ptr_rev_transf_augment:
   forall (b: block) (tf: B),
   find_funct_ptr (globalenv p') b = Some tf ->
@@ -1848,7 +1903,7 @@ Theorem find_funct_ptr_rev_transf_augment:
    In (Gfun tf) (map snd new_globs).
 Proof.
   intros. 
-  exploit find_funct_ptr_rev_match; eauto. eexact prog_match; eauto. auto. 
+  exploit find_funct_ptr_rev_match; eauto.
 Qed.
 
 Theorem find_funct_transf_augment:
@@ -1883,26 +1938,6 @@ Proof.
   rewrite H0; simpl. auto.
 Qed.
 
-Theorem find_new_var_exists:
-  list_norepet (List.map fst new_globs) ->
-  forall id gv, In (id, Gvar gv) new_globs -> 
-  exists b, find_symbol (globalenv p') id = Some b
-         /\ find_var_info (globalenv p') b = Some gv.
-Proof.
-  intros. destruct prog_match as [[tglob [P Q]] R]. 
-  unfold globalenv. rewrite Q. rewrite add_globals_app. 
-  eapply add_globals_norepet_ensures; eauto.
-(* preserves *)
-  intros. unfold find_symbol, find_var_info in *; simpl.
-  destruct H1 as [b [X Y]]. exists b; split.
-  rewrite PTree.gso; auto.
-  destruct g1 as [f1 | v1]. auto. rewrite PTree.gso. auto.
-  red; intros; subst b. eelim Plt_strict. eapply genv_vars_range; eauto.
-(* ensures *)
-  intros. unfold find_symbol, find_var_info in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
-Qed.
-
 Theorem find_var_info_rev_transf_augment:
   forall (b: block) (v': globvar W),
   find_var_info (globalenv p') b = Some v' ->
@@ -1934,9 +1969,12 @@ Proof.
   intros. eapply public_symbol_match. eexact prog_match. auto.
 Qed.
 
+Hypothesis new_ids_fresh:
+  forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False.
+Hypothesis new_ids_unique:
+  list_norepet (map fst new_globs).
+
 Theorem init_mem_transf_augment: 
-   (forall s', find_symbol (globalenv p) s' <> None -> 
-     ~ In s' (map fst new_globs)) ->
    forall m, init_mem p = Some m -> 
    init_mem p' = alloc_globals (globalenv p') m new_globs.
 Proof.
@@ -1944,18 +1982,32 @@ Proof.
 Qed.
  
 Theorem init_mem_inject_transf_augment:
-   (forall s', find_symbol (globalenv p) s' <> None -> 
-     ~ In s' (map fst new_globs)) ->
   forall m, init_mem p = Some m ->
   forall m', init_mem p' = Some m' -> 
   Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'.
 Proof.
   intros. 
-  pose proof (initmem_inject p H0). 
-  erewrite init_mem_transf_augment in H1; eauto. 
+  pose proof (initmem_inject p H). 
+  erewrite init_mem_transf_augment in H0; eauto. 
   eapply alloc_globals_augment; eauto. apply Ple_refl. 
 Qed.
 
+Theorem find_new_funct_ptr_exists: 
+  forall id f, In (id, Gfun f) new_globs -> 
+  exists b, find_symbol (globalenv p') id = Some b
+         /\ find_funct_ptr (globalenv p') b = Some f.
+Proof.
+  intros. eapply find_new_funct_ptr_match; eauto. 
+Qed.
+
+Theorem find_new_var_exists:
+  forall id gv, In (id, Gvar gv) new_globs -> 
+  exists b, find_symbol (globalenv p') id = Some b
+         /\ find_var_info (globalenv p') b = Some gv.
+Proof.
+  intros. eapply find_new_var_match; eauto. 
+Qed.
+
 End TRANSF_PROGRAM_AUGMENT.
 
 Section TRANSF_PROGRAM_PARTIAL2.