Require Import Arith. Require Import Bool. Require Import List. Require Import Natmap. Require Import FMaps. Require Import EqNat. Require Import lj. Require Import FMapFacts. Require Import Natmap. Require Import Classical. Require Import base2. Require Import Max. Module NatMapFacts := FMapFacts.Facts NatMap. Module XMapFacts := FMapFacts.Facts XMap. Lemma max_lelistA : forall (A : Set) (eqA leA: relation A) (eqA_refl : forall x : A, eqA x x) (leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z) (le_eq_A_trans : forall x y z:A, leA x y -> eqA y z -> leA x z) (le_list : list A) (b :A) , sort leA le_list -> In b le_list -> leA b (last le_list b) \/ eqA b (last le_list b). induction le_list; intros. elimtype False; exact H0. inversion H; inversion H4; subst. inversion H0. rewrite H1; simpl. po2; apply eqA_refl. elimtype False; exact H1. inversion H0; subst. inversion H4; subst. assert (In b0 (b0 :: l0)). simpl. po1. generalize (IHle_list b0 H3 H1); intros; clear IHle_list. destruct H6. po1. simpl. generalize (leA_trans _ _ _ H2 H6); intros. destruct l0. exact H7. generalize H7; clear; intros. generalize a H7; clear a H7; induction l0; intros. exact H7. simpl; simpl in IHl0; apply IHl0. exact H7. po1. simpl. generalize (le_eq_A_trans _ _ _ H2 H6); intros. destruct l0. exact H7. generalize H7; clear; intros. generalize a H7; clear a H7; induction l0; intros. exact H7. simpl; simpl in IHl0; apply IHl0. exact H7. fold (In b (b0::l0 ))in H1. simpl; apply (IHle_list b H3 H1). Qed. Lemma NatMap_max : forall (h : H), ~ NatMap.Empty h -> exists n, (NatMap.In n h /\ (forall m, NatMap.In m h -> m <= n)). intros. caseEq (NatMap.elements h); intros. unfold NatMap.elements in H0; unfold NatMap.Raw.elements in H0. unfold NatMap.Empty in H; unfold NatMap.Raw.Empty in H; subst. rewrite H0 in H. assert (exists a, exists e, NatMap.MapsTo a e h). apply NNPP. intro. apply H. unfold not; intros; apply H1. exists a; exists e. simpl in H2. unfold NatMap.MapsTo; rewrite H0. exact H2. destruct H1; destruct H1. unfold NatMap.MapsTo in H1; unfold NatMap.Raw.PX.MapsTo in H1. rewrite H0 in H1. inversion H1. clear H. generalize (NatMap.elements_3 h); intros. rewrite H0 in H. inversion H. exists (fst (last (NatMap.elements h) p)). pa. unfold NatMap.In; unfold NatMap.Raw.PX.In; exists (snd (last (NatMap.elements h)p ) ). apply NatMap.elements_2. rewrite H0. clear. generalize l p; clear l p. induction l; intros. simpl. apply InA_cons_hd. unfold NatMap.eq_key_elt; unfold NatMap.Raw.PX.eqke; unfold NatOrd.eq; simpl. pa; try apply eq_eq_nat; apply refl_equal. unfold last; fold (last (a :: l) p). apply InA_cons_tl. generalize (IHl a); clear IHl; intros H. assert (forall a0, last (a::l) a0 = last (a::l) p). clear. generalize l a p; clear. induction l; intros. simpl; apply refl_equal. unfold last; fold (last (a::l) a1); fold (last (a::l) p); apply IHl. rewrite H0 in H. exact H. intros. assert (forall x : NatMap.key * (cl * NatMap.t v), NatMap.eq_key x x). clear; intros. unfold NatMap.eq_key; unfold NatMap.Raw.PX.eqk; apply NatOrd.eq_refl. assert (forall x y z : NatMap.key * (cl * NatMap.t v), NatMap.lt_key x y -> NatMap.lt_key y z -> NatMap.lt_key x z). unfold NatMap.lt_key; unfold NatMap.Raw.PX.ltk; unfold NatOrd.lt; clear; intros; omega. assert (forall x y z : NatMap.key * (cl * NatMap.t v), NatMap.lt_key x y -> NatMap.eq_key y z -> NatMap.lt_key x z). unfold NatMap.eq_key; unfold NatMap.Raw.PX.eqk; unfold NatMap.lt_key; unfold NatMap.Raw.PX.ltk; unfold NatOrd.lt; unfold NatOrd.eq; clear; intros. generalize (eq_nat_eq _ _ H0); intros H1; rewrite H1 in H; exact H. unfold NatMap.In in H5; unfold NatMap.Raw.PX.In in H5; destruct H5. generalize (NatMap.elements_1 H5); intros. assert (In (m,x) (p::l)). rewrite H0 in H9. generalize p H9; clear. induction l; intros p H. unfold In. po1. inversion H; subst. unfold NatMap.eq_key_elt in H1; unfold NatMap.Raw.PX.eqke in H1; simpl in H1; destruct H1. generalize (eq_nat_eq _ _ H0); intros H2; rewrite H1; rewrite H2. case p; intros; apply refl_equal. inversion H1. inversion H; subst. unfold NatMap.eq_key_elt in H1; unfold NatMap.Raw.PX.eqke in H1; simpl in H1; destruct H1. generalize (eq_nat_eq _ _ H0); intros H2; rewrite H1; rewrite H2. unfold In; po1. case p; intros; apply refl_equal. unfold In; fold (In (m,x) (a::l)). po2; apply IHl; exact H1. generalize (max_lelistA _ (NatMap.eq_key(elt := cl * NatMap.t v)) (NatMap.lt_key(elt := cl * NatMap.t v)) H6 H7 H8 _ (m,x) H H10); intros. clear H6 H7 H8 H9. rewrite H0. assert (forall a0 a, last (a::l) a0 = last (a::l) p). clear. generalize l p; clear. induction l; intros. simpl; apply refl_equal. unfold last; fold (last (a::l) a0); fold (last (a::l) p); apply IHl. destruct H11; generalize p m x H6 H7; clear; intros p m x H H1. unfold NatMap.lt_key in H1; unfold NatMap.Raw.PX.ltk in H1; unfold NatOrd.lt in H1. rewrite H in H1; unfold fst at 1 in H1. auto with arith. unfold NatMap.eq_key in H1; unfold NatMap.Raw.PX.eqk in H1; unfold NatOrd.eq in H1. generalize (eq_nat_eq _ _ H1); intros. rewrite H in H0; unfold fst at 1 in H0. rewrite H0. auto with arith. Qed. Inductive le_xvar (x' : x) : x -> Prop := | le_n : le_xvar x' x' | le_S : forall m, le_xvar x' (x_var m) -> le_xvar x' (x_var (S m)). Lemma XMap_max : forall (l : L), ~ XMap.Empty l -> exists x', (XMap.In x' l /\ (forall y', XMap.In y' l -> (XOrd.lt y' x') \/ (XOrd.eq y' x'))). intros. caseEq (XMap.elements l); intros. unfold XMap.elements in H0; unfold XMap.Raw.elements in H0. unfold XMap.Empty in H; unfold XMap.Raw.Empty in H; subst. rewrite H0 in H. assert (exists a, exists e, XMap.MapsTo a e l). apply NNPP. intro. apply H. unfold not; intros; apply H1. exists a; exists e. simpl in H2. unfold XMap.MapsTo; rewrite H0. exact H2. destruct H1; destruct H1. unfold XMap.MapsTo in H1; unfold XMap.Raw.PX.MapsTo in H1. rewrite H0 in H1. inversion H1. clear H. generalize (XMap.elements_3 l); intros. rewrite H0 in H. inversion H. exists (fst (last (XMap.elements l) p)). pa. unfold XMap.In; unfold XMap.Raw.PX.In; exists (snd (last (XMap.elements l) p ) ). apply XMap.elements_2. rewrite H0. clear. generalize l0 p; clear l0 p. induction l0; intros. simpl. apply InA_cons_hd. unfold XMap.eq_key_elt; unfold XMap.Raw.PX.eqke; unfold NatOrd.eq; simpl. pa; try apply XOrd.eq_refl; try apply refl_equal. unfold last; fold (last (a :: l0) p). apply InA_cons_tl. generalize (IHl0 a); clear IHl0; intros H. assert (forall a0, last (a::l0) a0 = last (a::l0) p). clear. generalize l0 a p; clear. induction l0; intros. simpl; apply refl_equal. unfold last; fold (last (a::l0) a1); fold (last (a::l0) p); apply IHl0. rewrite H0 in H. exact H. intros. unfold XMap.In in H5; unfold XMap.Raw.PX.In in H5; destruct H5. generalize (XMap.elements_1 H5); intros. assert (In (y',x) (p::l0)). rewrite H0 in H6. generalize p H6; clear. induction l0; intros p H. unfold In. po1. inversion H; subst. unfold XMap.eq_key_elt in H1; unfold XMap.Raw.PX.eqke in H1; simpl in H1; destruct H1. unfold XOrd.eq in H0. destruct p; destruct y'; intros; simpl in H0; destruct k. generalize (eq_nat_eq _ _ H0); intros H2; rewrite H1; rewrite H2. apply refl_equal. elimtype False; apply H0. elimtype False; apply H0. inversion H1. apply refl_equal. inversion H1. inversion H; subst. unfold In; po1. destruct p; intros. inversion H1; subst. simpl in H2; rewrite H2. simpl in H0; unfold XOrd.eq in H0. destruct y'; destruct k; try (elimtype False; auto; fail). generalize (eq_nat_eq _ _ H0); intros. rewrite H3; apply refl_equal. apply refl_equal. unfold In; po2; apply IHl0; exact H1. assert (forall x : XMap.key * v, XMap.eq_key x x). clear; intros. unfold XMap.eq_key; unfold XMap.Raw.PX.eqk; apply XOrd.eq_refl. assert (forall x y z : XMap.key * v, XMap.lt_key x y -> XMap.lt_key y z -> XMap.lt_key x z). unfold XMap.lt_key; unfold XMap.Raw.PX.ltk; intros; apply (XOrd.lt_trans _ _ _ H9 H10). assert (forall x y z : XMap.key * v, XMap.lt_key x y -> XMap.eq_key y z -> XMap.lt_key x z). unfold XMap.eq_key; unfold XMap.Raw.PX.eqk; unfold XMap.lt_key; unfold XMap.Raw.PX.ltk; unfold XOrd.lt; unfold XOrd.eq; clear; intros. destruct x; destruct y; destruct z; simpl in *|-*. destruct k; destruct k0; destruct k1; auto. generalize (eq_nat_eq _ _ H0); intros H1; rewrite H1 in H; exact H. elimtype False; exact H0. generalize (max_lelistA _ (XMap.eq_key(elt := v)) (XMap.lt_key(elt := v)) H8 H9 H10 _ (y',x) H H7); intros. clear H8 H9 H10. rewrite H0. assert (forall a0 a, last (a::l0) a0 = last (a::l0) p). clear. generalize l0 p; clear. induction l0; intros. simpl; apply refl_equal. unfold last; fold (last (a::l0) a0); fold (last (a::l0) p); apply IHl0. destruct H11; generalize p m x H9 H8; clear; intros p m x H H1. unfold XMap.lt_key in H; unfold XMap.Raw.PX.ltk in H; unfold XMap.lt_key in H. rewrite H1 in H; unfold fst at 1 in H. po1. unfold XMap.eq_key in H; unfold XMap.Raw.PX.eqk in H; unfold XMap.eq_key in H. rewrite H1 in H. unfold fst at 1 in H. po2. Qed. Lemma XMap_max_x_var : forall (l : L) (k : nat), XMap.In (x_var k) l-> exists n, (XMap.In (x_var n) (XMap.remove x_this l) /\ (forall m, XMap.In (x_var m) (XMap.remove x_this l) -> m <= n)). intros. assert ( ~ (XMap.Empty (XMap.remove x_this l))). unfold not; intros. unfold XMap.In in H; unfold XMap.Raw.PX.In in H; destruct H. assert (~ (XMap.E.eq x_this (x_var k))). unfold not; intros. unfold XMap.E.eq in H1; unfold XOrd.eq in H1; exact H1. generalize (XMap.remove_2); intros H2; generalize (H2 _ _ _ _ _ H1 H); clear H2 H1; intros H2. unfold XMap.Empty in H0; unfold XMap.Raw.Empty in H0; subst. apply (H0 _ _ H2). generalize (XMap_max _ H0); intros. destruct H1; bd H1. assert (x <> x_this). unfold not; intros. rewrite H2 in H4. generalize (XMap.remove_1); intros. assert (XMap.E.eq x_this x_this). auto. apply (H3 v l _ _ H5 H4). destruct x; try (elimtype False; apply H2; apply refl_equal; fail). exists v. pa. intros. generalize (H1 _ H3); intros H5; destruct H5. unfold XOrd.lt in H5; auto with arith. unfold XOrd.eq in H5; generalize (eq_nat_eq _ _ H5); intros; rewrite H6; auto with arith. Qed. Lemma ex_fresh_oid : forall (h : H), exists o, NatMap.mem o h = false. intro h. caseEq (NatMap.is_empty h). exists 0. rewrite <- NatMapFacts.is_empty_iff in H. unfold NatMap.Empty in H. unfold NatMap.Raw.Empty in H. applyI (NatMapFacts.not_mem_in_iff). unfold not; intro. unfold NatMap.In in H0. unfold NatMap.Raw.PX.In in H0. inversion H0. apply (H 0 x). exact H1. intros. assert (~NatMap.Empty h). unfold not; intro H1; generalize (NatMap.is_empty_1 H1); intro H2; rewrite H2 in H; discriminate. clear H. generalize (NatMap_max _ H0); intros H; clear H0; destruct H; destruct H. exists (S x). generalize (classic (NatMap.In (S x) h)); intros H1; destruct H1. generalize (H0 _ H1); intros H2. elimtype False; omega. clear H0 H. caseEq (NatMap.mem (S x) h); intros. generalize (NatMap.mem_2 H); intro H0; elimtype False; apply H1; exact H0. apply refl_equal. Qed. Lemma ex_max_var_list : forall (l : list x), ~ In x_this l -> l <> nil -> exists n, In (x_var n) l /\ (forall (m : nat), In (x_var m) l -> m <= n). induction l; intros. elimtype False; apply H0; apply refl_equal. clear H0. simpl in H. generalize (not_or_and _ _ H); clear H; intros H; bd H. destruct a; try (elimtype False; apply H2; apply refl_equal); clear H2. destruct l. exists v; pa. simpl; po1. intros. simpl in H0; bd H0. inversion H0; auto with arith. assert (x :: l <> nil). unfold not; intros; discriminate. generalize (IHl H H0); intros; clear IHl; destruct H1; bd H1. case (le_lt_dec x0 v); intros. exists v; pa. simpl; po1; apply refl_equal. intros. simpl in H2; bd H2. inversion H2; auto with arith. rewrite H2 in H1. assert (In (x_var m) (x_var m :: l)); simpl; try po1. generalize (H1 m H3); intros. omega. assert (In (x_var m) (x :: l)); try po2. generalize (H1 m H3); intros. omega. exists x0; pa. simpl; po2. intros. simpl in H2. bd H2. inversion H2. rewrite H5 in l0. auto with arith. rewrite H2 in H1. apply H1. simpl; po1. apply H1. simpl; po2. Qed. Lemma ex_fresh_lookup_list : forall (l : L) (n: nat), exists fresh_list, length fresh_list = n /\ (distinct _ fresh_list) /\ (forall x, In x fresh_list -> ~ XMap.In x l) /\ ~ In x_this fresh_list. induction n; intros. exists (nil : list XMap.key). simpl; pa; pa; pa. intros; elimtype False; exact H. unfold not; intro H; exact H. destruct IHn; bd H. generalize (classic (exists n, XMap.In (x_var n) l)); intros. bd H0. destruct x. simpl in H2. rewrite <- H2. generalize (XMap_max_x_var _ _ H0); intros; destruct H1; bd H1. exists (cons (x_var (S x)) nil); simpl; repeat pa. intros. bd H5. unfold not; intros. rewrite <- H5 in H6. assert (~ XMap.E.eq x_this (x_var (S x))). unfold not; intros. unfold XMap.E.eq in H8; unfold XOrd.eq in H8; exact H8. generalize (XMap.remove_2). intros. unfold XMap.In in H6; unfold XMap.Raw.PX.In in H6; destruct H6. generalize (H9 _ _ _ _ _ H8 H6); intros. generalize (H1 (S x)). intros. unfold XMap.In in H11; unfold XMap.Raw.PX.In in H11. assert (exists e : v, XMap.MapsTo (x_var (S x)) e (XMap.remove x_this l)). exists x2; exact H10. unfold XMap.MapsTo in H12. generalize (H11 H12); intros. omega. unfold not; intros. bd H5. discriminate. assert (k :: x <> nil). unfold not; intros; discriminate. generalize (ex_max_var_list _ H H1); intros H5; destruct H5; bd H5. generalize (XMap_max_x_var _ _ H0); intros H6; destruct H6; bd H6. case (le_lt_dec x1 x2); intros. exists (cons (x_var (S x2)) (k :: x)); simpl; repeat pa. simpl in H2; rewrite H2; apply refl_equal. unfold not; intros. bd H7. assert (In (x_var (S x2)) (k :: x) ). rewrite H7; simpl; po1. generalize (H5 _ H9); intros. omega. assert (In (x_var (S x2)) (k :: x) ). simpl; po2. generalize (H5 _ H9); intros. omega. intros. unfold not; intros. bd H7. rewrite <- H7 in H9. assert (~XMap.E.eq x_this (x_var (S x2))). unfold not; intros H11; unfold XMap.E.eq in H11; simpl in H11; exact H11. generalize (XMap.remove_2); intros H12. unfold XMap.In in H9; unfold XMap.Raw.PX.In in H9; destruct H9. unfold XMap.MapsTo in H12. assert (exists e : v, XMap.MapsTo (x_var (S x2)) e (XMap.remove x_this l)). generalize (H12 v l _ _ x4 H11 H9); intros. exists x4; exact H13. unfold XMap.In in H6; unfold XMap.Raw.PX.In in H6. generalize (H6 _ H13); intros. omega. rewrite <- H7 in H9. generalize (H4 k); intros. apply H11. simpl; po1. exact H9. generalize (H4 x3); intros. apply H11. simpl; po2. exact H9. unfold not; intros H7; bd H7. discriminate. exists (cons (x_var (S x1)) (k :: x)); repeat pa. simpl; simpl in H2; rewrite H2; apply refl_equal. unfold not; intros. generalize (H5 _ H7); omega. intros. unfold not; intros. simpl in H7; bd H7. rewrite <- H7 in H9. assert (~XMap.E.eq x_this (x_var (S x1))). unfold not; intros H11; unfold XMap.E.eq in H11; simpl in H11; exact H11. generalize (XMap.remove_2); intros H12. unfold XMap.In in H9; unfold XMap.Raw.PX.In in H9; destruct H9. unfold XMap.MapsTo in H12. assert (exists e : v, XMap.MapsTo (x_var (S x1)) e (XMap.remove x_this l)). generalize (H12 v l _ _ x4 H11 H9); intros. exists x4; exact H13. unfold XMap.In in H6; unfold XMap.Raw.PX.In in H6. generalize (H6 _ H13); intros. omega. rewrite <- H7 in H9. generalize (H4 k); intros. apply H11. simpl; po1. exact H9. generalize (H4 x3); intros. apply H11. simpl; po2. exact H9. unfold not; intros H7; simpl in H7; bd H7. discriminate. destruct x. simpl in H2; rewrite <- H2. exists (cons (x_var 0) nil); repeat pa. intros; destruct x. apply H0. simpl in H1. bd H1; discriminate. unfold not; intros; simpl in H1. bd H1; discriminate. assert (k :: x <> nil). unfold not; intros; discriminate. generalize(ex_max_var_list _ H H1); intros H5; destruct H5; bd H5. exists (cons (x_var (S x0)) (k :: x)); repeat pa. simpl; simpl in H2; rewrite H2; apply refl_equal. unfold not; intros. generalize (H5 _ H6); intros. omega. unfold not; intros. simpl in H6; bd H6. rewrite <- H6 in H7. apply (H0 _ H7). rewrite <- H6 in H7. assert (In k (k :: x)). simpl; po1. apply (H4 _ H9 H7). assert (In x1 (k :: x)). simpl; po2. apply (H4 _ H9 H7). unfold not; intros. simpl in H6; bd H6. discriminate. Qed. Fixpoint strip_xvar (list_x : list x) {struct list_x} : list var := match list_x with nil => nil | cons (x_var var') list_x' => cons var' (strip_xvar list_x') | cons _ list_x' => strip_xvar list_x' end. Lemma ex_fresh_lookup_list' : forall (l : L) (n: nat), exists fresh_list, length fresh_list = n /\ (distinct _ fresh_list) /\ (forall var', In var' fresh_list -> ~ XMap.In (x_var var') l). intros. import (ex_fresh_lookup_list l n); destruct H; bd H. exists (strip_xvar x); repeat pa. generalize n H2 H; clear. induction x; intros. simpl in *|-*; auto. destruct a; simpl. simpl in H; bd H. simpl in H2. destruct n; try discriminate. rewrite (IHx (length x)); auto. simpl in H; bd H. clear l n H2 H4; induction x. simpl; auto. simpl in *|-*; destruct a. bd H3; bd H. simpl; pa. generalize H2; clear; induction x; simpl; intros. exact H2. destruct a; bd H2. simpl. unfold not; intros H; bd H. rewrite H in H2; apply H2; apply refl_equal. apply IHx; auto. auto. auto. bd H3; bd H; auto. intros. assert (In (x_var var') x). generalize H0; clear; intros. induction x. simpl in H0; elimtype False; exact H0. destruct a; simpl in H0; simpl; bd H0. rewrite H0; po1. po2; auto. po2; auto. apply H4; auto. Qed. Lemma wf_assign_lookupl : forall (p : P) (g : G) (l : L) (h : H) (var5 : var) (x5 : x), wf_stmt p g (s_ass var5 x5) -> wf_stck p g h l -> exists v', XMap.find x5 l = Some v'. intros. destruct H0. inversion H; subst. inversion H4; subst. assert (XMap.mem (x5) G5 = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists ty5. apply (XMap.find_2 H1). generalize (H0 _ H6); clear H0; intros H0; destruct H0; bd H0. inversion H0. exists v_null; apply refl_equal. exists (v_oid oid5). apply refl_equal. Qed. Lemma wf_fread_lookuplh : forall (p : P) (g : G) (l : L) (h : H) (var5 : var) (x5 : x) (f' :f), wf_stmt p g (s_read var5 x5 f') -> wf_stck p g h l -> (exists v', XMap.find x5 l = Some v' /\ ( forall (oid' : oid), v' = v_oid oid' -> exists clm, (NatMap.find (oid') h = Some clm) /\ sty_option p (Some (ty_def (fst clm))) (XMap.find x5 g))). intros. destruct H0. inversion H; subst. inversion H9; subst. assert (XMap.mem (x5) G5 = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty_def cl5). apply (XMap.find_2 H7). generalize (H0 _ H4); clear H0; intros H0; destruct H0; bd H0. inversion H0. exists v_null; pa. intros; discriminate. exists (v_oid oid5); pa; intros. inversion H17; rewrite <- H19; clear H17 H19. inversion H0; subst; rewrite <- H10 in H18; try discriminate. inversion H18; clear H18; rewrite H13 in H21. destruct (NatMap.find oid5 H5). exists p; pa. rewrite H11; exact H21. inversion H21; discriminate. Qed. Lemma wf_fread_lookuph : forall (p : P) (h : H) (f' : f) clm (oid' : oid), NatMap.find (oid') h = Some clm -> wf_hp p h -> In f' (fields p (fst clm)) -> exists v', NatMap.find f' (snd clm) = Some v'. intros. assert (NatMap.mem oid' h = true). apply NatMap.mem_1. unfold NatMap.In; unfold NatMap.Raw.PX.In; exists clm. apply (NatMap.find_2 H). inversion H0. generalize (H3 _ H2); clear H3; intros H3; destruct H3; bd H3. rewrite H in H9; inversion H9; clear H9. rewrite H8 in H1; generalize (H3 f' H1); clear H3; intros H3; destruct H3; destruct H3. rewrite H in H7. inversion H7; subst. exists v_null; apply refl_equal. exists (v_oid oid5); apply refl_equal. Qed. Lemma mtype_find_menv : forall (p : P) (cl' : cl) (m' : m) (mty' : mty), mtype p cl' m' = Some mty' -> exists md', find_menv p cl' m' = Some md'. intros. unfold mtype in H; unfold find_menv. destruct (get_md p cl' m'); try discriminate. unfold ext_mty in H; unfold ext_menv. exists ( match m with | md_def (ms_def _ _ vds') mb' => menv_def (get_vdsvars vds') mb' end). apply refl_equal. Qed. Lemma wf_tl_valid_lookup : forall (p : P) (g : G) (l : L) (h : H) (var' : var) (x' : x) (m' : m) (list_x : list x), wf_stmt p g (s_call var' x' m' list_x) -> wf_stck p g h l -> exists list_v : list v, (valid_lookup_list l (combine list_x list_v) /\ length list_v = length list_x). intros. inversion H; subst. generalize H9 H0; clear. induction y_ty_list; intros. simpl in H9. exists (nil : list v); pa. apply valid_lookup_nil. simpl; apply refl_equal. destruct a. inversion H9; inversion H2; subst. inversion H0; subst. assert (XMap.mem x g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists ty0. apply (XMap.find_2 H6). import (H _ H1); bd H3. import (IHy_ty_list H5 H0); bd H4. inversion H3; subst. exists (cons (v_null) x1); pa. apply (valid_lookup_cons _ _ _ _ (sym_eq H13) H14). simpl; rewrite H4; apply refl_equal. exists (cons (v_oid oid5) x1); pa. apply (valid_lookup_cons _ _ _ _ (sym_eq H13) H14). simpl; rewrite H4; apply refl_equal. Qed. Lemma ftype_in_fields : forall (p : P) (cl' : cl) (f' : f), ftype p cl' f' <> None <-> In f' (fields p cl'). intros. unfold ftype; unfold fields. induction (path p cl'). simpl. pa; intros; try discriminate; try tauto. destruct a. unfold ext_fs. unfold map at 1; fold (map (fun cld' : cld => match cld' with | cld_def _ _ fds' _ => get_fs fds' end) l ). unfold concat; fold concat (ext_fs l). unfold ext_fty; fold ext_fty. induction f. simpl; exact IHl. unfold get_fty; fold get_fty. unfold get_fs; fold get_fs. caseEq a; intros. case (eq_nat_dec f' f0); intros. pa; intros. unfold map; fold (map (fun fd' : fd => match fd' with | fd_def _ f'0 => f'0 end) (f)). simpl; po1; rewrite e; apply refl_equal. unfold not; intros; discriminate. unfold map; fold (map (fun fd' : fd => match fd' with | fd_def _ f'0 => f'0 end) (f)). pa; intros. simpl; po2. applyI IHf. simpl in H0; bd H0. elimtype False; congruence. applyI IHf. Qed. Lemma In_names : forall d0 c0 f0 l0 p, In (cld_def d0 c0 f0 l0) p -> In (cl_dcl d0) (names p). induction p. simpl; intros; po2; exact H. intros. simpl in H. bd H. rewrite H. simpl. po1. destruct a; simpl. po2; apply (IHp H). Qed. Lemma In_names2 : forall d0 p, In (cl_dcl d0) (names p) -> exists c0, exists f0, exists l0, In (cld_def d0 c0 f0 l0) p. induction p; simpl; intros. bd H; discriminate. destruct a. simpl in H; bd H; try inversion H. exists c; exists f; exists l; po1. import (IHp H); bd H0. exists x; exists x0; exists x1; po2. Qed. Lemma distinct_unique_names : forall (cld1 cld2 : cld) (p : P), distinct _ (names p) -> names (cld1 :: nil) = names ( cld2 :: nil) -> In cld1 p -> In cld2 p -> cld1 = cld2. induction p; intros. simpl in H1; elimtype False; apply H1. simpl in H1, H2. simpl in IHp. destruct cld1; destruct cld2. simpl in H0; inversion H0; clear H0. rewrite H4 in H1. bd H1; bd H2. rewrite <- H1; rewrite <- H2; apply refl_equal. rewrite H1 in H; unfold names in H; fold names in H. simpl in H; bd H. elimtype False; apply H5; apply (In_names _ _ _ _ _ H2). rewrite H2 in H; unfold names in H; fold names in H. simpl in H; bd H. elimtype False; apply H5; apply (In_names _ _ _ _ _ H1). rewrite H4 in IHp. apply IHp. destruct a. simpl in H; bd H. apply refl_equal. apply H1. apply H2. Qed. Lemma path_cl_obj : forall (p : P), path p cl_object = nil. destruct p; auto. simpl; destruct c; auto. Qed. Lemma wf_class_list_ordered : forall (cld' : cld) (l : list(P*cld)) (p : P), In (p,cld') l -> wf_class_list l -> (exists cl', get_parent cld' = cl' /\ In cl' (names' l)). induction l; intros. simpl in H; elimtype False; exact H. simpl in H. bd H. rewrite H in *|-*. destruct cld'. exists c; pa. apply refl_equal. inversion H0. simpl. generalize (classic (cl_dcl d = c)); intros H7; bd H7. po1. po2. destruct H6; bd H6. simpl in H10. rewrite H10; exact H6. inversion H0. generalize (IHl _ H H4); intros H6; destruct H6; bd H6. exists x; pa. simpl. destruct cld_. simpl; po2. Qed. Lemma names'_eq_names : forall p a, names' (map (fun cld_ : cld => (a, cld_)) p) = names p. clear. induction p; intros. apply refl_equal. destruct a; simpl. rewrite IHp. apply refl_equal. Qed. Lemma map_up : forall (A C : Type) (a : A) (b : list A) (c : C), In a b -> In (c, a) (map (fun (x : A) => (c, x)) b). induction b; intros. simpl in H; elimtype False; apply H. simpl in H; bd H. rewrite H. simpl; po1. simpl; po2; apply IHb; exact H. Qed. Lemma wf_prog1 : forall (p : P) (dcl1 : dcl) (cl1 : cl) (fds1 : fds) (md_list1 : list md), wf_prog ((cld_def dcl1 cl1 fds1 md_list1) :: p) -> forall cld', In cld' p -> get_parent cld' <> cl_dcl dcl1. intros; inversion H; clear H. simpl in H2. rewrite <- H1 in H3. simpl in H3. assert (In ((cld_def dcl1 cl1 fds1 md_list1 :: p), (cld_def dcl1 cl1 fds1 md_list1)) ( ( (cld_def dcl1 cl1 fds1 md_list1 :: p), cld_def dcl1 cl1 fds1 md_list1) :: map (fun cld_ : cld => ((cld_def dcl1 cl1 fds1 md_list1 :: p), cld_)) p)). po1. generalize (wf_class_list_ordered _ _ _ H H3); clear H; intros H; destruct H; bd H. inversion H3; clear H11 H9 H8 H3 H6 H5. simpl in H; rewrite names'_eq_names in H. simpl in H7. rewrite <- H7 in H. destruct cld'. simpl. unfold not; intros. rewrite H3 in H0; bd H2. generalize (map_up _ _ _ _ (cld_def dcl1 cl1 fds1 md_list1 :: p) H0 ); intros. generalize (wf_class_list_ordered _ _ _ H5 H10); intros H11; destruct H11; bd H6. simpl in H12; rewrite <- H12 in H6. rewrite names'_eq_names in H6. apply H8; exact H6. Qed. Lemma wf_prog2 : forall (p : P) (l : list (P*cld)) (cld' : cld), In (p, cld') l -> wf_class_list l -> distinct _ (names' l) -> get_parent cld' <> hd (get_parent cld') (names (cld' :: nil)). induction l; intros. simpl in H; elimtype False; exact H. unfold not; intro. destruct cld'. simpl in H2. destruct a. simpl in H. bd H. rewrite H2 in H. inversion H. assert (In (p0,c0) ((p0, c0) :: l)). simpl; po1. generalize (wf_class_list_ordered _ _ _ H3 H0); intros. destruct H6; bd H6. rewrite H5 in H9, H6. simpl in H9; rewrite <- H9 in H6. rewrite H5 in H1. simpl in H6. simpl in H1. rewrite H5 in *|-*; clear H5. inversion H0; subst. inversion H10. apply H9; apply refl_equal. rewrite H2 in H. inversion H0; subst. destruct c0; simpl in H1; bd H1. apply (IHl _ H H7 H1). simpl. apply refl_equal. Qed. Lemma In_names_In_p : forall (dcl' : dcl) (p : P), In (cl_dcl dcl') (names p) -> exists cl', exists fds, exists md_list, In (cld_def dcl' cl' fds md_list) p. induction p; intros. simpl in H; elimtype False; bd H; discriminate. destruct a; simpl in H; bd H. inversion H. exists c; exists f; exists l. simpl; po1. generalize (IHp H); intros H0; repeat destruct H0. exists x; exists x0; exists x1. simpl; po2. Qed. Lemma In_prog_In_path : forall (dcl' : dcl) (cl' : cl) (fds': fds) (mds' : list md) (p : P), In (cld_def dcl' cl' fds' mds') p -> distinct _ (names p) -> In (cld_def dcl' cl' fds' mds') (path p (cl_dcl dcl')). induction p; intros. simpl in H; elimtype False; apply H. simpl in H; bd H. rewrite H; simpl. case (eq_nat_dec dcl' dcl'). intros; simpl. po1. intros; elimtype False; apply n; apply refl_equal. simpl; destruct a. case (eq_nat_dec dcl' d); intros. rewrite <- e in *|-*; clear e. simpl in H0; bd H0. generalize (In_names _ _ _ _ _ H); intros. elimtype False; apply H3; apply H1. apply (IHp H). simpl in H0; bd H0. Qed. Lemma In_p_In_names : forall (dcl' : dcl) (cl' : cl) (fds': fds) (mds' : list md) (p : P), In (cld_def dcl' cl' fds' mds') p -> In (cl_dcl dcl') (names p). induction p; intros. simpl in H; elimtype False; apply H. simpl in H; bd H. rewrite H; simpl. po1. destruct a; simpl. po2. exact (IHp H). Qed. Lemma wf_prog_ext_path : forall (dcl' dcl'': dcl) (fds' : fds) (md_list : list md) (p : P), wf_prog ((cld_def dcl' (cl_dcl dcl'') fds' md_list) :: p) -> (exists cl', exists fds'', exists mds', In (cld_def dcl'' cl' fds'' mds') (path ((cld_def dcl' (cl_dcl dcl'') fds' md_list) :: p) (cl_dcl dcl'))). intros. inversion H; subst. assert (In (cld_def dcl' (cl_dcl dcl'') fds' md_list) (cld_def dcl' (cl_dcl dcl'') fds' md_list :: p)). simpl. po1. generalize (map_up _ _ _ _ (cld_def dcl' (cl_dcl dcl'') fds' md_list :: p) H0); clear H0; intros H0. rewrite <- (names'_eq_names (cld_def dcl' (cl_dcl dcl'') fds' md_list :: p) (cld_def dcl' (cl_dcl dcl'') fds' md_list :: p)) in H1. generalize (wf_prog2 _ _ _ H0 H2 H1); intros G1; simpl in G1. generalize (wf_class_list_ordered _ _ _ H0 H2); clear H0; intros H0; destruct H0; bd H0. rewrite names'_eq_names in H0; rewrite <- H5 in H0. generalize (In_names_In_p _ _ H0); intros; destruct H3; destruct H3; destruct H3. simpl in H3. bd H3. elimtype False; apply G1. inversion H3; apply refl_equal. rewrite names'_eq_names in H1. simpl in H1; bd H1. generalize (In_prog_In_path _ _ _ _ _ H3 H1); intros. exists x0; exists x1; exists x2. simpl; case (eq_nat_dec dcl' dcl'); intros. simpl; po2. elimtype False; apply n; apply refl_equal. Qed. Inductive ordered_p : P -> Prop := nil_p : ordered_p nil | cons_p : forall (p' : P) (cld' : cld) , ordered_p p' -> (exists cl', get_parent cld' = cl' /\ In cl' (names p') ) -> ordered_p (cons cld' p'). Lemma distinct_ordered_p : forall (p : P) (cld' : cld), In cld' p -> ordered_p p -> distinct _ (names p) -> get_parent cld' <> hd (get_parent cld') (names (cld' :: nil)). induction p; intros. simpl in H; elimtype False; apply H. destruct a; destruct cld'. simpl in *|-*. unfold not; intros. bd H. inversion H0; subst. destruct H6; bd H2; rewrite <- H6 in H2; clear H6. simpl in H2. inversion H; subst. bd H1; elimtype False; auto. inversion H0; bd H1. apply (IHp _ H H5 H1). simpl. exact H2. Qed. Lemma list_ordered_parent : forall (cld' : cld) (p : P), In cld' p -> ordered_p p -> (exists cl', get_parent cld' = cl' /\ In cl' (names p)). induction p; intros. simpl in H; elimtype False; exact H. inversion H0; subst. simpl in H. bd H. rewrite H in *|-*. destruct H4; bd H1. exists x. pa. destruct cld'. simpl. po2. generalize (IHp H H3); intros H1; destruct H1. bd H1. exists x; pa. destruct a. simpl. po2. Qed. Lemma ordered_wf_prog : forall (p l: P), wf_class_list (map (fun cld_ : cld => (l, cld_)) p) -> ordered_p p. induction p; intros. apply nil_p. destruct a. inversion H; subst. destruct H5; subst; bd H0. rewrite <- H5 in H0. apply cons_p. apply (IHp _ H4). exists x. pa. rewrite names'_eq_names in H0. rewrite H5 in H0. exact H0. Qed. Lemma wf_prog_ordered : forall (dcl' dcl'': dcl) (fds' : fds) (md_list : list md) (p : P), In (cld_def dcl' (cl_dcl dcl'') fds' md_list) p -> ordered_p p -> distinct _ (names p) -> (exists cl', exists fds', exists mds', In (cld_def dcl'' cl' fds' mds') (path p (cl_dcl dcl'))). intros. induction p. simpl in H; elimtype False; exact H. simpl in H; bd H. rewrite H in *|-*; simpl. case (eq_nat_dec dcl' dcl'); intros. simpl. inversion H0; clear H0. destruct H5; bd H0. simpl in H7; rewrite <- H7 in H0. generalize (In_names_In_p _ _ H0); intros H5; destruct H5; destruct H5; destruct H5. simpl in H1; bd H1. generalize (In_prog_In_path _ _ _ _ _ H5 H1); intros. exists x0; exists x1; exists x2; po2. elimtype False; apply n; apply refl_equal. inversion H0. destruct a; simpl in H1; bd H1. generalize (IHp H H4 H1); clear IHp; intros H6; destruct H6; destruct H6; destruct H6. simpl; case (eq_nat_dec dcl' d); intros. rewrite e in H. elimtype False; apply H8; apply (In_p_In_names _ _ _ _ _ H). exists x; exists x0; exists x1. exact H6. Qed. Lemma path_cl_object : forall (p : P), path p cl_object = nil. induction p. simpl. apply refl_equal. simpl. destruct a. apply refl_equal. Qed. Lemma field_eq_parent : forall (p : P) (cl' : cl) (dcl' : dcl) (fds' : fds) (md_list : list md), wf_prog p -> In (cld_def dcl' cl' fds' md_list) p -> fields p (cl_dcl dcl') = get_fs fds' ++ (fields p cl'). intros. inversion H; clear H; subst. generalize (ordered_wf_prog _ _ H3); clear H3; intros H3. induction cld_list. simpl in H0; elimtype False; apply H0. generalize (distinct_ordered_p _ _ H0 H3 H2); intros H8; simpl in H8. destruct a. simpl in H2, H0; inversion H3; subst. bd H0. rewrite H0. unfold fields. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). destruct cl'. case (eq_nat_dec d0 dcl'); intros. rewrite e in H8; elimtype False; apply H8; apply refl_equal. unfold ext_fs; simpl; fold (ext_fs (path cld_list (cl_dcl d0))). apply refl_equal. unfold ext_fs; simpl; fold (ext_fs (path cld_list cl_object)). rewrite path_cl_object. apply refl_equal. bd H2. generalize (IHcld_list H0 H2 H4); clear IHcld_list; intros. unfold fields. simpl. case (eq_nat_dec dcl' d); intros H7; try (elimtype False; apply H7; apply refl_equal). destruct cl'. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. unfold fields in H. rewrite H. destruct cl'. case (eq_nat_dec d0 d); intros. destruct H5; bd H1. simpl in H10; rewrite <- H10 in *|-*; clear H10. rewrite e in H0. generalize (list_ordered_parent _ _ H0 H4); intros. destruct H5. bd H5. simpl in H11; rewrite <- H11 in H5. elimtype False; apply H6; exact H5. apply refl_equal. rewrite path_cl_object; apply refl_equal. Qed. Lemma methods_eq_parent : forall (p : P) (cl' : cl) (dcl' : dcl) (fds' : fds) (md_list : list md), wf_prog p -> In (cld_def dcl' cl' fds' md_list) p -> methods p (cl_dcl dcl') = get_ms md_list ++ (methods p cl'). intros. inversion H; clear H; subst. generalize (ordered_wf_prog _ _ H3); clear H3; intros H3. induction cld_list. simpl in H0; elimtype False; apply H0. generalize (distinct_ordered_p _ _ H0 H3 H2); intros H8; simpl in H8. destruct a. simpl in H2, H0; inversion H3; subst. bd H0. rewrite H0. unfold methods. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). destruct cl'. case (eq_nat_dec d0 dcl'); intros. rewrite e in H8; elimtype False; apply H8; apply refl_equal. unfold ext_ms; simpl; fold (ext_ms (path cld_list (cl_dcl d0))). apply refl_equal. unfold ext_ms; simpl; fold (ext_ms (path cld_list cl_object)). rewrite path_cl_object. apply refl_equal. bd H2. generalize (IHcld_list H0 H2 H4); clear IHcld_list; intros. unfold methods. simpl. case (eq_nat_dec dcl' d); intros H7; try (elimtype False; apply H7; apply refl_equal). destruct cl'. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. unfold methods in H. rewrite H. destruct cl'. case (eq_nat_dec d0 d); intros. destruct H5; bd H1. simpl in H10; rewrite <- H10 in *|-*; clear H10. rewrite e in H0. generalize (list_ordered_parent _ _ H0 H4); intros. destruct H5. bd H5. simpl in H11; rewrite <- H11 in H5. elimtype False; apply H6; exact H5. apply refl_equal. rewrite path_cl_object; apply refl_equal. Qed. Lemma filter_mds_app : forall (m' : m) (mds1 mds2 : list md), filter_mds (mds1 ++ mds2) m' = (filter_mds mds1 m') ++ (filter_mds mds2 m'). induction mds1; intros. simpl; reflexivity. destruct a; unfold filter_mds at 1 2; destruct m; simpl. fold (filter_mds (mds1 ++ mds2) m'). fold (filter_mds mds1 m'). rewrite IHmds1. destruct (eq_nat_dec m m'); reflexivity. Qed. Lemma in_filtered : forall (mds' : list md) (md' : md) (m' : m), In md' (filter_mds mds' m') -> In md' mds'. induction mds'; simpl; try tauto; destruct a; destruct m. intros md' m'; case (eq_nat_dec m m'). simpl; intros; bd H. po1. po2; apply (IHmds' _ _ H). intros. po2; apply (IHmds' _ _ H). Qed. Lemma in_mtype_wf_prog : forall (p : P) (dcl' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md) (m' : m) (ty' : ty) (list_ty : list ty) (list_var : list var) (mb' : mb), wf_prog p -> In (cld_def dcl' cl' fds' mds') p -> mtype p (cl_dcl dcl') m' = Some (mty_def list_ty ty') -> find_menv p (cl_dcl dcl') m' = Some (menv_def list_var mb') -> In (md_def (ms_def ty' m' (map (fun (x: ty*var )=> vd_def (fst x) (snd x) ) (combine list_ty list_var))) mb') mds' \/ mtype p cl' m' = Some (mty_def list_ty ty'). intros. inversion H; clear H; subst. import (ordered_wf_prog _ _ H5). clear H5. generalize cld_list dcl' cl' fds' mds' m' ty' list_ty list_var mb' H0 H1 H2 H4 H; clear. induction cld_list; intros. simpl in H0; elimtype False; apply H0. import (distinct_ordered_p _ _ H0 H H4). destruct a. simpl in H2, H2, H0; inversion H; subst. bd H0. (****Break Point ***) generalize H2 H1; clear H2 H1. rewrite H0. unfold mtype; unfold find_menv. unfold get_md. unfold get_all_mds. destruct cl'. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). case (eq_nat_dec d0 dcl'); intros G7. simpl. fold (get_all_mds (path cld_list (cl_dcl d0))). rewrite (filter_mds_app). destruct (filter_mds mds' m'). simpl. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). fold (find_menv cld_list (cl_dcl d0) m'). intros. po2. simpl. po2. simpl. fold (get_all_mds (path cld_list (cl_dcl d0))). rewrite (filter_mds_app). caseEq (filter_mds mds' m'). simpl. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). fold (find_menv cld_list (cl_dcl d0) m'). intros. po2. simpl; intros. po1. inversion H2; inversion H5. assert (In m mds'). apply (in_filtered mds' m m'). rewrite H1; simpl; po1. inversion H11; inversion H10; destruct m. simpl in H13, H14; destruct m. inversion H13; inversion H14; subst. assert ( (map (fun x : ty * var => vd_def (fst x) (snd x)) (combine (get_vdstys l1) (get_vdsvars l1))) = l1). clear; induction l1. simpl; reflexivity. destruct a; simpl. rewrite IHl1; auto. rewrite H12. assert (m = m'). generalize H1; clear. induction mds'. simpl; intros; discriminate. simpl. destruct a; destruct m0. case (eq_nat_dec m0 m'); intros. inversion H1; subst. auto. apply (IHmds' H1). rewrite <- H15. exact H9. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). simpl. fold (get_all_mds (path cld_list cl_object)). rewrite (filter_mds_app). caseEq (filter_mds mds' m'). simpl. fold (get_md cld_list cl_object m'). fold (mtype cld_list cl_object m'). fold (find_menv cld_list cl_object m'). intros. elimtype False; generalize H2; clear; induction cld_list; unfold find_menv; simpl; intros. discriminate. destruct a. unfold get_md in H2. simpl in H2; discriminate. simpl; intros. po1. inversion H2; inversion H5. assert (In m mds'). apply (in_filtered mds' m m'). rewrite H1; simpl; po1. inversion H11; inversion H10; destruct m. simpl in H13, H14; destruct m. inversion H13; inversion H14; subst. assert ( (map (fun x : ty * var => vd_def (fst x) (snd x)) (combine (get_vdstys l1) (get_vdsvars l1))) = l1). clear; induction l1. simpl; reflexivity. destruct a; simpl. rewrite IHl1; auto. rewrite H12. assert (m = m'). generalize H1; clear. induction mds'. simpl; intros; discriminate. simpl. destruct a; destruct m0. case (eq_nat_dec m0 m'); intros. inversion H1; subst. auto. apply (IHmds' H1). rewrite <- H15. exact H9. cs (dcl' = d). import (In_names _ _ _ _ _ H0). simpl in H4; bd H4; elimtype False; apply H11; rewrite <- H5; exact H6. generalize H2 H1; clear H2 H1. unfold mtype; unfold find_menv. unfold get_md. simpl. case (eq_nat_dec dcl' d). intros; elimtype False; auto. fold (get_md cld_list (cl_dcl dcl') m'). fold (mtype cld_list (cl_dcl dcl') m'). fold (find_menv cld_list (cl_dcl dcl') m'). intros. destruct cl'. case (eq_nat_dec d0 d); intros. rewrite <- e in H8. simpl in H4; bd H4. import (list_ordered_parent _ _ H0 H7). bd H6. simpl in H12; rewrite <- H12 in H6. elimtype False; apply H10; rewrite <- e; exact H6. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). apply (IHcld_list _ _ _ _ _ _ _ _ _ H0 H1 H2); auto. simpl in H4; bd H4. simpl. simpl in H4; bd H4. inversion H. import (IHcld_list _ _ _ _ _ _ _ _ _ H0 H1 H2 H4 H11); bd H13. po1. elimtype False; generalize H13; clear; induction cld_list; intros; unfold mtype in H13; simpl in H13; try discriminate. destruct a. simpl in H13; discriminate. Qed. Lemma in_menv_wf_prog : forall (p : P) (dcl' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md) (m' : m) (ty' : ty) (list_ty : list ty) (list_var : list var) (mb' : mb), wf_prog p -> In (cld_def dcl' cl' fds' mds') p -> mtype p (cl_dcl dcl') m' = Some (mty_def list_ty ty') -> find_menv p (cl_dcl dcl') m' = Some (menv_def list_var mb') -> In (md_def (ms_def ty' m' (map (fun (x: ty*var )=> vd_def (fst x) (snd x) ) (combine list_ty list_var))) mb') mds' \/ find_menv p cl' m' = Some (menv_def list_var mb'). intros. inversion H; clear H; subst. import (ordered_wf_prog _ _ H5). clear H5. generalize cld_list dcl' cl' fds' mds' m' ty' list_ty list_var mb' H0 H1 H2 H4 H; clear. induction cld_list; intros. simpl in H0; elimtype False; apply H0. import (distinct_ordered_p _ _ H0 H H4). destruct a. simpl in H2, H2, H0; inversion H; subst. bd H0. generalize H2 H1; clear H2 H1. rewrite H0. unfold mtype; unfold find_menv. unfold get_md. unfold get_all_mds. destruct cl'. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). case (eq_nat_dec d0 dcl'); intros G7. simpl. fold (get_all_mds (path cld_list (cl_dcl d0))). rewrite (filter_mds_app). destruct (filter_mds mds' m'). simpl. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). fold (find_menv cld_list (cl_dcl d0) m'). intros. po2. simpl. po2. simpl. fold (get_all_mds (path cld_list (cl_dcl d0))). rewrite (filter_mds_app). caseEq (filter_mds mds' m'). simpl. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). fold (find_menv cld_list (cl_dcl d0) m'). intros. po2. simpl; intros. po1. inversion H2; inversion H5. assert (In m mds'). apply (in_filtered mds' m m'). rewrite H1; simpl; po1. inversion H11; inversion H10; destruct m. simpl in H13, H14; destruct m. inversion H13; inversion H14; subst. assert ( (map (fun x : ty * var => vd_def (fst x) (snd x)) (combine (get_vdstys l1) (get_vdsvars l1))) = l1). clear; induction l1. simpl; reflexivity. destruct a; simpl. rewrite IHl1; auto. rewrite H12. assert (m = m'). generalize H1; clear. induction mds'. simpl; intros; discriminate. simpl. destruct a; destruct m0. case (eq_nat_dec m0 m'); intros. inversion H1; subst. auto. apply (IHmds' H1). rewrite <- H15. exact H9. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). simpl. fold (get_all_mds (path cld_list cl_object)). rewrite (filter_mds_app). caseEq (filter_mds mds' m'). simpl. fold (get_md cld_list cl_object m'). fold (mtype cld_list cl_object m'). fold (find_menv cld_list cl_object m'). intros. elimtype False; generalize H2; clear; induction cld_list; unfold find_menv; simpl; intros. discriminate. destruct a. unfold get_md in H2. simpl in H2; discriminate. simpl; intros. po1. inversion H2; inversion H5. assert (In m mds'). apply (in_filtered mds' m m'). rewrite H1; simpl; po1. inversion H11; inversion H10; destruct m. simpl in H13, H14; destruct m. inversion H13; inversion H14; subst. assert ( (map (fun x : ty * var => vd_def (fst x) (snd x)) (combine (get_vdstys l1) (get_vdsvars l1))) = l1). clear; induction l1. simpl; reflexivity. destruct a; simpl. rewrite IHl1; auto. rewrite H12. assert (m = m'). generalize H1; clear. induction mds'. simpl; intros; discriminate. simpl. destruct a; destruct m0. case (eq_nat_dec m0 m'); intros. inversion H1; subst. auto. apply (IHmds' H1). rewrite <- H15. exact H9. cs (dcl' = d). import (In_names _ _ _ _ _ H0). simpl in H4; bd H4; elimtype False; apply H11; rewrite <- H5; exact H6. generalize H2 H1; clear H2 H1. unfold mtype; unfold find_menv. unfold get_md. simpl. case (eq_nat_dec dcl' d). intros; elimtype False; auto. fold (get_md cld_list (cl_dcl dcl') m'). fold (mtype cld_list (cl_dcl dcl') m'). fold (find_menv cld_list (cl_dcl dcl') m'). intros. destruct cl'. case (eq_nat_dec d0 d); intros. rewrite <- e in H8. simpl in H4; bd H4. import (list_ordered_parent _ _ H0 H7). bd H6. simpl in H12; rewrite <- H12 in H6. elimtype False; apply H10; rewrite <- e; exact H6. fold (get_md cld_list (cl_dcl d0) m'). fold (mtype cld_list (cl_dcl d0) m'). apply (IHcld_list _ _ _ _ _ _ _ _ _ H0 H1 H2); auto. simpl in H4; bd H4. simpl. simpl in H4; bd H4. inversion H. import (IHcld_list _ _ _ _ _ _ _ _ _ H0 H1 H2 H4 H11); bd H13. po1. elimtype False; generalize H13; clear; induction cld_list; intros; unfold mtype in H13; simpl in H13; try discriminate. destruct a. simpl in H13; discriminate. Qed. Lemma nil_fields : forall (p : P), fields p cl_object = nil. destruct p; unfold fields; simpl; try destruct c; unfold ext_fs; simpl; apply refl_equal. Qed. Lemma subtype_fields : forall (cl1 cl2 : cl) (ty1 ty2 : ty )(p : P) (f' : f) , ty1 = ty_def cl1 -> ty2 = ty_def cl2 -> sty_one p ty1 ty2 -> wf_prog p -> In f' (fields p cl2) -> In f' (fields p cl1). intros. generalize cl1 cl2 f' H H0 H2 H3; clear cl1 cl2 f' H0 H H2 H3. induction H1; intros. subst. inversion H; subst; clear H. rewrite (field_eq_parent _ _ _ _ _ H2 H5). apply in_or_app. po2. inversion H0. rewrite <- H4 in H3. rewrite nil_fields in H3. inversion H3. inversion H0; inversion H1; congruence. destruct ty'. apply (IHsty_one1 cl1 c); auto. apply (IHsty_one2 c cl2); auto. Qed. Lemma wf_fwrite_lookupl : forall (p : P) (g : G) (l : L) (h : H) (x' y: x) (f' :f), wf_stmt p g (s_write x' f' y) -> wf_stck p g h l -> (exists v1, (XMap.find x' l = Some v1 /\ ( forall (oid' : oid), v1 = v_oid oid' -> exists clm, (NatMap.find (oid') h = Some clm))) /\ exists v2, XMap.find y l = Some v2). intros. destruct H0. inversion H; subst. inversion H9; subst. assert (XMap.mem x' G5 = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty_def cl5). apply (XMap.find_2 H7). generalize (H0 _ H4); intros G0; destruct G0; bd H6. inversion H9; subst. assert (XMap.mem y G5 = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists ty1. apply (XMap.find_2 H10). generalize (H0 _ H15); intros G0; destruct G0; bd H16. inversion H6; subst. exists v_null; pa. pa. intros; discriminate. inversion H16; subst. exists v_null; apply refl_equal. exists (v_oid oid5); apply refl_equal. exists (v_oid oid5); pa. pa. intros. inversion H17. rewrite H22 in H23. destruct (NatMap.find oid' H5). exists p; apply refl_equal. inversion H23; subst. discriminate. inversion H16; subst. exists v_null; apply refl_equal. exists (v_oid oid0); apply refl_equal. Qed. Fixpoint build_big_list (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v) {struct list_x} : list (x*var*var*v) := match list_x, list_var1, list_var2, list_v with cons x' lx, cons v1' lv1, cons v2' lv2, cons v' lv => cons (((x', v1'), v2'), v') (build_big_list lx lv1 lv2 lv) | _, _, _, _ => nil end. Lemma map_snd_fst_fst : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v), length list_var1 = length (build_big_list list_x list_var1 list_var2 list_v) -> (map (fun (yp :x*var*var*v) => (snd (fst (fst yp)))) (build_big_list list_x list_var1 list_var2 list_v)) = list_var1. induction list_x; intros. simpl in *|-*. destruct list_var1; simpl in H. apply refl_equal. simpl in H; discriminate. destruct list_var1; destruct list_var2; destruct list_v; simpl in *|-*; try apply refl_equal; try discriminate. inversion H. rewrite IHlist_x. apply refl_equal. exact H1. Qed. Lemma map_fst_fst_fst : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v), length list_x = length (build_big_list list_x list_var1 list_var2 list_v) -> (map (fun (yp :x*var*var*v) => (fst (fst (fst yp)))) (build_big_list list_x list_var1 list_var2 list_v)) = list_x. induction list_x; intros. simpl in *|-*. apply refl_equal. destruct list_var1; destruct list_var2; destruct list_v; simpl in *|-*; try apply refl_equal; try discriminate. inversion H. rewrite IHlist_x. apply refl_equal. exact H1. Qed. Lemma map_snd_fst : forall (list_var2 : list var) (list_x : list x) (list_var1 : list var) (list_v : list v), length list_var2 = length (build_big_list list_x list_var1 list_var2 list_v) -> (map (fun (yp :x*var*var*v) => x_var (snd (fst yp)))) (build_big_list list_x list_var1 list_var2 list_v) = map (fun (var' : var) => x_var var') list_var2. induction list_var2; intros; destruct list_var1; destruct list_x; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. inversion H; clear H. rewrite IHlist_var2. apply refl_equal. exact H1. Qed. Lemma map_snd_fst' : forall (list_var2 : list var) (list_x : list x) (list_var1 : list var) (list_v : list v), length list_var2 = length (build_big_list list_x list_var1 list_var2 list_v) -> (map (fun (yp :x*var*var*v) => (snd (fst yp)))) (build_big_list list_x list_var1 list_var2 list_v) = map (fun var' => var') list_var2. induction list_var2; intros; destruct list_var1; destruct list_x; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. inversion H; clear H. rewrite IHlist_var2. apply refl_equal. exact H1. Qed. Lemma map_snd_fst'' : forall (list_var2 : list var) (list_x : list x) (list_var1 : list var) (list_v : list v), length list_var2 = length (build_big_list list_x list_var1 list_var2 list_v) -> (map (fun (yp :x*var*var*v) => (snd (fst yp)))) (build_big_list list_x list_var1 list_var2 list_v) = list_var2. induction list_var2; intros; destruct list_var1; destruct list_x; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. inversion H; clear H. rewrite IHlist_var2. apply refl_equal. exact H1. Qed. Lemma map_fst_pair : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v) (l : L), length list_var1 = length (build_big_list list_x list_var1 list_var2 list_v) -> length list_x = length list_var1 -> (map (fun (yp:x*var*var*v) => ( XMap.find (fst (fst (fst yp))) l, snd yp)) (build_big_list list_x list_var1 list_var2 list_v)) = combine (map (fun (x' : x) => XMap.find x' l) list_x) list_v. induction list_x; intros. simpl; apply refl_equal. destruct list_var1; destruct list_var2; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. rewrite IHlist_x. apply refl_equal. inversion H; apply refl_equal. inversion H0. rewrite H2; apply refl_equal. Qed. Lemma map_fst_pair' : forall x0 x1 x2 x3, length x0 = length (build_big_list x0 x1 x2 x3) -> length x3 = length (build_big_list x0 x1 x2 x3) -> map (fun yp : x * var * var * v => (fst (fst (fst yp)), snd yp)) (build_big_list x0 x1 x2 x3) = map (fun yp : x * v => (fst yp, snd yp)) (combine x0 x3). induction x0; intros. simpl; reflexivity. destruct x1; destruct x2; destruct x3; simpl in H; try discriminate. simpl. rewrite IHx0; try reflexivity. inversion H; reflexivity. simpl in H0; inversion H0; reflexivity. Qed. Lemma map_snd_fst_pair : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v) (l : L), length list_var2 = length (build_big_list list_x list_var1 list_var2 list_v) -> length list_v = length list_var2 -> fold_right (fun (yp:x*var*var*v) m=> XMap.add (x_var (snd (fst yp))) (snd yp) m) l (build_big_list list_x list_var1 list_var2 list_v) = fold_right (fun (yp:var*v) m=> XMap.add (x_var (fst yp)) (snd yp) m) l (combine list_var2 list_v). induction list_x; intros. simpl; simpl in H; rewrite H in H0. destruct list_var2; destruct list_v; try apply refl_equal; discriminate. destruct list_var1; destruct list_var2; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. rewrite IHlist_x. apply refl_equal. inversion H; apply refl_equal. inversion H0; apply refl_equal. Qed. Lemma map_snd_fst_fst_pair : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v), length list_var1 = length (build_big_list list_x list_var1 list_var2 list_v) -> length list_var2 = length list_var1 -> fold_right (fun (yp : x*var*var*v) m => XMap.add (x_var (snd (fst (fst yp)))) (x_var (snd (fst yp))) m) (XMap.empty x) (build_big_list list_x list_var1 list_var2 list_v) = fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine list_var1 list_var2). induction list_x; intros; destruct list_var1; destruct list_var2; destruct list_v; simpl in H; simpl; try apply refl_equal; try discriminate. simpl. rewrite IHlist_x. apply refl_equal. inversion H; clear H. apply refl_equal. inversion H0. apply refl_equal. Qed. Lemma wf_prog_wf_cld : forall (p p': P) (cld' : cld), wf_class_list (map (fun x => (p', x)) p) -> In cld' p -> wf_class p' cld'. induction p; intros. simpl in H0; elimtype False; apply H0. simpl in H. simpl in H0; bd H0. rewrite H0 in H; inversion H; subst. exact H4. inversion H; apply IHp; auto. Qed. Lemma not_in_ext_ms : forall (p : P) (cl' : cl) (m' : m), ~In m' (ext_ms (path p cl')) -> mtype p cl' m' = None. unfold mtype; unfold get_md. intros. induction (path p cl'); intros. simpl; reflexivity. destruct a; unfold ext_ms in H; simpl in H. fold (ext_ms l) in H. unfold get_all_mds; simpl; fold (get_all_mds l). rewrite filter_mds_app. assert ( ~ In m' (get_ms l0) /\ ~ In m' (ext_ms l)). pa; unfold not; intro; apply H; apply in_or_app. po1. po2. bd H0; clear H. caseEq (filter_mds l0 m'); intros. simpl; apply (IHl H0). elimtype False; apply H3. import (in_filtered l0 m m'). rewrite H in H1. simpl in H1. assert (In m l0). apply H1; po1. clear H1. destruct m; destruct m. assert (m = m'). generalize H; clear. induction l0. simpl; intros. discriminate. destruct a; destruct m1; simpl. case (eq_nat_dec m1 m'); intros. inversion H. congruence. apply (IHl0 H). rewrite H1 in H2; generalize H2; clear; induction l0. simpl; auto. simpl; intros. bd H2. rewrite H2; po1. po2. apply (IHl0 H2). Qed. Lemma path_eq_parent : forall (p : P) (cl' : cl) (dcl' : dcl) (fds' : fds) (md_list : list md), wf_prog p -> In (cld_def dcl' cl' fds' md_list) p -> path p (cl_dcl dcl') = (cld_def dcl' cl' fds' md_list) :: (path p cl'). intros. inversion H; clear H; subst. generalize (ordered_wf_prog _ _ H3); clear H3; intros H3. induction cld_list. simpl in H0; elimtype False; apply H0. generalize (distinct_ordered_p _ _ H0 H3 H2); intros H8; simpl in H8. destruct a. simpl in H2, H0; inversion H3; subst. bd H0. rewrite H0. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; apply refl_equal). destruct cl'. case (eq_nat_dec d0 dcl'); intros. rewrite e in H8; elimtype False; apply H8; apply refl_equal. apply refl_equal. rewrite path_cl_object. apply refl_equal. bd H2. generalize (IHcld_list H0 H2 H4); clear IHcld_list; intros. simpl. case (eq_nat_dec dcl' d); intros H7; try (elimtype False; apply H7; apply refl_equal). destruct cl'. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. rewrite H7 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros. elimtype False; apply H6; exact H1. rewrite H. destruct cl'. case (eq_nat_dec d0 d); intros. destruct H5; bd H1. simpl in H10; rewrite <- H10 in *|-*; clear H10. rewrite e in H0. generalize (list_ordered_parent _ _ H0 H4); intros. destruct H5. bd H5. simpl in H11; rewrite <- H11 in H5. elimtype False; apply H6; exact H5. apply refl_equal. rewrite path_cl_object; apply refl_equal. Qed. Lemma mtype_in_prog : forall (p : P) (cl' : cl) (m' : m) (mty' : mty), mtype p cl' m' = Some mty' -> exists dcl', cl' = cl_dcl dcl' /\ exists cl'', exists fds', exists mds', In (cld_def dcl' cl'' fds' mds') (path p cl'). intros; unfold mtype in H; unfold get_md in H. destruct cl'. exists d; pa. induction p. simpl in H; discriminate. destruct a; generalize H; clear H; simpl; case (eq_nat_dec d d0); intros. simpl; exists c; exists f; exists l; po1; congruence. auto. rewrite path_cl_object in *|-*; simpl in H; discriminate. Qed. Lemma mtype_in_md : forall (dcl' : dcl) (cl' : cl) (fds' : fds) (mds' : list md) (p : P) (m' : m) (ty' : ty) (vd_list : list vd) (mb' : mb), In (cld_def dcl' cl' fds' mds') p-> In (md_def (ms_def ty' m' vd_list) mb') mds' -> distinct _ (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds') -> distinct _ (names p) -> mtype p (cl_dcl dcl') m' = Some (mty_def (get_vdstys vd_list) ty'). induction p; intros. simpl in H; contradiction. destruct a; simpl in H; bd H. inversion H; subst. unfold mtype; unfold get_md; simpl. case (eq_nat_dec dcl' dcl'); intros. generalize H0 H1; clear; induction mds'; intros. simpl in H0; contradiction. destruct a; simpl in H0; bd H0. inversion H0; subst. simpl. case (eq_nat_dec m' m'); intros; simpl. reflexivity. congruence. simpl. simpl in H1; bd H1. destruct m; case (eq_nat_dec m m'); intros; simpl. subst; elimtype False; apply H3; generalize H0; clear; induction mds'; intros. simpl in H0; contradiction. simpl in H0; destruct a; bd H0. inversion H0; simpl; po1. simpl; po2; auto. auto. congruence. unfold mtype; unfold get_md; simpl; case (eq_nat_dec dcl' d); intros. simpl in H2; bd H2; subst. import (In_p_In_names _ _ _ _ _ H). congruence. rewrite <- (IHp _ _ _ _ H H0); auto. simpl in H2; bd H2. Qed. Lemma in_path_in_prog : forall (p : P) (cl' : cl) (cld' : cld), In cld' (path p cl') -> In cld' p. induction p; simpl; intros. elimtype False; apply H. destruct a; destruct cl'. generalize H; clear H. case (eq_nat_dec d0 d); intros. simpl in H. simpl in H; bd H; auto. po2; apply (IHp _ _ H). po2; apply (IHp _ _ H). simpl in H; elimtype False; apply H. Qed. Lemma path_eq_self : forall (p : P) (dcl' dcl'': dcl) (cl' : cl) (fds' : fds) (mds' : list md) (l : list cld), path p (cl_dcl dcl') = cld_def dcl'' cl' fds' mds' :: l -> dcl' = dcl''. induction p. simpl; intros; discriminate. simpl; destruct a; intro; case (eq_nat_dec dcl' d); intros. inversion H; congruence. apply (IHp _ _ _ _ _ _ H). Qed. Lemma in_path_sty : forall (p : P) (dcl' dcl'' : dcl) (cl' cl'' : cl) (fds' fds'' : fds) (mds' mds'' : list md), wf_prog p -> In (cld_def dcl' cl' fds' mds') p -> In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl dcl')) -> sty_one p (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')). intros p dcl'; assert (exists l, l = path p (cl_dcl dcl')). exists (path p (cl_dcl dcl')); reflexivity. bd H. intros; generalize p dcl' dcl'' cl' cl'' fds' fds'' mds' mds'' H H0 H1 H2; clear. induction x; intros. rewrite <- H in H2; simpl in H2; contradiction. rewrite <- H in H2; destruct a; simpl in H2; bd H2. rewrite (path_eq_self _ _ _ _ _ _ _ (sym_eq H)) in *|-*. inversion H2; subst; apply (sty_reflexive _ _ _ _ _ H1). rewrite (path_eq_parent _ _ _ _ _ H0 H1) in H. inversion H; subst. inversion H. destruct cl'. inversion H0; subst. import (ordered_wf_prog _ _ H5). import (wf_prog_ordered _ _ _ _ _ H1 H3 H4). bd H6. import (in_path_in_prog _ _ _ H6). import (IHx _ _ _ _ _ _ _ _ _ (refl_equal _) H0 H7 H2). apply (sty_transitive cld_list (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')) (ty_def (cl_dcl d))). apply sty_from_direct. apply (sty_dir _ _ _ _ _ H1). apply H8. rewrite path_cl_object in H2; simpl in H2; contradiction. Qed. Lemma in_path_sty' : forall (p : P) (dcl': dcl) (cl' : cl), ordered_p p -> distinct _ (names p) -> sty_one p (ty_def (cl_dcl dcl')) (ty_def cl') -> exists cl'', exists fds'', exists mds'', In (cld_def dcl' cl'' fds'' mds'') (path p (cl_dcl dcl')). intros p dcl'; assert (exists l, l = path p (cl_dcl dcl')). exists (path p (cl_dcl dcl')); reflexivity. bd H. intros; generalize p dcl' cl' H H0 H1 H2; clear. induction x; intros. elimtype False. assert (exists ty', ty' = ty_def (cl_dcl dcl')). exists (ty_def (cl_dcl dcl')); auto. assert (exists ty', ty' = ty_def cl'). exists (ty_def cl'); auto. bd H3; bd H4; rewrite <- H3 in H2; rewrite <- H4 in H2. generalize dcl' cl' H H1 H0 H3 H4; clear dcl' cl' H H1 H0 H3 H4. induction H2; intros; subst. inversion H. import (In_prog_In_path _ _ _ _ _ H6 H1). rewrite <- H0 in H7; simpl in H7; contradiction. discriminate. inversion H3; subst. import (In_prog_In_path _ _ _ _ _ H H1). rewrite <- H0 in H5; simpl in H5; contradiction. destruct ty'; auto. apply (IHsty_one1 dcl' c); auto. import (in_path_in_prog p (cl_dcl dcl') a). rewrite <- H in H3; simpl in H3. assert (a=a \/ In a x). po1. import (H3 H4). destruct a; rewrite (path_eq_self _ _ _ _ _ _ _ (sym_eq H)) in *|-*. exists c; exists f; exists l. apply (In_prog_In_path); auto. Qed. Lemma sty_mtype : forall (p : P) (cl' cl'' : cl) (m' : m) (mty' : mty) (ty' ty'' : ty), ty' = ty_def cl' -> ty'' = ty_def cl'' -> sty_one p ty' ty'' -> mtype p cl'' m' = Some mty' -> wf_prog p -> mtype p cl' m' = Some mty'. intros. generalize cl' cl'' m' mty' H H2 H3 H0; clear cl' cl'' m' mty' H H2 H3 H0. induction H1; intros. rewrite H1 in H; rewrite H0 in H. inversion H3; inversion H; subst. import (wf_prog_wf_cld _ _ _ H6 H11). inversion H0; clear H13; subst. cs (exists ty', exists vd_list, exists mb', In (md_def (ms_def ty' m' vd_list) mb') md_list). bd H1. cs (In m' (methods cld_list cl'')). import (H19 _ _ _ _ H1 H4). import (mtype_in_md _ _ _ _ _ _ _ _ _ H11 H1 H18 H5). congruence. elimtype False; apply H4; generalize H2; clear; intros. unfold mtype in H2; unfold get_md in H2. unfold methods. induction (path cld_list cl''). simpl in H2; discriminate. destruct a; unfold get_all_mds in H2; unfold ext_ms; fold (ext_ms l); simpl in *|-*. fold (ext_ms l). fold (get_all_mds l) in H2. induction l0. simpl in *|-*; auto. simpl in *|-*. destruct a; destruct m; generalize H2; clear H2; case (eq_nat_dec m m'); intros. po1. po2. auto. destruct mty'. rewrite <- H2; unfold mtype; unfold get_md; rewrite (path_eq_parent _ _ _ _ _ H3 H11). generalize H1 H18; clear; intros; induction md_list. simpl; auto. simpl; destruct a; destruct m; case (eq_nat_dec m m'); intros. bd H1; import (H1 t); bd H; import (H l); bd H0; import (H0 m0); bd H2. congruence. apply IHmd_list; auto. unfold not; intros; apply H1; bd H. exists x; exists x0; exists x1; simpl; po2. simpl in H18; bd H18. inversion H0; inversion H; subst. exact H2. congruence. caseEq ty'; intros. import (IHsty_one2 _ _ _ _ H1 H2 H3 H0). import (IHsty_one1 _ _ _ _ H H4 H3 H1). exact H5. Qed. Lemma find_menv_mtype_length : forall (p : P) (cl' : cl) (m' : m) (l0 : list var) (mb' : mb) (ty' : ty) (tys' : tys), find_menv p cl' m' = Some (menv_def l0 mb') -> mtype p cl' m' = Some (mty_def tys' ty') -> length tys' = length l0. intros. unfold find_menv in H; unfold mtype in H0. destruct (get_md p cl' m'); inversion H0; inversion H; clear H0 H. unfold ext_mty in H2; unfold ext_menv in H3. destruct m; destruct m. inversion H2; inversion H3. clear. induction l. simpl; apply refl_equal. simpl; rewrite IHl; apply refl_equal. Qed. Lemma length_build_big_list : forall (list_x : list x) (list_var1 list_var2 : list var) (list_v : list v), length list_x = length list_var2 -> length list_v = length list_x -> length list_var1 = length list_x -> length (build_big_list list_x list_var1 list_var2 list_v) = length list_x. induction list_x. simpl; congruence. simpl; intros. destruct list_var2; destruct list_var1; destruct list_v; simpl in *|-*; try discriminate. rewrite IHlist_x; auto. Qed. Theorem progress : forall (p : P) (g : G) (l : L) (h : H) (ss : Ss), ss <> nil -> wf_config p g (config_normal l h ss) ->exists config', reduce (config_normal l h ss) p config'. intros; destruct ss. elimtype False; unfold not in H; apply H; apply refl_equal. clear H. destruct s. (*** Var Assign ***) inversion H0; clear H0; simpl in H8; inversion H8; clear H8; 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. inversion H0; subst. inversion H9; subst. generalize (wf_assign_lookupl _ _ _ _ _ _ H2 H8); intros H10; destruct H10. exists (config_normal (XMap.add (x_var v) (x0) l) h ss). apply var_assign; auto. (*** Field Read ***) inversion H0; subst. inversion H9; subst. generalize (wf_fread_lookuplh _ _ _ _ _ _ _ H2 H8); intros H; destruct H; bd H. destruct x0. (*** Field Read NPE ***) exists (config_npe l h). apply field_read_npe; exact H5. (*** Field Read No NPE ***) generalize (H o (refl_equal _)); clear H; intros H; destruct H; bd H. inversion H2. inversion H7. assert (NatMap.mem o h = true). apply NatMap.mem_1. unfold NatMap.In; unfold NatMap.Raw.PX.In; exists x0. apply (NatMap.find_2 H10). generalize (H18 _ H21); clear H18; intros H18; destruct H18; bd H18. rewrite H10 in H24. inversion H24. rewrite H14 in H. assert (ftype p cl5 f <> None). unfold not; intros H39; rewrite H15 in H39; discriminate. generalize (proj1 (ftype_in_fields _ _ _) H22); intros. rewrite H23 in *|-*. inversion H. inversion H27. inversion H28. generalize (subtype_fields _ _ _ _ _ _ (sym_eq H34) (sym_eq H35) H29 H3 H26); intros. generalize (H18 _ H33); clear H18; intros H18; destruct H18; bd H18. rewrite H10 in H18. inversion H18. exists (config_normal (XMap.add (x_var v) v_null l) h ss). apply (field_read _ h v _ f ss p v_null o H5). rewrite H10; rewrite H37; 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 H5). rewrite H10; rewrite H37; apply refl_equal. (*** Field Write NPE***) inversion H0. inversion H9. generalize (wf_fwrite_lookupl _ _ _ _ _ _ _ H12 H8); intros H16; bd H16. destruct x1. exists (config_npe l h). apply field_write_npe; exact H20. (*** Field Write ***) generalize (H19 o (refl_equal _)); clear H19; intros H19. destruct H19. exists (config_normal l (match (NatMap.find o h) with None => h | Some tyfs => NatMap.add o (fst tyfs, (NatMap.add f x2 (snd tyfs))) h end) ss). apply field_write; auto. (*** Method Call NPE***) inversion H0. inversion H9; subst. import (ex_fresh_lookup_list' l (S (length l0))); bd H. import (wf_tl_valid_lookup _ _ _ _ _ _ _ _ H12 H8); bd H1. inversion H12; subst. inversion H8; subst. assert (XMap.mem x g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty_def cl5). apply (XMap.find_2 H17). import (H6 _ H2); clear H6; bd H11; inversion H11. exists (config_npe l h). apply mcall_npe; auto. (*** Method Call***) caseEq (NatMap.find oid5 h); intros; rewrite H25 in H23; inversion H23; subst; try discriminate. inversion H26; inversion H27. rewrite <- H22 in H28; rewrite <- H21 in H28. rewrite H21 in H28; destruct ty5; rewrite H17 in H14; inversion H14; rewrite <- H24 in H28. import (sty_mtype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _) H28 H18 H3). import (mtype_find_menv _ _ _ _ H6); bd H29. destruct x3; destruct m0. import (find_menv_mtype_length _ _ _ _ _ _ _ H29 H6). assert (length (map (fun y : lj.x * ty => fst y) y_ty_list) = length (map (fun y : lj.x * ty => snd y) y_ty_list)). clear; induction y_ty_list. simpl; apply refl_equal. simpl; rewrite IHy_ty_list; apply refl_equal. rewrite <- H31 in H30. destruct x0; simpl in H4; try discriminate; inversion H4. import (length_build_big_list (map (fun y : lj.x * ty => fst y) y_ty_list) l0 x0 x1 (sym_eq H33) H1 (sym_eq H30)). exists (config_normal (XMap.add (x_var v0) (v_oid oid5) (fold_right (fun (yp:var*lj.v) m=> XMap.add (x_var (fst yp)) (snd yp) m) l (combine x0 x1))) h (app (unmake_list_s (tr_Ss ( XMap.add x_this (x_var v0) (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj.x) (combine l0 x0)) ) (make_list_s s))) ((s_ass v (tr_x ( XMap.add x_this (x_var v0) (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj.x) (combine l0 x0))) x3 )) :: ss))). rewrite <- (map_fst_fst_fst (map (fun y : lj.x * ty => fst y) y_ty_list) l0 x0 x1); auto. apply (mcall (build_big_list (map (fun y : lj.x * ty => fst y) y_ty_list) l0 x0 x1) l h v x m ss p ( XMap.add (x_var v0) (v_oid oid5) (fold_right (fun (yp:var*lj.v) m=> XMap.add (x_var (fst yp)) (snd yp) m) l (combine x0 x1))) ( XMap.add x_this (x_var v0) (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj.x) (combine l0 x0))) s (tr_x ( XMap.add x_this (x_var v0) (fold_right (fun (yp : var*var) m => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj.x) (combine l0 x0))) x3 ) cl5 v0 x3 oid5 p0 (sym_eq H13)); auto. inversion H21. rewrite H35; rewrite map_snd_fst_fst. exact H29. congruence. rewrite map_snd_fst. generalize H5; clear; induction x0; simpl; intros; auto. bd H5. pa. unfold not in *|-*; intros; apply H2. generalize H; clear; intros. induction x0; simpl in *|-*. exact H. bd H. inversion H; po1. po2. apply (IHx0 H). apply (IHx0). simpl; pa. congruence. intros. rewrite map_snd_fst in H34. assert (forall var', In var' x0 -> ~XMap.In (x_var var') l). intros; apply H. simpl; po2. generalize H34 H35; clear; intros H25 H. induction x0. simpl in H25; elimtype False; apply H25. simpl in H25. bd H25. rewrite <- H25; apply H; simpl; po1. apply IHx0; auto. intros; apply H; simpl; po2. congruence. apply H. simpl; po1. rewrite map_snd_fst'. simpl in H5; bd H5. generalize H36; clear; induction x0. simpl; tauto. intros. simpl in H36; bd H36. unfold not; simpl; intros H; bd H. simpl in H; bd H. apply (IHx0 H0 H). congruence. generalize x0 x1 l0 H10; clear. induction (map (fun y : x * ty => fst y) y_ty_list); intros. simpl; apply valid_lookup_nil. simpl in H10. destruct l1; destruct x0; destruct x1; simpl; try apply valid_lookup_nil. inversion H10; subst. apply (valid_lookup_cons _ _ _ (map (fun yp : x * var * var * lj.v => (fst (fst (fst yp)), snd yp)) (build_big_list l0 l1 x0 x1)) H2). apply IHl0; auto. rewrite <- (map_snd_fst_pair (map (fun y : lj.x * ty => fst y) y_ty_list) l0 x0 x1 l); congruence. rewrite <- (map_snd_fst_fst_pair (map (fun y : lj.x * ty => fst y) y_ty_list) l0 x0 x1); congruence. (*** If ***) inversion H0; subst. inversion H9; subst. assert (exists v1, XMap.find x l = Some v1 /\ exists v2, XMap.find x0 l = Some v2). inversion H2. bd H11. inversion H11; inversion H8; subst. assert (XMap.mem x g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty5). apply (XMap.find_2 H15). assert (XMap.mem x0 g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty'). apply (XMap.find_2 H16). import (H22 _ H); import (H22 _ H1); bd H4; bd H5. inversion H4; subst. exists v_null; pa. inversion H5; subst. exists v_null; apply refl_equal. exists (v_oid oid5); apply refl_equal. exists (v_oid oid5); pa. inversion H5; subst. exists v_null; apply refl_equal. exists (v_oid oid0); apply refl_equal. inversion H11; inversion H8; subst. assert (XMap.mem x g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty'). apply (XMap.find_2 H16). assert (XMap.mem x0 g = true). apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists (ty5). apply (XMap.find_2 H15). import (H22 _ H); import (H22 _ H1); bd H4; bd H5. inversion H4; subst. exists v_null; pa. inversion H5; subst. exists v_null; apply refl_equal. exists (v_oid oid5); apply refl_equal. exists (v_oid oid5); pa. inversion H5; subst. exists v_null; apply refl_equal. exists (v_oid oid0); apply refl_equal. bd H. cs (x1 = x2). exists (config_normal l h (s1 :: ss)). apply (if_true _ h _ _ s1 s2 ss p _ _ H5 H H1). exists (config_normal l h (s2 :: ss)). apply (if_false _ h _ _ s1 s2 ss p _ _ H5 H H1). (*** Block ***) simpl. exists (config_normal l h (app (unmake_list_s l0) ss)). apply block. Qed. Lemma MapsTo_mem : forall (x' : x) (ty' : ty) (g : G), XMap.MapsTo x' ty' g -> XMap.mem x' g = true. intros. apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists ty'. exact H. Qed. Lemma XMapsTo_mem2 : forall (x' : x) (g : G), XMap.mem x' g = true -> exists ty', XMap.MapsTo x' ty' g. intros. import (XMap.mem_2 H). unfold XMap.In in H0; unfold XMap.Raw.PX.In in H0; destruct H0. exists x; exact H0. Qed. Lemma NatMapsTo_mem : forall (x' : nat) y (h : H), NatMap.MapsTo x' y h -> NatMap.mem x' h = true. intros. apply NatMap.mem_1. unfold NatMap.In; unfold NatMap.Raw.PX.In; exists y. exact H. Qed. Lemma NatMapsTo_mem2 : forall (x' : nat) (h : H), NatMap.mem x' h = true -> exists y', NatMap.MapsTo x' y' h. intros. import (NatMap.mem_2 H). unfold XMap.In in H0; unfold XMap.Raw.PX.In in H0; destruct H0. exists x; exact H0. Qed. Lemma sty_option_In_p : forall (p : P) (dcl' : dcl) (cl' : cl), sty_option p (Some (ty_def (cl_dcl dcl'))) (Some (ty_def cl')) -> exists cl'', exists fds, exists mds, In (cld_def dcl' cl'' fds mds) p. intros. inversion H. subst; clear H. inversion H0; inversion H1; clear H1 H0. generalize dcl' cl' H3 H4; clear dcl' cl' H3 H4. induction H2; intros. inversion H; subst. exists cl'; exists fds5; exists md_list; congruence. inversion H3. exists cl'; exists fds'; exists mds; congruence. destruct ty'; import (IHsty_one1 _ _ H3 (refl_equal (ty_def c))); clear IHsty_one1; bd H. Qed. Lemma wf_MapsTo_In_p : forall (x' : x) (cl' : cl) (g : G) (h : H) (l : L) (p : P), wf_stck p g h l -> XMap.MapsTo x' (ty_def cl') g -> In cl' (names p). intros. inversion H; subst. import (H1 _ (MapsTo_mem _ _ _ H0)); bd H2. inversion H6; subst. import (XMap.find_1 H0). congruence. Qed. Lemma Some_ftype_not_None : forall (p : P) (cl' : cl) (f' : f) (ty' : ty), ftype p cl' f' = Some ty' -> ftype p cl' f' <> None. unfold not; intros; rewrite H0 in H; discriminate. Qed. Lemma wf_class_in_list : forall (cld_list a : list cld) (dcl' : dcl) (cl' : cl) (fds' : fds) (md_list : list md), wf_class_list (map (fun cld_ : cld => (a, cld_)) cld_list) -> In (cld_def dcl' cl' fds' md_list) cld_list -> wf_class a (cld_def dcl' cl' fds' md_list). induction cld_list; intros. simpl in H0; elimtype False; exact H0. simpl in H0; bd H0. rewrite H0 in H. simpl in H. inversion H; subst; auto. inversion H. apply (IHcld_list); auto. Qed. Lemma sty_ftype: forall (p : P) (cl1 cl2 : cl) (f' : f) (ty1 ty2 ty' : ty), ty1 = ty_def cl1 -> ty2 = ty_def cl2 -> sty_one p ty1 ty2 -> wf_prog p -> ftype p cl2 f' = Some ty' -> ftype p cl1 f' = Some ty'. intros. generalize cl1 cl2 f' H H0 H2 H3; clear cl1 cl2 f' H0 H H2 H3. induction H1; intros. subst. inversion H; subst; clear H. assert (forall ty'', ~ In (fd_def ty'' f') fds5). import (proj1 (ftype_in_fields _ _ _) (Some_ftype_not_None _ _ _ _ H3)). destruct H2; subst. import (wf_class_in_list _ _ _ _ _ _ H2 H5). inversion H0. subst; generalize H H13; clear; intros. induction ty_f_list. simpl; tauto. simpl in H13. destruct a. unfold not; intros; simpl in H0; bd H0; subst. assert ( in_nat_list f' (fields cld_list cl2) = true). generalize H; clear; induction (fields cld_list cl2); intros. simpl in H; elimtype False; exact H. simpl in H; bd H. rewrite H; simpl. case eq_nat_dec; auto. simpl; rewrite (IHf H); case eq_nat_dec; auto. inversion H0; simpl in H13; subst; rewrite H1 in H13; inversion H13. destruct (in_nat_list (snd (t, f)) (fields cld_list cl2)); try (inversion H13; fail). apply (IHty_f_list H13); auto. unfold ftype in *. rewrite (path_eq_parent _ _ _ _ _ H2 H5). simpl. rewrite H3. assert (get_fty fds5 f' = None). generalize H; clear. induction fds5; intros. simpl; reflexivity. destruct a; simpl. case eq_nat_dec; intros. rewrite e in H. import (H t); elimtype False; apply H0; simpl; po1. apply IHfds5. intros. import (H ty''); simpl in H0; bd H0. rewrite H0; reflexivity. inversion H0. rewrite <- H4 in H3. unfold ftype in H3; rewrite path_cl_obj in H3; simpl in H3; discriminate. rewrite H0 in H1; inversion H1; congruence. caseEq ty'0; intros. apply (IHsty_one1 _ _ f' H H1 H2). apply (IHsty_one2 _ _ f' H1 H0); auto. Qed. Lemma big_list_breakdown : forall (big_list : list (x*var*var*v)), exists x_list, exists var1_list, exists var2_list, exists v_list, big_list = build_big_list x_list var1_list var2_list v_list /\ length big_list = length x_list /\ length big_list = length var1_list /\ length big_list = length v_list /\ length big_list = length var2_list. intros. exists (map (fun (yp :x*var*var*v) => fst (fst (fst yp))) big_list). exists (map (fun (yp :x*var*var*v) => snd (fst (fst yp))) big_list). exists (map (fun (yp :x*var*var*v) => snd (fst yp)) big_list). exists (map (fun (yp :x*var*var*v) => snd yp) big_list). induction big_list; simpl; repeat pa. destruct a; destruct p; destruct p; rewrite <- (proj1 IHbig_list); repeat pa. rewrite (proj1 (proj2 IHbig_list)); auto. rewrite (proj1 (proj2 (proj2 IHbig_list))); auto. rewrite (proj1 (proj2 (proj2 (proj2 IHbig_list)))); auto. rewrite (proj2 (proj2 (proj2 (proj2 IHbig_list)))); auto. Qed. Lemma tr_x_tr_var : forall (t : T) (var' : var), (forall x' : x, tr_x t x' <> x_this) -> tr_x t (x_var var') = x_var (tr_var t var'). intros; import (H (x_var var')). unfold tr_x in *|-*; unfold tr_var. destruct (XMap.find (x_var var') t); auto. destruct x; try reflexivity. elimtype False; apply H0; congruence. Qed. Lemma tr_x_tr_var' : forall (t : T) (var' : var), (forall x' : x, x' <> x_this -> tr_x t x' <> x_this) -> tr_x t (x_var var') = x_var (tr_var t var'). intros; import (H (x_var var')). unfold tr_x in *|-*; unfold tr_var. destruct (XMap.find (x_var var') t); auto. destruct x; try reflexivity. elimtype False; apply H0; congruence. Qed. Inductive wf_stmt_list' : P -> G -> list_s -> Prop := | Nil_wf_stmt_list' : forall (P5:P) (G5:G) , wf_stmt_list' P5 G5 Nil_list_s | Cons_wf_stmt_list' : forall (P5:P) (G5:G) (s_:s) (s_list : list_s), (wf_stmt P5 G5 s_) -> wf_stmt_list' P5 G5 s_list -> wf_stmt_list' P5 G5 (Cons_list_s s_ s_list). Lemma wf_stmt_list'_iff : forall (p : P) (g : G) (l : list_s), wf_stmt_list (map_list_s (fun s_ : s => (p, g, s_)) l) <-> wf_stmt_list' p g l. induction l; simpl; pa; intros. apply Nil_wf_stmt_list'. apply Nil_wf_stmt_list. inversion H; subst. apply Cons_wf_stmt_list'; auto. applyI IHl. inversion H; subst. apply Cons_wf_stmt_list; auto. applyI IHl. Qed. Lemma wf_stmt_list'_iff' : forall (p : P) (g : G) (l : list s), wf_stmt_list (map (fun s_ : s => (p, g, s_)) l) <-> wf_stmt_list' p g (make_list_s l). induction l; simpl; pa; intros. apply Nil_wf_stmt_list'. apply Nil_wf_stmt_list. inversion H; subst. apply Cons_wf_stmt_list'; auto. applyI IHl. inversion H; subst. apply Cons_wf_stmt_list; auto. applyI IHl. Qed. Scheme s_list_s_ind' := Minimality for list_s Sort Prop with s_s_list_ind' := Minimality for s Sort Prop. Lemma wf_trans_stmt : forall (p : P) (g g': G) (t : T) (Ss' : list_s), wf_stmt_list' p g Ss' -> (forall (x' : x), XMap.find x' g = XMap.find (tr_x t x') g') -> (forall (x' : x), tr_x t x' <> x_this) -> wf_stmt_list' p g' (tr_Ss t Ss'). intros p g g' t Ss'. elim Ss' using s_list_ind with (P := fun s => (wf_stmt p g s -> (forall (x' : x), XMap.find x' g = XMap.find (tr_x t x') g') -> (forall (x' : x), tr_x t x' <> x_this) -> wf_stmt p g' (tr_s t s))); intros; auto. inversion H; subst; simpl. apply wf_new; try congruence. rewrite H0 in H5. rewrite (tr_x_tr_var _ var H1) in H5; exact H5. inversion H; subst; simpl. apply wf_var_assign; try congruence. repeat rewrite H0 in H5. rewrite (tr_x_tr_var _ var H1) in H5; exact H5. inversion H; subst; simpl. rewrite H0 in H7. apply (wf_field_read p _ (tr_var t var) (tr_x t x) f _ ty5 H7); try congruence. rewrite H0 in H9; rewrite (tr_x_tr_var _ var H1) in H9; congruence. inversion H; subst; simpl; rewrite H0 in H9, H7. apply (wf_field_write p _ (tr_x t x) f (tr_x t y) _ ty5 H7); try congruence. inversion H; subst; simpl; repeat rewrite H0 in *|-*. assert (map (tr_x t) (map (fun y : lj.x * ty => fst y) y_ty_list) = map (fun y : lj.x * ty => fst y) (map (fun y => (tr_x t (fst y), snd y)) y_ty_list)). clear. induction y_ty_list. simpl; reflexivity. simpl; rewrite IHy_ty_list; reflexivity. rewrite H2; clear H2. apply (wf_mcall (map (fun y : lj.x * ty => (tr_x t (fst y), snd y)) y_ty_list) p g' (tr_var t var) _ m _ ty' H8). assert (map (fun y : lj.x * ty => snd y) (map (fun y : lj.x * ty => (tr_x t (fst y), snd y)) y_ty_list) = map (fun y : lj.x * ty => snd y) y_ty_list). clear; induction y_ty_list; simpl; intros; congruence. rewrite H2; auto. clear H9 H11 H8 H; induction y_ty_list. simpl; auto. simpl in *|-*. inversion H10; subst. apply Cons_sty_opt_list; auto. rewrite H0 in H3; auto. rewrite (tr_x_tr_var _ var H1) in H11; exact H11. inversion H1; subst; simpl in *|-*. apply wf_if; auto. repeat rewrite H2 in H9; auto. simpl. apply wf_block. applyI wf_stmt_list'_iff. inversion H0; subst. apply H; auto. applyI wf_stmt_list'_iff. simpl. apply Nil_wf_stmt_list'. simpl in *|-*. inversion H1; subst. apply Cons_wf_stmt_list'; auto. Qed. Lemma wf_trans_stmt'' : forall (p : P) (g g': G) (t : T) (Ss' : list_s), wf_stmt_list' p g Ss' -> (forall (x' : x) (ty' : ty), XMap.find x' g = Some ty' -> XMap.find (tr_x t x') g' = Some ty') -> (forall (x' : x), x' <> x_this -> tr_x t x' <> x_this) -> wf_stmt_list' p g' (tr_Ss t Ss'). intros p g g' t Ss'. elim Ss' using s_list_ind with (P := fun s => (wf_stmt p g s -> (forall (x' : x) (ty' : ty), XMap.find x' g = Some ty' -> XMap.find (tr_x t x') g' = Some ty') -> (forall (x' : x), x' <> x_this -> tr_x t x' <> x_this) -> wf_stmt p g' (tr_s t s))); intros; auto. inversion H; subst; simpl. apply wf_new; try congruence. inversion H5. rewrite H3 in H5; rewrite <- (H0 _ _ H3) in H5. rewrite (tr_x_tr_var' _ var H1) in H5; exact H5. inversion H; subst; simpl. apply wf_var_assign; try congruence. inversion H5. rewrite H2 in H5; rewrite H3 in H5; rewrite <- (H0 _ _ H2) in H5; rewrite <- (H0 _ _ H3) in H5. rewrite (tr_x_tr_var' _ var H1) in H5; exact H5. inversion H; subst; simpl. inversion H9. rewrite H3 in H9; rewrite <- (H0 _ _ H3) in H9. import (H0 _ _ H7). apply (wf_field_read p _ (tr_var t var) (tr_x t x) f _ ty5 H11); try congruence. rewrite (tr_x_tr_var' _ var H1) in H9; congruence. inversion H; subst; simpl. inversion H9. rewrite H2 in H9; rewrite <- (H0 _ _ H2) in H9; import (H0 _ _ H7). apply (wf_field_write p _ (tr_x t x) f (tr_x t y) _ ty5 H11); try congruence. inversion H; subst; simpl. import (H0 _ _ H8). inversion H11. rewrite H4 in H11; rewrite <- (H0 _ _ H4) in H11. assert (sty_opt_list (map (fun y : lj.x * ty => (p, XMap.find (tr_x t (fst y)) g', Some (snd y))) y_ty_list)). generalize H10 H0; clear; induction y_ty_list. simpl; intros. apply Nil_sty_opt_list. simpl; intros. apply Cons_sty_opt_list; try (exact (ty_def cl_object)). inversion H10. inversion H2. rewrite H6 in H2; rewrite <- (H0 _ _ H6) in H2. exact H2. inversion H10; apply IHy_ty_list; auto. assert (map (tr_x t) (map (fun y : lj.x * ty => fst y) y_ty_list) = map (fun y : lj.x * ty => fst y) (map (fun y => (tr_x t (fst y), snd y)) y_ty_list)). clear. induction y_ty_list. simpl; reflexivity. simpl; rewrite IHy_ty_list; reflexivity. rewrite H14; clear H14. apply (wf_mcall (map (fun y : lj.x * ty => (tr_x t (fst y), snd y)) y_ty_list) p g' (tr_var t var) _ m _ ty' H2). assert (map (fun y : lj.x * ty => snd y) (map (fun y : lj.x * ty => (tr_x t (fst y), snd y)) y_ty_list) = map (fun y : lj.x * ty => snd y) y_ty_list). clear; induction y_ty_list; simpl; intros; congruence. rewrite H14; auto. subst. generalize H13 H1 H0; clear; induction y_ty_list; intros. simpl; auto. simpl in *|-*. inversion H13; subst. apply Cons_sty_opt_list; auto. rewrite (tr_x_tr_var' _ var H1) in H11; exact H11. inversion H1; subst; simpl in *|-*. apply wf_if; auto. bd H9; inversion H9. rewrite H4 in H9; rewrite H5 in H9; rewrite <- (H2 _ _ H4) in H9; rewrite <- (H2 _ _ H5) in H9; po1. rewrite H4 in H9; rewrite H5 in H9; rewrite <- (H2 _ _ H4) in H9; rewrite <- (H2 _ _ H5) in H9; po2. simpl. apply wf_block. applyI wf_stmt_list'_iff. inversion H0; subst. apply H; auto. applyI wf_stmt_list'_iff. simpl. apply Nil_wf_stmt_list'. simpl in *|-*. inversion H1; subst. apply Cons_wf_stmt_list'; auto. Qed. Lemma wf_trans_stmt_list' : forall (p : P) (g g': G) (t : T) (Ss' : list_s), wf_stmt_list (map_list_s (fun s_ : s => (p, g, s_)) Ss') -> (forall (x' : x), XMap.find x' g = XMap.find (tr_x t x') g') -> (forall (x' : x), tr_x t x' <> x_this) -> wf_stmt_list (map_list_s (fun s_ : s => (p, g', s_)) (tr_Ss t Ss')). intros. applyI wf_stmt_list'_iff. apply (wf_trans_stmt p g g' t Ss'); auto. applyI wf_stmt_list'_iff. Qed. Lemma fold_right_find : forall (p : P) (g': G) (var_ty_list : list (var * ty)) (x' : x) (ty' : ty), XMap.find x' (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list) = Some ty' -> XMap.find x' (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g' var_ty_list) = Some ty'. induction var_ty_list; intros. simpl in H. elimtype False. assert (XMap.Empty (XMap.empty ty)). apply XMap.empty_1. unfold XMap.Empty in H0; unfold XMap.Raw.Empty in H0. apply (H0 _ _ (XMap.find_2 H)). simpl in *|-*. cs (XOrd.eq (x_var (fst a)) x'). import (XMap.add_1). rewrite (XMap.find_1 (H1 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g' var_ty_list) _ _ (snd a) H0)). rewrite (XMap.find_1 (H1 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list) _ _ (snd a) H0)) in H. exact H. import (XMap.add_3). import (XMap.find_1 (H1 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list) _ _ _ (snd a) H0 (XMap.find_2 H))). apply XMap.find_1. import (XMap.add_2). apply (H3 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g' var_ty_list) _ _ ty' (snd a) H0). apply XMap.find_2. apply IHvar_ty_list. exact H2. Qed. Lemma wf_stmt_list_add_g : forall (Ss' : list_s) (p : P) (g': G) (var_ty_list : list (var * ty)), wf_stmt_list' p (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list) Ss' -> wf_stmt_list' p (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g' var_ty_list) Ss'. intros Ss' p g' var_ty_list. elim Ss' using s_list_ind with (P := fun s => wf_stmt p (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list) s -> wf_stmt p (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g' var_ty_list) s); intros; auto. inversion H; subst. caseEq (XMap.find (x_var var) (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); intros; rewrite H0 in H3. apply wf_new. rewrite (fold_right_find p g' _ (x_var var) t H0); auto. inversion H3; discriminate. inversion H; subst. caseEq (XMap.find x (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); caseEq (XMap.find (x_var var) (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); intros; rewrite H0 in H3; rewrite H1 in H3. apply wf_var_assign. rewrite (fold_right_find p g' _ x t0 H1). rewrite (fold_right_find p g' _ _ t H0). exact H3. inversion H3; discriminate. inversion H3; discriminate. inversion H3; discriminate. inversion H; subst. caseEq (XMap.find (x_var var) (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); intros. apply (wf_field_read p (fold_right (fun (x0 : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x0)) (snd x0) g) g' var_ty_list) var x f cl5 ty5). rewrite (fold_right_find p g' _ x (ty_def cl5) H5). reflexivity. auto. rewrite H0 in H7. rewrite (fold_right_find p g' _ (x_var var) t H0 ). exact H7. rewrite H0 in H7; inversion H7; discriminate. inversion H; subst. caseEq ((XMap.find y (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list))); intros; rewrite H0 in H7. apply (wf_field_write p (fold_right (fun (x0 : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x0)) (snd x0) g) g' var_ty_list) x f y cl5 ty5). rewrite (fold_right_find p g' _ x (ty_def cl5) H5). reflexivity. exact H6. rewrite (fold_right_find p g' _ y t H0). exact H7. inversion H7; discriminate. inversion H; subst. apply (wf_mcall y_ty_list p (fold_right (fun (x0 : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x0)) (snd x0) g) g' var_ty_list) var x m cl5 ty'); auto. rewrite (fold_right_find p g' _ x (ty_def cl5) H6). reflexivity. generalize H8; clear; induction y_ty_list; simpl; intros; inversion H8; subst. apply Nil_sty_opt_list. apply Cons_sty_opt_list; auto. caseEq ( (XMap.find (fst a) (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)) ); intros; rewrite H in H1. rewrite (fold_right_find p g' _ (fst a) t H). exact H1. inversion H1; discriminate. caseEq ( (XMap.find (x_var var) (fold_right (fun (x : lj.var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list))); intros; rewrite H0 in H9. rewrite (fold_right_find p g' _ (x_var var) t H0). exact H9. inversion H9; discriminate. inversion H1; subst. caseEq (XMap.find x (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); caseEq (XMap.find y (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) var_ty_list)); intros; rewrite H2 in H7; rewrite H3 in H7. apply (wf_if p (fold_right (fun (x1 : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x1)) (snd x1) g) g' var_ty_list) x y s1 s2); auto. rewrite (fold_right_find p g' _ x t0 H3). rewrite (fold_right_find p g' _ y t H2). exact H7. bd H7; inversion H7; discriminate. bd H7; inversion H7; discriminate. bd H7; inversion H7; discriminate. inversion H0; subst. apply wf_block. applyI wf_stmt_list'_iff. apply H. applyI wf_stmt_list'_iff. applyI wf_stmt_list'_iff. simpl. apply Nil_wf_stmt_list. apply Cons_wf_stmt_list'. apply H. inversion H1; subst. apply H6. apply H0. inversion H1; subst; auto. Qed. Lemma find_var_empty : forall (x' y' : x) (ty' : ty), ~ XOrd.eq y' x' -> XMap.find x' (XMap.add y' ty' (XMap.empty ty)) = None. intros. import (XMap.add_3). caseEq ( XMap.find x' (XMap.add y' ty' (XMap.empty ty))); intros; auto. elimtype False. import (H0 _ _ _ _ _ _ H (XMap.find_2 H1)). apply ((proj1 (XMapFacts.empty_mapsto_iff _ _ ) H2)). Qed. Lemma find_in_add : forall (var_ty_list : list (var * ty)) (ty' : ty) (g : G) (y : x), XMap.find y (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) (XMap.empty ty) var_ty_list) = Some ty' -> XMap.find y (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g var_ty_list) = Some ty'. induction var_ty_list; simpl; intros. rewrite XMapFacts.empty_o in H. discriminate. destruct y. cs (XOrd.eq (x_var (fst a)) (x_var v)). import (XMap.add_1). import (XMap.find_1 (H1 _ (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) (XMap.empty ty) var_ty_list) _ _ (snd a) H0)). rewrite H2 in H. inversion H. apply XMap.find_1. apply (H1 _ (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g var_ty_list) (x_var (fst a)) (x_var v) (snd a) H0). import (XMap.add_3). import (IHvar_ty_list _ g _ (XMap.find_1 (H1 _ (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) (XMap.empty ty) var_ty_list) (x_var (fst a)) (x_var v) ty' (snd a) H0 (XMap.find_2 H)))). import XMap.add_2. apply (XMap.find_1 (H3 _ (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g var_ty_list) (x_var (fst a)) (x_var v) ty' (snd a) H0 (XMap.find_2 H2))). apply XMap.find_1. apply XMap.add_2. simpl; auto. apply XMap.find_2. apply IHvar_ty_list. import XMap.add_3. apply XMap.find_1. assert (~XMap.E.eq (x_var (fst a)) x_this); simpl; auto. apply (XMap.add_3 H1 (XMap.find_2 H)). Qed. Lemma wf_stmt_list_s : forall (p : P) (g: G) (Ss' : list_s), wf_stmt_list (map_list_s (fun s_ : s => (p, g, s_)) Ss') <-> wf_stmt_list (map (fun s_ : s => (p, g, s_)) (unmake_list_s Ss')). induction Ss'; simpl; pa; intros; auto. inversion H; subst; auto. apply Cons_wf_stmt_list; auto. applyI IHSs'. inversion H; subst; auto. apply Cons_wf_stmt_list; auto. applyI IHSs'. Qed. Lemma wf_stmt_list_app : forall (p : P) (g: G) (Ss1 Ss2 : Ss), wf_stmt_list (map (fun s => (p, g, s)) (Ss1 ++ Ss2)) <-> (wf_stmt_list (map (fun s => (p, g, s)) Ss1) /\ wf_stmt_list (map (fun s => (p, g, s)) Ss2)). induction Ss1; repeat pa; intros. simpl; apply Nil_wf_stmt_list. bd H. simpl in *|-*; inversion H; subst. apply Cons_wf_stmt_list. exact H2. apply (proj1 ((proj1 (IHSs1 Ss2)) H5)). inversion H; subst. apply (proj2 ((proj1 (IHSs1 Ss2)) H5)). simpl in *|-*; bd H. inversion H2; subst. apply Cons_wf_stmt_list. exact H3. applyI IHSs1. pa. Qed. Lemma combine_tail_eq : forall (A B: Type) (l1: list A) (l2 : list B) (a: A) (a2 : B), length l1 = length l2 -> combine (l1++ (a :: nil)) (l2 ++ a2 :: nil ) = (combine l1 l2) ++ (a, a2) :: nil. induction l1; intros; simpl. destruct l2; try discriminate. simpl; auto. destruct l2; try discriminate. simpl. inversion H. rewrite IHl1; auto. Qed. Lemma rev_combine_eq : forall (A B : Type) (l1 : list A) (l2 : list B), length l1 = length l2 -> rev (combine l1 l2) = combine (rev l1) (rev l2). induction l1; intros. simpl; reflexivity. destruct l2; simpl in *|-*. discriminate. inversion H. rewrite combine_tail_eq. rewrite IHl1; auto. repeat rewrite rev_length; exact H1. Qed. Lemma combine_nil : forall (A B: Type) (l : list A), combine l (nil : list B) = nil. induction l; simpl; auto. Qed. Lemma in_sty_opt_wf_type : forall (y : P*tyopt*tyopt) (l : list (P*tyopt*tyopt)) (ty' : ty), In y l -> sty_opt_list l -> snd y = Some ty' -> wf_prog (fst (fst y)) -> wf_type (fst (fst y)) ty'. induction l; intros. simpl in H; elimtype False; exact H. simpl in H. inversion H0; subst. bd H. rewrite <- H in H1. simpl in H1. rewrite H1 in H5. inversion H5; subst. inversion H4. generalize H7 H2; simpl; clear; intros. induction H7. inversion H. inversion H2. rewrite <- H5 in H7. apply wf_valid_dcl. import (list_ordered_parent _ _ H0 (ordered_wf_prog _ _ H7)). bd H9. simpl in H12; congruence. apply wf_valid_dcl. clear H2; induction P5. simpl. po1. destruct a; simpl. po2. apply wf_valid_dcl. apply (In_names _ _ _ _ _ H). apply (IHsty_one2 H2). apply IHl; auto. Qed. Lemma in_list_find : forall (var': var) (x1 : list var) (x2 : list v) (l : L), length x1 = length x2 -> In var' x1 -> exists v', In v' x2 /\ In (var',v') (combine x1 x2) /\ (XMap.find (x_var var') (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2))) = Some v'. induction x1; intros. simpl in H0; elimtype False; exact H0. destruct x2; inversion H. simpl in H0; bd H0. exists v; simpl; repeat pa. po1. rewrite H0. po1. rewrite H0. import XMap.add_1. rewrite (XMap.find_1 (H1 _ (fold_right (fun (yp : var * lj.v) (m : XMap.t lj.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ v (XOrd.eq_refl (x_var var')))). reflexivity. simpl; cs (XOrd.eq (x_var a) (x_var var')). exists v; simpl; repeat pa. po1. rewrite (eq_nat_eq _ _ H1); po1. rewrite (eq_nat_eq _ _ H1). import XMap.add_1. rewrite (XMap.find_1 (H3 _ (fold_right (fun (yp : var * lj.v) (m : XMap.t lj.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ v (XOrd.eq_refl (x_var var')))). reflexivity. import (IHx1 _ l H2 H0); bd H3. exists x; simpl; repeat pa. po2. po2. import XMap.add_2. rewrite (XMap.find_1 (H4 _ (fold_right (fun (yp : var * lj.v) (m : XMap.t lj.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ _ v H1 (XMap.find_2 H3))). reflexivity. Qed. Theorem In_combine_trans : forall (A B C : Type) (a : A) (b : B) (c : C) (la : list A) (lb : list B) (lc : list C), In (a,b) (combine la lb) -> In (a,c) (combine la lc) -> distinct _ la -> In (b,c) (combine lb lc). induction la; intros. simpl in H; elimtype False; apply H. destruct lb; destruct lc; try (simpl in H, H0; elimtype False; auto; fail). simpl in H, H0, H1. bd H; bd H0; bd H1. inversion H; inversion H0; simpl; po1. inversion H; subst. elimtype False; exact (H4 (in_combine_l _ _ _ _ H0)). inversion H0; subst. elimtype False; exact (H4 (in_combine_l _ _ _ _ H)). simpl; po2; apply IHla; auto. Qed. Lemma wf_cld_wf_md : forall (p : P) (dcl' :dcl) (cl' : cl) (fds' : fds) (mds : list md) (md' : md), wf_meth_list (map (fun md' : md => (p, ty_def (cl_dcl dcl'), md')) mds) -> In md' mds -> wf_meth p (ty_def (cl_dcl dcl')) md'. induction mds; simpl; intros. elimtype False; apply H0. bd H0. rewrite H0 in H; inversion H; subst. apply H3. inversion H. apply IHmds; auto. Qed. Lemma wf_cld_wf_md' : forall (p : P) (dcl' :dcl) (cl' : cl) (fds' : fds) (mds : list md) (md' : md), wf_class p (cld_def dcl' cl' fds' mds) -> In md' mds -> wf_meth p (ty_def (cl_dcl dcl')) md'. intros. inversion H; apply (wf_cld_wf_md p dcl' cl' fds' mds md'); auto. Qed. Lemma wf_md_wf_Ss' : forall (p : P) (ty' ty'': ty) (m' : m) (vds : list vd) (x' : x) (Ss' : Ss), wf_meth p ty' (md_def (ms_def ty'' m' vds) (mb_def Ss' x')) -> wf_stmt_list' p (fold_left (fun (m : XMap.t ty) (p : x*ty)=> XMap.add (fst p) (snd p) m) (cons (x_this, ty') (map (fun (vd' : vd) => match vd' with vd_def ty''' var' => (x_var var', ty''') end) vds)) (XMap.empty ty)) (make_list_s Ss') /\ distinct _ (map (fun (vd' : vd) => match vd' with vd_def ty''' var' => var' end) vds). intros; inversion H; pa. import ((proj1 (wf_stmt_list'_iff _ _ _)) H10). assert (map (fun vd' : vd => match vd' with | vd_def ty''' var' => (x_var var', ty''') end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list) = map (fun ty_var : ty * var => (x_var (snd ty_var), fst ty_var)) ty_var_list). clear; induction ty_var_list; intros. simpl; reflexivity. destruct a; simpl. rewrite IHty_var_list; auto. rewrite H13; clear H13. rewrite <- H9. assert (make_list_s (unmake_list_s s_list) = s_list). clear; induction s_list; simpl; intros; auto. rewrite IHs_list; reflexivity. rewrite H13. applyI wf_stmt_list'_iff. generalize H8; clear; induction ty_var_list; simpl; intros; auto. bd H8. pa. unfold not; intros; apply H1. generalize H; clear; induction ty_var_list. simpl; auto. simpl; intros. bd H. po1; auto. po2; apply (IHty_var_list H). apply (IHty_var_list H8). Qed. Lemma in_cld_wf_prog : forall (p : P) (dcl' : dcl) (m' : m) (ty' : ty) (list_ty : list ty) (list_var : list var) (x' : x) (Ss' : Ss), mtype p (cl_dcl dcl') m' = Some (mty_def list_ty ty') -> find_menv p (cl_dcl dcl') m' = Some (menv_def list_var (mb_def Ss' x')) -> exists cl', exists mds', exists fds', In (cld_def dcl' cl' fds' mds') p. induction p; intros. unfold mtype in H; unfold find_menv in H0. simpl in H; discriminate. destruct a; unfold mtype in H; unfold find_menv in H0; simpl in *. unfold get_md in H, H0. simpl in H, H0. caseEq (eq_nat_dec dcl' d); intros. rewrite e in *; simpl in H0. exists c; exists l; exists f; simpl; auto. rewrite H1 in H0, H. fold (get_md p (cl_dcl dcl') m') in H0, H. fold ( mtype p (cl_dcl dcl') m') in H. fold ( find_menv p (cl_dcl dcl') m') in H0. import (IHp _ _ _ _ _ _ _ H H0); bd H2. exists x; exists x0; exists x1. po2. Qed. Inductive sty_list : P -> cl -> list cld -> Prop := | Nil_sty_list : forall (p : P), sty_list p cl_object nil | Cons_sty_list : forall (p : P) (dcl' : dcl) (cl' cl'' : cl) (fds' : fds) (mds' : list md) (l : list cld), sty_one p (ty_def (cl_dcl dcl')) (ty_def cl') -> sty_list p cl' l -> sty_list p (cl_dcl dcl') (cons (cld_def dcl' cl'' fds' mds') l). Lemma sty_list_subtype : forall (l : list cld) (p : P) (dcl' : dcl) (cl' cl'': cl) (fds' : fds) (mds' : list md), In (cld_def dcl' cl'' fds' mds') p -> In (cld_def dcl' cl'' fds' mds') l -> sty_list p cl' l -> sty_one p (ty_def cl') (ty_def (cl_dcl dcl')). induction l; simpl; intros. contradiction. inversion H1; bd H0; subst. inversion H0; subst. apply (sty_reflexive _ _ _ _ _ H). apply (sty_transitive p _ _ _ H6 (IHl _ _ _ _ _ _ H H0 H7)). Qed. Lemma add_prog_sty_list : forall (p : P) (cld': cld) (cl' : cl) (l : list cld), sty_list p cl' l -> sty_list (cld' :: p) cl' l. intros. induction H. apply Nil_sty_list. assert (sty_one (cld' :: p) (ty_def (cl_dcl dcl')) (ty_def cl')). generalize H; clear. intros. induction H. inversion H. apply sty_from_direct. apply (sty_dir md_list (cld' :: P5) dcl5 cl5 fds5). simpl; po2. apply sty_opt_refl. apply (sty_reflexive (cld' :: P5) dcl'0 cl'0 fds' mds). simpl; po2. apply (sty_transitive _ _ _ _ IHsty_one1 IHsty_one2). intros. apply (Cons_sty_list _ _ _ cl'' fds' mds' _ H1 IHsty_list). Qed. Lemma path_sty_head : forall (p : P) (dcl' dcl'': dcl) (cl' cl'' : cl) (fds' fds'' : fds) (mds' mds'' : list md), wf_prog p -> In (cld_def dcl' cl' fds' mds') p -> hd (cld_def dcl' cl' fds' mds') (tail (path p (cl_dcl dcl'))) = (cld_def dcl'' cl'' fds'' mds'') -> sty_one p (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')). intros. rewrite (path_eq_parent _ _ _ _ _ H H0) in H1. destruct cl'. caseEq (path p (cl_dcl d)); intros. rewrite H2 in H1; simpl in H1. inversion H1; subst; apply (sty_reflexive _ _ _ _ _ H0). destruct c. import (path_eq_self _ _ _ _ _ _ _ H2). rewrite <- H3 in H2. rewrite H2 in H1. simpl in H1. inversion H1. rewrite <- H5. apply sty_from_direct. apply (sty_dir _ _ _ _ _ H0). rewrite path_cl_object in H1; simpl in H1; inversion H1. subst; apply (sty_reflexive _ _ _ _ _ H0). Qed. Lemma in_md_wf_prog : forall (p : P) (dcl' : dcl) (m' : m) (ty' : ty) (list_ty : list ty) (list_var : list var) (x' : x) (Ss' : Ss), wf_prog p -> mtype p (cl_dcl dcl') m' = Some (mty_def list_ty ty') -> find_menv p (cl_dcl dcl') m' = Some (menv_def list_var (mb_def Ss' x')) -> exists dcl'', exists cl', exists fds', exists mds', In (cld_def dcl'' cl' fds' mds') p /\ In (md_def (ms_def ty' m' (map (fun (x: ty*var )=> vd_def (fst x) (snd x) ) (combine list_ty list_var)) ) (mb_def Ss' x')) mds' /\ sty_one p (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')). intros. import (in_cld_wf_prog _ _ _ _ _ _ _ _ H0 H1); bd H2. import (in_mtype_wf_prog _ _ _ _ _ _ _ _ _ _ H H2 H0 H1). import (in_menv_wf_prog _ _ _ _ _ _ _ _ _ _ H H2 H0 H1). import (in_path_in_prog p x). destruct x. import (in_path_sty p d). clear H0 H1. unfold mtype in *; unfold find_menv in *; unfold get_md in *. induction (path p (cl_dcl d)). bd H3; bd H4; try discriminate; try (exists dcl'; exists (cl_dcl d); exists x1; exists x0; repeat pa; apply (sty_reflexive _ _ _ _ _ H2)). bd H3; bd H4; try (exists dcl'; exists (cl_dcl d); exists x1; exists x0; repeat pa; apply (sty_reflexive _ _ _ _ _ H2)). destruct a. unfold get_all_mds in H3, H4; simpl in H3, H4. fold (get_all_mds l) in H3, H4. rewrite filter_mds_app in H3, H4. caseEq (filter_mds l0 m'); intros; try rewrite H0 in *; simpl in H3, H4, H5. apply IHl. po2. po2. intros. apply (H5 cld'). po2. intros. apply (H6 dcl'' _ cl'' _ fds'' _ mds'' H H7). simpl; po2. exists d0; exists c; exists f; exists l0; pa. apply (H5 (cld_def d0 c f l0)); po1. inversion H4; inversion H3. destruct m; destruct m. simpl in H7, H8; inversion H7; inversion H8; subst. assert (In (md_def (ms_def ty' m l2) (mb_def Ss' x')) l0). apply (in_filtered l0 (md_def (ms_def ty' m l2) (mb_def Ss' x')) m'). rewrite H0. simpl; po1. assert (m' = m). generalize H0; clear; induction l0. simpl; intros; discriminate. destruct a; destruct m0; simpl. case (eq_nat_dec m0 m'); intros. rewrite e in H0; inversion H0. reflexivity. auto. rewrite H9. assert ((map (fun x2 : ty * var => vd_def (fst x2) (snd x2)) (combine (get_vdstys l2) (get_vdsvars l2))) = l2). clear; induction l2; simpl; auto. destruct a; simpl; rewrite IHl2; auto. pa. rewrite H10; exact H1. inversion H. import (ordered_wf_prog _ _ H13). rewrite H11 in *. import (wf_prog_ordered _ _ _ _ _ H2 H15 H12). bd H16. import (in_path_in_prog _ _ _ H16). import (H6 d0 _ c _ f _ l0 H H17). apply (sty_transitive cld_list (ty_def (cl_dcl dcl')) (ty_def (cl_dcl d0)) (ty_def (cl_dcl d))). apply sty_from_direct. apply (sty_dir _ _ _ _ _ H2). apply H18; po1. clear H0 H1. unfold mtype in *; unfold find_menv in *; unfold get_md in *. rewrite path_cl_object in *. simpl in H3; simpl in H4. bd H3; bd H4; try discriminate; try (exists dcl'; exists cl_object; exists x1; exists x0; repeat pa; apply (sty_reflexive _ _ _ _ _ H2)). Qed. Lemma spurious_map_vd : forall (y_ty_list : list (x*ty)) (list_var : list var), 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) y_ty_list) list_var)) = (map (fun x : var *ty => ((x_var (fst x)), (snd x))) (combine list_var (map (fun y : x * ty => snd y) y_ty_list) )). induction y_ty_list; simpl; intros; destruct list_var; simpl; try reflexivity. rewrite IHy_ty_list. auto. Qed. Lemma wf_prog_wf_mb : forall (p : P) (dcl' : dcl) (m' : m) (ty' : ty) (list_ty : list ty) (list_var : list var) (x' : x) (Ss' : Ss), wf_prog p -> mtype p (cl_dcl dcl') m' = Some (mty_def list_ty ty') -> find_menv p (cl_dcl dcl') m' = Some (menv_def list_var (mb_def Ss' x')) -> exists ty'', wf_stmt_list' p (fold_left (fun (m : XMap.t ty) (p : x*ty)=> XMap.add (fst p) (snd p) m) (cons (x_this, ty'') (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 list_ty list_var)) )) (XMap.empty ty)) (make_list_s Ss') /\ distinct _ (list_var) /\ sty_option p (XMap.find x' (fold_left (fun (m : XMap.t ty) (p : x*ty)=> XMap.add (fst p) (snd p) m) (cons (x_this, ty'') (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 list_ty list_var)) )) (XMap.empty ty))) (Some ty') /\ wf_type p ty'' /\ sty_one p (ty_def (cl_dcl dcl')) ty''. intros; import (in_md_wf_prog _ _ _ _ _ _ _ _ H H0 H1). bd H2. exists (ty_def (cl_dcl x)). inversion H; subst. import (wf_prog_wf_cld cld_list cld_list (cld_def x x0 x1 x2) H7 H5); auto. import (wf_cld_wf_md' cld_list x x0 x1 x2 (md_def (ms_def ty' m' (map (fun x3 : ty * var => vd_def (fst x3) (snd x3)) (combine list_ty list_var))) (mb_def Ss' x')) H3 H6); auto. import (wf_md_wf_Ss' cld_list (ty_def (cl_dcl x)) ty' m' (map (fun x3 : ty * var => vd_def (fst x3) (snd x3)) (combine list_ty list_var)) x' Ss' H8); bd H9; repeat pa. import (find_menv_mtype_length _ _ _ _ _ _ _ H1 H0). generalize list_ty H9 H10; clear; induction list_var; simpl; intros. auto. destruct list_ty; simpl in H9. simpl in H10; discriminate. simpl in H9. bd H9; pa. unfold not; intros; apply H1. inversion H10. generalize list_ty H H2; clear; induction list_var; simpl; intros. elimtype False; apply H. destruct list_ty; simpl in H2. discriminate. bd H. simpl; po1. simpl; po2. apply IHlist_var. exact H. inversion H2; auto. apply (IHlist_var _ H9); auto. inversion H8. assert (map (fun vd' : vd => match vd' with | vd_def ty''' var' => (x_var var', ty''') end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list) = map (fun (k :ty*var) => (x_var (snd k), fst k)) ty_var_list). clear; induction ty_var_list; intros; simpl; auto. simpl; rewrite IHty_var_list; auto. rewrite H23; clear H23. rewrite H20 in H22; exact H22. exact (In_names _ _ _ _ _ H5). Qed. Lemma find_in_list_iff : forall (y : x) (ty' : ty) (y_ty_list : list (x*ty)), distinct _ (map (fun x => fst x) y_ty_list) -> (XMap.find y (fold_right (fun (p : x * ty) (m : XMap.t ty) => XMap.add (fst p) (snd p) m) (XMap.empty ty) y_ty_list) = Some ty' <-> In (y, ty') y_ty_list). induction y_ty_list; intros; pa; intros. simpl in H0. rewrite (XMapFacts.empty_o) in H0; discriminate. elimtype False; simpl in H0; exact H0. simpl in H0. destruct a; simpl in H0. cs (XOrd.eq x y). import (XMap.add_1). rewrite (XMap.find_1 (H2 _ (fold_right (fun (p : lj.x * ty) (m : XMap.t ty) => XMap.add (fst p) (snd p) m) (XMap.empty ty) y_ty_list) x y t H1)) in H0. inversion H0. simpl; po1. destruct x; destruct y; simpl in H1; try (elimtype False; apply H1). rewrite (eq_nat_eq _ _ H1). reflexivity. reflexivity. import (XMap.add_3). simpl; po2. simpl in H; bd H. applyI IHy_ty_list. apply (XMap.find_1 (H2 _ (fold_right (fun (p : lj.x * ty) (m : XMap.t ty) => XMap.add (fst p) (snd p) m) (XMap.empty ty) y_ty_list) x y ty' t H1 (XMap.find_2 H0))). simpl in *|-*. bd H; bd H0. rewrite H0; simpl. rewrite H0 in H3; simpl in H3. import (XMap.add_1). rewrite (XMap.find_1 (H1 _ (fold_right (fun (p : x * ty) (m : XMap.t ty) => XMap.add (fst p) (snd p) m) (XMap.empty ty) y_ty_list) y y ty' (XOrd.eq_refl y))). reflexivity. import ((proj2 (IHy_ty_list H)) H0). assert (~ XOrd.eq (fst a) y). unfold not; intros; apply H3. destruct (fst a); destruct y; simpl in H2; try (elimtype False; apply H2). rewrite <- (eq_nat_eq _ _ H2) in H0, H1. generalize H1; clear; induction y_ty_list. simpl; intros. rewrite XMapFacts.empty_o in H1; discriminate. simpl; intros. destruct a; simpl in H1. cs (XOrd.eq x (x_var v)). destruct x; simpl in H. rewrite (eq_nat_eq _ _ H); po1. simpl; reflexivity. elimtype False; apply H. po2; apply IHy_ty_list. import (XMap.add_3). apply (XMap.find_1 (H0 _ _ _ _ _ _ H (XMap.find_2 H1))). generalize H0; clear; induction y_ty_list. simpl; auto. simpl; intros. bd H0. destruct a; inversion H0; po1. reflexivity. po2. apply (IHy_ty_list H0). import (XMap.add_2). apply (XMap.find_1 (H4 _ _ _ _ _ (snd a) H2 (XMap.find_2 H1))). Qed. Lemma find_in_var_list_iff : forall (C : Set) (y : var) (z: C) (var_ty_list : list (var*C)), distinct _ (map (fun x => fst x) var_ty_list) -> (XMap.find (x_var y) (fold_right (fun (p : var * C) (m : XMap.t C) => XMap.add (x_var (fst p)) (snd p) m) (XMap.empty C) var_ty_list) = Some z <-> In (y, z) var_ty_list). induction var_ty_list; intros; pa; intros. simpl in H0. rewrite (XMapFacts.empty_o) in H0; discriminate. elimtype False; simpl in H0; exact H0. simpl in H0. destruct a; simpl in H0. cs (XOrd.eq (x_var v) (x_var y)). import (XMap.add_1). rewrite (XMap.find_1 (H2 _ (fold_right (fun (p : lj.var * C) (m : XMap.t C) => XMap.add (x_var (fst p)) (snd p) m) (XMap.empty C) var_ty_list) (x_var v) (x_var y) c H1)) in H0. inversion H0. simpl; po1. simpl in H1. rewrite (eq_nat_eq _ _ H1). reflexivity. import (XMap.add_3). simpl; po2. simpl in H; bd H. applyI IHvar_ty_list. apply (XMap.find_1 (H2 _ (fold_right (fun (p : lj.var * C) (m : XMap.t C) => XMap.add (x_var (fst p)) (snd p) m) (XMap.empty C) var_ty_list) (x_var v) (x_var y) z c H1 (XMap.find_2 H0))). simpl in *|-*. bd H; bd H0. rewrite H0; simpl. rewrite H0 in H3; simpl in H3. import (XMap.add_1). rewrite (XMap.find_1 (H1 _ (fold_right (fun (p : var * C) (m : XMap.t C) => XMap.add (x_var (fst p)) (snd p) m) (XMap.empty C) var_ty_list) (x_var y) (x_var y) z (XOrd.eq_refl (x_var y)))). reflexivity. import ((proj2 (IHvar_ty_list H)) H0). assert (~ XOrd.eq (x_var (fst a)) (x_var y)). unfold not; intros; apply H3. simpl in H2; rewrite <- (eq_nat_eq _ _ H2) in H0, H1. generalize H1; clear; induction var_ty_list. simpl; intros. rewrite XMapFacts.empty_o in H1; discriminate. simpl; intros. destruct a; simpl in H1. cs (XOrd.eq (x_var (fst a0)) (x_var v)). simpl in H; rewrite (eq_nat_eq _ _ H); po1. simpl; reflexivity. po2; apply IHvar_ty_list. import (XMap.add_3). apply (XMap.find_1 (H0 _ _ _ _ _ _ H (XMap.find_2 H1))). import (XMap.add_2). apply (XMap.find_1 (H4 _ _ _ _ _ (snd a) H2 (XMap.find_2 H1))). Qed. Lemma find_in_var_list_iff' : forall (y z: var) (var_ty_list : list (var*var)), distinct _ (map (fun x => fst x) var_ty_list) -> (XMap.find (x_var y) (fold_right (fun (p : var * var) (m : XMap.t x) => XMap.add (x_var (fst p)) (x_var (snd p)) m) (XMap.empty x) var_ty_list) = Some (x_var z) <-> In (y, z) var_ty_list). induction var_ty_list; intros; pa; intros. simpl in H0. rewrite (XMapFacts.empty_o) in H0; discriminate. elimtype False; simpl in H0; exact H0. simpl in H0. destruct a; simpl in H0. cs (XOrd.eq (x_var v) (x_var y)). import (XMap.add_1). rewrite (XMap.find_1 (H2 _ (fold_right (fun (p : lj.var * var) (m : XMap.t x) => XMap.add (x_var (fst p)) (x_var (snd p)) m) (XMap.empty x) var_ty_list) (x_var v) (x_var y) (x_var v0) H1)) in H0. inversion H0. simpl; po1. simpl in H1. rewrite (eq_nat_eq _ _ H1). reflexivity. import (XMap.add_3). simpl; po2. simpl in H; bd H. applyI IHvar_ty_list. apply (XMap.find_1 (H2 _ (fold_right (fun (p : lj.var * var) (m : XMap.t x) => XMap.add (x_var (fst p)) (x_var (snd p)) m) (XMap.empty x) var_ty_list) (x_var v) (x_var y) (x_var z) (x_var v0) H1 (XMap.find_2 H0))). simpl in *|-*. bd H; bd H0. rewrite H0; simpl. rewrite H0 in H3; simpl in H3. import (XMap.add_1). rewrite (XMap.find_1 (H1 _ (fold_right (fun (p : var * var) (m : XMap.t x) => XMap.add (x_var (fst p)) (x_var (snd p)) m) (XMap.empty x) var_ty_list) (x_var y) (x_var y) (x_var z) (XOrd.eq_refl (x_var y)))). reflexivity. import ((proj2 (IHvar_ty_list H)) H0). assert (~ XOrd.eq (x_var (fst a)) (x_var y)). unfold not; intros; apply H3. simpl in H2; rewrite <- (eq_nat_eq _ _ H2) in H0, H1. generalize H1; clear; induction var_ty_list. simpl; intros. rewrite XMapFacts.empty_o in H1; discriminate. simpl; intros. destruct a; simpl in H1. cs (XOrd.eq (x_var (fst a0)) (x_var v)). simpl in H; rewrite (eq_nat_eq _ _ H); po1. simpl; reflexivity. po2; apply IHvar_ty_list. import (XMap.add_3). apply (XMap.find_1 (H0 _ _ _ _ _ _ H (XMap.find_2 H1))). import (XMap.add_2). apply (XMap.find_1 (H4 _ _ (x_var (fst a)) (x_var y) (x_var z) (x_var (snd a)) H2 (XMap.find_2 H1))). Qed. Lemma distinct_app : forall (A : Type) (la' la'' : list A), distinct A (la' ++ la'') -> distinct A la' /\ distinct A la''. induction la'. simpl; tauto. simpl; repeat pa; intros. bd H. unfold not; intros; apply H2; apply in_or_app. po1. bd H. apply (proj1 (( (IHla' _ )) H)). bd H. apply (proj2 (( (IHla' _ )) H)). Qed. Lemma distinct_app' : forall (A : Type) (a : A) (la : list A), (~ In a la /\ distinct A la) <-> distinct A (la ++ a :: nil). induction la; simpl; pa; intros; try tauto; bd H. pa. unfold not; intros. apply H3. generalize H0 H2; clear; induction la. simpl; intros. bd H0. apply H2; congruence. simpl; intros. bd H0. po1. po2. apply IHla; auto. applyI IHla; auto. pa. apply and_not_or. pa. generalize H2; clear; induction la; intros. simpl in H2; bd H2. congruence. apply IHla. simpl in H2; bd H2. generalize H; clear; induction la; intros. simpl; tauto. simpl in H. simpl. apply and_not_or. pa. bd H. unfold not; intros; apply H2. apply in_or_app. po2; simpl. po1; congruence. bd H; apply IHla; auto. pa. unfold not; intros. apply H2. apply in_or_app. po1. generalize H; clear; induction la. simpl; tauto. simpl; intros. pa. bd H. unfold not; intros; apply H2; apply in_or_app. po1. apply IHla; bd H; auto. Qed. Lemma distinct_rev : forall (A : Type) (la : list A), distinct A la <-> distinct A (rev la). induction la. simpl; tauto. simpl; pa; intros. bd H. import ((proj1 IHla) H). clear H IHla. assert( ~ In a (rev la)). unfold not; intros. apply H2. applyI In_rev. clear H2. apply (proj1 ((distinct_app' _ a (rev la)))). pa. import ((proj2 (distinct_app' _ _ _)) H). bd H0; pa. unfold not; intros; apply H3; applyI In_rev. applyI IHla. Qed. Lemma find_in_list_iff' : forall (y : x) (ty' : ty) (y_ty_list : list (x*ty)), distinct _ (map (fun x => fst x) y_ty_list) -> (XMap.find y (fold_left (fun (m : XMap.t ty) (p : x * ty) => XMap.add (fst p) (snd p) m) y_ty_list (XMap.empty ty)) = Some ty' <-> In (y, ty') y_ty_list). intros. import (( proj1 (distinct_rev _ _ )) H). clear H. rewrite <- fold_left_rev_right. pa; intros. applyI In_rev. applyI find_in_list_iff; auto. rewrite <- map_rev in H0. exact H0. applyI find_in_list_iff. rewrite map_rev; exact H0. applyI In_rev; auto. Qed. Lemma map_snd : forall (A B: Type) (l :list (A * B)), exists snd_list, (map (fun y0 : A * B => snd y0) l) = snd_list. induction l. simpl; exists (nil : list B); reflexivity. bd IHl. destruct a. exists (b :: x). simpl. rewrite IHl; auto. Qed. Lemma combine_distinct : forall (A B : Type) (l1 : list A) (l2 : list B), distinct A l1 -> distinct (A*B) (combine l1 l2). induction l1; simpl; intros. auto. destruct l2; simpl. auto. bd H; pa. unfold not; intros; apply H2; generalize l2 H0; clear; induction l1; simpl; intros. exact H0. destruct l2. simpl in H0; elimtype False; exact H0. simpl in H0. bd H0. inversion H0; po1; auto. po2; apply (IHl1 _ H0). apply (IHl1 l2 H). Qed. Lemma equiv_lists : forall (y_ty_list : list (x*ty)) (new_var old_var : list var) (v v0 x': var) (t t0 ty' : ty), distinct var new_var -> distinct var old_var -> ~ In x' new_var -> In (x_var v0, t)((x_this, ty') :: map (fun x0 : var * ty => (x_var (fst x0), snd x0)) (combine old_var (map (fun y0 : x * ty => snd y0) y_ty_list))) -> In (v, t0) (combine (x' :: new_var) (map (fun y0 : x * ty => snd y0) ((x_var x', ty') :: y_ty_list))) -> In (v0, v) (combine old_var new_var) -> Some t = Some t0. simpl. intros y_ty_list. import (map_snd x ty y_ty_list); bd H; rewrite H. intros; bd H3. inversion H3. bd H4. inversion H4; elimtype False. apply H2. rewrite H7. exact (in_combine_r _ _ _ _ H5). clear H2. generalize new_var x H1 H0 H5 H3 H4; clear; induction old_var. simpl; intros. elimtype False; apply H5. intros new_var x; destruct new_var; destruct x; simpl; intros; try (elimtype False; auto; fail). bd H1; bd H0. bd H5; bd H3; bd H4. inversion H5; inversion H3; inversion H4; congruence. inversion H5; inversion H3; subst. elimtype False; apply H7; apply (in_combine_l _ _ _ _ H4). inversion H5; inversion H4; subst. elimtype False; apply H6. generalize x H3; clear; induction old_var; simpl; intros. exact H3. destruct x. simpl in H3; elimtype False; apply H3. simpl in H3. bd H3. inversion H3. po1. po2. apply (IHold_var _ H3). inversion H5; subst. elimtype False; apply H6. generalize x H3; clear; induction old_var; simpl; intros. exact H3. destruct x. simpl in H3; elimtype False; apply H3. simpl in H3. bd H3. inversion H3. po1. po2. apply (IHold_var _ H3). inversion H3; inversion H4; subst. elimtype False; apply H7; apply (in_combine_r _ _ _ _ H5). inversion H3; subst. elimtype False; apply H6; apply (in_combine_l _ _ _ _ H5). inversion H4; subst. elimtype False; apply H7; apply (in_combine_r _ _ _ _ H5). apply (IHold_var _ _ H1 H0 H5 H3 H4). Qed. Lemma In_map_xvar : forall (vl : list var) (v : var) (t : ty) (tyl : list ty), In (x_var v, t) (map (fun x0 : var * ty => (x_var (fst x0), snd x0)) (combine vl tyl)) -> In v vl. induction vl; simpl; auto. destruct tyl; simpl. tauto. intros. bd H. inversion H. po1. po2; apply (IHvl _ _ _ H). Qed. Lemma in_combine_equal : forall (A B : Type) (la : list A) (lb : list B) (a : A), length la = length lb -> In a la -> exists b, In (a,b) (combine la lb). induction la; simpl; intros. elimtype False; apply H0. destruct lb; try discriminate. bd H0. exists b; simpl; po1; congruence. inversion H. destruct (IHla _ _ H2 H0). exists x; po2. Qed. Lemma distinct_map : forall (A B : Type) (la : list A) (lb : list B), distinct A la -> distinct A (map (fun x : A * B => fst x) (combine la lb)). induction la; simpl; auto; intros. bd H. destruct lb; simpl; auto. pa. unfold not; intros H1; apply H2; generalize lb H1; clear; induction la; simpl; auto; intros. destruct lb. simpl in H1; contradiction. simpl in H1; bd H1. po1. po2; apply (IHla _ H1). apply (IHla lb H). Qed. Lemma tr_x_vars : forall (old_var new_var : list var) (x' : var) (y : x), distinct var old_var -> tr_x (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) y <> x_this. intros. caseEq ( tr_x (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) y). unfold not; intros; discriminate. intros. destruct y. assert (~XOrd.eq x_this (x_var v)); simpl; auto. import (XMap.add_3). unfold tr_x in H0. caseEq ( XMap.find (x_var v) (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)))); intros. rewrite H3 in H0. import (XMap.find_1 (H2 _ _ _ _ _ _ H1 (XMap.find_2 H3))); subst. generalize new_var H4; clear; induction old_var; intros. simpl in H4. rewrite XMapFacts.empty_o in H4; discriminate. destruct new_var; simpl in H4. rewrite XMapFacts.empty_o in H4; discriminate. cs (XOrd.eq (x_var a) (x_var v)). import (XMap.add_1). rewrite (XMap.find_1 (H0 _ (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)) _ _ (x_var v0) H)) in H4. discriminate. import (XMap.add_3). apply (IHold_var new_var). apply XMap.find_1. apply (H0 _ _ _ _ _ _ H (XMap.find_2 H4)). rewrite H3 in H0. discriminate. import (XMap.add_1). unfold tr_x in H0. rewrite (XMap.find_1 (H1 _ (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)) x_this x_this (x_var x') (XOrd.eq_refl x_this)) ) in H0. discriminate. Qed. Lemma in_list_find' : forall (y_ty_list : list (x * ty)) (old_var new_var : list var) (y x' v : var) (ty' : ty), ~ In x' new_var -> In (v, y) (combine old_var new_var) -> length y_ty_list = length new_var -> XMap.find (x_var y) (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine (x' :: new_var) (map (fun y0 : lj.x * ty => snd y0) ((x_var x', ty') :: y_ty_list)))) <> None. intros. import (in_combine_r _ _ _ _ H0); clear H0. simpl. cs (XOrd.eq (x_var x') (x_var y)). import (XMap.add_1). rewrite (XMap.find_1 (H3 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine new_var (map (fun y0 : x * ty => snd y0) y_ty_list))) (x_var x') (x_var y) ty' H0)). congruence. import XMap.add_2. assert (exists ty'', XMap.find (x_var y) (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine new_var (map (fun y0 : x * ty => snd y0) y_ty_list))) = Some ty''). generalize y_ty_list H2 H1; clear; induction new_var; simpl; intros. unfold not; intros. elimtype False; apply H2. destruct y_ty_list; try discriminate. bd H2. simpl. rewrite H2; exists (snd p). import (XMap.add_1). rewrite (XMap.find_1 (H _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine new_var (map (fun y0 : x * ty => snd y0) y_ty_list))) (x_var y) (x_var y) (snd p) (XOrd.eq_refl _))). reflexivity. simpl. cs (XOrd.eq (x_var a) (x_var y)). exists (snd p). import (XMap.add_1). rewrite (XMap.find_1 (H0 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine new_var (map (fun y0 : x * ty => snd y0) y_ty_list))) (x_var a) (x_var y) (snd p) H)). reflexivity. simpl in H1; inversion H1. destruct (IHnew_var _ H2 H3). exists x. import (XMap.add_2). apply XMap.find_1. apply (H4 _ _ _ _ _ (snd p) H (XMap.find_2 H0)). bd H4. rewrite (XMap.find_1 (H3 _ _ _ _ _ ty' H0 (XMap.find_2 H4))). congruence. Qed. Lemma equiv_contexts : forall (y_ty_list : list (x*ty)) (old_var new_var : list var) (x' : var) (y : x) (ty' ty'': ty), ~ In x' new_var -> distinct _ new_var -> distinct _ old_var -> length old_var = length new_var -> length new_var = length y_ty_list -> XMap.find y (fold_left (fun (m : XMap.t ty) (p0 : lj.x * ty) => XMap.add (fst p0) (snd p0) m) ((x_this, ty') :: map (fun vd' : vd => match vd' with | vd_def ty''' var' => (x_var var', ty''') end) (map (fun x4 : ty * var => vd_def (fst x4) (snd x4)) (combine (map (fun y0 : lj.x * ty => snd y0) y_ty_list) old_var))) (XMap.empty ty)) = Some ty'' -> XMap.find (tr_x (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t lj.x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj.x) (combine old_var new_var))) y) (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) (XMap.empty ty) (combine (x' :: new_var) (map (fun y0 : lj.x * ty => snd y0) ((x_var x', ty') :: y_ty_list)))) = Some ty''. intros. assert (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) y_ty_list) old_var)) = (map (fun x : var *ty => ((x_var (fst x)), (snd x))) (combine old_var (map (fun y : x * ty => snd y) y_ty_list) ))). rewrite H3 in H2; generalize old_var H2; clear; induction y_ty_list; simpl; intros; destruct old_var; try discriminate. simpl; reflexivity. simpl in H2. simpl. rewrite IHy_ty_list. auto. inversion H2; auto. rewrite H5 in H4. clear H5. assert (distinct x (map (fun x0 : x * ty => fst x0) ((x_this, ty') :: map (fun x0 : var * ty => (x_var (fst x0), snd x0)) (combine old_var (map (fun y0 : x * ty => snd y0) y_ty_list))))). rewrite H3 in H2; generalize y_ty_list H1 H2; clear; induction old_var; intros; destruct y_ty_list; try (simpl in *|-*; discriminate). simpl; tauto. simpl in *|-*; pa. apply and_not_or; pa. unfold not; intros; discriminate. bd H1. inversion H2. import (IHold_var _ H1 H0); bd H. inversion H2. pa. bd H1. unfold not; intros; apply H4; generalize y_ty_list H0 H; clear; induction old_var; intros. simpl; auto. destruct y_ty_list; simpl in *|-*; try discriminate. bd H. inversion H; po1. inversion H0. po2; apply (IHold_var _ H2 H). bd H1. apply (proj2 (IHold_var _ H1 H0) ). import ((proj1 (find_in_list_iff' y ty'' ((x_this, ty') :: map (fun x0 : var * ty => (x_var (fst x0), snd x0)) (combine old_var (map (fun y0 : x * ty => snd y0) y_ty_list))) H5)) H4). clear H5 H4. assert (distinct _ (map (fun x : var * ty => fst x) (combine (x' :: new_var) (map (fun y0 : x * ty => snd y0) ((x_var x', ty') :: y_ty_list))))). generalize x' y_ty_list H H3 H0; clear; induction new_var; intros; destruct y_ty_list; try discriminate. simpl; auto. simpl in *|-*. bd H0. pa. apply and_not_or; pa. bd H. bd H. unfold not; intros; apply H2. inversion H3. generalize y_ty_list H1 H6; clear; induction new_var; intros. simpl in H1; elimtype False; exact H1. destruct y_ty_list; simpl in H6; inversion H6. simpl. simpl in H1; bd H1. po1. po2. apply (IHnew_var _ H1 H0). bd H. inversion H3. apply (( (IHnew_var _ _ H4 H5 H0)) ). caseEq ( XMap.find (tr_x (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) y) (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine (x' :: new_var) (map (fun y0 : x * ty => snd y0) ((x_var x', ty') :: y_ty_list))))); intros; auto. import find_in_var_list_iff. caseEq (tr_x (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) y); intros; rewrite H8 in H5. import ((proj1 (H7 ty v t (combine (x' :: new_var) (map (fun y0 : x * ty => snd y0) ((x_var x', ty') :: y_ty_list))) H4)) H5). clear H5 H7 H4. unfold tr_x in H8. destruct y. assert (XMap.find (x_var v0) (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) = XMap.find (x_var v0) (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))). caseEq (XMap.find (x_var v0) (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))); intros. assert (~ XOrd.eq x_this (x_var v0)). simpl; auto. apply XMap.find_1. import (XMap.add_2). apply (H7 _ _ _ _ _ (x_var x') H5 (XMap.find_2 H4)). caseEq ( XMap.find (x_var v0) (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)))); auto; intros. assert (~ XOrd.eq x_this (x_var v0)). simpl; auto. import (XMap.add_3). rewrite (XMap.find_1 (H10 _ _ _ _ _ (x_var x') H7 (XMap.find_2 H5))) in H4. discriminate. rewrite H4 in H8; clear H4. simpl in H6; bd H6. inversion H6. destruct (in_combine_equal _ _ _ _ _ H2 (In_map_xvar _ _ _ _ H6)). assert (distinct var (map (fun x : var * var => fst x) (combine old_var new_var))). generalize new_var H1; clear; induction old_var; intros. simpl; auto. simpl; destruct new_var. simpl; auto. simpl in *|-*. bd H1. pa. unfold not; intros; apply H2. generalize new_var H; clear; induction old_var; simpl; intros. exact H. destruct new_var. simpl in H. elimtype False; exact H. simpl in H; bd H. po1. po2; apply (IHold_var _ H). apply (IHold_var new_var H1). import (proj2 ((find_in_var_list_iff' v0 x (combine old_var new_var) H5)) H4). rewrite H7 in H8. inversion H8. assert (In (x_var v0, ty'') ((x_this, ty') :: (map (fun x0 : var * ty => (x_var (fst x0), snd x0)) (combine old_var (map (fun y0 : lj.x * ty => snd y0) y_ty_list))))). po2. rewrite H11 in H4. import equiv_lists. apply (sym_eq (equiv_lists y_ty_list new_var old_var v v0 x' ty'' t ty' H0 H1 H H10 H9 H4)). simpl in H6; bd H6. inversion H6. simpl in H9; bd H9. inversion H9; congruence. import (XMap.add_1). rewrite (XMap.find_1 (H4 _ (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)) x_this x_this (x_var x') (XOrd.eq_refl _))) in H8. inversion H8. rewrite H10 in H; elimtype False; apply H. apply (in_combine_l _ _ _ _ H9). destruct (map_snd _ _ y_ty_list). rewrite H4 in H6; elimtype False; generalize x H6; clear. induction old_var. simpl; auto. simpl; intros. destruct x. simpl in H6; exact H6. simpl in H6. bd H6. inversion H6. apply (IHold_var _ H6). import (tr_x_vars old_var new_var x' y H1). elimtype False; apply (H9 H8). unfold tr_x in H5. destruct y. assert (XMap.find (x_var v) (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))) = XMap.find (x_var v) (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))). caseEq (XMap.find (x_var v) (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var))); intros. assert (~ XOrd.eq x_this (x_var v)). simpl; auto. apply XMap.find_1. import (XMap.add_2). apply (H9 _ _ _ _ _ (x_var x') H8 (XMap.find_2 H7)). caseEq ( XMap.find (x_var v) (XMap.add x_this (x_var x') (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)))); auto; intros. assert (~ XOrd.eq x_this (x_var v)). simpl; auto. import (XMap.add_3). rewrite (XMap.find_1 (H10 _ _ _ _ _ (x_var x') H9 (XMap.find_2 H8))) in H7. discriminate. rewrite H7 in H5; clear H7. simpl in H6; bd H6. inversion H6. destruct (in_combine_equal _ _ _ _ _ H2 (In_map_xvar _ _ _ _ H6)). import (distinct_map _ _ _ new_var H1). import (proj2 ((find_in_var_list_iff' v x (combine old_var new_var) H8)) H7). rewrite H9 in H5. import (in_list_find' y_ty_list old_var new_var x x' v ty' H H7 (sym_eq H3)). rewrite H5 in H10; congruence. import (XMap.add_1). rewrite (XMap.find_1 (H7 _ (fold_right (fun (yp : var * var) (m : XMap.t x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty x) (combine old_var new_var)) x_this x_this (x_var x') (XOrd.eq_refl _))) in H5. simpl in H5. rewrite (XMap.find_1 (H7 _ (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) (XMap.empty ty) (combine new_var (map (fun y0 : x * ty => snd y0) y_ty_list))) (x_var x') (x_var x') ty' (XOrd.eq_refl _) ) ) in H5. discriminate. Qed. Lemma find_in_add' : forall (var_list : list var) (ty_list : list ty) (y : x) (ty' : ty) (g : G), (forall x', In x' (map (fun var' : var => x_var var') var_list) -> ~ XMap.In x' g) -> XMap.find y g = Some ty' -> XMap.find y (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) = Some ty'. induction var_list. simpl; intros. exact H0. simpl; intros. destruct ty_list; simpl. exact H0. destruct y. cs (XOrd.eq (x_var a) (x_var v)). assert (~ XMap.In (x_var v) g). apply H. po1. simpl in H1; rewrite (eq_nat_eq _ _ H1). reflexivity. unfold XMap.In in H2; unfold XMap.Raw.PX.In in H2; elimtype False; apply H2. exists ty'; apply (XMap.find_2 H0). apply XMap.find_1. apply XMap.add_2. exact H1. apply XMap.find_2. apply IHvar_list. intros. apply H. po2. exact H0. apply XMap.find_1. apply XMap.add_2. simpl; auto. apply XMap.find_2. apply IHvar_list. intros. apply H. po2. exact H0. Qed. Lemma wf_stmt_list_add : forall (var_list : list var) (ty_list : list ty) (g : G) (p : P) (Ss' : list_s), (forall x', In x' (map (fun var' : var => x_var var') var_list) -> ~ XMap.In x' g) -> wf_stmt_list' p g Ss' -> wf_stmt_list' p (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) Ss'. intros var_list ty_list g p Ss'. elim Ss' using s_list_ind with (P := fun s => (wf_stmt p g s -> (forall x', In x' (map (fun var' : var => x_var var') var_list) -> ~ XMap.In x' g) -> wf_stmt p (fold_right (fun (x4 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) s)); intros; auto. apply wf_new. inversion H; inversion H4; subst. rewrite (find_in_add' var_list ty_list _ _ _ H0 H7); rewrite H7 in H4; exact H4. apply wf_var_assign; inversion H; subst. inversion H4; subst. rewrite (find_in_add' var_list ty_list _ _ _ H0 H1); rewrite H1 in H4; rewrite (find_in_add' var_list ty_list _ _ _ H0 H2); rewrite H2 in H4; exact H4. inversion H; inversion H8; subst. apply (wf_field_read p (fold_right (fun (x4 : lj.var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) var x f cl5 ty5). rewrite (find_in_add' var_list ty_list _ _ _ H0 H6); reflexivity. auto. rewrite (find_in_add' var_list ty_list _ _ _ H0 H10); rewrite H10 in H8; exact H8. inversion H; inversion H8; subst. apply (wf_field_write p (fold_right (fun (x4 : lj.var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) x f y cl5 ty5). rewrite (find_in_add' var_list ty_list _ _ _ H0 H6); reflexivity. auto. rewrite (find_in_add' var_list ty_list _ _ _ H0 H9); rewrite H9 in H8; exact H8. inversion H; inversion H10. apply (wf_mcall y_ty_list p (fold_right (fun (x4 : lj.var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x4)) (snd x4) g0) g (combine var_list ty_list)) var x m cl5 ty'); auto. rewrite (find_in_add' var_list ty_list _ _ _ H0 H7); reflexivity. generalize var_list H9 H0; clear; induction y_ty_list; simpl; intros; auto. apply Cons_sty_opt_list; (try exact (ty_def cl_object)). inversion H9; inversion H2; subst. rewrite (find_in_add' var_list ty_list _ _ _ H0 H6); rewrite H6 in H2; exact H2. inversion H9; apply (IHy_ty_list _ H5 H0). rewrite (find_in_add' var_list ty_list _ _ _ H0 H12); rewrite H12 in H10; exact H10. apply wf_if. inversion H1; subst. bd H8; inversion H8. rewrite (find_in_add' var_list ty_list _ _ _ H2 H3); rewrite H3 in H8; rewrite (find_in_add' var_list ty_list _ _ _ H2 H4); rewrite H4 in H8; po1. rewrite (find_in_add' var_list ty_list _ _ _ H2 H3); rewrite H3 in H8; rewrite (find_in_add' var_list ty_list _ _ _ H2 H4); rewrite H4 in H8; po2. inversion H1; apply H; auto. inversion H1; apply H0; auto. apply wf_block. applyI wf_stmt_list'_iff. apply H; auto. applyI wf_stmt_list'_iff; inversion H0; auto. apply Nil_wf_stmt_list'. apply Cons_wf_stmt_list'. inversion H2; subst. apply H; auto. inversion H2; subst. apply H0; auto. Qed. Lemma in_stack_in_context : forall (p : P) (g : G) (h : H) (l : L) (x' : x), ~ XMap.In x' l -> wf_stck p g h l -> ~ XMap.In x' g. intros. unfold XMap.In in *|-*; unfold XMap.Raw.PX.In in *|-*. unfold not; intros H1; apply H; bd H1; clear H. inversion H0; subst. import (H _ (MapsTo_mem _ _ _ H1)). bd H2. inversion H2. exists v_null; apply XMap.find_2; auto. exists (v_oid oid5); apply XMap.find_2; auto. Qed. Lemma sty_cl_object : forall (ty' ty'': ty) (p : P), ty' = (ty_def cl_object) -> sty_one p ty' ty'' -> ty'' = (ty_def cl_object). intros. induction H0. rewrite H in H0; inversion H0. auto. inversion H. auto. Qed. Theorem preservation : forall (config1 config2 : config) (g : G) (p : P), wf_config p g config1 -> reduce config1 p config2 -> exists g', (wf_config p g' config2 /\ (forall (x': x) (ty': ty), XMap.MapsTo x' ty' g-> XMap.MapsTo x' ty' g')). Proof. intros. inversion H0; subst; (*** All the NPEs***) try (exists g; pa; try apply wf_all_npe; intros; auto; fail). (***S_New***) exists g; pa. clear H0. inversion H; subst. apply wf_all; auto. apply wf_heap; intros. case (eq_nat_dec oid5 oid0); intros. subst; exists cl5; repeat pa. assert ( NatMap.find oid0 (NatMap.add oid0 (cl5, init_field_map (fields p cl5)) H5) = Some (cl5, init_field_map (fields p cl5))). clear. apply NatMap.find_1. apply (proj2 (NatMapFacts.add_mapsto_iff H5 oid0 oid0 (cl5, init_field_map (fields p cl5)) (cl5, init_field_map (fields p cl5)))). po1; pa; unfold NatMap.E.eq; unfold NatOrd.eq; apply eq_nat_refl. rewrite H2; simpl; apply refl_equal. inversion H11; inversion H4; inversion H16; subst. destruct cl5; destruct ty'. rewrite H19 in H16; import (sty_option_In_p _ _ _ H16); bd H2; apply (In_names _ _ _ _ _ H2). clear; induction p; simpl; try po1; destruct a; simpl; po2. intros. import (proj2 (ftype_in_fields _ _ _) H2). caseEq (ftype p cl5 f5); try (intros G1; rewrite G1 in H3; elimtype False; apply H3; apply refl_equal). intros t G1; rewrite G1 in H3. exists t; pa. import (NatMap.add_1). rewrite (NatMap.find_1 (H4 _ H5 oid0 oid0 (cl5, init_field_map (fields p cl5))(eq_nat_refl _))). assert (NatMap.find f5 (snd (cl5, init_field_map (fields p cl5))) = Some v_null). generalize H2; clear. induction (fields p cl5); intros. inversion H2. case (eq_nat_dec a f5); intros. rewrite e; simpl. apply NatMap.find_1; apply NatMap.add_1; auto. simpl in H2; bd H2. simpl. apply NatMap.find_1. apply NatMap.add_2. unfold not; unfold NatMap.E.eq; unfold NatOrd.eq; intros. import (eq_nat_eq _ _ H); auto. apply NatMap.find_2; auto. rewrite H7. apply (wf_null p (NatMap.add oid0 (cl5, init_field_map (fields p cl5)) H5) (Some t) t). reflexivity. assert (NatMap.mem oid0 H5 = true). assert (~NatMap.E.eq oid5 oid0). unfold NatMap.E.eq; unfold NatOrd.eq; auto with arith. import NatMapFacts.mem_in_iff. import ((proj2 (H3 _ _ _) H0)). unfold NatMap.In in H4; unfold NatMap.Raw.PX.In in H4; destruct H4. import (NatMap.add_3 H2 H4). apply (NatMapsTo_mem _ _ _ H7). inversion H9. import (H4 _ H2); bd H12; clear H4. import NatMapFacts.mem_in_iff. import ((proj2 (H4 _ _ _) H2)). clear H4; unfold NatMap.In in H13; unfold NatMap.Raw.PX.In in H13; destruct H13. exists x. import NatMap.add_2. unfold NatMap.E.eq in H13; unfold NatOrd.eq in H13. assert (~ eq_nat oid5 oid0). unfold not; intros. rewrite (eq_nat_eq _ _ H14) in n. apply n; reflexivity. unfold NatMap.MapsTo in H13. import (H13 _ _ _ _ _ (cl5, init_field_map (fields p cl5)) H14 H4). rewrite (proj1 (NatMapFacts.find_mapsto_iff _ _ _) H17); repeat pa. rewrite (proj1 (NatMapFacts.find_mapsto_iff _ _ _ )H4 ) in H15. exact H15. intros. import (proj2 (ftype_in_fields _ _ _) H18). import (H12 f5 H18); bd H20. exists x1; pa. rewrite (NatMap.find_1 H4) in H20. inversion H20; subst. apply (wf_null p (NatMap.add oid5 (cl5, init_field_map (fields p cl5)) H5) (Some x1) x1 ); auto. apply (wf_object p (NatMap.add oid5 (cl5, init_field_map (fields p cl5)) H5) oid1 (Some x1)). cs (oid1 = oid5). rewrite H3. import NatMap.add_1. import (H7 _ H5 oid5 oid5 (cl5, init_field_map (fields p cl5)) (eq_nat_refl oid5)). rewrite (NatMap.find_1 H8). simpl. rewrite H3 in H26. assert (NatMap.find oid5 H5 = None). applyI (NatMapFacts.not_find_mapsto_iff). applyI (NatMapFacts.not_mem_in_iff). rewrite H21 in H26; inversion H26; discriminate. assert (~ eq_nat oid5 oid1). unfold not; intros. rewrite (eq_nat_eq _ _ H7) in H3. apply H3; reflexivity. caseEq ( NatMap.find oid1 H5); intros; rewrite H8 in H26. import NatMap.find_2. unfold NatMap.MapsTo in H21. import (H21 _ _ _ _ H8). import (H13 _ H5 oid5 oid1 p0 (cl5, init_field_map (fields p cl5)) H7 H24). rewrite (NatMap.find_1 H25); auto. inversion H26; discriminate. inversion H10. apply wf_stack; intros; subst. import (H2 _ H12); bd H0. exists x; repeat pa. cs (x5 = x_var var5). rewrite H3. import XMap.add_1. import XMap.find_1. rewrite (H13 _ _ _ _ (H4 _ L5 (x_var var5) (x_var var5) (v_oid oid5) (XMap.E.eq_refl (x_var var5)))). apply wf_object. clear H4 H13. import NatMap.add_1. import NatMap.find_1. rewrite (H13 _ _ _ _ (H4 _ H5 _ _ (cl5, init_field_map (fields p cl5)) (NatMap.E.eq_refl oid5))). simpl. inversion H11; inversion H16; congruence. import XMap.add_2. assert (~ XMap.E.eq (x_var var5) x5). unfold not; intros; unfold XMap.E.eq in H13; unfold XOrd.eq in H13. apply H3; destruct x5; try (rewrite (eq_nat_eq var5 v); auto; reflexivity). elimtype False; apply H13. caseEq (XMap.find x5 L5); intros. import XMap.find_1. rewrite (H15 _ _ _ _ (H4 _ _ _ _ v (v_oid oid5) H13 (XMap.find_2 H14))). inversion H0; subst. rewrite <- H14; rewrite <- H17; rewrite H20. apply (wf_null p (NatMap.add oid5 (cl5, init_field_map (fields p cl5)) H5) (Some ty5) ty5); auto. rewrite <- H14; rewrite <- H17. apply wf_object. cs (oid0 = oid5). assert (NatMap.find oid0 H5 = None). applyI (NatMapFacts.not_find_mapsto_iff). applyI (NatMapFacts.not_mem_in_iff). rewrite <- H16 in H1; exact H1. rewrite H18 in H20; inversion H20; discriminate. assert (~ eq_nat oid5 oid0). unfold not; intros. rewrite (eq_nat_eq _ _ H18) in H16. apply H16; reflexivity. caseEq (NatMap.find oid0 H5); intros; rewrite H19 in H20. clear H15 H4. import (NatMap.add_2); import (NatMap.find_1). rewrite (H15 _ _ _ _ (H4 _ _ _ _ _ (cl5, init_field_map (fields p cl5)) H18 (NatMap.find_2 H19))); exact H20. inversion H20; discriminate. rewrite H14 in H0; inversion H0. inversion H11; auto. intros. auto. (*** var_assign ***) exists g; pa. inversion H; subst. apply wf_all; auto. inversion H11. apply wf_stack; intros. import (H3 _ H13); bd H14. exists x; repeat pa. cs (x0 = x_var var5). rewrite H15. import (XMap.add_1). assert (XOrd.eq (x_var var5) (x_var var5)). simpl; apply (eq_nat_refl). inversion H12; subst; inversion H22; subst. rewrite H17 in H8; inversion H8; subst. import (H3 _ (MapsTo_mem _ _ _ (XMap.find_2 H2))); bd H9. rewrite H1 in H9. rewrite <- H21 in H9; rewrite H2 in H9. rewrite (XMap.find_1 ((H16 _ L5 (x_var var5) (x_var var5) v5) H19)). destruct v5. apply (wf_null p H5 (Some x) x); reflexivity. apply wf_object. inversion H9. destruct (NatMap.find o H5). rewrite H2 in H8. apply (sty_opt p (Some (ty_def (fst p0))) (Some x) (ty_def (fst p0)) x); auto. inversion H27; inversion H8; subst. rewrite H35 in H30; inversion H30. rewrite <- H20 in H31. inversion H36; inversion H29. rewrite H26; apply (sty_transitive p _ _ _ H31 H37). inversion H27. inversion H29. assert (~XMap.E.eq (x_var var5) x0). unfold not; intros. apply H15. unfold XMap.E.eq in H16; unfold XOrd.eq in H16. destruct x0. rewrite (eq_nat_eq _ _ H16); reflexivity. elimtype False; exact H16. import (XMap.add_2). caseEq (XMap.find x0 L5); intros. rewrite (XMap.find_1 (H19 _ _ _ _ _ v5 H16 (XMap.find_2 H20))). rewrite H20 in H14; exact H14. rewrite H20 in H14; inversion H14. inversion H12; auto. auto. (*** field read ***) exists g; pa. inversion H; subst. apply wf_all; auto. apply wf_stack; intros. cs (x0 = x_var var5). inversion H13; inversion H9. inversion H11; inversion H12; subst. import (H29 _ (MapsTo_mem _ _ _ (XMap.find_2 H21))); bd H4. rewrite H1 in H4. inversion H4; subst. caseEq (NatMap.find oid5 H5); intros; rewrite H6 in H18; rewrite H6 in H2; try discriminate. import (H25 _ (NatMapsTo_mem _ _ _ (NatMap.find_2 H6))); bd H7; clear H25. rewrite H6 in H19; inversion H19. inversion H18; inversion H16. rewrite <- H31 in H25; inversion H24; rewrite <- H32 in H25; destruct x. rewrite H21 in H10; inversion H10. assert (ftype p c f5 <> None); try (unfold not; intro G1; rewrite H33 in H22; rewrite G1 in H22; discriminate). import (subtype_fields _ _ _ _ _ _ (refl_equal (ty_def (fst p0))) (refl_equal (ty_def c)) H25 H8 (proj1 (ftype_in_fields _ _ _) H30)). inversion H19; subst; import (H7 _ H34); bd H17; rewrite H6 in H17. inversion H9; subst. rewrite H21 in H35; inversion H35; subst. clear H10 H24 H35. import (H29 _ H3); bd H10. exists x0; repeat pa. import (XMap.add_1). assert (XOrd.eq (x_var var5) (x_var var5)). simpl; apply (eq_nat_refl). rewrite (XMap.find_1 ((H24 _ L5 (x_var var5) (x_var var5) v5) H26)). clear H26 H24. rewrite <- H2. rewrite <- H27. rewrite <- H28 in H17. rewrite <- H37 in H38. import (sty_ftype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _ ) H25 H8 H22). rewrite H24 in H17. rewrite H22 in H38. rewrite H2. destruct v5. apply (wf_null p H5 _ _ H27). apply wf_object. rewrite H2 in H17. inversion H17. destruct (NatMap.find o H5); destruct (XMap.find (x_var var5) g). apply (sty_opt p _ _ _ _ (refl_equal (Some (ty_def (fst p1)))) (refl_equal (Some t))). apply (sty_transitive p (ty_def (fst p1)) t ty5). inversion H39; congruence. inversion H38; congruence. inversion H38; discriminate. inversion H39; discriminate. inversion H39; discriminate. inversion H12. import (H7 _ H3); bd H16. exists x; repeat pa. assert (~XOrd.eq (x_var var5) x0). unfold not; intros; destruct x0. simpl in H17. rewrite (eq_nat_eq _ _ H17) in H4; apply H4; reflexivity. simpl in H17; exact H17. import (XMap.add_2). inversion H16. rewrite (XMap.find_1 (H18 _ L5 (x_var var5) x0 v_null v5 H17 (XMap.find_2 (sym_eq H22)))). apply (wf_null p H5 (Some x) x); apply refl_equal. rewrite (XMap.find_1 (H18 _ L5 (x_var var5) x0 (v_oid oid0) v5 H17 (XMap.find_2 (sym_eq H22)))). congruence. inversion H13; auto. auto. (*** field_write ***) exists g; pa. inversion H; subst. apply wf_all; auto. inversion H11; subst. inversion H13. import (wf_fwrite_lookupl _ _ _ _ _ _ _ H7 H12); bd H15. rewrite H1 in H19; inversion H19. import (H18 _ (sym_eq H17)); bd H16. rewrite H16. import (H4 _ (NatMapsTo_mem _ _ _ (NatMap.find_2 H16))); bd H20. rewrite H16 in H23. apply wf_heap; intros. cs (oid0 = oid5); subst. exists (fst x1); repeat pa. import (NatMap.add_1). rewrite (NatMap.find_1 (H3 _ H5 oid5 oid5 (fst x1, NatMap.add f5 v5 (snd x1)) (NatOrd.eq_refl oid5))). simpl; auto. inversion H23. rewrite <- H6 in H24. inversion H24; auto. clear H0. inversion H23; intros. rewrite <- H3 in *|-*; clear H3 H21 H19 H18. import (H20 _ H0); bd H3. destruct x1; simpl in *|-*. exists x; pa. import (NatMap.add_1). rewrite (NatMap.find_1 (H6 _ H5 oid5 oid5 (c, NatMap.add f5 v5 t) (NatOrd.eq_refl oid5))). simpl. inversion H12. cs (f0 = f5); subst. inversion H7; subst. import (H17 _ (MapsTo_mem _ _ _ (XMap.find_2 H25))); bd H9. rewrite H1 in H9; rewrite <- H21 in H9; rewrite H25 in H9. inversion H9. rewrite H16 in H30. simpl in H30. rewrite <- H10. inversion H30; inversion H32; inversion H33. rewrite <- H40 in H34; rewrite <- H39 in H34. rewrite (sty_ftype p c cl5 f5 _ _ _ (refl_equal (ty_def c)) (refl_equal (ty_def cl5)) H34 H8 H26). caseEq (XMap.find y g); intros. import (H17 _ (MapsTo_mem _ _ _ (XMap.find_2 H38))); bd H41. rewrite <- H44 in H41; rewrite H2 in H41. import NatMap.add_1. rewrite (NatMap.find_1 (H6 _ t f5 f5 v5 (NatOrd.eq_refl f5))). inversion H41. apply (wf_null p (NatMap.add oid5 (c, NatMap.add f5 v_null t) H5) (Some ty5) ty5); reflexivity. apply wf_object. cs (oid1 = oid5). rewrite H51. rewrite (NatMap.find_1 (H6 _ H5 oid5 oid5 (c, NatMap.add f5 (v_oid oid5) t) (NatOrd.eq_refl oid5))). simpl; subst. rewrite H44 in H27; rewrite H44 in H41. inversion H41; subst. rewrite H16 in H31. simpl in H31. inversion H27; inversion H31. rewrite H18 in H39; inversion H39; rewrite H50 in H28. import (sty_transitive p _ _ _ H40 H28). inversion H37; inversion H19. rewrite <- H52 in H48. apply (sty_opt p (Some (ty_def c)) (Some ty') _ _ (refl_equal _) (refl_equal _) H48). assert (~NatOrd.eq oid5 oid1). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H51; apply H51; reflexivity. import NatMap.add_2. caseEq (NatMap.find oid1 H5); intros. rewrite (NatMap.find_1 (H53 _ H5 oid5 oid1 _ (c, NatMap.add f5 (v_oid oid1) t) H52 (NatMap.find_2 H54))). rewrite H54 in H49. generalize H27 H49; clear; intros. inversion H27; inversion H49; subst. inversion H0; inversion H5; rewrite H in H6; inversion H6. rewrite H8 in H1. rewrite <- H4 in H7. import (sty_transitive p _ _ _ H7 H1). apply (sty_opt p (Some (ty_def (fst p0))) (Some ty') _ _ (refl_equal _) (refl_equal _) H2). rewrite H54 in H49; inversion H49; discriminate. rewrite H38 in H27; inversion H27; discriminate. assert (~NatOrd.eq f5 f0). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H25; apply H25; reflexivity. import NatMap.add_2. rewrite H16 in H3. caseEq (NatMap.find f0 t); intros. rewrite (NatMap.find_1 (H18 _ t f5 f0 _ v5 H9 (NatMap.find_2 H19))). simpl in H3; rewrite H19 in H3. inversion H3. apply (wf_null p (NatMap.add oid5 (c, NatMap.add f5 v5 t) H5) _ x (refl_equal _)). apply wf_object. cs (oid0 = oid5). rewrite H30. rewrite (NatMap.find_1 (H6 _ H5 oid5 oid5 (c, NatMap.add f5 v5 t) (NatOrd.eq_refl oid5))). simpl. rewrite H30 in H28; rewrite H16 in H28; simpl in H28; exact H28. assert (~NatOrd.eq oid5 oid0). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H30; apply H30; reflexivity. import NatMap.add_2. caseEq (NatMap.find oid0 H5); intros. rewrite (NatMap.find_1 (H32 _ H5 oid5 oid0 _ (c, NatMap.add f5 v5 t) H31 (NatMap.find_2 H33))). simpl; rewrite H33 in H28; exact H28. rewrite H33 in H28; inversion H28; discriminate. simpl in H3; rewrite H19 in H3. inversion H3. clear H18 H20 H23 H24 x2 H19. import (NatMapsTo_mem2 _ _ H21); destruct H3; clear H21. assert (~NatOrd.eq oid5 oid0). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H22; apply H22; reflexivity. import NatMap.add_3. import (H9 _ H5 oid5 oid0 x _ H6 H3). import (NatMapsTo_mem _ _ _ H10); clear H10 H3 H9. import (H4 _ H17); bd H3. import (NatMap.add_2). caseEq (NatMap.find oid0 H5); intros; rewrite H10 in H18; try discriminate. inversion H18; clear H18. rewrite (NatMap.find_1 (H9 _ H5 oid5 oid0 p0 (fst x1, NatMap.add f5 v5 (snd x1)) H6 (NatMap.find_2 H10))). exists x2; repeat pa. congruence. intros. import (H3 _ H18); bd H20. exists x3; pa. rewrite <- H25 in *|-*. rewrite H10 in H20. inversion H20. apply (wf_null p (NatMap.add oid5 (fst x1, NatMap.add f5 v5 (snd x1)) H5) (ftype p x2 f0) _ H28). cs (oid1 = oid5). rewrite H30. apply wf_object. import (NatMap.add_1). rewrite (NatMap.find_1 (H31 _ H5 oid5 oid5 (fst x1, NatMap.add f5 v5 (snd x1)) (NatOrd.eq_refl _ ))). simpl. inversion H7; subst. rewrite H16 in H28. exact H28. assert (~NatOrd.eq oid5 oid1). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H30; apply H30; reflexivity. caseEq (NatMap.find oid1 H5); intros; rewrite H32 in H28; try (inversion H28; discriminate). import (NatMap.add_2). apply wf_object. rewrite (NatMap.find_1 (H33 _ H5 oid5 oid1 p1 (fst x1, NatMap.add f5 v5 (snd x1)) H31 (NatMap.find_2 H32) )). exact H28. apply wf_stack; intros. inversion H12. import (H6 _ H3); bd H15; subst. exists x; repeat pa. inversion H13; inversion H9; subst. import (H6 _ (MapsTo_mem _ _ _ (XMap.find_2 H24))); bd H4. rewrite H1 in H4; inversion H4; subst. caseEq (NatMap.find oid5 H5); intros; rewrite H7 in H22; try (inversion H22; discriminate). destruct (XMap.find x0 L5); inversion H15; try discriminate. apply (wf_null p (NatMap.add oid5 (fst p0, NatMap.add f5 v5 (snd p0)) H5) (Some x) x (refl_equal _)). apply wf_object. cs (oid0 = oid5). rewrite H29. import (NatMap.add_1). rewrite (NatMap.find_1 (H30 _ H5 oid5 oid5 (fst p0, NatMap.add f5 v5 (snd p0)) (NatOrd.eq_refl _ ))). simpl. rewrite H29 in H27. rewrite H7 in H27. exact H27. assert (~NatOrd.eq oid5 oid0). unfold not; intros G1; rewrite (eq_nat_eq _ _ G1) in H29; apply H29; reflexivity. caseEq (NatMap.find oid0 H5); intros; rewrite H31 in H27; try (inversion H27; discriminate). import (NatMap.add_2). rewrite (NatMap.find_1 (H32 _ H5 oid5 oid0 p1 (fst p0, NatMap.add f5 v5 (snd p0)) H30 (NatMap.find_2 H31) )). exact H27. inversion H13. exact H10. auto. (*** mcall ***) import (big_list_breakdown big_list); bd H10; rewrite H13 in *|-*; clear H13. 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 H14 in H10, H15, H16; clear H14 H0. inversion H; subst. inversion H21; inversion H12; subst. destruct cl0. destruct z; destruct c; simpl in H3. inversion H20; subst. import (H11 _ (MapsTo_mem _ _ _ (XMap.find_2 H28))); bd H0. rewrite H1 in H0; rewrite <- H22 in H0; rewrite H28 in H0. inversion H0. rewrite H2 in H26; inversion H26; subst. inversion H32; inversion H33. rewrite <- H17 in H34; rewrite <- H24 in H34. import (sty_mtype _ _ _ _ _ _ _ (refl_equal _) (refl_equal _) H34 H29 H14). import (wf_prog_wf_mb _ _ _ _ _ _ _ _ H14 H13 H3); bd H25. exists (fold_right (fun (x : var*ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g (combine (cons x' x1) (map (fun y : lj.x * ty => snd y) (cons (x_var x', x3) y_ty_list)))); pa. apply wf_all; auto. (** wf_stack**) apply wf_stack; intros. cs (XMap.find x4 g = None). (***XMap.find x4 g = None ***) cs (x4 = x_var x'). (*** x4 = x_var x' ***) exists x3; simpl; repeat pa. rewrite H40. apply XMap.find_1. apply XMap.add_1. simpl; auto. apply eq_nat_refl. import XMap.add_1. rewrite H40; rewrite (XMap.find_1 (H41 _ (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) L5 (combine x1 x2)) (x_var x') (x_var x') (v_oid o) (XOrd.eq_refl _))). apply wf_object. rewrite H2. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) H25). (*** x4 <> x_var x'***) assert (exists ty', exists v', x4 = (x_var v') /\ In (v', ty') (combine x1 (map (fun y : lj.x * ty => snd y) y_ty_list))). assert (~ XOrd.eq (x_var x') x4). destruct x4; simpl; auto; unfold not; intros G1; apply H40; rewrite (eq_nat_eq _ _ G1); auto. generalize y_ty_list H27 H35 H2 H41; clear; induction x1; intros. simpl. simpl in H27. elimtype False. import (XMapsTo_mem2 _ _ H27); clear H27; bd H. import (XMap.add_3 H41 H). rewrite (XMap.find_1 H0) in H35. discriminate. destruct y_ty_list. simpl in H27. import (XMapsTo_mem2 _ _ H27); clear H27; bd H. import (XMap.add_3 H41 H). rewrite (XMap.find_1 H0) in H35. discriminate. simpl in *|-*. fold (XOrd.eq (x_var x') x4) in *. cs (XOrd.eq (x_var a) x4). exists (snd p); exists a; pa. unfold XOrd.eq in H. destruct x4. rewrite (eq_nat_eq _ _ H); reflexivity. contradiction. po1. import (XMap.add_3). import (XMapsTo_mem2 _ _ H27); bd H1. import (XMap.add_3 H41 H1). import (XMap.add_3 H H3). import (IHx1 _ (MapsTo_mem _ _ _ (XMap.add_2 x3 H41 H4)) H35 H2 H41). bd H6. exists x0; exists x2; auto. bd H41. assert (~ XOrd.eq (x_var x') x4). destruct x4; simpl; auto; unfold not; intros G1; apply H40; rewrite (eq_nat_eq _ _ G1); auto. exists x6; repeat pa. rewrite H44 in *. simpl; apply XMap.find_1. import XMap.add_2. apply (H43 _ (fold_right (fun (x8 : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x8)) (snd x8) g0) g (combine x1 (map (fun y0 : lj.x * ty => snd y0) y_ty_list))) (x_var x') (x_var x7) x6 x3 H42). generalize y_ty_list H41 H10 H4; clear; induction x1; intros y_ty_list H H0 H1. simpl in H; elimtype False; exact H. destruct (y_ty_list). simpl in H; elimtype False; exact H. simpl in H, H0, H1; simpl. bd H1; bd H. inversion H. apply XMap.add_1. auto. cs (XOrd.eq (x_var a) (x_var x7)). import (in_combine_l _ _ _ _ H). rewrite (eq_nat_eq _ _ H2) in H4. elimtype False; apply H4; generalize H3; clear; induction x1; simpl; intros; auto. bd H3. po1; congruence. po2; auto. inversion H0. apply (XMap.add_2 (snd p) H2 (IHx1 _ H H5 H1)). import (in_combine_r _ _ _ _ H41); clear H41. assert (exists ty', In (ty',x6) y_ty_list). generalize H43; clear; induction y_ty_list; simpl; intros. contradiction. destruct a; simpl; intros. bd H43. simpl in H43; rewrite H43; exists x; po1. import (IHy_ty_list H43). bd H. exists x0; po2. bd H41. assert (In (p, XMap.find x8 g, Some x6) (map (fun y : lj.x * ty => (p, XMap.find (fst y) g, Some (snd y))) y_ty_list)). generalize H41; clear; induction y_ty_list. intros H; simpl in H. elimtype False; apply H. intros H. simpl in H. bd H. rewrite H; simpl. po1. destruct a; simpl; po2. apply (IHy_ty_list H). import (in_sty_opt_wf_type _ _ x6 H45 H30 (refl_equal _) H14); simpl in *|-*; auto. import (in_combine_l _ _ _ _ H41). rewrite map_fst_pair' in H9. rewrite H10 in H16; import (in_list_find x7 x1 x2 L5 H16 H43); bd H45. rewrite H44 in H42. rewrite H44. rewrite (XMap.find_1 (XMap.add_2 (v_oid o) H42 (XMap.find_2 H45))). destruct x8. apply (wf_null p H5 _ _ (refl_equal (Some x6) )). apply wf_object. assert (exists y, In (x7, (y,x6)) (combine x1 y_ty_list)). generalize y_ty_list H41; clear; induction x1. simpl; intros yl H; elimtype False; exact H. destruct y_ty_list; simpl; intros. contradiction. bd H41. exists (fst p). inversion H41; destruct p; simpl; po1. destruct (IHx1 _ H41). exists x; po2. bd H46. assert (XMap.find x8 L5 = Some (v_oid o0)). assert (distinct var x1). generalize H4; clear; induction x1; simpl; intros. exact H4. bd H4. pa. unfold not; intros; apply H1. clear H1 IHx1 H4; induction x1. simpl in H; elimtype False; apply H. simpl in H; bd H. rewrite H; simpl; po1. simpl; po2; apply (IHx1 H). auto. import (In_combine_trans _ _ _ _ _ _ _ _ _ H49 H46 H47). generalize x2 y_ty_list H9 H50; clear. induction x2; simpl; intros. contradiction. destruct (y_ty_list); simpl in H50; try (contradiction). bd H50. inversion H50; subst; inversion H9. exact H2. simpl in H9; inversion H9; subst. apply (IHx2 _ H4 H50). assert (sty_option p (XMap.find x8 g) (Some x6)). import (in_combine_r _ _ _ _ H46). generalize H50 H30; clear; induction y_ty_list; simpl; intros H H1. contradiction. bd H. rewrite H in H1; inversion H1; subst. exact H3. apply (IHy_ty_list H). simpl in H1; inversion H1; auto. inversion H50; subst. inversion H52. import (H11 _ (MapsTo_mem _ _ _ (XMap.find_2 H51))). bd H17. rewrite H47 in H17; rewrite H55 in H51, H50; inversion H17. destruct (NatMap.find o0 H5); inversion H59. rewrite <- H24 in *|-*. apply (sty_opt p (Some (ty_def (fst p0))) (Some x6) _ _ (refl_equal _ ) (refl_equal _)); subst. inversion H62; inversion H59; subst. inversion H24. rewrite H58; inversion H54. rewrite <- H60 in H57; inversion H51; subst. rewrite H64 in H57; apply (sty_transitive p _ _ _ H57 H53). discriminate. import (length_build_big_list (map (fun y : lj.x * ty => fst y) y_ty_list) x0 x1 x2). rewrite H45; congruence. rewrite (length_build_big_list (map (fun y : lj.x * ty => fst y) y_ty_list) x0 x1 x2); congruence. (*** XMap.find x4 = Some t***) caseEq (XMap.find x4 g); intros; try congruence. simpl. assert (~XOrd.eq (x_var x') x4). import (in_stack_in_context _ _ _ _ _ H7 H20). unfold not; intros; unfold XMap.In in H41; unfold XMap.Raw.PX.In in H41; bd H41. destruct x4; try contradiction. simpl in H42; rewrite <- (eq_nat_eq _ _ H42) in H35, H40. apply (H41 t0); apply XMap.find_2; auto. assert (XMap.find x4 (XMap.add (x_var x') x3 (fold_right (fun (x : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g0) g (combine x1 (map (fun y : lj.x * ty => snd y) y_ty_list)))) = Some t0). generalize x1 x0 x2 y_ty_list H7 H6 H4 H10 H8 H20 H40 H41 H15 H16; clear; intros x1. induction x1; intros x0 x2 y_ty_list H H0 H2 H3 H4 H6 H7 H8 H9 H10. simpl; auto. apply XMap.find_1. apply (XMap.add_2 x3 H8 (XMap.find_2 H7)). destruct y_ty_list; simpl; auto. apply XMap.find_1. apply (XMap.add_2 x3 H8 (XMap.find_2 H7)). simpl in H2; bd H2; simpl in H3; inversion H3. destruct x2; simpl; try discriminate; destruct x0; simpl; try discriminate. simpl in H4; bd H4; simpl in H9; inversion H9; simpl in H10; inversion H10. assert ( (forall x' : x, In x' (map (fun var' : var => x_var var') x1) -> ~ XMap.In x' L5)). intros; apply H0; simpl; po2. import (XMap.add_3 H8 (XMap.find_2 (IHx1 x0 x2 y_ty_list H H1 H2 H11 H13 H6 H7 H8 H14 H15))). apply XMap.find_1. cs (XOrd.eq (x_var a) x4). destruct x4; try contradiction. assert (~XMap.In (x_var a) L5). apply H0; simpl; po1. import (in_stack_in_context _ _ _ _ _ H18 H6). unfold XMap.In in H19; unfold XMap.Raw.PX.In in H19; bd H19. simpl in H17; rewrite <- (eq_nat_eq _ _ H17) in H7. elimtype False; apply (H19 t0); apply (XMap.find_2 H7). apply (XMap.add_2 x3 H8 (XMap.add_2 (snd p0) H17 H16)). exists t0; repeat pa. import (H11 _ (MapsTo_mem _ _ _ (XMap.find_2 H40))). bd H43. rewrite H46 in H40; inversion H40; subst. exact H47. assert (forall a1 a2 t, XMap.find x4 L5 = Some t -> ~XMap.In (x_var x') L5 -> (forall x' : lj.x, In x' (map (fun var' : var => x_var var') a1) -> ~ XMap.In x' L5) -> ~ XOrd.eq (x_var x') x4 -> XMap.find x4 (XMap.add (x_var x') (v_oid o) (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) L5 (combine a1 a2))) = XMap.find x4 L5). clear; induction a1; intros. simpl; auto. rewrite H. apply (XMap.find_1 (XMap.add_2 (v_oid o) H2 (XMap.find_2 H))). destruct a2; simpl; auto. rewrite H; apply (XMap.find_1 (XMap.add_2 (v_oid o) H2 (XMap.find_2 H))). assert (~XOrd.eq (x_var a) x4). unfold not; intros. destruct x4; simpl in H1. apply (H1 (x_var a)). simpl; po1. rewrite <- (eq_nat_eq _ _ H3) in H. unfold XMap.In; unfold XMap.Raw.PX.In. exists t; apply XMap.find_2; exact H. exact H3. assert (forall x' : x, In x' (map (fun var' : var => x_var var') a1) -> ~ XMap.In x' L5). intros; apply H1; po2. rewrite H in IHa1; import (XMap.add_3 H2 (XMap.find_2 (IHa1 a2 t (refl_equal _) H0 H4 H2))). rewrite H; apply (XMap.find_1 (XMap.add_2 (v_oid o) H2 (XMap.add_2 v H3 H5))). import (H11 _ (MapsTo_mem _ _ _ (XMap.find_2 H40))). bd H44. rewrite H40 in H47; inversion H47; subst. inversion H44. rewrite (H43 x1 x2 _ (sym_eq H24) H7 H6 H41). exact H44. rewrite (H43 x1 x2 _ (sym_eq H24) H7 H6 H41). exact H44. (*** Well-formedness of new statements***) applyI wf_stmt_list_app; pa. (*** Block of Translated Statements***) applyI wf_stmt_list_s. applyI wf_stmt_list'_iff. apply wf_stmt_list_add_g. apply (wf_trans_stmt'' p (fold_left (fun (m : XMap.t ty) (p : lj.x * ty) => XMap.add (fst p) (snd p) m) ((x_this, x3) :: 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 : lj.x * ty => snd y) y_ty_list) x0))) (XMap.empty ty))). exact H36. intros; apply equiv_contexts; try congruence. rewrite map_snd_fst'' in H8. exact H8. rewrite length_build_big_list; congruence. generalize H4; clear; induction x1. simpl; auto. simpl; intros. bd H4; pa. unfold not; intros H2; apply H1; generalize H2; clear; induction x1; simpl; auto. intros H2; bd H2. rewrite H2; po1. po2; apply (IHx1 H2). apply (IHx1 H4). generalize y_ty_list H10; clear; induction x1; simpl; intros. destruct y_ty_list; auto; discriminate. destruct y_ty_list; auto. simpl in *|-*; auto. exact H27. intros; apply tr_x_vars. auto. (***Original Statement Block***) simpl. apply Cons_wf_stmt_list. apply wf_var_assign. caseEq ((XMap.find y (fold_left (fun (m : XMap.t ty) (p : lj.x * ty) => XMap.add (fst p) (snd p) m) ((x_this, x3) :: 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 : lj.x * ty => snd y) y_ty_list) x0))) (XMap.empty ty)))). intros. assert (~ In x' x1). rewrite map_snd_fst'' in H8. exact H8. rewrite length_build_big_list; congruence. assert ( distinct var x1). generalize H4; clear; induction x1. simpl; auto. simpl; intros. bd H4; pa. unfold not; intros H2; apply H1; generalize H2; clear; induction x1; simpl; auto. intros H2; bd H2. rewrite H2; po1. po2; apply (IHx1 H2). apply (IHx1 H4). assert (length x0 = length x1). congruence. assert (length x1 = length y_ty_list). generalize y_ty_list H10; clear; induction x1; simpl; intros. destruct y_ty_list; auto; discriminate. destruct y_ty_list; auto. simpl in *|-*; auto. import (find_in_add _ _ g _ (equiv_contexts y_ty_list x0 x1 x' y x3 t0 H35 H40 H37 H41 H42 H27)); subst. simpl in H43; rewrite H43; clear H43. destruct (map_snd _ _ y_ty_list). rewrite H17. inversion H31. import (find_in_add' (x' :: x1) (x3 :: x4) (x_var var_5) ty'0 g). simpl in H48; rewrite H48; subst. inversion H12. rewrite H27 in H38. inversion H38. inversion H55; inversion H56; inversion H24. rewrite <- H62 in H57; rewrite <- H63 in H57; rewrite <- H64 in H44. apply (sty_opt p _ _ ty0 ty'0 (refl_equal _) (refl_equal _)). rewrite <- H62; apply (sty_transitive _ _ _ _ H57 H44). intros. bd H17. inversion H17. apply (in_stack_in_context _ _ _ _ _ H7 H20). apply (in_stack_in_context p g H5 L5 x'0 (H6 _ H17) H20). auto. intros G1; rewrite G1 in H38; inversion H38. discriminate. applyI wf_stmt_list'_iff'. import (wf_stmt_list_add (cons x' x1) (cons x3 (map (fun y0 : lj.x * ty => snd y0) y_ty_list)) g p (make_list_s Ss5)). simpl in H27; apply H27; auto; intros. bd H35. inversion H35. apply (in_stack_in_context _ _ _ _ _ H7 H20). apply (in_stack_in_context _ _ _ _ _ (H6 _ H35) H20). applyI wf_stmt_list'_iff'. intros. import (XMap.find_1 H27); apply XMap.find_2. apply find_in_add'; auto. intros. simpl in H40; bd H40. rewrite <- H40. apply (in_stack_in_context _ _ _ _ _ H7 H20). apply (in_stack_in_context _ _ _ _ _ (H6 _ H40) H20). inversion H20. import (H11 _ (MapsTo_mem _ _ _ (XMap.find_2 H28))). bd H24; rewrite H1 in H24; inversion H24. rewrite H28 in H27; inversion H27; subst. rewrite H2 in H35; simpl in H35; inversion H35; inversion H0; inversion H13. rewrite <- H33 in H17; rewrite <- H34 in H17. import (sty_cl_object _ _ _ (refl_equal _) H17). discriminate. unfold mtype in H29; unfold get_md in H29; rewrite path_cl_object in H29; simpl in H29; discriminate. (*** if_true ***) exists g; pa. inversion H. apply wf_all; auto. simpl. inversion H13. inversion H16; subst. apply (Cons_wf_stmt_list p g s1 _ H27 H19). auto. (*** if_false ***) exists g; pa. inversion H. apply wf_all; auto. simpl. inversion H14; inversion H17; subst. apply (Cons_wf_stmt_list p g s2 _ H29 H20). auto. (*** block ***) exists g; pa. inversion H; subst. apply wf_all; auto. inversion H11. inversion H3; subst. applyI wf_stmt_list_app. pa. generalize H15; clear; induction s_list; simpl; intros; auto. apply Cons_wf_stmt_list; auto. inversion H15; auto. inversion H15. apply (IHs_list H4). auto. Qed.