Module PreservationStackKdestrcell

 inversion Hs1.
 Opaque concat cs_le_dec Zminus.
 inversion step; intros; subst; unfold stackframe_weak_inv in *; simpl in *; unfold Globals.update in *; simpl in *; subst; try exact (stack _ Hin); try exact (stack _ (or_intror _ Hin)); try (destruct Hin as [? | Hin2]; [ discriminate | exact (stack _ Hin2) ]).

symmetry in H1.
unfold Globals.new in H1.
injection H1; intros; subst; simpl in *.
destruct Hin as [ | Hin2].
 discriminate.
generalize (stack _ Hin2).
intro.
destruct (peq (Globals.next_object gl) obj').
 invall; subst.
 apply False_rect.
 generalize (Globals.valid_none valid_global (Ple_refl (Globals.next_object gl))).
 congruence.
rewrite PTree.gso; eauto.

 destruct Hin as [Heq | Hin2].
  discriminate.
 generalize (stack _ (or_intror _ Hin2)).
 sdestruct (
pointer_eq_dec (A:=A)
            (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
 ).
  intro; invall.
  apply False_rect.
  revert kind.
  unfold state_kind_inv.
  simpl.
  intros; invall; subst.
  assert (i <= i < n) by abstract omega.
  generalize (H16 _ H13).
  intro.
  injection e; intros; subst.
  destruct H9; unfold_ident_in_all; abstract congruence.
 intro; assumption.

generalize (stack _ (or_intror _ Hin)).
intro.
sdestruct (
 pointer_eq_dec (A:=A)
            (obj, (ar, i, (Class.Inheritance.Repeated, cn :: nil)))
            (obj', (ar', i'0, (Class.Inheritance.Repeated, cn' :: nil)))
); [| assumption].
apply False_rect.
injection e; intros; subst.
destruct (stack_wf _ nil _ (refl_equal _) _ Hin).
simpl in *.
destruct (H1 _ _ (refl_equal _) _ (refl_equal _)).
invall.
generalize (refl_equal (length ar')).
rewrite H5 at 1.
rewrite app_length.
destruct x.
 congruence.
simpl; intro; omegaContradiction.

sdestruct (
pointer_eq_dec (A:=A)
            (obj,
            (ar, i,
            (match k2 with
             | Constructor.direct_non_virtual => h
             | Constructor.virtual => Class.Inheritance.Shared
             end,
            match k2 with
            | Constructor.direct_non_virtual => p ++ b :: nil
            | Constructor.virtual => b :: nil
            end)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
).
 apply False_rect.
 revert kind.
 unfold state_kind_inv.
 simpl.
 intro; invall; subst.
 destruct k2; invall; subst.
  destruct p; simpl in *.
   discriminate.
  destruct p0; simpl in *; discriminate.
 discriminate.
destruct Hin as [| Hin2].
 discriminate.
exact (stack _ (or_intror _ Hin2)).

sdestruct (
pointer_eq_dec (A:=A)
            (obj,
            (ar, i,
            (match k2 with
             | Constructor.direct_non_virtual => h
             | Constructor.virtual => Class.Inheritance.Shared
             end,
            match k2 with
            | Constructor.direct_non_virtual => p ++ b :: nil
            | Constructor.virtual => b :: nil
            end)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
).
 apply False_rect.
 generalize (stack _ (or_introl _ (refl_equal _))).
 simpl.
 intro; invall; subst.
 destruct k2; invall; subst.
  destruct p; simpl in *.
   discriminate.
  destruct p; simpl in *; discriminate.
 discriminate.
exact (stack _ (or_intror _ Hin)).

generalize (stack _ Hin).
intro.
sdestruct (
pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
).
 apply False_rect.
 injection e; intros; subst.
 invall; subst.
 revert kind.
 unfold state_kind_inv; simpl.
 intros; invall; subst.
 destruct H6; unfold_ident_in_all; abstract congruence.
assumption.


destruct Hin as [ | Hin2] .
 discriminate.
destruct Hin2 as [ Heq | Hin ].
  injection Heq; intros; subst.
  sdestruct (
pointer_eq_dec (A:=A)
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
  ); try abstract congruence.
  unfold state_kind_inv in *; simpl in *; invall; eauto 9.
 generalize (stack _ (Hin)).
 sdestruct (
pointer_eq_dec (A:=A)
            (obj, (ar, j, (Class.Inheritance.Repeated, cn :: nil)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
 ).
  intro; invall; eauto 9.
 intro; assumption.

sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
).
 2 : exact (stack _ Hin).
injection e; intros; subst.
injection H; intros; subst.
generalize (stack _ Hin).
intro; invall; subst; eauto 9.

destruct Hin as [ | Hin2].
 discriminate.
destruct Hin2 as [ | Hin].
 discriminate.
sdestruct (
pointer_eq_dec (A:=A)
            (obj,
            (ar, i,
            (match beta with
             | Constructor.direct_non_virtual => h
             | Constructor.virtual => Class.Inheritance.Shared
             end,
            match beta with
            | Constructor.direct_non_virtual => p ++ b :: nil
            | Constructor.virtual => b :: nil
            end)))
            (obj', (ar', i', (Class.Inheritance.Repeated, cn' :: nil)))
).
 2 : exact (stack _ (Hin)).
generalize (stack _ Hin).
intro; invall; subst; eauto 9.

sdestruct (
 pointer_eq_dec (A:=A) (obj, (ar, i, hp))
            (obj'0, (ar'0, i'0, (Class.Inheritance.Repeated, cn' :: nil)))
).
 2 : exact (stack _ (or_intror _ Hin)).
apply False_rect.
injection e; intros; subst.
revert kind.
unfold state_kind_inv.
simpl.
intros; invall; subst.
destruct hp'.
destruct beta; invall; subst.
 generalize (stack _ (or_introl _ (refl_equal _))).
  simpl.
  intros; invall.
  destruct l.
   discriminate.
  destruct l; discriminate.
discriminate.

sdestruct (pointer_eq_dec (A:=A) (obj, (ar, i, (h, p)))
            (obj', (ar', i'0, (Class.Inheritance.Repeated, cn' :: nil)))
).
 2 : exact (stack _ (Hin)).
apply False_rect.
injection e; intros; subst.
destruct (stack_state_wf _ Hin _ (refl_equal _)).
invall.
generalize (refl_equal (length ar')).
rewrite H1 at 1.
rewrite app_length.
destruct x.
 congruence.
simpl; intro; omegaContradiction.

Qed.