Require Import VST.floyd.base2.

Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.nested_field_lemmas.
Require Import VST.floyd.efield_lemmas.
Require Import VST.floyd.mapsto_memory_block.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.data_at_rec_lemmas.
Require Import VST.floyd.field_at.
Require Import VST.floyd.stronger.
Require Import VST.floyd.entailer.
Require Import VST.floyd.closed_lemmas.
Require Import VST.floyd.proj_reptype_lemmas.
Require Import VST.floyd.replace_refill_reptype_lemmas.
Require Import VST.floyd.loadstore_field_at.
Import DataCmpNotations.

Local Open Scope logic.

Section NESTED_RAMIF.

Context {cs: compspecs}.

Lemma reptype_Tarray_JMeq_constr0: forall t gfs t0 n a (v: reptype (nested_field_type t gfs)),
  legal_nested_field t gfs ->
  nested_field_type t gfs = Tarray t0 n a ->
  {v': list (reptype (nested_field_type t (ArraySubsc 0 :: gfs))) |
   JMeq v v'}.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @sig (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) (fun v' : @nested_reptype_unionlist cs t gfs (co_members (@get_co cs id)) => @JMeq (@reptype cs (@nested_field_type cs t gfs)) v (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) v') *)
  apply JMeq_sigT.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc i) gfs))) (@reptype cs (@gfield_type cs (@nested_field_type cs t gfs) (ArraySubsc i))) *)
  rewrite nested_field_type_ind with (gfs0 := cons _ _).
  rewrite !H0.
  rewrite reptype_eq.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  auto.
Qed.

Lemma reptype_Tarray_JMeq_constr1: forall t gfs t0 n a i (v: reptype (nested_field_type t (ArraySubsc i :: gfs))),
  legal_nested_field t gfs ->
  nested_field_type t gfs = Tarray t0 n a ->
  {v': reptype (gfield_type (nested_field_type t gfs) (ArraySubsc i)) |
   JMeq v v'}.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @sig (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) (fun v' : @nested_reptype_unionlist cs t gfs (co_members (@get_co cs id)) => @JMeq (@reptype cs (@nested_field_type cs t gfs)) v (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) v') *)
  apply JMeq_sigT.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc i) gfs))) (@reptype cs (@gfield_type cs (@nested_field_type cs t gfs) (ArraySubsc i))) *)
  rewrite nested_field_type_ind with (gfs0 := cons _ _).
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
  reflexivity.
Qed.

Lemma reptype_Tarray_JMeq_constr2: forall t gfs t0 n a i (v': reptype (nested_field_type t (ArraySubsc i :: gfs))),
  legal_nested_field t gfs ->
  nested_field_type t gfs = Tarray t0 n a ->
  {v: reptype (nested_field_type t (ArraySubsc 0 :: gfs)) |
   JMeq v' v}.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @sig (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) (fun v' : @nested_reptype_unionlist cs t gfs (co_members (@get_co cs id)) => @JMeq (@reptype cs (@nested_field_type cs t gfs)) v (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) v') *)
  apply JMeq_sigT.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc i) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  rewrite nested_field_type_ArraySubsc with (i0 := i).
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  auto.
Qed.

Lemma reptype_Tstruct_JMeq_constr0: forall t gfs id a (v: reptype (nested_field_type t gfs)),
  legal_nested_field t gfs ->
  nested_field_type t gfs = Tstruct id a ->
  {v' : nested_reptype_structlist t gfs (co_members (get_co id)) |
   JMeq v v'}.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @sig (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) (fun v' : @nested_reptype_unionlist cs t gfs (co_members (@get_co cs id)) => @JMeq (@reptype cs (@nested_field_type cs t gfs)) v (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) v') *)
  apply JMeq_sigT.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  eapply nested_reptype_structlist_lemma; eauto.
Qed.

Lemma reptype_Tunion_JMeq_constr0: forall t gfs id a (v: reptype (nested_field_type t gfs)),
  legal_nested_field t gfs ->
  nested_field_type t gfs = Tunion id a ->
  {v' : nested_reptype_unionlist t gfs (co_members (get_co id)) |
   JMeq v v'}.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @sig (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) (fun v' : @nested_reptype_unionlist cs t gfs (co_members (@get_co cs id)) => @JMeq (@reptype cs (@nested_field_type cs t gfs)) v (@nested_reptype_unionlist cs t gfs (co_members (@get_co cs id))) v') *)
  apply JMeq_sigT.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  eapply nested_reptype_unionlist_lemma; eauto.
Qed.

(* This lemma is mainly dealing with all JMeq subtle issues and combine 3 ramif lemmas together. *)
Lemma gfield_ramif: forall sh t gfs gf v v0 p,
  JMeq (proj_gfield_reptype (nested_field_type t gfs) gf v) v0 ->
  field_compatible t (gf :: gfs) p ->
  field_at sh t gfs v p |-- field_at sh t (gf :: gfs) v0 p *
    (ALL v0': _,
      (field_at sh t (gf :: gfs) v0' p -*
         field_at sh t gfs
           (upd_gfield_reptype (nested_field_type t gfs) gf v
              (eq_rect_r reptype v0' (eq_sym (nested_field_type_ind t _))))
           p)).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
  destruct gf.
  + (* ArraySubsc *)
    pose proof H0.
    rewrite field_compatible_cons in H1.
    (* A Coq bug here. I cannot do destruct eqn in H1. So using next two lines instead. *)
    remember (nested_field_type t gfs) as t0 eqn:H2 in H1.
    destruct t0; try tauto; symmetry in H2.
    destruct H1.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    destruct (reptype_Tarray_JMeq_constr0 t gfs t0 z a v) as [v' ?H]; auto.
    erewrite field_at_Tarray; [| eauto | eauto | omega | eauto].
    replace
      (ALL  v0' : _,
        field_at sh t (gfs SUB i) v0' p -*
        field_at sh t gfs
          (upd_gfield_reptype (nested_field_type t gfs)
             (ArraySubsc i) v
             (eq_rect_r reptype v0'
                (eq_sym (nested_field_type_ind t (gfs SUB i))))) p)
    with
      (ALL  v0' : _, (ALL  v0'': _,
        !!JMeq v0' v0'' -->
        (field_at sh t (gfs SUB i) v0' p -*
         array_at sh t gfs 0 z (upd_Znth (i - 0) v' v0'') p))).
    2:{
      rewrite Z.sub_0_r.
      clear v0 H.
      apply pred_ext.
      + apply allp_right; intro v0.
        apply (allp_left _ v0).
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        destruct (reptype_Tarray_JMeq_constr2 t gfs t0 z a i v0) as [v0' ?H]; auto.
        apply (allp_left _ v0').
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        rewrite prop_imp by auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        apply wand_derives; auto.
        erewrite field_at_Tarray; [apply derives_refl | eauto | eauto | omega |].
        set (v0'' := eq_rect_r reptype v0 (eq_sym (nested_field_type_ind t (gfs SUB i)))).
        assert (JMeq v0' v0'') by (apply JMeq_sym; eapply JMeq_trans; [apply eq_rect_r_JMeq | auto]).
        clearbody v0''; clear v0 H.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
        revert v v0'' H4 H5; rewrite H2; intros.
        unfold upd_gfield_reptype.
        eapply JMeq_trans; [apply fold_reptype_JMeq |].
        apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
        revert v' v0' H4 H5; rewrite nested_field_type_ind with (gfs0 := cons _ _), H2; simpl; intros.
        apply JMeq_eq in H4; apply JMeq_eq in H5.
        subst; apply JMeq_refl.
      + apply allp_right; intro v0.
        apply allp_right; intro v0'.
        apply (allp_left _ v0).
        apply imp_andp_adjoint; normalize.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        apply wand_derives; auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        destruct (reptype_Tarray_JMeq_constr1 t gfs t0 z a i v0) as [v0'' ?H]; auto.
        erewrite field_at_Tarray; [apply derives_refl | eauto | eauto | omega |].
        clear v0'' H5.
        set (v0'' := eq_rect_r reptype v0 (eq_sym (nested_field_type_ind t (gfs SUB i)))).
        assert (JMeq v0' v0'') by (apply JMeq_sym; eapply JMeq_trans; [apply eq_rect_r_JMeq | auto]).
        clearbody v0''; clear v0 H.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
        revert v v0'' H4 H5; rewrite H2; intros.
        unfold upd_gfield_reptype.
        eapply JMeq_trans; [apply fold_reptype_JMeq |].
        apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
        revert v' v0' H4 H5; rewrite nested_field_type_ind with (gfs0 := cons _ _), H2; simpl; intros.
        apply JMeq_eq in H4; apply JMeq_eq in H5.
        subst; apply JMeq_refl.
    }
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    apply (array_at_ramif sh t gfs t0 z a 0 z i v' v0 p); auto.
    eapply JMeq_trans; [apply @JMeq_sym, H |]; clear v0 H.
    revert v v' H4.
    rewrite nested_field_type_ind with (gfs0 := cons _ _), H2.
    unfold proj_gfield_reptype, gfield_type.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
    intros.
    apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
    apply JMeq_eq in H4; subst.
    rewrite Z.sub_0_r.
    subst; apply JMeq_refl.
  + pose proof H0.
    rewrite field_compatible_cons in H1.
    (* A Coq bug here. I cannot do destruct eqn in H1. So using next two lines instead. *)
    remember (nested_field_type t gfs) as t0 eqn:H2 in H1.
    destruct t0; try tauto; symmetry in H2.
    destruct H1.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    destruct (reptype_Tstruct_JMeq_constr0 t gfs i0 a v) as [v' ?H]; auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    erewrite field_at_Tstruct by eauto.
    eapply derives_trans; [eapply nested_sfieldlist_at_ramif; eauto |].
    apply sepcon_derives.
    - apply derives_refl'.
      f_equal.
      apply JMeq_eq.
      eapply JMeq_trans; [| exact H].
      clear v0 H.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      revert v H4; rewrite H2; intros.
      unfold proj_gfield_reptype.
      apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
      forget (unfold_reptype v) as v''; clear v.
      cbv iota beta in v''.
      unfold reptype_structlist in v''.
      unfold nested_reptype_structlist in v'.
      apply (@proj_compact_prod_JMeq _ (i, field_type i (co_members (get_co i0)))
             _
             (fun it : prod ident type => @reptype cs (@nested_field_type cs t (@cons gfield (StructField (@fst ident type it)) gfs)))
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
             (fun it => reptype (field_type (fst it) (co_members (get_co i0))))); auto.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      * intros.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
        rewrite nested_field_type_ind, H2; reflexivity.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      * apply in_members_field_type; auto.
    - clear v0 H.
      apply allp_derives; intro v0.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      apply wand_derives; auto.
      erewrite field_at_Tstruct; [apply derives_refl | eauto |].
      set (v0' := eq_rect_r reptype v0 (eq_sym (nested_field_type_ind t (gfs DOT i)))).
      assert (JMeq v0' v0) by apply eq_rect_r_JMeq.
      clearbody v0'.
      revert v v0' H H4.
      rewrite H2.
      unfold gfield_type, upd_gfield_reptype.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      intros.
      apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
      forget (unfold_reptype v) as v''; clear v.
      cbv iota beta in v''.
      eapply JMeq_trans; [apply fold_reptype_JMeq |].
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      apply upd_compact_prod_JMeq; auto.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      intros.
      rewrite nested_field_type_ind, H2.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
      reflexivity.
  + pose proof H0.
    rewrite field_compatible_cons in H1.
    (* A Coq bug here. I cannot do destruct eqn in H1. So using next two lines instead. *)
    remember (nested_field_type t gfs) as t0 eqn:H2 in H1.
    destruct t0; try tauto; symmetry in H2.
    destruct H1.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    destruct (reptype_Tunion_JMeq_constr0 t gfs i0 a v) as [v' ?H]; auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    erewrite field_at_Tunion by eauto.
    eapply derives_trans; [eapply nested_ufieldlist_at_ramif; eauto |].
    apply sepcon_derives.
    - apply derives_refl'.
      f_equal.
      apply JMeq_eq.
      eapply JMeq_trans; [| exact H].
      clear v0 H.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      revert v H4; rewrite H2; intros.
      unfold proj_gfield_reptype.
      apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
      forget (unfold_reptype v) as v''; clear v.
      cbv iota beta in v''.
      unfold reptype_structlist in v''.
      unfold nested_reptype_unionlist in v'.
      apply (@proj_compact_sum_JMeq' _ (i, field_type i (co_members (get_co i0)))
             _
             (fun it => reptype (nested_field_type t (gfs UDOT fst it)))
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
             (fun it => reptype (field_type (fst it) (co_members (get_co i0))))); auto.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      * intros.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
        rewrite nested_field_type_ind, H2; reflexivity.
      * rewrite nested_field_type_ind, H2; apply JMeq_refl.
    - clear v0 H.
      apply allp_derives; intro v0.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      apply wand_derives; auto.
      erewrite field_at_Tunion; [apply derives_refl | eauto |].
      set (v0' := eq_rect_r reptype v0 (eq_sym (nested_field_type_ind t (gfs UDOT i)))).
      assert (JMeq v0' v0) by apply eq_rect_r_JMeq.
      clearbody v0'.
      revert v v0' H H4.
      rewrite H2.
      unfold gfield_type, upd_gfield_reptype.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      intros.
      apply (JMeq_trans (unfold_reptype_JMeq _ v)) in H4.
      forget (unfold_reptype v) as v''; clear v.
      cbv iota beta in v''.
      eapply JMeq_trans; [apply fold_reptype_JMeq |].
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      apply upd_compact_sum_JMeq; auto.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      intros.
      rewrite nested_field_type_ind, H2.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
      reflexivity.
Qed.

Lemma nested_field_ramif: forall sh t gfs0 gfs1 v v0 p,
  JMeq (proj_reptype (nested_field_type t gfs0) gfs1 v) v0 ->
  field_compatible t (gfs1 ++ gfs0) p ->
  field_at sh t gfs0 v p |--
    field_at sh t (gfs1 ++ gfs0) v0 p *
    (ALL v0': _, ALL v0'': _, !! JMeq v0' v0'' -->
      (field_at sh t (gfs1 ++ gfs0) v0' p -*
         field_at sh t gfs0 (upd_reptype (nested_field_type t gfs0) gfs1 v v0'') p)).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
  rewrite allp_uncurry'.
  RAMIF_Q'.formalize.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  revert v0 H; induction gfs1 as [| gf gfs1]; intros.
  + simpl app in *.
    apply RAMIF_Q'.solve with emp.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    - simpl; auto.
    - simpl in H. unfold eq_rect_r in H; rewrite <- eq_rect_eq in H; apply JMeq_eq in H.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      rewrite H, sepcon_emp; auto.
    - clear v0 H.
      intros [v0 v0']; unfold fst, snd.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible cs t gfs0 p)) (@field_at cs sh t gfs0 v p)) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@allp mpred Nveric (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v0' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => @allp mpred Nveric (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (fun v0'' : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1) => @imp mpred Nveric (@prop mpred Nveric (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0' (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0'')) (@wand mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0' p) (@field_at cs sh t gfs0 (@upd_reptype cs (@nested_field_type cs t gfs0) gfs1 v v0'') p)))))) *)
      normalize.
(* Goal: @eq expr (nested_efield (nested_efield t gfs0 tts0) (@cons efield a gfs1) (@cons type t0 tts1)) (nested_efield t (@app efield (@cons efield a gfs1) gfs0) (@app type (@cons type t0 tts1) tts0)) *)
      simpl.
      unfold eq_rect_r; rewrite <- eq_rect_eq; apply JMeq_eq in H.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      rewrite H; auto.
  + simpl app in H0, v0, H |- *.
    assert ({v1: reptype (nested_field_type t (gfs1 ++ gfs0)) | JMeq (proj_reptype (nested_field_type t gfs0) gfs1 v) v1})
      by (apply JMeq_sigT; rewrite nested_field_type_nested_field_type; auto).
    destruct X as [v1 ?H].
    change
      (fun st: reptype (nested_field_type t (gf :: gfs1 ++ gfs0)) *
               reptype (nested_field_type (nested_field_type t gfs0) (gf :: gfs1)) =>
       field_at sh t (gf :: gfs1 ++ gfs0) (fst st) p)
    with
      (Basics.compose
        (fun v => field_at sh t (gf :: gfs1 ++ gfs0) v p)
        (fun st: reptype (nested_field_type t (gf :: gfs1 ++ gfs0)) *
               reptype (nested_field_type (nested_field_type t gfs0) (gf :: gfs1)) =>
         fst st)).
    change (fun st: reptype (nested_field_type t (gf :: gfs1 ++ gfs0)) *
               reptype (nested_field_type (nested_field_type t gfs0) (gf :: gfs1)) =>
       field_at sh t gfs0
         (upd_reptype (nested_field_type t gfs0) (gf :: gfs1) v (snd st)) p)
      with
      (Basics.compose
        (fun st: reptype (nested_field_type t (gfs1 ++ gfs0)) *
                 reptype (nested_field_type (nested_field_type t gfs0) gfs1) =>
         field_at sh t gfs0
           (upd_reptype (nested_field_type t gfs0) gfs1 v (snd st)) p)
        (fun st: reptype (nested_field_type t (gf :: gfs1 ++ gfs0)) *
                 reptype (nested_field_type (nested_field_type t gfs0) (gf :: gfs1)) =>
           (upd_gfield_reptype _ gf v1 (eq_rect_r reptype (fst st) (eq_sym (nested_field_type_ind _ (gf :: _)))),
            upd_gfield_reptype _ gf (proj_reptype _ gfs1 v) (eq_rect_r reptype (snd st) (eq_sym (nested_field_type_ind _ (gf :: _))))))).
    eapply RAMIF_Q'.trans with
      (pL := fun _ => !! True)
      (pG := fun st => !! JMeq (fst st) (snd st)).
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    - simpl; auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    - simpl; auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    - simpl; auto.
    - apply IHgfs1; clear IHgfs1.
      * clear - H0.
        rewrite field_compatible_cons in H0.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        destruct (nested_field_type t (gfs1 ++ gfs0)), gf; tauto.
      * exact H1.
    - eapply derives_trans; [apply gfield_ramif |].
      * instantiate (1 := v0).
        eapply JMeq_trans; [| apply H].
        clear - H1.
        unfold proj_reptype; fold proj_reptype.
        eapply JMeq_trans; [| apply @JMeq_sym, eq_rect_r_JMeq].
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
        revert v1 H1; rewrite <- nested_field_type_nested_field_type; intros.
        apply JMeq_eq in H1; subst v1.
        apply JMeq_refl.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      * auto.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
      * apply sepcon_derives; auto.
        apply allp_derives; intros v0'.
(* Goal: @eq expr (nested_efield (nested_efield t gfs0 tts0) (@cons efield a gfs1) (@cons type t0 tts1)) (nested_efield t (@app efield (@cons efield a gfs1) gfs0) (@app type (@cons type t0 tts1) tts0)) *)
        Opaque nested_field_type_ind. simpl. Transparent nested_field_type_ind.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
        rewrite prop_imp by auto.
        apply derives_refl.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    - intros; apply prop_right; auto.
    - clear v0 H.
      intros [v0 v0']; unfold fst, snd.
      apply andp_derives; [| auto].
      apply prop_derives; intro.
      clear - H H1.
      set (v0'' := eq_rect_r reptype v0 (eq_sym (nested_field_type_ind t (gf :: gfs1 ++ gfs0)))).
      set (v0''' := eq_rect_r reptype v0' (eq_sym (nested_field_type_ind (nested_field_type t gfs0) (gf :: gfs1)))).
      assert (JMeq v0'' v0''') by (eapply JMeq_trans; [apply eq_rect_r_JMeq | apply (JMeq_trans H), @JMeq_sym, eq_rect_r_JMeq]).
      clearbody v0'' v0'''.
      clear v0 v0' H.
      revert v0'' v1 H0 H1.
      change (gf :: gfs1 ++ gfs0) with ((gf :: gfs1) ++ gfs0).
      rewrite <- nested_field_type_nested_field_type.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
      intros.
      apply JMeq_eq in H1; subst v1.
      apply JMeq_eq in H0; subst v0'''.
      apply JMeq_refl.
Qed.

Lemma nested_field_ramif_load: forall sh t gfs0 gfs1 (v_reptype: reptype (nested_field_type t gfs0)) (v_val: val) p,
  field_compatible t (gfs1 ++ gfs0) p ->
  JMeq (proj_reptype (nested_field_type t gfs0) gfs1 v_reptype) v_val ->
  exists v_reptype',
    JMeq v_reptype' v_val /\
    field_at sh t gfs0 v_reptype p |--
      field_at sh t (gfs1 ++ gfs0) v_reptype' p * TT.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  generalize (JMeq_refl (proj_reptype (nested_field_type t gfs0) gfs1 v_reptype)).
(* Goal: forall _ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  set (v0 := proj_reptype (nested_field_type t gfs0) gfs1 v_reptype) at 2.
(* Goal: forall _ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0, @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  clearbody v0.
(* Goal: forall _ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0, @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  revert v0.
(* Goal: forall (v0 : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (_ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  pattern (reptype (nested_field_type (nested_field_type t gfs0) gfs1)) at 1 3.
(* Goal: (fun T : Type => forall (v0 : T) (_ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) T v0), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric))))) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) *)
  rewrite nested_field_type_nested_field_type at 1.
(* Goal: forall (v0 : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (_ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  intros; exists v0.
(* Goal: and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0 val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric))) *)
  split.
(* Goal: @JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0 val v_val *)
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric)) *)
  1: eapply JMeq_trans; [apply @JMeq_sym |]; eassumption.
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric)) *)
  eapply derives_trans; [apply nested_field_ramif; eassumption |].
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  apply sepcon_derives; auto.
Qed.

Lemma nested_field_ramif_store: forall sh t gfs0 gfs1 (v_reptype: reptype (nested_field_type t gfs0)) (v0_reptype: reptype (nested_field_type (nested_field_type t gfs0) gfs1)) (v_val: val) p,
  field_compatible t (gfs1 ++ gfs0) p ->
  JMeq v0_reptype v_val ->
  exists v0_reptype',
    JMeq v0_reptype' v_val /\
    field_at sh t gfs0 v_reptype p |--
      field_at_ sh t (gfs1 ++ gfs0) p *
       (field_at sh t (gfs1 ++ gfs0) v0_reptype' p -*
          field_at sh t gfs0 (upd_reptype (nested_field_type t gfs0) gfs1 v_reptype v0_reptype) p).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  generalize (JMeq_refl (proj_reptype (nested_field_type t gfs0) gfs1 v_reptype)).
(* Goal: forall _ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  set (v0 := proj_reptype (nested_field_type t gfs0) gfs1 v_reptype) at 2.
(* Goal: forall _ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0, @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric)))) *)
  clearbody v0.
  generalize (JMeq_refl v0_reptype).
  set (v0_reptype' := v0_reptype) at 2.
  clearbody v0_reptype'.
  revert v0 v0_reptype'.
  pattern (reptype (nested_field_type (nested_field_type t gfs0) gfs1)) at 1 2 4 6.
(* Goal: (fun T : Type => forall (v0 : T) (_ : @JMeq (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (@proj_reptype cs (@nested_field_type cs t gfs0) gfs1 v_reptype) T v0), @ex (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v_reptype' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v_reptype' val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v_reptype' p) (@TT mpred Nveric))))) (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) *)
  rewrite nested_field_type_nested_field_type at 1.
  intros; exists v0_reptype'.
(* Goal: and (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0 val v_val) (@derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric))) *)
  split.
(* Goal: @JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0 val v_val *)
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric)) *)
  1: eapply JMeq_trans; [apply @JMeq_sym |]; eassumption.
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v_reptype p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@TT mpred Nveric)) *)
  eapply derives_trans; [apply nested_field_ramif; eassumption |].
  apply sepcon_derives.
  1: apply field_at_field_at_.
  eapply allp_left.
  eapply allp_left.
  rewrite prop_imp; [apply derives_refl |].
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  auto.
Qed.

Lemma nested_field_ramif': forall sh t gfs0 gfs1 v v0 p,
  JMeq (proj_reptype (nested_field_type t gfs0) gfs1 v) v0 ->
  legal_nested_field t (gfs1 ++ gfs0) ->
  field_at sh t gfs0 v p |--
    field_at sh t (gfs1 ++ gfs0) v0 p *
    (ALL v0': _, ALL v0'': _, !! JMeq v0' v0'' -->
      (field_at sh t (gfs1 ++ gfs0) v0' p -*
         field_at sh t gfs0 (upd_reptype (nested_field_type t gfs0) gfs1 v v0'') p)).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@allp mpred Nveric (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v0' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => @allp mpred Nveric (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (fun v0'' : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1) => @imp mpred Nveric (@prop mpred Nveric (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0' (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0'')) (@wand mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0' p) (@field_at cs sh t gfs0 (@upd_reptype cs (@nested_field_type cs t gfs0) gfs1 v v0'') p)))))) *)
  rewrite field_at_compatible'.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible cs t gfs0 p)) (@field_at cs sh t gfs0 v p)) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@allp mpred Nveric (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v0' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => @allp mpred Nveric (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (fun v0'' : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1) => @imp mpred Nveric (@prop mpred Nveric (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0' (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0'')) (@wand mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0' p) (@field_at cs sh t gfs0 (@upd_reptype cs (@nested_field_type cs t gfs0) gfs1 v v0'') p)))))) *)
  normalize.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  eapply nested_field_ramif; eauto.
  unfold field_compatible in *.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  tauto.
Qed.

Lemma nested_field_ramif'': forall sh t gfs0 gfs1 v v0 p,
  JMeq (proj_reptype (nested_field_type t gfs0) gfs1 v) v0 ->
  legal_nested_field (nested_field_type t gfs0) gfs1 ->
  field_at sh t gfs0 v p |--
    field_at sh t (gfs1 ++ gfs0) v0 p *
    (ALL v0': _, ALL v0'': _, !! JMeq v0' v0'' -->
      (field_at sh t (gfs1 ++ gfs0) v0' p -*
         field_at sh t gfs0 (upd_reptype (nested_field_type t gfs0) gfs1 v v0'') p)).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs0 v p) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@allp mpred Nveric (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v0' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => @allp mpred Nveric (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (fun v0'' : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1) => @imp mpred Nveric (@prop mpred Nveric (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0' (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0'')) (@wand mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0' p) (@field_at cs sh t gfs0 (@upd_reptype cs (@nested_field_type cs t gfs0) gfs1 v v0'') p)))))) *)
  rewrite field_at_compatible'.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible cs t gfs0 p)) (@field_at cs sh t gfs0 v p)) (@sepcon mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0 p) (@allp mpred Nveric (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) (fun v0' : @reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0)) => @allp mpred Nveric (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) (fun v0'' : @reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1) => @imp mpred Nveric (@prop mpred Nveric (@JMeq (@reptype cs (@nested_field_type cs t (@app gfield gfs1 gfs0))) v0' (@reptype cs (@nested_field_type cs (@nested_field_type cs t gfs0) gfs1)) v0'')) (@wand mpred Nveric Sveric (@field_at cs sh t (@app gfield gfs1 gfs0) v0' p) (@field_at cs sh t gfs0 (@upd_reptype cs (@nested_field_type cs t gfs0) gfs1 v v0'') p)))))) *)
  normalize.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  eapply nested_field_ramif; eauto.
(* Goal: @field_compatible cs t (@app gfield gfs1 gfs0) p *)
  pose proof legal_nested_field_app_inv t gfs0 gfs1.
  unfold field_compatible in *.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  tauto.
Qed.

End NESTED_RAMIF.

Lemma semax_extract_later_prop' {cs: compspecs}:
  forall {Espec: OracleKind},
    forall (Delta : tycontext) (PP : Prop) P Q R c post,
      ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |-- !!PP ->
      (PP -> semax Delta (|>PROPx P (LOCALx Q (SEPx R))) c post) ->
      semax Delta (|>PROPx P (LOCALx Q (SEPx R))) c post.
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
  eapply semax_pre_simple.
  + hoist_later_left.
    apply later_derives.
    rewrite (add_andp _ _ H).
    rewrite andp_assoc.
    apply andp_left2.
(* Goal: @eq mpred (@andp mpred Nveric (fold_right_sepcon R) (@liftx (LiftEnviron mpred) R1 rho)) (@sepcon mpred Nveric Sveric (@andp mpred Nveric R1 (@emp mpred Nveric Sveric)) (fold_right_sepcon R)) *)
    rewrite andp_comm.
    apply derives_refl.
  + apply semax_extract_later_prop1.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
    auto.
Qed.

Lemma insert_corable_sep: forall R1 P Q R,
  corable R1 ->
  `R1 && PROPx P (LOCALx Q (SEPx R)) = PROPx P (LOCALx Q (SEPx (R1 && emp :: R))).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @eq mpred (@andp mpred Nveric (fold_right_sepcon R) (@liftx (LiftEnviron mpred) R1 rho)) (@sepcon mpred Nveric Sveric (@andp mpred Nveric R1 (@emp mpred Nveric Sveric)) (fold_right_sepcon R)) *)
  rewrite andp_comm.
(* Goal: @eq (lifted (LiftEnviron mpred)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (LiftEnviron mpred) R1)) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) (@andp (lift_T (LiftEnviron mpred)) Nveric R1 (@emp (lift_T (LiftEnviron mpred)) Nveric Sveric)) R)))) *)
  unfold PROPx.
  rewrite andp_assoc; f_equal.
(* Goal: @eq (lifted (LiftEnviron mpred)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (LOCALx Q (SEPx R)) (@liftx (LiftEnviron mpred) R1)) (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) (@andp (lift_T (LiftEnviron mpred)) Nveric R1 (@emp (lift_T (LiftEnviron mpred)) Nveric Sveric)) R))) *)
  unfold LOCALx.
  rewrite andp_assoc; f_equal.
(* Goal: @eq (lifted (LiftEnviron mpred)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (SEPx R) (@liftx (LiftEnviron mpred) R1)) (SEPx (@cons (lift_T (LiftEnviron mpred)) (@andp (lift_T (LiftEnviron mpred)) Nveric R1 (@emp (lift_T (LiftEnviron mpred)) Nveric Sveric)) R)) *)
  unfold SEPx.
(* Goal: @eq (lifted (LiftEnviron mpred)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (fun _ : environ => fold_right_sepcon R) (@liftx (LiftEnviron mpred) R1)) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) (@andp (lift_T (LiftEnviron mpred)) Nveric R1 (@emp (lift_T (LiftEnviron mpred)) Nveric Sveric)) R)) *)
  extensionality rho.
(* Goal: @eq expr (nested_efield (nested_efield t gfs0 tts0) (@cons efield a gfs1) (@cons type t0 tts1)) (nested_efield t (@app efield (@cons efield a gfs1) gfs0) (@app type (@cons type t0 tts1) tts0)) *)
  simpl.
(* Goal: @eq mpred (@andp mpred Nveric (fold_right_sepcon R) (@liftx (LiftEnviron mpred) R1 rho)) (@sepcon mpred Nveric Sveric (@andp mpred Nveric R1 (@emp mpred Nveric Sveric)) (fold_right_sepcon R)) *)
  rewrite andp_comm.
(* Goal: @eq Type (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) (@reptype cs (@nested_field_type cs t (@cons gfield (ArraySubsc Z0) gfs))) *)
  rewrite andp_left_corable by auto.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
  reflexivity.
Qed.

(************************************************

Lemmas of field nested load/store

************************************************)

Lemma nested_efield_app: forall t gfs0 gfs1 tts0 tts1,
  length gfs1 = length tts1 ->
  nested_efield (nested_efield t gfs0 tts0) gfs1 tts1 =
    nested_efield t (gfs1 ++ gfs0) (tts1 ++ tts0).
Proof.
(* Goal: forall (t : expr) (gfs0 gfs1 : list efield) (tts0 tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  intros.
(* Goal: @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  revert tts1 H.
(* Goal: forall (tts1 : list type) (_ : @eq nat (@Datatypes.length efield gfs1) (@Datatypes.length type tts1)), @eq expr (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) *)
  induction gfs1; intros; destruct tts1; try solve [inversion H].
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
  + reflexivity.
  + inversion H.
(* Goal: @eq expr (nested_efield (nested_efield t gfs0 tts0) (@cons efield a gfs1) (@cons type t0 tts1)) (nested_efield t (@app efield (@cons efield a gfs1) gfs0) (@app type (@cons type t0 tts1) tts0)) *)
    simpl.
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) i t0 | eUnionField i => Efield (nested_efield (nested_efield t gfs0 tts0) gfs1 tts1) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
    rewrite (IHgfs1 tts1 H1).
(* Goal: @eq expr match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end match a with | eArraySubsc ei => Ederef (Ebinop Cop.Oadd (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) ei (tptr t0)) t0 | eStructField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 | eUnionField i => Efield (nested_efield t (@app efield gfs1 gfs0) (@app type tts1 tts0)) i t0 end *)
    reflexivity.
Qed.
