Module PreservationConstructionStatesDirectNonVirtual

 inversion Hs1.
 inversion step; subst; simpl in *; unfold Globals.update in *; simpl in *; subst; try assumption.

intros until 1.
symmetry in H1.
unfold Globals.new in H1.
injection H1; intros until 2; subst; simpl in *.
inversion H2; subst; simpl in *.
destruct (peq (obj0) (Globals.next_object gl)).
 rewrite e in H5.
rewrite PTree.gss in H5.
injection H5; intros; subst; simpl in *.
rewrite (construction_states_none _ (Globals.valid_none valid_global (Ple_refl _))).
rewrite (construction_states_none _ (Globals.valid_none valid_global (Ple_refl _))).
fin.
rewrite PTree.gso in H5.
 2 : assumption.
assert (valid_pointer (Program.hierarchy prog) (Globals.heap gl) (Value.subobject (obj0) ar i h p hp0)).
 econstructor; eauto.
eauto.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p)))
).
2: eauto.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl.
intros; invall; subst.
assert (i0 <= i0 < n) by abstract omega.
generalize (H14 _ H11).
intro.
injection H3; intros; subst.
generalize (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H2 _ (refl_equal _) _ H4 _ H5).
simpl.
unfold_ident_in_all.
rewrite H16.
destruct 1.
rewrite (constructed_base_child_of_none (refl_equal _)).
fin.

intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p ++ b :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i0, (h, p)))
).
 2 : eauto.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl.
intro; invall; subst.
injection H0; intros; subst.
generalize (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H _ (refl_equal _) _ H1 _ H2).
simpl.
unfold_ident_in_all.
rewrite H3.
destruct 1.
rewrite (
  constructed_base_child_of_constructed
  (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some BasesConstructed)) (refl_equal _))
  (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some StartedDestructing)) (refl_equal _))
).
fin.

intros.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
 ).
  injection e; intros; subst.
  sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, (p ++ b :: nil) ++ b0 :: nil)))
  ).
   fin.
  revert kind.
  unfold state_kind_inv.
  simpl.
  intro.
  invall; subst.
  generalize (H14 _ (or_introl _ (refl_equal _))).
  intro.
  destruct (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H2 _ H3 _ H4 _ H5).
  unfold_ident_in_all.
  rewrite (constructed_base_child_of_none H6).
  fin.
 sdestruct (
   pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
 ).
 2 : eauto.
 injection e; intros; subst.
 generalize (last_complete p b).
 unfold_ident_in_all; rewrite H6.
 rewrite last_complete.
 injection 1; intros; subst.
 generalize (app_reg_r H6).
 intro; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 intro; invall; subst.
 unfold_ident_in_all.
 rewrite H10.
 fin.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
).
 2 : eauto.
forward.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl; intro; invall; subst; unfold_ident_in_all.
generalize (H17 _ (or_introl _ (refl_equal _))).
intro.
destruct (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H2 _ H3 _ H4 _ H5).
simpl in *.
rewrite (constructed_base_child_of_none H7).
simpl; omega.

intros.
destruct k2.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
 ).
  injection e; intros; subst.
  sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, (p ++ b :: nil) ++ b0 :: nil)))
  ).
   fin.
  revert kind.
  unfold state_kind_inv.
  simpl.
  intro.
  invall; subst.
  destruct (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H _ H0 _ H1 _ H2).
  unfold_ident_in_all.
  rewrite H3 in *.
  rewrite (constructed_base_child_of_constructed
    (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some BasesConstructed)) (refl_equal _))
    (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some StartedDestructing)) (refl_equal _))
  ).
  fin.
 sdestruct (
   pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
 ).
 2 : eauto.
 injection e; intros; subst.
 generalize (last_complete p b).
 unfold_ident_in_all; rewrite H3.
 rewrite last_complete.
 injection 1; intros; subst.
 generalize (app_reg_r H3).
 intro; subst.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl.
 intro; invall; subst.
 unfold_ident_in_all.
 rewrite H5.
 fin.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
).
 2 : eauto.
forward.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl; intro; invall; subst; unfold_ident_in_all.
destruct (construction_states_direct_non_virtual_bases _ _ _ _ _ _ H _ H0 _ H1 _ H2).
rewrite H5 in *.
exact (constructed_base_child_of_constructed
    (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some BasesConstructed)) (refl_equal _))
    (proj_sumbool_true (cs_le_dec (Some BasesConstructed) (Some StartedDestructing)) (refl_equal _))
  ).

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0)))
).
 injection e; intros; subst.
 sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0)))
           (obj0, (ar0, i0, (h0, p0 ++ b :: nil)))
 ).
  apply False_rect.
  injection e0.
  intro.
  generalize (refl_equal (length p0)).
  rewrite H5 at 1.
  rewrite app_length.
  simpl.
  unfold_ident_in_all.
  intro; omegaContradiction.
 forward.
 revert kind.
 unfold state_kind_inv; simpl.
 intro; invall; subst.
 intros.
 apply H13.
 rewrite <- app_nil_end in H12.
 subst.
 eapply in_map_bases_intro.
 congruence.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b :: nil)))
).
 2 : eauto.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl.
intros; invall; subst.
destruct stk; try contradiction.
destruct t; simpl in H12; try contradiction.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl.
 destruct inhpath.
 destruct k; try contradiction.
  destruct kind; intros; invall; subst.
   generalize (last_complete p0 b).
   unfold_ident_in_all.
   rewrite H25.
   rewrite last_complete.
   injection 1; intros; subst.
   generalize (app_reg_r H25).
   intro; subst.
   rewrite H5.
   fin.
  destruct p0.
   discriminate.
  destruct p0; discriminate.
 invall; subst.
 destruct p0.
  discriminate.
 destruct p0; discriminate.


intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i, (h, p ++ b :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
           (obj0, (ar0, i, (h, p)))
).
 2 : eauto.
injection e; intros; subst.
forward.
intros.
revert kind.
unfold state_kind_inv; simpl.
intros; invall; subst.
assert (0 <= i <= i) by omega.
generalize (H15 _ H14).
intro.
unfold_ident_in_all.
change (cn :: b :: nil) with ((cn :: nil) ++ b :: nil).
eapply construction_states_direct_non_virtual_bases.
eassumption.
3 : eassumption.
2 : eassumption.
assumption.
rewrite H19.
simpl; omega.
rewrite H19; simpl; omega.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0)))
).
 injection e; intros; subst.
 sdestruct (
pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p0)))
           (obj0, (ar0, i0, (h0, p0 ++ b :: nil)))
 ).
  injection e0.
  intro.
  generalize (refl_equal (length p0)).
  rewrite H6 at 1.
  rewrite app_length.
  unfold_ident.
  simpl; intro; omegaContradiction.
 unfold state_kind_inv in kind.
 simpl in kind.
 invall; subst.
 cut (
   (assoc (pointer_eq_dec (A:=A)) (obj0, (ar0, i0, (h0, p0 ++ b :: nil)))
     cs) = (Some Constructed)).
 intros.
 unfold_ident_in_all.
 rewrite H6.
 fin.
eapply construction_states_direct_non_virtual_bases.
eassumption.
3 : eassumption.
2 : eassumption.
assumption.
rewrite H7.
simpl; omega.
rewrite H7; simpl; omega.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
           (obj0, (ar0, i0, (h0, p0 ++ b :: nil)))
).
 2 : eauto.
injection e; intros; subst.
unfold state_kind_inv in kind.
simpl in kind; invall; subst.
destruct stk; try contradiction.
destruct t; simpl in H13; try contradiction.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl.
 destruct inhpath.
 destruct k; intro; invall; subst; try contradiction.
 destruct kind; invall; subst.
  generalize (last_complete p0 b).
  unfold_ident_in_all.
  rewrite H24.
  rewrite last_complete.
  injection 1; intros; subst.
  generalize (app_reg_r H24).
  intro; subst.
  rewrite H6.
  fin.
 destruct p0.
  discriminate.
 destruct p0; discriminate.
invall; subst.
destruct p0.
 discriminate.
destruct p0; discriminate.

intros.
destruct beta.
 sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
 ).
  injection e; intros; subst.
  sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h0, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, (p ++ b :: nil) ++ b0 :: nil)))
  ).
   injection e0.
   intro.
   generalize (refl_equal (length (p ++ b :: nil))).
   unfold_ident_in_all.
   rewrite H7 at 1.
   rewrite app_length at 1.
   simpl. intros. omegaContradiction.
  revert kind.
  unfold state_kind_inv.
  simpl.
  intro.
  invall; subst.
  generalize (H15 _ (or_introl _ (refl_equal _))).
  intro.
  forward.
  eapply constructed_base_child_of_constructed.
  eapply construction_states_direct_non_virtual_bases.
  4 : eassumption.
  eassumption.
  2 : eassumption.
  assumption.
  unfold_ident_in_all; rewrite H7; simpl; omega.
  unfold_ident_in_all; rewrite H7; simpl; omega.
 sdestruct (
   pointer_eq_dec (A:=A) (obj, (ar, i, (h, p ++ b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
 ).
 2 : eauto.
 injection e; intros; subst.
 generalize (last_complete p b).
 unfold_ident_in_all; rewrite H7.
 rewrite last_complete.
 injection 1; intros; subst.
 generalize (app_reg_r H7).
 intro; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 intro; invall; subst.
 unfold_ident_in_all.
 rewrite H10.
 fin.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0 ++ b0 :: nil)))
).
 destruct p0.
  discriminate.
 destruct p0; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Shared, b :: nil)))
           (obj0, (ar0, i0, (h0, p0)))
).
 2 : eauto.
forward.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl; intro; invall; subst; unfold_ident_in_all.
generalize (H18 _ (or_introl _ (refl_equal _))).
intro.
change (b :: b0 :: nil) with ((b :: nil) ++ b0 :: nil).
eapply constructed_base_child_of_constructed.
eapply construction_states_direct_non_virtual_bases.
4 : eassumption.
3 : eassumption.
eassumption.
assumption.
unfold_ident_in_all; rewrite H9; simpl; omega.
unfold_ident_in_all; rewrite H9; simpl; omega.

intros.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (hp)))
           (obj0, (ar0, i0, (h, p)))
).
 injection e; intros; subst.
 sdestruct (
    pointer_eq_dec (A:=A) (obj0, (ar0, i0, (h, p)))
           (obj0, (ar0, i0, (h, p ++ b0 :: nil)))
 ).
  apply False_rect.
  injection e0.
  intro.
  generalize (refl_equal (length p)).
  rewrite H3 at 1.
  rewrite app_length.
  simpl.
  unfold_ident_in_all.
  intro; omegaContradiction.
 forward.
 revert kind.
 unfold state_kind_inv; simpl.
 intro; invall; subst.
 intros.
 apply H10.
 rewrite <- app_nil_end in H9.
 subst.
 eapply in_rev_intro.
 eapply in_map_bases_intro.
 congruence.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (hp)))
           (obj0, (ar0, i0, (h, p ++ b0 :: nil)))
).
 2 : eauto.
injection e; intros; subst.
revert kind.
unfold state_kind_inv; simpl.
intros; invall; subst.
destruct hp'.
generalize (stack _ (or_introl _ (refl_equal _))).
simpl.
destruct beta; intros; invall; subst.
 unfold_ident_in_all.
 generalize (last_complete p b0).
 unfold_ident_in_all.
 rewrite H23.
 rewrite last_complete.
 injection 1; intros; subst.
 generalize (app_reg_r H23).
 intro; subst.
 rewrite H3.
 fin.
  destruct p.
   discriminate.
  destruct p; discriminate.

unfold state_kind_inv in kind.
simpl in kind.
invall; subst.
intros.
sdestruct (
pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, x1 :: nil)))
           (obj0, (ar0, i0, (h, p ++ b :: nil)))
).
 destruct p.
  discriminate.
 destruct p; discriminate.
sdestruct (
 pointer_eq_dec (A:=A)
           (obj, (ar, i, (Class.Inheritance.Repeated, x1 :: nil)))
           (obj0, (ar0, i0, (h, p)))
).
 2: eauto.
injection e; intros; subst.
forward.
eapply H11.
unfold_ident_in_all. congruence.

Qed.