Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Natmap.
Require Import FMaps.
Require Import EqNat.
Require Import FMapFacts.
Require Import Natmap.
Require Import Classical.
Require Import base2.
Require Import Max.
Require Import lj_definitions.
Require Import lj_infrastructure.

Section Progress.

Lemma new_var_progress : forall (p : P) (g : G) (l : L) (h : H) (v' : var) (c : cl) (ss : list s),
  wf_config p g (config_normal l h (s_new v' c :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_new v' c :: ss)) p config'.
Proof.
  intros p g l h v' c ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List WFStmt_List'; subst.
  destruct (ex_fresh_oid h).
  exists (config_normal (XMap.add (x_var v') (v_oid x) l) (NatMap.add x (c, init_field_map (fields p c)) h) ss).
  apply (new (fields p c)); auto.
Qed.

Lemma var_assign_progress : forall (p : P) (g : G) (l : L) (h : H) (v' : var) (x' : x) (ss : list s),
  wf_config p g (config_normal l h (s_ass v' x' :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_ass v' x' :: ss)) p config'.
Proof.
  intros p g l h v' c ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List']; clear WFStmt_List WFStmt_List'; subst.
  generalize (wf_assign_lookupl _ _ _ _ _ _ WFStmt WFStack) as H10; intros H10; destruct H10.
  exists (config_normal (XMap.add (x_var v') (x) l) h ss).
  apply var_assign; auto.
Qed.

Lemma field_read_progress : forall (p : P) (g : G) (l : L) (h : H) (v' : var) (x' : x) (f' : f) (ss : list s),  
  wf_config p g (config_normal l h (s_read v' x' f' :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_read v' x' f' :: ss)) p config'.
Proof.
  intros p g l h v' x' f' ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List']; clear WFStmt_List WFStmt_List'; subst.
  generalize (wf_fread_lookuplh _ _ _ _ _ _ _ WFStmt WFStack) as H; intros H; destruct H as [v'' [H0 H1]]. 
  destruct v''.
  (*** Field Read NPE ***)
  exists (config_npe l h).
  apply field_read_npe; exact H0.
  (*** Field Read v_oid ***)
  generalize (H1 o (refl_equal _)); clear H1; intros H1; destruct H1 as [clm [H1 H3]].
  inversion WFStmt as [ |  | p' g' v'' x'' f'' cl' ty' WF_stmt1 WF_stmt2 WF_stmt3 | | | | ];
    inversion WFHP as [null null' WF_HP1]; subst.
  destruct (WF_HP1 _ (NatMap_find_mem _ _ _ H1)) as [cl'' [wf_HP1 [wf_HP2 wf_HP3]]]; clear WF_HP1.
  rewrite H1 in wf_HP1; inversion wf_HP1; subst; clear wf_HP1.
  rewrite WF_stmt1 in H3.
  inversion H3 as [p' tyopt' tyopt'' ty'' ty''' tyeq1 tyeq2 STY]; inversion tyeq1; inversion tyeq2; subst; clear tyeq1 tyeq2.
  destruct (wf_HP3 _ (subtype_fields _ _ _ _ _ _ (refl_equal _) (refl_equal _) STY WFProg (proj1 (ftype_in_fields _ _ _) (None_neq_Some _ _ _ WF_stmt2)))) as [ty'' [wf_HP4 wf_HP5]].
  rewrite H1 in wf_HP5.
  inversion wf_HP5; subst.
  exists (config_normal (XMap.add (x_var v') v_null l) h ss).
  apply (field_read _ h v' _ f' ss p v_null o H0).
  rewrite H1; rewrite H; apply refl_equal.
  exists (config_normal (XMap.add (x_var v') (v_oid oid5) l) h ss).
  apply (field_read _ h v' _ f' ss p (v_oid oid5) o H0).
  rewrite H1; rewrite H; apply refl_equal.
Qed.

Lemma field_write_progress : forall (p : P) (g : G) (l : L) (h : H) (x' y: x) (f' : f) (ss : list s),  
  wf_config p g (config_normal l h (s_write x' f' y :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_write  x' f' y :: ss)) p config'.
Proof.
  intros p g l h x' y' f' ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List']; clear WFStmt_List WFStmt_List'; subst.
  destruct (wf_fwrite_lookupl _ _ _ _ _ _ _ WFStmt WFStack) as [v' [[WF_Write1 WF_Write2][v'' WF_Write3 ]]].
  destruct v'.
  exists (config_npe l h).
  apply field_write_npe; exact WF_Write1.
  destruct (WF_Write2 _ (refl_equal _)) as [clm WF_Write4].
  exists (config_normal l (match (NatMap.find o h) with 
                             None => h 
			     | Some tyfs => NatMap.add o (fst tyfs, (NatMap.add f' v'' (snd tyfs))) h
			   end) ss).
  apply field_write; auto.
Qed.

Lemma method_call_progress : forall (p : P) (g : G) (l : L) (h : H) (v' : var) (x': x) (m' : m) (param : list x) (ss : list s),  
  wf_config p g (config_normal l h (s_call v' x' m' param :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_call v' x' m' param :: ss)) p config'.
Proof.
  intros p g l h v' x' m' param ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List']; clear WFStmt_List WFStmt_List'; subst.
  destruct (ex_fresh_lookup_list' l (S (length param))) as [fresh_vars [Fresh_Len [Fresh_Distinct Fresh_map]]].
  destruct (wf_tl_valid_lookup _ _ _ _ _ _ _ _ WFStmt WFStack) as [list_v [Valid_list_v Length_v]].
  inversion WFStmt as [ | | | | yty_list p' g' v'' x'' m'' cl'' ty'' WF_stmt1 WF_stmt2 WF_stmt3 WF_stmt4 | | ];
    inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst.
  destruct (WF_Stk1 _ (XMap_find_mem _ _ _ WF_stmt1)) as [ty''' [WF_Stck2 [WF_Stck3 WF_Stck4]]].
  inversion WF_Stck4 as [p1 h1 tyopt1 ty1 HNPE1 | p1 h1 o' tyopt' STY]; subst.
  (*** Method Call NPE ***)
  exists (config_npe l h).
  apply mcall_npe; auto.
  (***Valid Method Call ***)
  rename H2 into XMap_Find.
  inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; 
    inversion STY2; subst; clear STY STY2.
  rewrite WF_Stck2 in WF_stmt1; inversion WF_stmt1; subst; clear WF_stmt1.
  destruct ty1; generalize (sty_mtype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _) STY_One WF_stmt2 WFProg); 
    intro MType_m'.
  destruct (mtype_find_menv _ _ _ _ MType_m') as [md' Find_m'].
  destruct md'; generalize (find_menv_mtype_length _ _ _ _ _ _ _ Find_m' MType_m'); intro L0_Len.
  rewrite <- length_map_r in L0_Len.
  destruct m as [ss'' y']; destruct fresh_vars as [ | v'' fresh_vars]; simpl in Fresh_Len; 
    inversion Fresh_Len as [Fresh_Len'].
  caseEq (NatMap.find (elt:=cl * NatMap.t v) o' h); try (intros find_o'; rewrite find_o' in STY1; discriminate).
  intros l'' find_o'; rewrite find_o' in STY1.
  exists (config_normal (XMap.add (x_var v'') (v_oid o') (fold_right (fun (yp:var*lj_definitions.v) m=> XMap.add (x_var (fst yp)) (snd yp) m) l (combine fresh_vars list_v)))
    h (app (unmake_list_s (tr_Ss (XMap.add x_this (x_var v'') (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj_definitions.x) (combine l0 fresh_vars))) (make_list_s ss'')))
      ((s_ass v' (tr_x (XMap.add x_this (x_var v'') (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj_definitions.x) (combine l0 fresh_vars))) y')) :: ss))).
  rewrite  <- (map_fst_fst_fst  (map (fun y => fst y) yty_list) l0 fresh_vars list_v).
  apply (mcall (build_big_list (map (fun y : lj_definitions.x * ty => fst y) yty_list) l0 fresh_vars list_v) 
    l h v' x' m' ss p  
    (XMap.add (x_var v'') (v_oid o') (fold_right (fun  (yp:var*lj_definitions.v) m=> XMap.add (x_var (fst yp)) 
      (snd yp) m) l (combine fresh_vars list_v))) 
    (XMap.add x_this (x_var v'') (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m)
      (XMap.empty lj_definitions.x) (combine l0 fresh_vars))) 
    ss'' (tr_x (XMap.add x_this (x_var v'') (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp))
      (x_var (snd yp)) m) (XMap.empty lj_definitions.x) (combine l0 fresh_vars))) y') v'' y' o' l''
    (sym_eq XMap_Find)); auto.
  inversion STY1; subst; rewrite map_snd_fst_fst; auto; rewrite length_build_big_list; congruence.
  rewrite map_snd_fst; simpl in Fresh_Distinct; destruct Fresh_Distinct as [FD1 FD2].
  exact (distinct_map_xvar _ FD2).
  rewrite length_build_big_list; congruence.
  rewrite map_snd_fst.
  intros x'' In_x''; destruct (In_map_xvar' _ _ In_x'') as [v3 [In_x'1 In_x'2]]; subst.
  apply Fresh_map; simpl; auto.
  rewrite length_build_big_list; congruence.
  apply Fresh_map; simpl; auto.
  rewrite map_snd_fst'.
  rewrite map_var_var_id; simpl in Fresh_Distinct; destruct Fresh_Distinct as [FD1 FD2]; exact FD1.
  rewrite length_build_big_list; congruence.
  rewrite map_fffst_snd_pair; auto; try rewrite length_build_big_list; congruence.
  rewrite map_snd_fst_pair; auto; try rewrite length_build_big_list; congruence.
  rewrite map_snd_fst_fst_pair; auto; try rewrite length_build_big_list; congruence.
  rewrite length_build_big_list; congruence.
Qed.

Lemma if_progress : forall (p : P) (g : G) (l : L) (h : H) (x' y': x) (s1 s2 : s) (ss: list s),  
  wf_config p g (config_normal l h (s_if x' y' s1 s2 :: ss)) ->
  exists config' : config,
    reduce (config_normal l h (s_if x' y' s1 s2 :: ss)) p config'.
Proof.
  intros p g l h x' y' s1 s2 ss WFConfig.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List']; clear WFStmt_List WFStmt_List'; subst.
  inversion WFStmt as [ | | | | | p' g' x'' y'' s1' s2' [WF_Ifl | WF_Ifr] WF_s1 WF_s2 | ]; subst.
  (*** x' <: y' ***)
  inversion WF_Ifl as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; 
    inversion STY2; subst; clear WF_Ifl STY2; rename H0 into STY2.
  inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst.
  destruct (WF_Stk1 _ (XMap_find_mem _ _ _ STY1)) as [ty' [WF_s11 [WF_s12 WF_s13]]].
  destruct (WF_Stk1 _ (XMap_find_mem _ _ _ STY2)) as [ty'' [WF_s21 [WF_s22 WF_s23]]].
  inversion WF_s13 as [p' h' tyopt' ty3 tyopt_eq1 | p' h' o' ty3 tyopt_eq1]; subst;
    inversion WF_s23 as [p' h' tyopt'' ty4 tyopt_eq2 | p' h' o'' ty4 tyopt_eq2]; subst.
  exists (config_normal l h (s1 :: ss)).
  apply (if_true _ h _ _ s1 s2 ss p _ _ (sym_eq H2) (sym_eq H3) (refl_equal _)).
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H2) (sym_eq H3)); congruence.
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H2) (sym_eq H3)); congruence.
  case (eq_nat_dec o' o''); intros.
  exists (config_normal l h (s1 :: ss)).
  apply (if_true _ h _ _ s1 s2 ss p _ _ (sym_eq H2) (sym_eq H3)); congruence.
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H2) (sym_eq H3)); congruence.
  (*** y' <: x' ***)
  inversion WF_Ifr as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; 
    inversion STY2; subst; clear WF_Ifr STY2; rename H0 into STY2.
  inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst.
  destruct (WF_Stk1 _ (XMap_find_mem _ _ _ STY1)) as [ty' [WF_s11 [WF_s12 WF_s13]]].
  destruct (WF_Stk1 _ (XMap_find_mem _ _ _ STY2)) as [ty'' [WF_s21 [WF_s22 WF_s23]]].
  inversion WF_s13 as [p' h' tyopt' ty3 tyopt_eq1 | p' h' o' ty3 tyopt_eq1]; subst;
    inversion WF_s23 as [p' h' tyopt'' ty4 tyopt_eq2 | p' h' o'' ty4 tyopt_eq2]; subst.
  exists (config_normal l h (s1 :: ss)).
  apply (if_true _ h _ _ s1 s2 ss p _ _ (sym_eq H3) (sym_eq H2) (refl_equal _)).
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H3) (sym_eq H2)); congruence.
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H3) (sym_eq H2)); congruence.
  case (eq_nat_dec o' o''); intros.
  exists (config_normal l h (s1 :: ss)).
  apply (if_true _ h _ _ s1 s2 ss p _ _ (sym_eq H3) (sym_eq H2)); congruence.
  exists (config_normal l h (s2 :: ss)).
  apply (if_false _ h _ _ s1 s2 ss p _ _ (sym_eq H3) (sym_eq H2)); congruence.
Qed.

Theorem progress_result : progress.
Proof.
  unfold progress; intros p g l h ss ssNonEmpty WFConfig.
  destruct ss.
  elimtype False; unfold not in ssNonEmpty; tauto.
  clear ssNonEmpty.
  destruct s.
  (*** New Var Assign ***)
  eapply new_var_progress; eauto.
  (*** Var Assign ***)
  eapply var_assign_progress; eauto.
  (*** Field Read ***)
  eapply field_read_progress; eauto.
  (*** Field Write ***)
  eapply field_write_progress; eauto.
  (*** Method Call ***)
  eapply method_call_progress; eauto.
  (*** If ***)
  eapply if_progress; eauto.
  (*** Block ***)
  simpl.
  exists (config_normal l h (app (unmake_list_s l0) ss)).
  apply block.
Qed.

End Progress.

Section Preservation.

Lemma add_new_wf_heap : forall (p : P) (g : G) (h : H) (var' : var) (cl' : cl) (o' : oid),
  wf_hp p h ->  NatMap.mem (elt:=cl * NatMap.t v) o' h = false -> wf_stmt p g (s_new var' cl') ->
  wf_hp p (NatMap.add o' (cl', init_field_map (fields p cl')) h).
Proof.
  intros until o'; intros WFHP FreshOid WFStmt.
  apply wf_heap; intros o'' In_HP_o''.
  case (eq_nat_dec o' o''); intros; subst.
  exists cl'; rewrite add_Natmap_find_eq; repeat split.
  inversion WFStmt as [ p' g' var'' cl'' STY | | | | | | ]; subst.
  destruct cl'.
  inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; rewrite STY2 in STY;
    destruct ty2; destruct (sty_option_In_p _ _ _ STY) as [cl' [fds' [mds' In_d]]];
      apply (In_names _ _ _ _ _ In_d).
  apply cl_object_in_names.
  intros f' In_f_fds.
  generalize (proj2 (ftype_in_fields _ _ _) In_f_fds); intro FType_f'.
  destruct (ftype p cl' f') as [ty' | ].
  clear FType_f'; exists ty'; split; auto.
  simpl; rewrite find_init_fields_null.
  eapply wf_null; eauto.
  exact In_f_fds.
  contradiction FType_f'; reflexivity.
  destruct (NatMapsTo_mem2 _ _ In_HP_o'') as [clm MapsTo_clm]; destruct clm as [cl'' ty''].
  generalize (NatMap.find_1 MapsTo_clm); intro NatMapFind; 
    rewrite add_Natmap_find_neq in NatMapFind; auto.
  inversion WFHP as [null null' WF_HP1]; subst;
    destruct (WF_HP1 _ (NatMapsTo_mem _ _ _ (NatMap.find_2 NatMapFind))) as
      [cl''' [NatMapFind' [WFType_cl''' CL_Fields]]].
  inversion WFType_cl'''; subst;
    rewrite NatMapFind in NatMapFind'; simpl in NatMapFind';
      inversion NatMapFind'; subst; clear NatMapFind'.
  exists cl'''; rewrite (NatMap.find_1 MapsTo_clm); repeat split.
  exact H1.
  intros f' In_f'; destruct (CL_Fields f' In_f') as [ty''' [FType_ty''' WF_obj_o'']];
    rewrite NatMapFind in WF_obj_o''; simpl in WF_obj_o''.
  exists ty'''; split; auto.
  inversion WF_obj_o'' as [p' h' tyopt' ty' null' null'' null''' Find_VNull | 
    p' h' o''' ty' STY Find_o''' foo Find_o]; subst.
  inversion null'; subst; clear null'; simpl; rewrite <- Find_VNull; eapply wf_null; eauto.
  destruct (eq_nat_dec o' o''') as [eq_o'_o''' | neq_o'_o''']; subst; 
    simpl; rewrite <- Find_o; eapply wf_object.
  caseEq (NatMap.find (elt:=cl * NatMap.t v) o''' h).
  intros p0 H; rewrite (NatMapsTo_mem _ _ _ (NatMap.find_2 H)) in FreshOid; discriminate.
  intros H; rewrite H in STY; inversion STY; discriminate.
  rewrite add_Natmap_find_neq; auto; apply STY.
Qed.

Lemma add_new_wf_stack : forall (p : P) (g : G) (l : L) (h : H) (var' : var) (cl' : cl) (o' : oid),
  wf_hp p h -> wf_stck p g h l -> NatMap.mem (elt:=cl * NatMap.t v) o' h = false ->
  wf_stmt p g (s_new var' cl') ->
  wf_stck p g (NatMap.add o' (cl', init_field_map (fields p cl')) h)
  (XMap.add (x_var var') (v_oid o') l).
Proof.
  intros until o'; intros WFHP WFStack FreshOid WFStmt.
  apply wf_stack; intros y XMap_y; inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst;
    destruct (WF_Stk1 y XMap_y) as [ty' [WF_Stk1' [WF_Stk2 WF_Stk3]]]; clear WF_Stk1.
  exists ty'; repeat split; auto.
  destruct y as [var'' | ].
  destruct (eq_nat_dec var'' var') as [var_eq | var_neq].
  subst; rewrite add_Xmap_find_eq; apply wf_object; rewrite add_Natmap_find_eq; 
    simpl; inversion WFStmt as [ p' g' var'' cl'' STY | | | | | | ]; congruence.
  rewrite add_Xmap_find_neq.
  inversion WF_Stk3 as [p' h' tyopt' ty'' null' null'' null''' XMap_vnull | 
    p' h' o'' tyopt' STY null' null'' XMap_o'].
  inversion null'; subst; clear null'.
  eapply wf_null; eauto.
  subst.
  apply wf_object.
  destruct (eq_nat_dec o' o'') as [eq_o'_o'' | neq_o'_o'']; subst.
  caseEq (NatMap.find (elt:=cl * NatMap.t v) o'' h).
  intros p0 H; rewrite (NatMapsTo_mem _ _ _ (NatMap.find_2 H)) in FreshOid; discriminate.
  intros H; rewrite H in STY; inversion STY; discriminate.
  rewrite add_Natmap_find_neq; auto; apply STY.
  congruence.
  rewrite add_Xmap_find_neq.
  inversion WF_Stk3 as [p' h' tyopt' ty'' null' null'' null''' XMap_vnull | 
    p' h' o'' tyopt' STY null' null'' XMap_o'].
  inversion null'; subst; clear null'.
  eapply wf_null; eauto.
  subst.
  apply wf_object.
  destruct (eq_nat_dec o' o'') as [eq_o'_o'' | neq_o'_o'']; subst.
  caseEq (NatMap.find (elt:=cl * NatMap.t v) o'' h).
  intros p0 H; rewrite (NatMapsTo_mem _ _ _ (NatMap.find_2 H)) in FreshOid; discriminate.
  intros H; rewrite H in STY; inversion STY; discriminate.
  rewrite add_Natmap_find_neq; auto; apply STY.
  congruence.
Qed. 

Lemma new_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (var' : var) (cl' : cl), 
   wf_config p g (config_normal l h (s_new var' cl' :: ss)) ->
   reduce (config_normal l h (s_new var' cl' :: ss)) p config' ->
   exists g' : G, wf_config p g' config' /\
     (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros p g l h ss config' var' cl' WFConfig ReduceCFG;
    inversion ReduceCFG as [| | | f_list l' h'' var'' cl'' ss' p' o' h' FreshOid | | | | | | |]; 
      subst; clear ReduceCFG.
  exists g; split; auto.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  apply wf_all; auto.
  eapply add_new_wf_heap; eauto.
  eapply add_new_wf_stack; eauto.
Qed.

Lemma var_assign_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (var' : var) (x' : x), 
   wf_config p g (config_normal l h (s_ass var' x' :: ss)) ->
   reduce (config_normal l h (s_ass var' x' :: ss)) p config' ->
   exists g' : G, wf_config p g' config' /\
     (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros p g l h ss config' var' x' WFConfig ReduceCFG;
    inversion ReduceCFG as [| | | | f_list l' h'' var'' cl'' ss' v' XFind_x' | | | | | |];
      subst; clear ReduceCFG.
  exists g; split; auto.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  apply wf_all; auto.
  apply wf_stack; intros y XMap_y; inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst;
    destruct (WF_Stk1 y XMap_y) as [ty' [WF_Stk1' [WF_Stk2 WF_Stk3]]].
  inversion WFStmt as [ | p' g' var'' x'' STY | | | | | ]; subst.
  exists ty'; repeat split; auto.
  destruct y as [var'' | ].
  destruct (eq_nat_dec var'' var') as [var_eq | var_neq].
  subst; rewrite add_Xmap_find_eq.
  inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; rewrite STY2 in STY.
  destruct (WF_Stk1 x' (MapsTo_mem _ _ _(XMap.find_2 STY1))) as 
    [ty'' [WF_Stk1'' [WF_Stk2' WF_Stk3']]]; rewrite XFind_x' in WF_Stk3'.
  rewrite STY2 in WF_Stk1'; inversion WF_Stk1'; subst; clear WF_Stk1';
    rewrite STY1 in WF_Stk1''; inversion WF_Stk1''; subst; clear WF_Stk1'';
      rewrite STY1 in STY.
  destruct v'.
  eapply wf_null; eauto.
  apply wf_object.
  inversion WF_Stk3' as [| p' h' o'' tyopt' STY' null' null'' XMap_o']; subst.
  destruct (NatMap.find (elt:=cl * NatMap.t v) o h).
  inversion STY'; inversion H; inversion H0; subst;
    eapply sty_opt; eauto;
      eapply sty_transitive; eauto.
  inversion STY'; discriminate.
  rewrite add_Xmap_find_neq; congruence.
  rewrite add_Xmap_find_neq; congruence.
Qed.

Lemma field_read_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (var' : var) (x' : x) (f' : f),  
   wf_config p g (config_normal l h (s_read var' x' f' :: ss)) ->
   reduce (config_normal l h (s_read var' x' f' :: ss)) p config' ->
   exists g' : G, wf_config p g' config' /\
     (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros p g l h ss config' var' x' f' WFConfig ReduceCFG;
    inversion ReduceCFG as [| | | | | f_list l' h'' var'' cl'' ss' v'' v' o' LFind_x' HFind_o' | | | | |];
      subst; clear ReduceCFG.
  exists g; split; auto; apply wf_all_npe.  
  exists g; split; auto.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  apply wf_all; auto; clear WFStmt_List'.
  apply wf_stack; intros y XMap_y; inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst;
    destruct (WF_Stk1 y XMap_y) as [ty' [WF_Stk1' [WF_Stk2 WF_Stk3]]].
  inversion WFStmt as [ | | p' g' var'' x'' f'' cl'' ty'' XFind_x' FType_f' STY | | | | ]; subst.
  exists ty'; repeat split; auto.
  destruct y as [var'' | ].
  destruct (eq_nat_dec var'' var') as [var_eq | var_neq].
  subst; rewrite add_Xmap_find_eq.
  inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One]; subst; rewrite STY2 in STY;
    inversion STY1; subst; clear STY1 STY.
  destruct v'.
  eapply wf_null; eauto.
  apply wf_object.
  caseEq (NatMap.find (elt:=cl * NatMap.t v) o' h).
  intros clm Find_o'; rewrite Find_o' in HFind_o'; inversion HFind_o' as [Find_f']; subst.
  destruct (WF_Stk1 x' (MapsTo_mem _ _ _(XMap.find_2 XFind_x'))) as 
    [ty'' [WF_Stk1'' [WF_Stk2' WF_Stk3']]]; rewrite LFind_x' in WF_Stk3';
      rewrite XFind_x' in WF_Stk1''; inversion WF_Stk1''; subst; clear WF_Stk1''.
  inversion WF_Stk3' as [| p' h' o'' tyopt' STY' null' null'' XMap_o']; subst;
    rewrite Find_o' in STY'.
  inversion STY' as [p' tyopt' tyopt'' ty'1 ty'2 STY'1 STY'2 STY'_One]; subst; inversion
    STY'1; inversion STY'2; subst; clear STY'1 STY'2.
  inversion WFHP as [null null' WF_HP1]; subst.
  destruct (WF_HP1 _ (NatMap_find_mem _ _ _ Find_o')) as [cl''' [wf_HP1 [wf_HP2 wf_HP3]]]; clear WF_HP1;
    rewrite Find_o' in wf_HP1; destruct clm; simpl in wf_HP1; inversion wf_HP1; subst; 
      clear wf_HP1 Find_f'; simpl in *|-*.
  destruct (wf_HP3 _ (subtype_fields _ _ _ _ _ _ (refl_equal _) (refl_equal _) STY'_One WFProg 
  (proj1 (ftype_in_fields _ _ _) (None_neq_Some _ _ _ FType_f')))) as [ty'' [FType_ty'' WF_Obj_ty'']];
  rewrite Find_o' in WF_Obj_ty''; simpl in WF_Obj_ty''; rewrite HFind_o' in WF_Obj_ty''.
  rewrite WF_Stk1' in STY2; inversion STY2; subst; clear STY2.
  inversion WF_Obj_ty''; inversion H2; subst; inversion H6; subst;
    destruct (NatMap.find (elt:=cl * NatMap.t v) o h).
  rewrite (sty_ftype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _) STY'_One WFProg FType_f') in FType_ty''; 
    inversion FType_ty''; subst.
  inversion H2; subst; inversion H; inversion H0; subst.
  eapply sty_opt; eauto; eapply sty_transitive; eauto.
  discriminate.
  intros Find_None; rewrite Find_None in HFind_o'; discriminate.
  rewrite add_Xmap_find_neq; congruence.
  rewrite add_Xmap_find_neq; congruence.
Qed.

Lemma wf_hp_field_write : forall (p : P) (g : G) (l : L) (h : H) (y : x) (f' : f)
  (o' : oid) (v' : v) (ty1 ty2: ty) (cl3 cl'': cl) (m'' : NatMap.t v),
  wf_prog p -> wf_hp p h -> wf_stck p g h l -> XMap.find (elt:=v) y l = Some v' -> 
  XMap.find (elt:=ty) y g = Some ty1 -> NatMap.find (elt:=cl * NatMap.t v) o' h = Some (cl3, m'') -> 
   sty_one p (ty_def cl3) (ty_def cl'') -> ftype p cl'' f' = Some ty2 -> XMap.find (elt:=ty) y g = Some ty1 ->
   sty_one p ty1 ty2 -> 
   wf_hp p (NatMap.add o' (cl3, NatMap.add f' v' m'') h).
Proof.
  intros until m''; intros WFProg WFHP WFStack LFind_y GFind_y HFind_o' STY_cl3_cl'' FType_f' STY1 STY_One.
  apply wf_heap; intros o'' HFind_o''; destruct (eq_nat_dec o' o'') as [Eq_o | Neq_o].
  subst; exists cl3; repeat split.
  rewrite add_Natmap_find_eq; simpl; reflexivity.
  destruct cl3.
  destruct (sty_option_In_p _ _ _ (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) STY_cl3_cl'')) as [cl3 [fds' [mds' In_p]]];
    apply (In_p_In_names _ _ _ _ _ In_p).
  apply cl_object_in_names.
  intros f'' In_f''.
  rewrite add_Natmap_find_eq; simpl.
  destruct (eq_nat_dec f' f'') as [Eq_f | Neq_f].
  subst; exists ty2; split.
  destruct ty2; eapply sty_ftype; eauto.
  rewrite add_Natmap_find_eq; simpl; destruct v'.
  eapply wf_null; eauto.
  destruct (In_L_In_H _ _ _ _ _ _ _ WFStack WFHP LFind_y STY1) as [cl4 [m''' [HFind_o STY'']]].
  apply wf_object; destruct (eq_nat_dec o'' o) as [Eq_o | Neq_o].
  subst; rewrite add_Natmap_find_eq; simpl;
    rewrite HFind_o in HFind_o'; inversion HFind_o'; subst; clear HFind_o'.
  eapply sty_opt; eauto; eapply sty_transitive; eauto.
  subst; rewrite add_Natmap_find_neq; auto;
    rewrite HFind_o; simpl; eapply sty_opt; eauto; eapply sty_transitive; eauto.
  rewrite add_Natmap_find_neq; auto; simpl;
    destruct (Some_neq_None ty _ (proj2 (ftype_in_fields _ _ _) In_f'')) as [ty' Ftype_f''];
      exists ty'; split; auto.
  destruct (In_H_In_fs _ _ _ _ _ _ _ HFind_o' WFHP Ftype_f'') as [v'' [MFind_f' Sty_ty']];
    rewrite MFind_f'; destruct v''.
  eapply wf_null; eauto.
  apply wf_object; destruct (eq_nat_dec o'' o) as [Eq_o | Neq_o].
  subst; rewrite add_Natmap_find_eq; simpl.
  eapply sty_opt; eauto.
  subst; rewrite add_Natmap_find_neq; auto.
  inversion WFHP as [null null' WF_HP1]; subst.
  destruct (WF_HP1 _ (NatMap_find_mem _ _ _ HFind_o')) as [cl''' [wf_HP1 [wf_HP2 wf_HP3]]]; clear WF_HP1;
    rewrite HFind_o' in wf_HP1; simpl in wf_HP1; inversion wf_HP1; subst; clear wf_HP1; simpl in *|-*.
  destruct (wf_HP3 _ (proj1 (ftype_in_fields _ _ _) (None_neq_Some _ _ _ Ftype_f''))) as [ty'' [FType_ty'' WF_Obj]];
    rewrite HFind_o' in WF_Obj; simpl in WF_Obj; rewrite MFind_f' in WF_Obj; inversion WF_Obj; subst;
      congruence.
  inversion WFHP as [null null' WF_HP1]; subst.
  rewrite add_Natmap_find_neq; auto; simpl;
  destruct (NatMapsTo_mem2 _ _ HFind_o'') as [clm' H]; generalize (NatMap.find_1 H); destruct clm' as [cl4 m'];
    clear H HFind_o''; intro HFind_o''; rewrite add_Natmap_find_neq in HFind_o''; auto; simpl;
      rewrite HFind_o''; destruct (WF_HP1 _ (NatMap_find_mem _ _ _ HFind_o'')) as [cl''' [wf_HP1 [wf_HP2 wf_HP3]]]; 
        clear WF_HP1; rewrite HFind_o'' in wf_HP1; simpl in wf_HP1; inversion wf_HP1; subst; clear wf_HP1; simpl in *|-*;
          exists cl'''; simpl; repeat split.
  inversion wf_HP2; auto.
  intros f'' In_f''; destruct (wf_HP3 _ In_f'') as [ty'' [FType_f'' WF_Obj]]; exists ty''; split; auto;
    rewrite HFind_o'' in WF_Obj; simpl in WF_Obj; inversion WF_Obj as [| p' h' o tyopt' STY]; subst.
  eapply wf_null; eauto.
  apply wf_object; destruct (eq_nat_dec o' o) as [Eq_o | Neq_o'].
  subst; rewrite add_Natmap_find_eq; simpl; rewrite HFind_o' in STY; simpl in STY; exact STY.
  subst; rewrite add_Natmap_find_neq; auto;
    rewrite HFind_o; simpl; eapply sty_opt; eauto; eapply sty_transitive; eauto.
Qed.

Lemma field_write_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (x' y : x) (f' : f),  
   wf_config p g (config_normal l h (s_write x' f' y :: ss)) ->
   reduce (config_normal l h (s_write x' f' y :: ss)) p config' ->
   exists g' : G, wf_config p g' config' /\
     (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros p g l h ss config' x' y f' WFConfig ReduceCFG;
    inversion ReduceCFG as [| | | | | | f_list l' h'' var'' cl'' ss' v'' o' v' LFind_x' LFind_y | | | |];
      subst; clear ReduceCFG.
  exists g; split; auto; apply wf_all_npe.  
  exists g; split; auto.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  inversion WFStmt as [ | | | p' g' var'' x'' f'' cl'' ty'' GFind_x' FType_f' STY | | | ]; subst.
  inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One null' GFind_y]; subst; rewrite STY2 in STY;
    inversion STY1; inversion STY2; subst; clear STY STY2 H0.
  destruct (In_L_In_H _ _ _ _ _ _ _ WFStack WFHP LFind_x' GFind_x') as [cl3 [m'' [HFind_o' STY_cl3_cl'']]];
    rewrite HFind_o'; simpl.
  apply wf_all; auto; clear WFStmt_List'.
  eapply wf_hp_field_write; eauto.
  apply wf_stack; intros y' XMap_y'; inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst;
    destruct (WF_Stk1 y' XMap_y') as [ty' [WF_Stk1' [WF_Stk2 WF_Stk3]]].
  exists ty'; repeat split; auto.
  destruct (XMap.find (elt:=v) y' l) as [var' | ].
  destruct var'.
  eapply wf_null; eauto.
  apply wf_object; destruct (eq_nat_dec o' o) as [Eq_o | Neq_o].
  subst; rewrite add_Natmap_find_eq; simpl.
  inversion WF_Stk3 as [| p' h' o''' tyopt' STY]; subst; rewrite HFind_o' in STY; simpl in STY; auto.
  subst; rewrite add_Natmap_find_neq; auto.
  inversion WF_Stk3 as [| p' h' o''' tyopt' STY]; auto.
  inversion WF_Stk3; discriminate.
Qed.

Lemma mcall_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (var' : var) (x' : x) (m' : m) (actuals : list x),  
  wf_config p g (config_normal l h (s_call var' x' m' actuals :: ss)) ->
  reduce (config_normal l h (s_call var' x' m' actuals :: ss)) p config' ->
  exists g' : G, wf_config p g' config' /\
    (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros p g l h ss config' var' x' m' actuals_list WFConfig ReduceCFG;
    inversion ReduceCFG as [ | | | | | | | big_list l'' h'' var''' x'' m'' ss3 p' l' tr' ss'' y' var'' y'' o' z'
      LFind_x' HFind_o' Find_m' Distinct_BL Fresh_BL Fresh_var'' Fresh2_var'' Vld_Ll' Eq_l' Eq_tr' Eq_tr_y'' | | |];
      subst. clear ReduceCFG.
  exists g; split; auto; apply wf_all_npe.
  destruct (big_list_breakdown big_list) as [x_list' [var1_list [var2_list [v_list 
    [Big_list_eq [Len_x_list [Len_var1_list [Len_v_list Len_var2_list]]]]]]]];
  rewrite Big_list_eq in *|-*.
  rewrite map_snd_fst_fst in *|-*; auto.
  rewrite map_fst_fst_fst in *|-*; auto.
  rewrite map_snd_fst in *|-*; auto.
  rewrite map_snd_fst_pair in *|-*; try omega.
  rewrite map_snd_fst_fst_pair in *|-*; try omega.  
  rewrite map_snd_fst' in *|-*; auto.
  rewrite map_fst_pair' in *|-*; auto.
  clear big_list Big_list_eq.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  inversion WFStmt as [ | | | | param_list p' g' var''' x'' m'' cl'' ty'' GFind_x' MType_m' Sty_List STY_Opt | | ]; subst.
  inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst;
    destruct (WF_Stk1 _ (MapsTo_mem _ _ _ (XMap.find_2 GFind_x'))) as [ty''' [WF_Stk1' [WF_Stk2 WF_Stk3]]];
      rewrite LFind_x' in WF_Stk3; inversion WF_Stk3 as [| p' h' o''' tyopt' STY]; subst; 
        rewrite HFind_o' in STY; simpl in STY.
  inversion WF_Stk3 as [p' h' o''' tyopt' tyopt'' null' null'' LFind_z | p' h' o''' tyopt' STY']; subst;
    rewrite HFind_o' in STY';
      inversion STY' as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One null' GFind_y]; subst; rewrite STY2 in STY;
        inversion STY1; inversion STY2; subst; clear STY STY2.
  destruct z' as [cl3 ty3]; simpl in *|-*; destruct ty2; destruct cl3;
    rewrite GFind_x' in WF_Stk1'; inversion WF_Stk1'; subst; clear WF_Stk1'.
  destruct (wf_prog_wf_mb _ _ _ _ _ _ _ _ WFProg (sty_mtype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _) STY_One MType_m' WFProg) Find_m') as [ty4 [WFMB [Dist_LVar [Sty_Opt_x' [WF_Type_ty'' Sty_One_ty']]]]].
  exists (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g (combine (cons var'' var2_list)  (map (fun y : x * ty => snd y) (cons (x_var var'', ty4) param_list)))); pa.
  apply wf_all; auto.
  (*** Well-Formedness of the Stack ***)
  apply wf_stack.
  intros z GMem_z; destruct (XMapsTo_mem2 _ _ GMem_z) as [ty' GFind_z]; clear GMem_z.
  destruct (find_add_context _ _ _ _ _ (proj1 (distinct_map_distinct _ ) 
    (Distinct_map_cons _ _ (distinct_fold _ _ _ Distinct_BL (Not_In_var2_list _ _ Fresh2_var'')))) (XMap.find_1 GFind_z)) as [[var''' [Eq_var'' In_z_param]] | [NIn_z_param GFind_var'']].
  simpl; subst; exists ty'; repeat split.
  apply XMap.find_1; auto.
  simpl in In_z_param; destruct In_z_param as [Eq_var | Neq_var].
  inversion Eq_var; subst; clear Eq_var.
  destruct (WF_Stk1 _ (MapsTo_mem _ _ _ (XMap.find_2 GFind_x'))) as [ty4 [WF_Stk1'' [WF_Stk2' WF_Stk3']]];
    rewrite WF_Stk1'' in GFind_x'; inversion GFind_x'; subst; auto.
  assert (exists tyopt', In (p, tyopt', Some ty') 
    (map (fun y : x * ty => (p, XMap.find (elt:=ty) (fst y) g, Some (snd y))) param_list)).
     revert Neq_var; clear; revert var2_list; induction param_list; simpl; intros.
     rewrite combine_nil in Neq_var; simpl in Neq_var; contradiction.
     destruct var2_list; simpl in Neq_var.
     contradiction; auto.
     simpl in Neq_var; destruct Neq_var as [Eq | In_var''].
     exists (XMap.find (elt:=ty) (fst a) g); left; congruence.
     destruct (IHparam_list _ In_var'') as [tyopt'' In_tyopt'']; exists tyopt''; right; auto.
  destruct H as [tyopt' In_tyopt'];
    apply in_sty_opt_wf_type with (y:= (p, tyopt', Some ty'))
      (l:=(map (fun y : x * ty => (p, XMap.find (elt:=ty) (fst y) g, Some (snd y))) param_list));
      auto.
  simpl in In_z_param; destruct In_z_param as [Eq_var | Neq_var].
  inversion Eq_var; subst; clear Eq_var.
  rewrite add_Xmap_find_eq; simpl.
  apply wf_object.
  rewrite HFind_o'; simpl in *|-*.
  apply sty_opt with (ty5 := (ty_def (cl_dcl d))) (ty' := ty'); auto.
  (*** congruence.***)
  rewrite add_Xmap_find_neq; simpl in *|-*.
  rewrite Len_v_list in Len_var2_list.
  destruct (Combine_var_list_exists_v _ _ _ _ _ l Len_var2_list Neq_var) as [v' [Find_v' In_v']];
    rewrite Find_v'; destruct v'.
  apply wf_null with (ty5 := ty'); auto.
  apply wf_object.
  rewrite <- length_map in Len_x_list; rewrite Len_v_list in Len_x_list; rewrite Len_var2_list in Len_x_list.
  destruct (distinct_common _ _ _ _ _ _ (proj1 (distinct_map_distinct _ ) Distinct_BL)
    (sym_eq Len_var2_list) Len_x_list Neq_var (find_in_combine _ _ _ _ _ (in_combine_l _ _ _ _ Neq_var) 
      (sym_eq Len_var2_list) Find_v')) as [z'' [In_z'' In_z''']].
  generalize (In_sty_opt_list_sty_opt _ _ (In_map_sty_list _ _ _ p g In_z'') Sty_List); intros Sty_Opt';
    simpl in Sty_Opt'; inversion Sty_Opt'; subst.
  inversion H0; subst; clear H0.
  destruct (Find_In_lookup_list _ _ _ _ _ _ _ _ _ WFStack H Vld_Ll' In_z''') as
    [clm' [HFind_o STY'']]; inversion STY''; subst; inversion H0; subst; clear H0.
  rewrite HFind_o; simpl; apply sty_opt with (ty5 := (ty_def (fst clm'))) (ty' := ty'0); auto.
  rewrite H in H2; inversion H2; subst; apply sty_transitive with (ty' := ty'); auto.
  generalize Neq_var Fresh2_var''; clear; revert param_list; induction var2_list.
  simpl; intros; contradiction.
  destruct param_list; simpl; intros.
  contradiction.
  destruct Neq_var as [Eq_a | In_var'''].
  inversion Eq_a; subst.
  unfold not; intros; apply Fresh2_var''; left; congruence.
  apply (IHvar2_list _ In_var'''); auto.
  (*** inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst.***)
  destruct (WF_Stk1 _ (MapsTo_mem _ _ _ (XMap.find_2 GFind_var''))) as [ty5 [WF_Stk1'' [WF_Stk2' WF_Stk3']]];
    exists ty'; repeat split; auto; rewrite WF_Stk1'' in GFind_var''; inversion GFind_var''; subst.
  rewrite (Find_Not_In_map_list _ _ _ _ _ NIn_z_param WF_Stk1''); reflexivity.
  exact WF_Stk2'.
  rewrite add_Xmap_find_neq; simpl.
  inversion WF_Stk3' as [p' h' o''' tyopt' tyopt'' null' null'' LFind_z | p' h' o''' tyopt' STY'']; subst.
  rewrite Find_Not_In_map_list' with (v' := v_null) (x_ty_list := param_list).
  apply wf_null with (ty5 := ty') ; auto.
  rewrite <- Len_var2_list; rewrite Len_x_list; clear; induction param_list; simpl; auto.
  unfold not in *|-*; intros; apply (NIn_z_param var'0 ty'0); simpl; try right; auto.
  auto.
  rewrite Find_Not_In_map_list' with (v' := v_oid o''') (x_ty_list := param_list).
  rewrite <- H2 in WF_Stk3'; apply WF_Stk3'.
  rewrite <- Len_var2_list; rewrite Len_x_list; clear; induction param_list; simpl; auto.
  unfold not in *|-*; intros; eapply NIn_z_param; simpl; try right; eauto.
  auto.
  unfold not in *|-*; intros; eapply NIn_z_param; simpl; eauto.
  (*** Well-formedness of the statements ***) 
  applyI wf_stmt_list_app; split.
  (*** Well-formedness of the Method Body ***)
  applyI wf_stmt_list_s.
  applyI wf_stmt_list'_iff.
  apply wf_stmt_list_add_g.
  simpl in WFMB.
  apply (wf_trans_stmt'' p  (fold_left (fun (m : XMap.t ty) (p : x * ty) =>
    XMap.add (fst p) (snd p) m) ((x_this, ty4) :: map
      (fun vd' : vd =>  match vd' with
                          | vd_def ty''' var' => (x_var var', ty''')
                        end)
      (map (fun x : ty * var => vd_def (fst x) (snd x))
        (combine (map (fun y : x * ty => snd y) param_list)
          var1_list))) (XMap.empty ty))); auto.
  intros; apply equiv_contexts; auto.
  rewrite spurious_map in Fresh2_var''; apply Fresh2_var''.
  apply distinct_map_xvar'; auto.
  congruence.
  rewrite <- Len_var2_list; rewrite Len_x_list.
  clear; induction param_list; simpl; auto.
  intros; apply tr_x_vars; auto.
  (*** Well-formedness of original statements ***)
  simpl; apply Cons_wf_stmt_list.
  apply wf_var_assign.
  rewrite XMap_find_Not_In with (l := l) (x' := x_var var'); auto.
  inversion Sty_Opt_x' as [p' tyopt' tyopt'' ty1 ty2 Sty1 Sty2 Sty_One null' GFind_y]; 
    subst; rewrite Sty2 in Sty_Opt_x'; inversion Sty2; subst; clear Sty2.
  generalize equiv_contexts; intros Eqv_Cxt; simpl in Eqv_Cxt.
  rewrite find_in_add'' with (ty' := ty1).
  inversion STY_Opt; rewrite H0; inversion H; subst.
  eapply sty_opt; eauto; eapply sty_transitive; eauto.
  apply (Eqv_Cxt param_list var1_list var2_list var'' y'' ty4 ty1); auto.
  rewrite spurious_map in Fresh2_var''; apply Fresh2_var''.
  apply distinct_map_xvar'; auto.
  congruence.
  rewrite <- Len_var2_list; rewrite Len_x_list; clear; induction param_list; simpl; auto.
  applyI XMapFacts.in_find_iff.
  inversion STY_Opt; subst;
  destruct (WF_Stk1 _ (MapsTo_mem _ _ _ (XMap.find_2 H0))) as [ty6 [WF_Stk1'' [WF_Stk2' WF_Stk3']]];
    inversion WF_Stk3'; subst; congruence.
  applyI wf_stmt_list'_iff'.
  generalize (wf_stmt_list_add (var'' :: var2_list) (ty4 :: (map (fun y0 : x * ty => snd y0) param_list)) g p (make_list_s ss)); intros H; simpl in H; apply H; auto.
  intros x0 In_x0; destruct In_x0 as [Eq_x0 | In_x0].
  inversion Eq_x0; eapply in_stack_in_context; eauto.
  eapply in_stack_in_context; eauto.
  applyI wf_stmt_list'_iff'.
  intros; apply XMap.find_2; apply find_in_add'.
  intros x0 In_x0; destruct In_x0 as [Eq_x0 | In_x0].
  inversion Eq_x0; eapply in_stack_in_context; eauto.
  eapply in_stack_in_context; eauto.
  apply XMap.find_1; exact H.
  unfold find_menv in Find_m'; unfold get_md in Find_m'. rewrite path_cl_object in Find_m'; 
    simpl in MType_m'; discriminate.
Qed.
  
Lemma if_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss : list s) 
  (config' : config) (x' y': x) (s1 s2 : s) ,  
  wf_config p g (config_normal l h (s_if x' y' s1 s2  :: ss)) ->
  reduce (config_normal l h (s_if x' y' s1 s2 :: ss)) p config' ->
  exists g' : G, wf_config p g' config' /\
    (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
Proof.
  intros until s2; intros WFConfig ReduceCFG;
    inversion ReduceCFG as [| | | | | | | | l' h' x'' y'' s1' s2' ss' p' var' var'' | 
      l' h' x'' y'' s1' s2' ss' p' var' var''| ];
      subst; clear ReduceCFG.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  inversion WFStmt as [ | | | | | p' g' x'' y'' s1' s2' STY_Opt WF_Stmt1 WF_Stmt2 | ]; subst.
  exists g; split; auto.
  apply wf_all; auto.
  simpl; apply Cons_wf_stmt_list; auto.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  inversion WFStmt as [ | | | | | p' g' x'' y'' s1' s2' STY_Opt WF_Stmt1 WF_Stmt2 | ]; subst.
  exists g; split; auto.
  apply wf_all; auto.
  simpl; apply Cons_wf_stmt_list; auto.
Qed.

Lemma block_preservation : forall (p : P) (g : G) (l : L) (h : H) (ss' : list_s) (ss : list s) 
  (config' : config),  
  wf_config p g (config_normal l h (s_block ss' :: ss)) ->
  reduce (config_normal l h (s_block ss' :: ss)) p config' ->
  exists g' : G, wf_config p g' config' /\
    (forall (x' : x) (ty' : ty),
      XMap.MapsTo x' ty' g -> XMap.MapsTo x' ty' g').
  intros until config'; intros WFConfig ReduceCFG;
  inversion ReduceCFG as [| | | | | | | | | | ss'' l' h' ss''' p' ];
      subst; clear ReduceCFG.
  inversion WFConfig as [s' p' g' l' h' WFProg WFHP WFStack WFStmt_List | ]; clear WFConfig; subst.
  simpl in WFStmt_List; inversion WFStmt_List as [| p' g' s' l' WFStmt WFStmt_List' H1]; clear WFStmt_List; subst.
  inversion WFStmt as [ | | | | | | ss'' p' g' WF_Stmt1]; subst.
  exists g; split; auto.
  apply wf_all; auto.
  applyI wf_stmt_list_app; split; auto.
  generalize WF_Stmt1; clear; induction ss'; simpl; intros; auto.
  inversion WF_Stmt1; subst.
  apply Cons_wf_stmt_list; auto.
Qed.
  

Theorem preservation_result : preservation.
Proof.
  unfold preservation; intros config1 config2 g p WFConfig1 ReduceCFG.
  destruct config1 as [l h ss | ].
  destruct ss.
  inversion ReduceCFG.
  destruct s.
  eapply new_preservation; eauto.
  eapply var_assign_preservation; eauto.
  eapply field_read_preservation; eauto.
  eapply field_write_preservation; eauto.
  eapply mcall_preservation; eauto.
  eapply if_preservation; eauto.
  eapply block_preservation; eauto.
  exists g; pa; intros; auto; inversion ReduceCFG.
Qed.

End Preservation.