Require Import Arith. Require Import Bool. Require Import List. Require Import Natmap. Require Import FMaps. Require Import EqNat. Require Import FMapFacts. Require Import Natmap. Require Import Classical. Require Import base2. Require Import Max. Require Import lj_definitions. Module NatMapFacts := FMapFacts.Facts NatMap. Module XMapFacts := FMapFacts.Facts XMap. Section Fresh_Vars. (**Freshness section: There is always a variable name not in a map.**) Lemma max_lelistA : forall (A : Type) (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 lelist_last : forall (A : Type) (listA : list A) (a b c: A) (R : relation A), transitive A R -> sort R (b :: listA) -> lelistA R a (b :: listA) -> R a (last (b :: listA) c). induction listA; simpl; intros a' b' c' R H H0 H1. inversion H1; exact H3. inversion H1; inversion H0; subst. unfold transitive in H; apply H with (y := b'). exact H3. simpl in IHlistA. apply IHlistA; auto. Qed. Lemma In_sorted_list : forall (A : Type) (a : A) (listA : list A) (R : relation A), transitive A R -> In a (listA) -> sort R listA -> (R a (last listA a) \/ a = (last listA a)). induction listA. simpl; intros R H0 H; inversion H. intros R H0 H H1 ; simpl in H; inversion H; subst. inversion H1; subst. inversion H4. simpl; right; reflexivity. left; rewrite <- H6 in H5. unfold last at 1; fold (last (a0 :: l) a). apply lelist_last; auto. destruct listA. destruct H2. unfold last at 1 2; fold (last (a1 :: listA) a). inversion H1; auto. Qed. Lemma last_cons_eq : forall (A : Type) (listA : list A) (x y z : A), last (x :: listA) y = last (x :: listA) z. induction listA; simpl; intros; auto. apply IHlistA. Qed. 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. elimtype False; apply H; clear; intros; unfold not; intros. unfold XMap.Raw.PX.MapsTo in H. inversion H. clear H. generalize (XMap.elements_3 l); intros. rewrite H0 in H. inversion H. exists (fst (last (XMap.elements l) p)). split. 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. rewrite H0. generalize H7 H3 H4; clear. intros. cut (transitive (XMap.key * v) (XMap.lt_key (elt:=v))); intros. destruct (In_sorted_list _ (y', x) (p :: l0) (XMap.lt_key (elt:=v)) H H7 (cons_sort H3 H4)) as [Hlt | Heq]. left; generalize p Hlt; clear; induction l0; auto. intros p; unfold last; fold (last (a :: l0) (y', x)); fold (last (a :: l0) p). rewrite (last_cons_eq _ _ a p a); auto. right. generalize p Heq; clear; induction l0; intro p. simpl; intros; rewrite <- Heq; simpl; auto. unfold last; fold (last (a :: l0) (y', x)); fold (last (a :: l0) p). rewrite (last_cons_eq _ _ a p a); auto. unfold transitive; clear; unfold XMap.lt_key; unfold XMap.Raw.PX.ltk; intros x y z; destruct x; destruct y; destruct z; simpl; intros; destruct k; destruct k0; destruct k1; auto;try omega. 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_var k) x_this)). unfold not; intros. unfold XMap.E.eq in H1; unfold XOrd.eq in H1; exact H1. generalize (XMap.remove_2). intros H2; generalize (H2 _ l x_this (x_var k) x 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 H3. assert (XMap.E.eq x_this x_this). auto. apply (H3 v l x_this x_this H5 H4). destruct x; try (elimtype False; apply H2; apply refl_equal; fail). exists v. split; auto. 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 _ l x_this (x_var (S x)) x2 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 x_this (x_var (S x2)) 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 (x_this) (x_var (S x1)) 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. End Fresh_Vars. 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 l0. simpl; exact IHl. unfold get_fty; fold get_fty. unfold get_fs; fold get_fs. caseEq a; intros. case (eq_nat_dec f' f); intros. pa; intros. unfold map; fold (map (fun fd' : fd => match fd' with | fd_def _ f'0 => f'0 end) (l0)). 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) (l0)). pa; intros. simpl; po2. applyI IHl0. simpl in H0; bd H0. elimtype False; congruence. applyI IHl0. 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 l; exists l0; 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 : list fd) (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 l; exists l0. 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': list fd) (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': list fd) (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' : list fd) (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' : list fd) (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' : list fd) (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' : list fd) (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. 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 l2) (get_vdsvars l2))) = l2). clear; induction l2. simpl; reflexivity. destruct a; simpl. rewrite IHl2; 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 l2) (get_vdsvars l2))) = l2). clear; induction l2. simpl; reflexivity. destruct a; simpl. rewrite IHl2; 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 l2) (get_vdsvars l2))) = l2). clear; induction l2. simpl; reflexivity. destruct a; simpl. rewrite IHl2; 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 l2) (get_vdsvars l2))) = l2). clear; induction l2. simpl; reflexivity. destruct a; simpl. rewrite IHl2; 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 l1) /\ ~ In m' (ext_ms l)). pa; unfold not; intro; apply H; apply in_or_app. po1. po2. bd H0; clear H. caseEq (filter_mds l1 m'); intros. simpl; apply (IHl H0). elimtype False; apply H3. import (in_filtered l1 m m'). rewrite H in H1. simpl in H1. assert (In m l1). apply H1; po1. clear H1. destruct m; destruct m. assert (m = m'). generalize H; clear. induction l1. simpl; intros. discriminate. destruct a; destruct m1; simpl. case (eq_nat_dec m1 m'); intros. inversion H. congruence. apply (IHl1 H). rewrite H1 in H2; generalize H2; clear; induction l1. simpl; auto. simpl; intros. bd H2. rewrite H2; po1. po2. apply (IHl1 H2). Qed. Lemma path_eq_parent : forall (p : P) (cl' : cl) (dcl' : dcl) (fds' : list fd) (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 l; exists l0; po1; congruence. auto. rewrite path_cl_object in *|-*; simpl in H; discriminate. Qed. Lemma mtype_in_md : forall (dcl' : dcl) (cl' : cl) (fds' : list fd) (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' : list fd) (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'' : list fd) (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 l; exists l0. 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 l1. 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' : list ty), 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. 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' : list fd) (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 (IHl 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. 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_definitions.x * ty => fst y) y_ty_list) = map (fun y : lj_definitions.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_definitions.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_definitions.x * ty => snd y) (map (fun y : lj_definitions.x * ty => (tr_x t (fst y), snd y)) y_ty_list) = map (fun y : lj_definitions.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_definitions.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_definitions.x * ty => fst y) y_ty_list) = map (fun y : lj_definitions.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_definitions.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_definitions.x * ty => snd y) (map (fun y : lj_definitions.x * ty => (tr_x t (fst y), snd y)) y_ty_list) = map (fun y : lj_definitions.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 XOrd_eq_check : forall x y, XOrd.eq x y -> (fun t1 t2 : XOrd.t => match t1 with | x_var n1 => match t2 with | x_var n2 => eq_nat n1 n2 | x_this => False end | x_this => match t2 with | x_var _ => False | x_this => True end end) x y. intros x y H; destruct x; destruct y; unfold XOrd.eq in H; auto. Qed. Lemma XOrd_neq_check : forall x y, ~ XOrd.eq x y -> ~ (fun t1 t2 : XOrd.t => match t1 with | x_var n1 => match t2 with | x_var n2 => eq_nat n1 n2 | x_this => False end | x_this => match t2 with | x_var _ => False | x_this => True end end) x y. intros x y H; destruct x; destruct y; unfold XOrd.eq in H; auto. 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) (XOrd_eq_check _ _ 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) (XOrd_eq_check _ _ 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) (XOrd_neq_check _ _ 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) (XOrd_neq_check _ _ 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_definitions.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_definitions.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_definitions.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_definitions.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_definitions.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_definitions.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_definitions.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_definitions.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_definitions.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) (XOrd_eq_check _ _ 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 (XOrd_neq_check _ _ 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 : list s), 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_definitions.v) (m : XMap.t lj_definitions.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ v (XOrd_eq_check _ _ (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_definitions.v) (m : XMap.t lj_definitions.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ v (XOrd_eq_check _ _ (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_definitions.v) (m : XMap.t lj_definitions.v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine x1 x2)) _ _ _ v (XOrd_neq_check _ _ 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' : list fd) (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' : list fd) (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' : list s), 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' : list s), 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 l0; exists l; 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' : list fd) (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' : list fd) (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'' : list fd) (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' : list s), 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 l1 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 l0; exists l1; pa. apply (H5 (cld_def d0 c l0 l1)); 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 l3) (mb_def Ss' x')) l1). apply (in_filtered l1 (md_def (ms_def ty' m l3) (mb_def Ss' x')) m'). rewrite H0. simpl; po1. assert (m' = m). generalize H0; clear; induction l1. 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 l3) (get_vdsvars l3))) = l3). clear; induction l3; simpl; auto. destruct a; simpl; rewrite IHl3; 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 _ l0 _ l1 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' : list s), 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_definitions.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_definitions.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 _ _ _ _ _ _ (XOrd_neq_check _ _ 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_definitions.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_definitions.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 _ _ _ _ _ _ (XOrd_neq_check _ _ H) (XMap.find_2 H1))). import (XMap.add_2). apply (XMap.find_1 (H4 _ _ _ _ _ (snd a) (XOrd_neq_check _ _ 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_definitions.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_definitions.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 _ _ _ _ _ _ (XOrd_neq_check _ _ 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 _ _ _ _ _ _ (XOrd_neq_check _ _ 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) (XOrd_eq_check _ _ H))) in H4. discriminate. import (XMap.add_3). apply (IHold_var new_var). apply XMap.find_1. apply (H0 _ _ _ _ _ _ (XOrd_neq_check _ _ 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_definitions.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_check _ _ (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) (XOrd_neq_check _ _ H) (XMap.find_2 H0)). bd H4. rewrite (XMap.find_1 (H3 _ _ _ _ _ ty' (XOrd_neq_check _ _ 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_definitions.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_definitions.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_definitions.x) => XMap.add (x_var (fst yp)) (x_var (snd yp)) m) (XMap.empty lj_definitions.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_definitions.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') (XOrd_neq_check _ _ 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') (XOrd_neq_check _ _ 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_definitions.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_check _ _ (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') (XOrd_neq_check _ _ 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') (XOrd_neq_check _ _ 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_check _ _ (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_check _ _ (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_definitions.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_definitions.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_definitions.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. Lemma NatMap_find_mem : forall o h clm, NatMap.find (elt:=cl * NatMap.t v) o h = Some clm -> NatMap.mem o h = true. Proof. intros o h clm H. apply NatMap.mem_1. unfold NatMap.In; unfold NatMap.Raw.PX.In; exists clm. exact (NatMap.find_2 H). Qed. Lemma None_neq_Some : forall (A : Type) (a : A) (b : option A), b = Some a -> b <> None. Proof. congruence. Qed. Lemma Some_neq_None : forall (A : Type) (b : option A), b <> None -> exists a, b = Some a. Proof. intros; destruct b as [a' | ]. exists a'; reflexivity. congruence. Qed. Lemma XMap_find_mem : forall x' g ty', XMap.find (elt:=ty) x' g = Some ty' -> XMap.mem x' g = true. Proof. intros x' g ty' H. apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists ty'. exact (XMap.find_2 H). Qed. Lemma length_map_r : forall (A B : Type) (A_B_list : list (A * B)), (length (map (fun y => fst y) A_B_list) = length (map (fun y => snd y) A_B_list)). induction A_B_list; simpl; congruence. Qed. Lemma distinct_map_xvar : forall (var_list : list var), distinct _ var_list -> distinct _ (map (fun var' : var => x_var var') var_list). induction var_list; simpl; auto; intros. destruct H as [H1 H2]; split. clear IHvar_list H2; induction var_list. simpl; tauto. simpl in *|-*; unfold not in *|-*; intros. destruct H as [H | H]; auto. apply H1. left; inversion H; reflexivity. auto. Qed. Lemma distinct_map_xvar' : forall (var_list : list var), distinct _ (map (fun var' : var => x_var var') var_list) -> distinct _ var_list. induction var_list; simpl; auto; intros. destruct H as [H1 H2]; split. clear IHvar_list H2; induction var_list. simpl; tauto. simpl in *|-*; unfold not in *|-*; intros. destruct H as [H | H]; auto. auto. Qed. Lemma In_map_xvar' : forall (x' : x) (var_list : list var ), In x' (map (fun var' : var => x_var var') var_list) -> exists v', x' = x_var v' /\ In v' var_list. induction var_list; simpl; intros In_x'. destruct In_x'. destruct In_x' as [In_x'1 | In_x'2]. exists a; split; auto. destruct (IHvar_list In_x'2) as [v' [H1 H2]]; exists v'; split; auto. Qed. Lemma map_var_var_id : forall (var_list : list var), (map (fun var' => var') var_list) = var_list. induction var_list; simpl; congruence. Qed. Lemma map_fffst_snd_pair : forall (yty_list : list (x * ty)) (list_var1 list_var2: list var) (list_v : list v), length list_var1 = length (build_big_list (map (fun y : x * ty => fst y) yty_list) list_var1 list_var2 list_v) -> length list_v = length list_var1 -> (map (fun yp : x * var * var * v => (fst (fst (fst yp)), snd yp)) (build_big_list (map (fun y : x * ty => fst y) yty_list) list_var1 list_var2 list_v)) = (combine (map (fun y : x * ty => fst y) yty_list) list_v). induction yty_list; simpl; intros list_var1 list_var2 list_v Len1 Len2. reflexivity. destruct list_var1; destruct list_var2; destruct list_v; simpl in *|-*; try discriminate; auto. rewrite IHyty_list; congruence. Qed. Lemma add_Natmap_find_eq : forall (elt : Type) (m : NatMap.t elt) (x : NatMap.key) (e : elt), NatMap.find (elt := elt) x (NatMap.add x e m) = Some e. intros elt m x e. apply NatMap.find_1. apply (proj2 (NatMapFacts.add_mapsto_iff _ _ _ _ _)). left; split; auto with arith. Qed. Lemma add_Natmap_find_neq : forall (elt : Type) (m : NatMap.t elt) (x y: NatMap.key) (e : elt), y <> x -> NatMap.find (elt := elt) x (NatMap.add y e m) = NatMap.find (elt := elt) x m. intros elt m x y e Neq_x_y. caseEq (NatMap.find (elt:=elt) x m); intros. apply NatMap.find_1. apply (proj2 (NatMapFacts.add_mapsto_iff _ _ _ _ _)). right; split. unfold not; intros; apply Neq_x_y. apply (eq_nat_eq _ _ H0). apply NatMap.find_2; exact H. apply (proj1 (NatMapFacts.not_find_in_iff _ _)). unfold not; intros. destruct (proj1 (NatMapFacts.add_in_iff _ _ _ _) H0) as [eq | In]. rewrite (eq_nat_eq _ _ eq) in Neq_x_y; auto. eapply (proj2 (NatMapFacts.not_find_in_iff _ _)). apply H. exact In. Qed. Lemma add_Xmap_find_eq : forall (elt : Type) (m : XMap.t elt) (x : XMap.key) (e : elt), XMap.find (elt := elt) x (XMap.add x e m) = Some e. intros elt m x e. apply XMap.find_1. apply (proj2 (XMapFacts.add_mapsto_iff _ _ _ _ _)). left; split; auto; destruct x; auto with arith. Qed. Lemma add_Xmap_find_neq : forall (elt : Type) (m : XMap.t elt) (x y: XMap.key) (e : elt), y <> x -> XMap.find (elt := elt) x (XMap.add y e m) = XMap.find (elt := elt) x m. intros elt m x y e Neq_x_y. caseEq (XMap.find (elt:=elt) x m); intros. apply XMap.find_1. apply (proj2 (XMapFacts.add_mapsto_iff _ _ _ _ _)). right; split. unfold not; intros; apply Neq_x_y. destruct x; destruct y; try (destruct H0; fail). rewrite (eq_nat_eq _ _ H0); reflexivity. reflexivity. apply XMap.find_2; exact H. apply (proj1 (XMapFacts.not_find_in_iff _ _)). unfold not; intros. destruct (proj1 (XMapFacts.add_in_iff _ _ _ _) H0) as [eq | In]. destruct x; destruct y; try congruence. rewrite (eq_nat_eq _ _ eq) in Neq_x_y; auto. eapply (proj2 (XMapFacts.not_find_in_iff _ _)). apply H. exact In. Qed. Lemma LMapsTo_mem : forall (x' : x) (v' : v) (l : L), XMap.MapsTo x' v' l -> XMap.mem x' l = true. intros. apply XMap.mem_1. unfold XMap.In; unfold XMap.Raw.PX.In; exists v'. exact H. Qed. Lemma LMapsTo_mem2 : forall (x' : x) (l : L), XMap.mem x' l = true -> exists v', XMap.MapsTo x' v' l. 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 cl_object_in_names : forall (p : P), In cl_object (names p). induction p; simpl; auto. destruct a; simpl; auto. Qed. Lemma find_init_fields_null : forall (f' : f) (f_list : list f), In f' f_list -> NatMap.find (elt:=v) f' (init_field_map f_list) = Some v_null. induction f_list; simpl; intros. destruct H. destruct H as [eq_a_f | In_f']. subst; apply add_Natmap_find_eq. destruct (eq_nat_dec f' a) as [eq_f_a | neq_f_a]. subst; apply add_Natmap_find_eq. rewrite add_Natmap_find_neq; auto. Qed. Lemma In_H_In_fs : forall (o' : oid) (ty' : ty) (f' : f) (cl' : cl) (p : P) (h : H) (m' : NatMap.t v), NatMap.find (elt:=cl * NatMap.t v) o' h = Some (cl', m') -> wf_hp p h -> ftype p cl' f' = Some ty' -> exists v', (NatMap.find (elt:=v) f' m') = Some v' /\ (forall o' (cl'': cl) m'', NatMap.find (elt:=v) f' m' = Some (v_oid o') -> NatMap.find (elt:=cl * NatMap.t v) o' h = Some (cl'', m'') -> sty_one p (ty_def cl'') ty'). intros until m'; intros HFind_o' WFHP FType_f'. inversion WFHP as [null null' WF_HP1]; subst. destruct (WF_HP1 _ (NatMap_find_mem _ _ _ HFind_o')) as [cl'' [wf_HP1 [wf_HP2 wf_HP3]]]; clear WF_HP1; rewrite HFind_o' in wf_HP1; simpl in wf_HP1; inversion wf_HP1; subst; clear wf_HP1; simpl in *|-*. destruct (wf_HP3 _ (proj1 (ftype_in_fields _ _ _) (None_neq_Some _ _ _ FType_f'))) as [ty'' [FType_ty'' WF_Obj]]. rewrite HFind_o' in WF_Obj; simpl in WF_Obj; inversion WF_Obj; subst. exists v_null; split; congruence. exists (v_oid oid5); split; auto; intros o'' cl3 m3 H0 H1; inversion H0; subst; clear H0; destruct (NatMap.find (elt:=cl * NatMap.t v) o'' h); inversion H2; subst. inversion H1; inversion H3; inversion H0; subst;simpl in H4; congruence. discriminate. Qed. Lemma In_L_In_H : forall (x' : x) (o' : oid) (ty' : ty) (p : P) (g : G) (l : L) (h : H), wf_stck p g h l -> wf_hp p h -> XMap.find (elt := v) x' l = Some (v_oid o') -> XMap.find (elt := ty) x' g = Some ty' -> exists cl', exists m, NatMap.find (elt := cl * NatMap.t v) o' h = Some (cl', m) /\ sty_one p (ty_def cl') ty'. intros until h; intros WFStack WFHP LFind_x' GFind_x'. inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst; destruct (WF_Stk1 x' (MapsTo_mem _ _ _ (XMap.find_2 GFind_x'))) as [ty'' [WF_Stk1' [WF_Stk2 WF_Stk3]]]; rewrite LFind_x' in WF_Stk3; inversion WF_Stk3 as [| p'' h'' o''' null'' STY]; subst. caseEq (NatMap.find (elt:=cl * NatMap.t v) o' h). intros p0 HFind_o'; rewrite HFind_o' in STY. inversion STY as [p' tyopt' tyopt'' ty1 ty2 STY1 STY2 STY_One null' GFind_y]; subst; rewrite STY2 in STY; inversion STY1; inversion STY2; subst; clear STY2. destruct p0 as [cl' m]; exists cl'; exists m; split. reflexivity. rewrite GFind_x' in WF_Stk1'; inversion WF_Stk1'; subst; simpl in STY_One; exact STY_One. intros Neq; rewrite Neq in STY; inversion STY; subst; discriminate. Qed. Lemma find_add_context : forall (x' : x) (var_list : list var) (ty_list : list ty) (g : G) (ty' : ty), distinct _ var_list -> XMap.find (elt:=ty) x' (fold_right (fun (x : var * ty) (g : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g) g (combine var_list ty_list)) = Some ty' -> (exists var', x' = x_var var' /\ In (var', ty') (combine var_list ty_list)) \/ ((forall var' ty'', x' = x_var var' -> ~ In (var', ty'') (combine var_list ty_list)) /\ XMap.find x' g = Some ty'). induction var_list; simpl; intros ty_list g ty' Distinct_var GFind_var'. right; auto. destruct ty_list; simpl; auto. destruct x' as [var' | ]. destruct (eq_nat_dec a var') as [Eq_v | Neq_v]; subst. simpl in GFind_var'; rewrite add_Xmap_find_eq in GFind_var'; inversion GFind_var'; subst. left; exists var'; auto. simpl in GFind_var'; rewrite add_Xmap_find_neq in GFind_var'. destruct (IHvar_list _ _ _ (proj2 Distinct_var) GFind_var'); auto. destruct H as [var'' [Eq In_var'']]. inversion Eq; subst; clear Eq. left; intros; exists var''; split; auto. right; split; intros. destruct H as [Neq GFind_var'']. unfold not; intros H1; destruct H1 as [Neq' | NIn']. congruence. apply (Neq _ _ H0 NIn'). tauto. congruence. right; split; intros. discriminate. simpl in GFind_var'; rewrite add_Xmap_find_neq in GFind_var'. destruct (IHvar_list _ _ _ (proj2 Distinct_var) GFind_var'); auto. destruct H as [var'' [Eq In_var'']]. discriminate. tauto. congruence. Qed. Lemma Not_In_var_list : forall (var' : var) (var_list : list var), In (x_var var') (map (fun var' : var => x_var var') var_list) <-> In var' var_list. induction var_list; simpl; split; auto; intros. destruct H as [Eq | In]. left; congruence. right; tauto. destruct H as [Eq | In]. left; congruence. right; tauto. Qed. Lemma distinct_map_distinct : forall (var_list : list var), distinct x (map (fun var' : var => x_var var') var_list) <-> distinct _ var_list. induction var_list; simpl; split; auto; intros; destruct H as [NIn Distinct_var_list]; split. unfold not; intros; apply NIn; apply (proj2 (Not_In_var_list _ _) H). tauto. unfold not; intros; apply NIn; apply (proj1 (Not_In_var_list _ _) H). tauto. Qed. Lemma distinct_fold : forall (A : Type) (a : A) (list_a : list A), distinct _ list_a -> ~ In a list_a -> distinct _ (a :: list_a). simpl; tauto. Qed. Lemma spurious_map_var : forall (var_list : list var), (map (fun var' : var => var') var_list) = var_list. induction var_list; simpl; congruence. Qed. Lemma Not_In_var2_list : forall (var'' : var) (var_list : list var), ~ In var'' (map (fun var' : var => var') var_list) -> ~ In (x_var var'') (map (fun var' : var => x_var var') var_list). intros; rewrite spurious_map_var in H; unfold not; intros; apply H. apply (proj1 (Not_In_var_list _ _ ) H0). Qed. Lemma Distinct_map_cons : forall (var'' : var) (var_list : list var), distinct x (x_var var'' :: map (fun var' : var => x_var var') var_list) -> distinct x (map (fun var' : var => x_var var') (var'' :: var_list)). simpl; auto. Qed. Lemma sty_wf_type : forall (ty' : ty) (tyopt' : tyopt) (p : P), sty_option p (Some ty') tyopt' -> wf_type p ty'. intros; inversion H; destruct ty'; destruct ty'0; destruct c; subst. destruct (sty_option_In_p _ _ _ H) as [cl' [fds' [mds' In_p]]]. apply wf_valid_dcl; eapply In_p_In_names; eauto. apply wf_valid_dcl; apply cl_object_in_names. Qed. Lemma find_menv_in_prog : forall (dcl' : dcl) (p : P) (m' : m) (menv' : menv), find_menv p (cl_dcl dcl') m' = Some menv' -> exists cl', exists fds', exists mds', In (cld_def dcl' cl' fds' mds') p. induction p; unfold find_menv; unfold get_md; simpl; intros. discriminate. destruct a; destruct (eq_nat_dec dcl' d) as [Eq_dcl | Neq_dcl]. exists c; exists l; exists l0; left; subst; reflexivity. fold (get_md p (cl_dcl dcl') m') in H; fold (find_menv p (cl_dcl dcl') m') in H. destruct (IHp _ _ H) as [cl' [fds' [mds' In_dcl]]]. exists cl'; exists fds'; exists mds'; right; auto. Qed. Lemma Combine_var_list_exists_v : forall (var' : var) (ty' : ty) (var_list : list var) (ty_list : list ty) (v_list : list v) (l : L), length v_list = length var_list -> In (var', ty') (combine var_list ty_list) -> exists v', XMap.find (elt:=v) (x_var var') (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine var_list v_list)) = Some v' /\ In v' v_list. induction var_list; simpl; intros until l; intros length_eq In_var'. contradiction. destruct ty_list; simpl in *|-*. contradiction. destruct v_list; simpl in *|-*. discriminate. destruct In_var' as [Eq | In_var']. inversion Eq; subst; clear Eq. rewrite add_Xmap_find_eq; exists v; split; auto. destruct (eq_nat_dec a var') as [Eq | Neq]. subst; rewrite add_Xmap_find_eq; exists v; split; auto. inversion length_eq; rewrite add_Xmap_find_neq. destruct (IHvar_list _ _ l H0 In_var') as [v' [Find_v' In_v']]; exists v'; split; auto. congruence. Qed. Lemma In_vlist_valid_lookup_list : forall (x' : x) (v' : v) (l : L) (x_v_list : list (x*v)), valid_lookup_list l x_v_list -> In (x', v') x_v_list -> XMap.find (elt:=v) x' l = Some v'. induction x_v_list; simpl; intros. contradiction. inversion H; subst. destruct H0 as [In_y | NIn_y]. inversion In_y; subst; auto. auto. Qed. Lemma In_sty_opt_list_sty_opt : forall (el : P * tyopt * tyopt) (opt_list : list (P * tyopt * tyopt)), In el opt_list -> sty_opt_list opt_list -> sty_option (fst (fst el)) (snd (fst el)) (snd el). induction opt_list; simpl; intros. contradiction. inversion H0; subst. destruct H as [In_y | NIn_y]; subst; auto. Qed. Lemma In_map_sty_list : forall (x' : x) (ty' : ty) (x_ty_list : list (x * ty)) (p : P) (g : G), In (x', ty') x_ty_list -> In (p, XMap.find (elt:=ty) x' g, Some ty') (map (fun y : x * ty => (p, XMap.find (elt:=ty) (fst y) g, Some (snd y))) x_ty_list). induction x_ty_list; simpl; intros; auto. destruct H as [In_x | NIn_x]; auto. subst; simpl; left; reflexivity. Qed. Lemma find_in_combine : forall (var' : var) (v' : v) (var_list : list var) (v_list : list v) (l : L), In var' var_list -> length var_list = length v_list -> XMap.find (elt:=v) (x_var var') (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine var_list v_list)) = Some v' -> In (var', v') (combine var_list v_list). induction var_list; simpl; intros. contradiction. destruct H as [Eq_var' | In_var']; subst; auto. destruct v_list; simpl in H0; inversion H0. simpl in H1; rewrite add_Xmap_find_eq in H1; simpl; left; congruence. destruct v_list; simpl in H0; inversion H0. simpl in H1; destruct (eq_nat_dec var' a); subst. rewrite add_Xmap_find_eq in H1; simpl; left; congruence. rewrite add_Xmap_find_neq in H1; simpl; auto. right; eapply IHvar_list; eauto. congruence. Qed. Lemma distinct_common : forall (var' : var) (v' : v) (var_list : list var) (v_list : list v) (ty' : ty) (x_ty_list : list (x * ty)), distinct _ var_list -> length var_list = length v_list -> length var_list = length x_ty_list -> In (var', ty') (combine var_list (map (fun y : x * ty => snd y) x_ty_list)) -> In (var', v') (combine var_list v_list) -> exists x', In (x', ty') x_ty_list /\ In (x', v') (map (fun yp : x * v => (fst yp, snd yp)) (combine (map (fun y : x * ty => fst y) x_ty_list) v_list)). induction var_list; intros; destruct v_list; try (simpl in *|-*; discriminate); destruct x_ty_list; simpl in *|-*; try discriminate. contradiction. destruct H. destruct H2; destruct H3. inversion H2; inversion H3; subst. exists (fst p); split; destruct p; auto. inversion H2; subst; elimtype False; apply H; eapply in_combine_l; eauto. inversion H3; subst; elimtype False; apply H; eapply in_combine_l; eauto. inversion H0; inversion H1; subst. destruct (IHvar_list _ _ _ H4 H6 H7 H2 H3) as [x'' [In1 In2]]. exists x''; split; right; auto. Qed. Lemma length_map : forall (A B: Type) (a_list : list A) (f : A -> B), length a_list = length (map f a_list). induction a_list; simpl; auto. Qed. Lemma Find_In_lookup_list : forall (p : P) (g : G) (h : H) (l : L) (v_list : list v) (x_ty_list : list (x * ty)) (x' : x) (o' : oid) (ty' : ty), wf_stck p g h l -> XMap.find x' g = Some ty'-> valid_lookup_list l (map (fun yp : x * v => (fst yp, snd yp)) (combine (map (fun y : x * ty => fst y) x_ty_list) v_list)) -> In (x', v_oid o') (map (fun yp : x * v => (fst yp, snd yp)) (combine (map (fun y : x * ty => fst y) x_ty_list) v_list)) -> exists clm, (NatMap.find o' h) = Some clm /\ sty_option p (Some (ty_def (fst clm))) (XMap.find x' g). induction v_list. intros until ty'; intros WFStack GFind_x' Valid_LL In_x_o'; rewrite combine_nil in In_x_o'; simpl in In_x_o'; contradiction. intros until ty'; intros WFStack GFind_x' Valid_LL In_x_o'; destruct x_ty_list; simpl in *|-*. contradiction. destruct In_x_o' as [Eq | In_x_o']. inversion Eq; subst; clear Eq. inversion Valid_LL; subst. destruct p0; simpl in *|-*. inversion WFStack as [p'' g'' h'' l'' WF_Stk1]; subst; destruct (WF_Stk1 _ (MapsTo_mem _ _ _ (XMap.find_2 GFind_x'))) as [ty'' [WF_Stk1' [WF_Stk2 WF_Stk3]]]. rewrite H2 in WF_Stk3; inversion WF_Stk3; subst. destruct (NatMap.find (elt:=cl * NatMap.t v) o' h). exists p0; split; congruence. inversion H3; discriminate. inversion Valid_LL; subst. eapply IHv_list; eauto. Qed. Lemma Find_Not_In_map_list : forall (x' : x) (ty' : ty) (var_list : list var) (x_ty_list : list (x * ty)) (g : G), (forall var' ty', x' = x_var var' -> ~ In (var', ty') (combine var_list (map (fun y : x * ty => snd y) x_ty_list))) -> XMap.find x' g = Some ty' -> XMap.find x' (fold_right (fun (x : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g0) g (combine var_list (map (fun y : x * ty => snd y) x_ty_list))) = Some ty'. induction var_list; simpl; intros; auto. destruct x_ty_list; simpl; auto. destruct x'. destruct (eq_nat_dec a v) as [Eq_a | Neq_a]. subst; elimtype False; apply (H _ (snd p) (refl_equal _)); simpl; auto. rewrite add_Xmap_find_neq. apply IHvar_list; auto. unfold not in *|-*; intros; eapply (H _ _ H1); simpl; eauto. congruence. rewrite add_Xmap_find_neq. apply IHvar_list; auto. intros; discriminate. congruence. Qed. Lemma Find_Not_In_map_list' : forall (x' : x) (v' : v) (var_list : list var) (v_list : list v) (x_ty_list : list (x * ty)) (l : L), length var_list = length x_ty_list -> (forall var' ty', x' = x_var var' -> ~ In (var', ty') (combine var_list (map (fun y : x * ty => snd y) x_ty_list))) -> XMap.find x' l = Some v' -> (XMap.find (elt:=v) x' (fold_right (fun (yp : var * v) (m : XMap.t v) => XMap.add (x_var (fst yp)) (snd yp) m) l (combine var_list v_list))) = Some v'. induction var_list; simpl; intros; auto. destruct v_list; simpl; auto. destruct x_ty_list; simpl in H0, H. discriminate. destruct x'. destruct (eq_nat_dec a v0) as [Eq_a | Neq_a]. subst; elimtype False; apply (H0 _ (snd p) (refl_equal _)); simpl; auto. rewrite add_Xmap_find_neq. eapply IHvar_list; eauto. unfold not in *|-*; intros; eapply (H0 _ _ H2); simpl; eauto. congruence. rewrite add_Xmap_find_neq. eapply IHvar_list; eauto. intros; discriminate. congruence. Qed. Lemma spurious_map : forall (A : Type) (a_list : list A), (map (fun a' : A => a') a_list) = a_list. induction a_list; simpl; congruence. Qed. Lemma XMap_find_Not_In : forall (x' : x) (var' : var) (ty' : ty) (g : G) (l : L) (var_list : list var) (ty_list : list ty), XMap.In (elt:=v) x' l -> (forall x' : x, In x' (map (fun var' : var => x_var var') var_list) -> ~ XMap.In (elt:=v) x' l) -> ~ XMap.In (elt:=v) (x_var var') l -> XMap.find (elt:=ty) x' (XMap.add (x_var var') ty' (fold_right (fun (x : var * ty) (g0 : XMap.t ty) => XMap.add (x_var (fst x)) (snd x) g0) g (combine var_list ty_list))) = XMap.find x' g. intros; rewrite add_Xmap_find_neq; simpl in *|-*. clear H1; revert H H0 ty_list; clear. induction var_list; simpl; intros. reflexivity. destruct ty_list; simpl. reflexivity. rewrite add_Xmap_find_neq. rewrite (IHvar_list); auto. unfold not; intros; eapply H0; eauto. unfold not; intros; eapply H1; eauto. congruence. Qed. Lemma find_in_add'' : forall (var_ty_list : list (var * ty)) (ty' ty'': ty) (g : G) (y y' : x) , XMap.find (elt:=ty) y (XMap.add y' ty'' (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 (elt:=ty) y (XMap.add y' ty'' (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'. intros. destruct y; destruct y'. destruct (eq_nat_dec v v0). subst; rewrite add_Xmap_find_eq in *|-*; congruence. rewrite add_Xmap_find_neq in *|-*; try congruence. apply find_in_add; auto. rewrite add_Xmap_find_neq in *|-*; try congruence. apply find_in_add; auto. rewrite add_Xmap_find_neq in *|-*; try congruence. apply find_in_add; auto. subst; rewrite add_Xmap_find_eq in *|-*; congruence. Qed.