Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.type_induction.
Require Import VST.floyd.nested_pred_lemmas.
Require Import VST.floyd.mapsto_memory_block.
Require VST.floyd.aggregate_pred. Import VST.floyd.aggregate_pred.aggregate_pred.
Import VST.floyd.aggregate_pred.auxiliary_pred.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.jmeq_lemmas.
Require Import VST.floyd.sublist.
Require Export VST.floyd.fieldlist.
Require Export VST.floyd.aggregate_type.

Opaque alignof.

Local Open Scope logic.

Arguments align !n !amount / .
Arguments Z.max !n !m / .

Definition offset_in_range ofs p :=
  match p with
  | Vptr b iofs => 0 <= Ptrofs.unsigned iofs + ofs <= Ptrofs.modulus
  | _ => True
  end.

Definition offset_strict_in_range ofs p :=
  match p with
  | Vptr b iofs => 0 <= Ptrofs.unsigned iofs + ofs < Ptrofs.modulus
  | _ => True
  end.

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

Definition of data_at_rec

Always assume in arguments of data_at_rec has argument pos with alignment criterion.

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

Section CENV.

Context {cs: compspecs}.

(*
Lemma proj_struct_default: forall i m d,
  in_members i m ->
  members_no_replicate m = true ->
  proj_struct i m (struct_default_val m) d = default_val (field_type i m).
Proof.
Qed.

Lemma proj_union_default: forall i m d,
  i = fst (members_union_inj (union_default_val m)) ->
  m <> nil ->
  members_no_replicate m = true ->
  proj_union i m (union_default_val m) d = default_val (field_type2 i m).
Proof.
  unfold field_type2.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  destruct m as [| (i0, t0) m]; [congruence |].
  destruct m as [| (i1, t1) m].
  + simpl in d, H |- *; subst.
    if_tac; [| congruence].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    unfold eq_rect_r; rewrite <- eq_rect_eq; auto.
  + simpl in H; subst.
    simpl in d |- *; subst.
    if_tac; [| congruence].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    unfold eq_rect_r; rewrite <- eq_rect_eq; auto.
Qed.
*)
Section WITH_SHARE.

Variable sh: share.

Definition data_at_rec: forall t, reptype t -> val -> mpred :=
  type_func (fun t => reptype t -> val -> mpred)
    (fun t v p =>
       if type_is_volatile t
       then memory_block sh (sizeof t) p
       else mapsto sh t p (repinject t v))
    (fun t n a P v => array_pred 0 (Z.max 0 n) (fun i v => at_offset (P v) (sizeof t * i)) (unfold_reptype v))
    (fun id a P v => struct_data_at_rec_aux sh (co_members (get_co id)) (co_members (get_co id)) (co_sizeof (get_co id)) P (unfold_reptype v))
    (fun id a P v => union_data_at_rec_aux sh (co_members (get_co id)) (co_members (get_co id)) (co_sizeof (get_co id)) P (unfold_reptype v)).

Lemma data_at_rec_eq: forall t v,
  data_at_rec t v =
  match t return REPTYPE t -> val -> mpred with
  | Tvoid
  | Tfunction _ _ _ => fun _ _ => FF
  | Tint _ _ _
  | Tfloat _ _
  | Tlong _ _
  | Tpointer _ _ => fun v p =>
                      if type_is_volatile t
                      then memory_block sh (sizeof t) p
                      else mapsto sh t p v
  | Tarray t0 n a => array_pred 0 (Z.max 0 n) (fun i v => at_offset (data_at_rec t0 v) (sizeof t0 * i))
  | Tstruct id a => struct_pred (co_members (get_co id))
                      (fun it v => withspacer sh
                        (field_offset cenv_cs (fst it) (co_members (get_co id)) + sizeof (field_type (fst it) (co_members (get_co id))))
                        (field_offset_next cenv_cs (fst it) (co_members (get_co id)) (co_sizeof (get_co id)))
                        (at_offset (data_at_rec (field_type (fst it) (co_members (get_co id))) v) (field_offset cenv_cs (fst it) (co_members (get_co id)))))
  | Tunion id a => union_pred (co_members (get_co id))
                     (fun it v => withspacer sh
                      (sizeof (field_type (fst it) (co_members (get_co id))))
                      (co_sizeof (get_co id))
                      (data_at_rec (field_type (fst it) (co_members (get_co id))) v))
  end (unfold_reptype v).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq (forall _ : val, mpred) (data_at_rec t v) (match t return (forall (_ : match t with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t0 a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : val), mpred) with | Tvoid => fun (_ : match Tvoid with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t a => val | Tarray t0 z a => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : val) => @FF mpred Nveric | Tint i s a => fun (v : match Tint i s a with | Tvoid => unit | Tint i0 s0 a0 => val | Tlong s0 a0 => val | Tfloat f a0 => val | Tpointer t a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end) (p : val) => if type_is_volatile t then memory_block sh (@sizeof (@cenv_cs cs) t) p else mapsto sh t p v | Tlong s a => fun (v : match Tlong s a with | Tvoid => unit | Tint i s0 a0 => val | Tlong s0 a0 => val | Tfloat f a0 => val | Tpointer t a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end) (p : val) => if type_is_volatile t then memory_block sh (@sizeof (@cenv_cs cs) t) p else mapsto sh t p v | Tfloat f a => fun (v : match Tfloat f a with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f0 a0 => val | Tpointer t a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t t0 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end) (p : val) => if type_is_volatile t then memory_block sh (@sizeof (@cenv_cs cs) t) p else mapsto sh t p v | Tpointer t0 a => fun (v : match Tpointer t0 a with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t a0 => val | Tarray t1 z a0 => list (@reptype cs t1) | Tfunction t t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end) (p : val) => if type_is_volatile t then memory_block sh (@sizeof (@cenv_cs cs) t) p else mapsto sh t p v | Tarray t0 n a => @array_pred (@reptype cs t0) (@Inhabitant_reptype cs t0) Z0 (Z.max Z0 n) (fun (i : Z) (v : @reptype cs t0) => at_offset (data_at_rec t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) | Tfunction t t0 c => fun (_ : match Tfunction t t0 c with | Tvoid => unit | Tint i s a => val | Tlong s a => val | Tfloat f a => val | Tpointer t1 a => val | Tarray t1 z a => list (@reptype cs t1) | Tfunction t1 t2 c0 => unit | Tstruct id a => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a => @reptype_unionlist cs (co_members (@get_co cs id)) end) (_ : val) => @FF mpred Nveric | Tstruct id a => @struct_pred (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun (it : prod ident type) (v : (fun it0 : prod ident type => @reptype cs (field_type (@fst ident type it0) (co_members (@get_co cs id)))) it) => withspacer sh (Z.add (field_offset (@cenv_cs cs) (@fst ident type it) (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (field_type (@fst ident type it) (co_members (@get_co cs id))))) (field_offset_next (@cenv_cs cs) (@fst ident type it) (co_members (@get_co cs id)) (co_sizeof (@get_co cs id))) (at_offset (data_at_rec (field_type (@fst ident type it) (co_members (@get_co cs id))) v) (field_offset (@cenv_cs cs) (@fst ident type it) (co_members (@get_co cs id))))) | Tunion id a => @union_pred (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun (it : prod ident type) (v : (fun it0 : prod ident type => @reptype cs (field_type (@fst ident type it0) (co_members (@get_co cs id)))) it) => withspacer sh (@sizeof (@cenv_cs cs) (field_type (@fst ident type it) (co_members (@get_co cs id)))) (co_sizeof (@get_co cs id)) (data_at_rec (field_type (@fst ident type it) (co_members (@get_co cs id))) v)) end (@unfold_reptype cs t v)) *)
  unfold data_at_rec at 1.
(* Goal: @eq Prop (@type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) t v) (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => fun v0 : @reptype cs Tvoid => if type_is_volatile Tvoid then True else tc_val' Tvoid (@repinject cs Tvoid v0) | Tint i s a => fun v0 : @reptype cs (Tint i s a) => if type_is_volatile (Tint i s a) then True else tc_val' (Tint i s a) (@repinject cs (Tint i s a) v0) | Tlong s a => fun v0 : @reptype cs (Tlong s a) => if type_is_volatile (Tlong s a) then True else tc_val' (Tlong s a) (@repinject cs (Tlong s a) v0) | Tfloat f a => fun v0 : @reptype cs (Tfloat f a) => if type_is_volatile (Tfloat f a) then True else tc_val' (Tfloat f a) (@repinject cs (Tfloat f a) v0) | Tpointer t a => fun v0 : @reptype cs (Tpointer t a) => if type_is_volatile (Tpointer t a) then True else tc_val' (Tpointer t a) (@repinject cs (Tpointer t a) v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v0)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n0 : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n0 a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n0 a0) v)) (Z.max Z0 n0)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n0 a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) t') (@unfold_reptype cs (Tarray t' n a) v0)) | Tfunction t t1 c => fun v0 : @reptype cs (Tfunction t t1 c) => if type_is_volatile (Tfunction t t1 c) then True else tc_val' (Tfunction t t1 c) (@repinject cs (Tfunction t t1 c) v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a0) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a0) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) *)
  rewrite type_func_eq.
  destruct t; auto;
  try solve [destruct (readable_share_dec sh); reflexivity];
  try solve [
  match goal with
  | |- context[repinject ?tt] =>
    rewrite (repinject_unfold_reptype tt); auto
  end].
  + rewrite <- struct_data_at_rec_aux_spec; reflexivity.
  + rewrite <- union_data_at_rec_aux_spec; reflexivity.
Qed.

End WITH_SHARE.

Lemma data_at_rec_type_changable: forall (sh: Share.t) (t1 t2: type) v1 v2,
  t1 = t2 ->
  JMeq v1 v2 ->
  data_at_rec sh t1 v1 = data_at_rec sh t2 v2.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq Prop (value_fits t1 v1) (value_fits t2 v2) *)
  subst t2.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v))) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  apply JMeq_eq in H0.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v))) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  rewrite H0.
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  reflexivity.
Qed.
(*
Lemma data_at_type_changable: forall (sh: Share.t) (t1 t2: type) v1 v2,
  t1 = t2 ->
  JMeq v1 v2 ->
  data_at sh t1 v1 = data_at sh t2 v2.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  unfold data_at.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
  simpl. extensionality.
  erewrite data_at_rec_type_changable; [| exact H| exact H0].
  rewrite H.
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  reflexivity.
Qed.
*)
Lemma by_value_default_val: forall t:type,
  type_is_by_value t = true -> JMeq (default_val t) Vundef.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @JMeq (@reptype cs t) (@default_val cs t) val Vundef *)
  destruct t; try inversion H; try tauto; apply JMeq_refl.
Qed.

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

Transformation between data_at/data_at_ and mapsto.

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

Lemma by_value_reptype: forall t, type_is_by_value t = true -> reptype t = val.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq Type (@reptype cs t) val *)
  destruct t; simpl in H; try inversion H; tauto.
Qed.

Lemma by_value_data_at_rec_volatile: forall sh t v p,
  type_is_by_value t = true ->
  type_is_volatile t = true ->
  data_at_rec sh t v p = memory_block sh (sizeof t) p.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  rewrite data_at_rec_eq; destruct t; try solve [inversion H];
  match goal with
  | |- context[type_is_volatile ?tt] =>
    destruct (type_is_volatile tt) eqn:HH; auto;
    rewrite <- (repinject_unfold_reptype tt); auto
  end;
  inversion H0.
Qed.

Lemma by_value_data_at_rec_nonvolatile: forall sh t v p,
  type_is_by_value t = true ->
  type_is_volatile t = false ->
  data_at_rec sh t v p = mapsto sh t p (repinject t v).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  rewrite data_at_rec_eq; destruct t; try solve [inversion H]; rewrite H0;
  match goal with
  | |- context[repinject ?tt] =>
    rewrite (repinject_unfold_reptype tt); auto
  end.
Qed.

Lemma by_value_data_at_rec_default_val: forall sh t p,
  type_is_by_value t = true ->
  size_compatible t p ->
  align_compatible t p ->
  data_at_rec sh t (default_val t) p = memory_block sh (sizeof t) p.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq mpred (data_at_rec sh t v p) (memory_block sh (@sizeof (@cenv_cs cs) t) p) *)
  destruct (type_is_volatile t) eqn:?H.
  + apply by_value_data_at_rec_volatile; auto.
  + rewrite data_at_rec_eq; destruct t; try solve [inversion H]; rewrite H2;
    symmetry;
    rewrite memory_block_mapsto_ by auto; unfold mapsto_;
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    try rewrite if_true by auto; auto.
Qed.

Lemma by_value_data_at_rec_nonreachable: forall sh t p v,
  type_is_by_value t = true ->
  size_compatible t p ->
  align_compatible t p ->
  ~ readable_share sh ->
  tc_val' t (repinject t v) ->
  data_at_rec sh t v p = memory_block sh (sizeof t) p.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq mpred (data_at_rec sh t v p) (memory_block sh (@sizeof (@cenv_cs cs) t) p) *)
  destruct (type_is_volatile t) eqn:?H.
  + apply by_value_data_at_rec_volatile; auto.
  + rewrite by_value_data_at_rec_nonvolatile by auto.
    symmetry;
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    apply nonreadable_memory_block_mapsto; auto.
Qed.

Lemma by_value_data_at_rec_default_val2: forall sh t b ofs,
  type_is_by_value t = true ->
  0 <= ofs /\ ofs + sizeof t < Ptrofs.modulus ->
  align_compatible_rec cenv_cs t ofs ->
  data_at_rec sh t (default_val t) (Vptr b (Ptrofs.repr ofs)) =
  memory_block sh (sizeof t) (Vptr b (Ptrofs.repr ofs)).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq mpred (data_at_rec sh t (@default_val cs t) (Vptr b (Ptrofs.repr ofs))) (memory_block sh (@sizeof (@cenv_cs cs) t) (Vptr b (Ptrofs.repr ofs))) *)
  apply by_value_data_at_rec_default_val; auto.
  + unfold size_compatible.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
    solve_mod_modulus.
(* Goal: Z.lt (Z.add (Z.modulo ofs Ptrofs.modulus) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
    pose_mod_le ofs.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    omega.
  + unfold align_compatible.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
    solve_mod_modulus.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Z.modulo ofs Ptrofs.modulus) *)
    pose proof sizeof_pos t.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    rewrite Zmod_small by omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    auto.
Qed.

Lemma by_value_data_at_rec_nonreachable2: forall sh t b ofs v,
  type_is_by_value t = true ->
  0 <= ofs /\ ofs + sizeof t < Ptrofs.modulus ->
  align_compatible_rec cenv_cs t ofs ->
  ~ readable_share sh ->
  tc_val' t (repinject t v) ->
  data_at_rec sh t v (Vptr b (Ptrofs.repr ofs)) = memory_block sh (sizeof t) (Vptr b (Ptrofs.repr ofs)).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  apply by_value_data_at_rec_nonreachable; auto.
  + unfold size_compatible.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
    solve_mod_modulus.
(* Goal: Z.lt (Z.add (Z.modulo ofs Ptrofs.modulus) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
    pose_mod_le ofs.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    omega.
  + unfold align_compatible.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
    solve_mod_modulus.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Z.modulo ofs Ptrofs.modulus) *)
    pose proof sizeof_pos t.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    rewrite Zmod_small by omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    auto.
Qed.

(*
Lemma by_value_data_at_: forall sh t p,
  type_is_by_value t = true ->
  data_at_ sh t p = !! field_compatible t nil p && mapsto_ sh t p.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  unfold data_at_, mapsto_.
  destruct t; simpl in H; try inversion H; try tauto; simpl default_val;
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  apply by_value_data_at; reflexivity.
Qed.
*)

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

Transformation between data_at and data_at_rec. This is used in transformation
between field_at and data_at.

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

Lemma lower_sepcon_val':
  forall (P Q: val->mpred) v,
  ((P*Q) v) = (P v * Q v).
Proof. reflexivity. Qed.

(*
Lemma unsigned_add: forall i pos, 0 <= pos -> Int.unsigned (Int.add i (Int.repr pos)) = (Int.unsigned i + pos) mod Int.modulus.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  unfold Int.add.
  pose proof Int.modulus_pos.
  pose proof Int.unsigned_range i.
  pose proof Int.unsigned_range (Int.repr pos).
  rewrite !Int.unsigned_repr_eq in *.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
  rewrite Z.add_mod by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
  rewrite Z.mod_mod by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
  rewrite <- Z.add_mod by omega.
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  reflexivity.
Qed.

Lemma memory_block_data_at__aux1: forall i pos t,
  0 <= pos /\ pos + sizeof t <= Int.modulus - Int.unsigned i ->
  Int.unsigned (Int.add i (Int.repr pos)) + sizeof t <= Int.modulus.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  destruct H.
  rewrite (unsigned_add i pos H).
  cut ((Int.unsigned i + pos) mod Int.modulus <= Int.unsigned i + pos).
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    { intros. omega. }
  pose proof Int.modulus_pos.
  pose proof Int.unsigned_range i.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
  apply Z.mod_le; omega.
Qed.

Lemma memory_block_data_at__aux2: forall i pos t,
  0 <= pos /\ pos + sizeof t <= Int.modulus - Int.unsigned i ->
  (alignof t | Int.unsigned i) ->
  (alignof t | pos) ->
  (alignof t | Int.unsigned (Int.add i (Int.repr pos))).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  destruct H.
  rewrite (unsigned_add i pos H).
  destruct (zlt (Int.unsigned i + pos) Int.modulus).
  + pose proof Int.unsigned_range i.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    rewrite Z.mod_small by omega.
    apply Z.divide_add_r; assumption.
  + pose proof sizeof_pos cenv_cs t.
    assert (Int.unsigned i + pos = Int.modulus) by omega.
    rewrite H4.
    rewrite Z_mod_same_full.
    apply Z.divide_0_r.
Qed.
*)
Lemma Znth_nil: forall {A}{d: Inhabitant A} n, Znth n nil = default.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq A (@Znth A d n (@nil A)) (@default A d) *)
  unfold Znth.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  if_tac; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
  simpl.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  destruct (Z.to_nat n); auto.
Qed.

Lemma offset_val_zero_Vptr: forall b i, offset_val 0 (Vptr b i) = Vptr b i.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq val (offset_val Z0 (Vptr b i)) (Vptr b i) *)
  unfold offset_val, Ptrofs.add.
(* Goal: @eq val (Vptr b (Ptrofs.repr (Z.add (Ptrofs.unsigned i) (Ptrofs.unsigned (Ptrofs.repr Z0))))) (Vptr b i) *)
  change (Ptrofs.unsigned (Ptrofs.repr 0)) with 0.
(* Goal: @eq val (Vptr b (Ptrofs.repr (Z.add (Ptrofs.unsigned i) Z0))) (Vptr b i) *)
  rewrite Z.add_0_r.
(* Goal: @eq val (Vptr b (Ptrofs.repr (Ptrofs.unsigned i))) (Vptr b i) *)
  rewrite Ptrofs.repr_unsigned.
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  reflexivity.
Qed.
(*
Ltac AUTO_IND :=
  match goal with
  | H: complete_legal_cosu_type (Tarray ?t ?n ?a) = true |- complete_legal_cosu_type ?t = true =>
    simpl in H; auto
  | H: (alignof (Tarray ?t ?z ?a) | ?ofs)
    |- (alignof ?t | ?ofs + _) =>
    apply Z.divide_add_r;
    [ eapply Z.divide_trans; [eapply alignof_divide_alignof_Tarray |]; eauto
    | apply Z.divide_mul_l; eapply legal_alignas_type_Tarray; eauto]
  | H: legal_alignas_type (Tstruct ?id ?a) = true |-
    legal_alignas_type (field_type ?i (co_members (get_co ?id))) = true =>
    unfold legal_alignas_type in H;
    apply nested_pred_Tstruct2 with (i0 := i) in H;
    [exact H | auto]
  | H: legal_cosu_type (Tstruct ?id ?a) = true |-
    legal_cosu_type (field_type ?i (co_members (get_co ?id))) = true =>
    unfold legal_cosu_type in H;
    apply nested_pred_Tstruct2 with (i0 := i) in H;
    [exact H | auto]
  | |- complete_type ?env (field_type ?i (co_members (get_co ?id))) = true =>
    apply complete_type_field_type; auto
  | H: (alignof (Tstruct ?id ?a) | ?ofs)
    |- (alignof (field_type ?i (co_members (get_co ?id))) | ?ofs + _) =>
    apply Z.divide_add_r;
    [ eapply Z.divide_trans; [apply alignof_field_type_divide_alignof; auto |];
      eapply Z.divide_trans; [apply legal_alignas_type_Tstruct; eauto | auto]
    | apply field_offset_aligned]
  | H: legal_alignas_type (Tunion ?id ?a) = true |-
    legal_alignas_type (field_type ?i (co_members (get_co ?id))) = true =>
    unfold legal_alignas_type in H;
    apply nested_pred_Tunion2 with (i0 := i) in H;
    [exact H | auto]
  | H: legal_cosu_type (Tunion ?id ?a) = true |-
    legal_cosu_type (field_type ?i (co_members (get_co ?id))) = true =>
    unfold legal_cosu_type in H;
    apply nested_pred_Tunion2 with (i0 := i) in H;
    [exact H | auto]
  | H: (alignof (Tunion ?id ?a) | ?ofs)
    |- (alignof (field_type ?i (co_members (get_co ?id))) | ?ofs) =>
    eapply Z.divide_trans; [apply alignof_field_type_divide_alignof; auto |];
    eapply Z.divide_trans; [apply legal_alignas_type_Tunion; eauto | auto]
  end.
*)

Lemma nth_list_repeat: forall A i n (x :A),
    nth i (list_repeat n x) x = x.
Proof.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
 induction i; destruct n; simpl; auto.
Qed.

Lemma nth_list_repeat': forall A i n (x y :A),
    (i < n)%nat ->
    nth i (list_repeat n x) y = x.
Proof.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
 induction i; destruct n; simpl; intros; auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
 omega. omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
 apply IHi; auto. omega.
Qed.

 Lemma Z2Nat_max0: forall z, Z.to_nat (Z.max 0 z) = Z.to_nat z.
 Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq nat (Z.to_nat (Z.max Z0 z)) (Z.to_nat z) *)
  rewrite Z.max_comm, <- nat_of_Z_max, Nat2Z.id.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  auto.
Qed.

Lemma range_max0: forall x z, 0 <= x < Z.max 0 z <-> 0 <= x < z.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x (Z.max Z0 z))) (and (Z.le Z0 x) (Z.lt x z)) *)
  destruct (zlt z 0).
  + rewrite Z.max_l by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    omega.
  + rewrite Z.max_r by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    omega.
Qed.
  
(* We use (Vptr b (Int.repr ofs)) instead of p because size_compatible is more  *)
(* difficult to use than simple arithmetic in induction proof.                  *)
Lemma memory_block_data_at_rec_default_val: forall sh t b ofs
  (LEGAL_COSU: complete_legal_cosu_type t = true),
  0 <= ofs /\ ofs + sizeof t < Ptrofs.modulus ->
  align_compatible_rec cenv_cs t ofs ->
  data_at_rec sh t (default_val t) (Vptr b (Ptrofs.repr ofs)) =
    memory_block sh (sizeof t) (Vptr b (Ptrofs.repr ofs)).
Proof.
  intros sh t.
  type_induction t; intros;
  try solve [inversion COMPLETE];
  try solve [apply by_value_data_at_rec_default_val2; auto];
  rewrite data_at_rec_eq.
  + rewrite (default_val_eq (Tarray t z a)).
    rewrite unfold_fold_reptype.
    rewrite array_pred_ext with
     (P1 := fun i _ p => memory_block sh (sizeof t)
                          (offset_val (sizeof t * i) p))
     (v1 := list_repeat (Z.to_nat (Z.max 0 z)) (default_val t));
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
     auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite memory_block_array_pred; auto.
    - apply Z.le_max_l.
    - f_equal.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
      f_equal.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      rewrite Z2Nat_max0; auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
      rewrite at_offset_eq3.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
      unfold offset_val; solve_mod_modulus.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      unfold Znth. rewrite if_false by omega.
      rewrite nth_list_repeat.
      unfold sizeof in H, H1; fold @sizeof in H,H1.
      pose_size_mult cenv_cs t (0 :: i :: i + 1 :: Z.max 0 z :: nil).
      assert (sizeof t = 0 -> sizeof t * i = 0)%Z by (intros HH; rewrite HH, Z.mul_0_l; auto).
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      apply IH; auto; try omega.
      eapply align_compatible_rec_Tarray_inv; [eassumption |].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply range_max0; auto.
  + rewrite default_val_eq.
    rewrite unfold_fold_reptype.
    rewrite struct_pred_ext with
     (P1 := fun it _ p =>
              memory_block sh
               (field_offset_next cenv_cs (fst it) (co_members (get_co id)) (co_sizeof (get_co id)) -
                  field_offset cenv_cs (fst it) (co_members (get_co id)))
               (offset_val (field_offset cenv_cs (fst it) (co_members (get_co id))) p))
     (v1 := (struct_default_val (co_members (get_co id))));
    [| apply get_co_members_no_replicate |].
    - rewrite memory_block_struct_pred.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * rewrite sizeof_Tstruct; auto.
      * apply get_co_members_nil_sizeof_0.
      * apply get_co_members_no_replicate.
      * rewrite sizeof_Tstruct in H.
        pose proof co_consistent_sizeof cenv_cs (get_co id) (get_co_consistent id).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        erewrite complete_legal_cosu_type_Tstruct in H1 by eauto.
        pose proof co_consistent_sizeof cenv_cs (get_co id) (get_co_consistent id).
        unfold sizeof_composite in H1.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        revert H1; pose_align_le; intros; omega.
      * rewrite sizeof_Tstruct in H.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        omega.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
      pose proof get_co_members_no_replicate id as NO_REPLI.
      rewrite withspacer_spacer.
      simpl @fst.
      rewrite spacer_memory_block by (simpl; auto).
      rewrite at_offset_eq3.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
      unfold offset_val; solve_mod_modulus.
      unfold struct_default_val.
      unfold proj_struct.
      rewrite compact_prod_proj_gen by (apply in_members_field_type; auto).
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
      rewrite Forall_forall in IH.
      specialize (IH (i, field_type i (co_members (get_co id)))).
      spec IH; [apply in_members_field_type; auto |].
      unfold snd in IH.
      rewrite IH.
      * rewrite Z.add_assoc, sepcon_comm, <- memory_block_split by (pose_field; omega).
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        f_equal; omega.
      * apply complete_legal_cosu_type_field_type.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      * simpl fst. pose_field; omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * simpl fst. eapply align_compatible_rec_Tstruct_inv'; eauto.
  + assert (co_members (get_co id) = nil \/ co_members (get_co id) <> nil)
      by (destruct (co_members (get_co id)); [left | right]; congruence).
    destruct H1.
    - rewrite sizeof_Tunion.
      rewrite (get_co_members_nil_sizeof_0 _ H1).
      generalize (unfold_reptype (default_val (Tunion id a)));
      rewrite H1 in *;
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      intros.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
      simpl.
      rewrite memory_block_zero.
      normalize.
    - rewrite default_val_eq.
      rewrite unfold_fold_reptype.
      rewrite union_pred_ext with
       (P1 := fun it _ => memory_block sh (co_sizeof (get_co id)))
       (v1 := (union_default_val (co_members (get_co id))));
      [| apply get_co_members_no_replicate | reflexivity |].
      * rewrite memory_block_union_pred by (apply get_co_members_nil_sizeof_0).
        rewrite sizeof_Tunion.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      * intros.
        pose proof get_co_members_no_replicate id as NO_REPLI.
        pose proof @compact_sum_inj_in _ _ (co_members (get_co id)) (union_default_val (co_members (get_co id))) _ _ H3.
        apply in_map with (f := fst) in H4; unfold fst in H4.
        rewrite withspacer_spacer.
        simpl @fst.
        rewrite spacer_memory_block by (simpl; auto).
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
        unfold offset_val; solve_mod_modulus.
        unfold union_default_val.
        unfold proj_union.
        unfold members_union_inj in *.
        rewrite compact_sum_proj_gen; [| auto].
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
        rewrite Forall_forall in IH.
        specialize (IH (i, field_type i (co_members (get_co id)))).
        spec IH; [apply in_members_field_type; auto |].
        unfold snd in IH.
        rewrite IH.
        {
          rewrite sepcon_comm, <- memory_block_split by (pose_field; omega).
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          f_equal; f_equal; omega.
        } {
          apply complete_legal_cosu_type_field_type.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          auto.
        } {
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          pose_field; omega.
        } {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          simpl fst. eapply align_compatible_rec_Tunion_inv'; eauto.
        }
Qed.

(*
Lemma align_1_memory_block_data_at_: forall (sh : share) (t : type),
  legal_alignas_type t = true ->
  nested_legal_fieldlist t = true ->
  nested_non_volatile_type t = true ->
  alignof t = 1%Z ->
  (sizeof t < Ptrofs.modulus)%Z ->
  memory_block sh (Ptrofs.repr (sizeof t)) = data_at_ sh t.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  extensionality p.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  rewrite data_at__memory_block by auto.
  rewrite andp_comm.
  apply add_andp.
  normalize.
  apply prop_right.
(* Goal: @align_compatible cs t (Vptr b (Ptrofs.repr ofs)) *)
  unfold align_compatible.
  rewrite H2.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  destruct p; auto.
  split; [| auto].
  apply Z.divide_1_l.
Qed.

*)

(*
Lemma data_at_rec_readable:
  forall sh t v p, data_at_rec sh t v p |-- !! readable_share sh.
Proof.
intros sh t.
type_induction t; intros;
rewrite data_at_rec_eq; try apply FF_left.
if_tac.
+ simpl. destruct i; simpl.
rewrite memory_block_eq.
saturate_local.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
simpl.
*)

Lemma data_at_rec_data_at_rec_ : forall sh t v b ofs
  (LEGAL_COSU: complete_legal_cosu_type t = true),
  0 <= ofs /\ ofs + sizeof t < Ptrofs.modulus ->
  align_compatible_rec cenv_cs t ofs ->
  data_at_rec sh t v (Vptr b (Ptrofs.repr ofs)) |-- data_at_rec sh t (default_val t) (Vptr b (Ptrofs.repr ofs)).
Proof.
  intros sh t.
  type_induction t; intros;
  try solve [inversion LEGAL_COSU];
  try solve [rewrite !data_at_rec_eq; try (simple_if_tac; auto);
  try solve [rewrite default_val_eq, unfold_fold_reptype; apply mapsto_mapsto_]].
  + rewrite !data_at_rec_eq.
    apply array_pred_ext_derives.
    {
      intros; rewrite default_val_eq.
      rewrite unfold_fold_reptype.
      rewrite Zlength_correct in H1.
      rewrite <- Z2Nat_max0.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      rewrite Zlength_list_repeat by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      omega.
    }
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
    rewrite default_val_eq. simpl.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    rewrite !at_offset_eq3.
    rewrite default_val_eq with (t0 := (Tarray t z a)), unfold_fold_reptype.
    eapply derives_trans.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    apply IH; auto.
    - pose_size_mult cenv_cs t (0 :: i :: i + 1 :: Z.max 0 z :: nil); simpl in H; try omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - eapply align_compatible_rec_Tarray_inv; eauto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply range_max0; auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    - apply derives_refl'. f_equal. unfold Znth. rewrite if_false by omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      rewrite nth_list_repeat'; auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      apply Nat2Z.inj_lt. rewrite Z2Nat.id, Z2Nat_id' by omega. omega.
  + rewrite !data_at_rec_eq.
    rewrite default_val_eq, unfold_fold_reptype.
    assert (members_no_replicate (co_members (get_co id)) = true) as NO_REPLI
(* Goal: @eq bool (members_no_replicate (co_members (@get_co cs id))) true *)
      by apply get_co_members_no_replicate.
    apply struct_pred_ext_derives; [auto |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    rewrite !withspacer_spacer.
    simpl @fst.
    apply sepcon_derives; [auto |].
    rewrite !at_offset_eq3.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
    rewrite Forall_forall in IH.
    specialize (IH (i, (field_type i (co_members (get_co id))))).
    spec IH; [apply in_members_field_type; auto |].
    unfold snd in IH.
    unfold struct_default_val.
    unfold proj_struct.
    rewrite compact_prod_proj_gen by (apply in_members_field_type; auto).
    apply IH; try unfold fst.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - apply complete_legal_cosu_type_field_type; auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
    - pose_field; omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - eapply align_compatible_rec_Tstruct_inv'; eauto.
  + assert (co_members (get_co id) = nil \/ co_members (get_co id) <> nil)
      by (destruct (co_members (get_co id)); [left | right]; congruence).
    destruct H1.
    - rewrite !data_at_rec_eq.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      generalize (unfold_reptype v) (unfold_reptype (default_val (Tunion id a))); rewrite H1; intros.
      apply derives_refl.
    - rewrite data_at_rec_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      rewrite memory_block_data_at_rec_default_val by auto.
      eapply derives_trans.
      * assert (members_no_replicate (co_members (get_co id)) = true) as NO_REPLI
(* Goal: @eq bool (members_no_replicate (co_members (@get_co cs id))) true *)
          by apply get_co_members_no_replicate.
        apply union_pred_ext_derives with
          (P1 := fun _ _ => memory_block sh (sizeof (Tunion id a)));
          [auto | reflexivity | ].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
        intros.
        clear H3.
        pose proof @compact_sum_inj_in _ _ (co_members (get_co id)) (unfold_reptype v) _ _ H2.
        apply in_map with (f := fst) in H3; unfold fst in H3.
        rewrite withspacer_spacer, sizeof_Tunion.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
        simpl.
        pattern (co_sizeof (get_co id)) at 2;
        replace (co_sizeof (get_co id)) with (sizeof (field_type i (co_members (get_co id))) +
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          (co_sizeof (get_co id) - sizeof (field_type i (co_members (get_co id))))) by omega.
        rewrite sepcon_comm.
        rewrite memory_block_split by (pose_field; omega).
        apply sepcon_derives; [| rewrite spacer_memory_block by (simpl; auto);
                                 unfold offset_val; solve_mod_modulus; auto ].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        rewrite <- memory_block_data_at_rec_default_val; auto.
        { 
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
          rewrite Forall_forall in IH.
          specialize (IH (i, (field_type i (co_members (get_co id))))).
          spec IH; [apply in_members_field_type; auto |].
          unfold snd in IH.
          apply IH.
          + apply complete_legal_cosu_type_field_type; auto.
          + pose_field; omega.
          + eapply align_compatible_rec_Tunion_inv'; eauto.
        } {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          apply complete_legal_cosu_type_field_type; auto.
        } {
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          pose_field; omega.
        } {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          eapply align_compatible_rec_Tunion_inv'; eauto.
        }
        apply derives_refl.
      * rewrite sizeof_Tunion.
        rewrite memory_block_union_pred by (apply get_co_members_nil_sizeof_0).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        auto.
Qed.

Definition value_fits: forall t, reptype t -> Prop :=
  type_func (fun t => reptype t -> Prop)
    (fun t v =>
       if type_is_volatile t then True else tc_val' t (repinject t v))
    (fun t n a P v => Zlength (unfold_reptype v) =  Z.max 0 n /\ Forall P (unfold_reptype v))
    (fun id a P v => struct_value_fits_aux (co_members (get_co id)) (co_members (get_co id)) P (unfold_reptype v))
    (fun id a P v => union_value_fits_aux (co_members (get_co id)) (co_members (get_co id)) P (unfold_reptype v)).

Lemma value_fits_eq:
  forall t v,
  value_fits t v =
  match t as t0 return (reptype t0 -> Prop)  with
  | Tarray t' n a => fun v0 : reptype (Tarray t' n a) =>
    (fun v1 : list (reptype t') =>
     Zlength v1 = Z.max 0 n /\ Forall (value_fits t') v1)
      (unfold_reptype v0)
| Tstruct i a =>
    fun v0 : reptype (Tstruct i a) =>
     struct_Prop (co_members (get_co i))
       (fun it : ident * type =>
        value_fits (field_type (fst it) (co_members (get_co i)))) (unfold_reptype v0)
| Tunion i a =>
    fun v0 : reptype (Tunion i a) =>
     union_Prop (co_members (get_co i))
       (fun it : ident * type =>
        value_fits (field_type (fst it) (co_members (get_co i)))) (unfold_reptype v0)
  | t0 => fun v0: reptype t0 =>
             (if type_is_volatile t0
              then True
              else tc_val' t0 (repinject t0 v0))
  end v.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros.
(* Goal: @eq Prop (value_fits t v) (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => let t0 := Tvoid in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tint i s a => let t0 := Tint i s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tlong s a => let t0 := Tlong s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tfloat f a => let t0 := Tfloat f a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tpointer t a => let t0 := Tpointer t a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => (fun v1 : list (@reptype cs t') => and (@eq Z (@Zlength (@reptype cs t') v1) (Z.max Z0 n)) (@Forall (@reptype cs t') (value_fits t') v1)) (@unfold_reptype cs (Tarray t' n a) v0) | Tfunction t t1 c => let t0 := Tfunction t t1 c in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) *)
unfold value_fits.
(* Goal: @eq Prop (@type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) t v) (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => fun v0 : @reptype cs Tvoid => if type_is_volatile Tvoid then True else tc_val' Tvoid (@repinject cs Tvoid v0) | Tint i s a => fun v0 : @reptype cs (Tint i s a) => if type_is_volatile (Tint i s a) then True else tc_val' (Tint i s a) (@repinject cs (Tint i s a) v0) | Tlong s a => fun v0 : @reptype cs (Tlong s a) => if type_is_volatile (Tlong s a) then True else tc_val' (Tlong s a) (@repinject cs (Tlong s a) v0) | Tfloat f a => fun v0 : @reptype cs (Tfloat f a) => if type_is_volatile (Tfloat f a) then True else tc_val' (Tfloat f a) (@repinject cs (Tfloat f a) v0) | Tpointer t a => fun v0 : @reptype cs (Tpointer t a) => if type_is_volatile (Tpointer t a) then True else tc_val' (Tpointer t a) (@repinject cs (Tpointer t a) v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v0)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n0 : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n0 a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n0 a0) v)) (Z.max Z0 n0)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n0 a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) t') (@unfold_reptype cs (Tarray t' n a) v0)) | Tfunction t t1 c => fun v0 : @reptype cs (Tfunction t t1 c) => if type_is_volatile (Tfunction t t1 c) then True else tc_val' (Tfunction t t1 c) (@repinject cs (Tfunction t t1 c) v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a0) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a0 : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a0)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a0) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a0) v))) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a0)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a0) v)) (fun (id : positive) (a0 : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a0)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a0) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) *)
rewrite type_func_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
destruct t; auto.
(* Goal: @eq Prop (@struct_value_fits_aux cs (co_members (@get_co cs i)) (co_members (@get_co cs i)) (@FTI_aux cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) i) (@unfold_reptype cs (Tstruct i a) v)) (@struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v)) *)
(* Goal: @eq Prop (@union_value_fits_aux cs (co_members (@get_co cs i)) (co_members (@get_co cs i)) (@FTI_aux cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) i) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v)) *)
apply struct_value_fits_aux_spec.
(* Goal: @eq Prop (@union_value_fits_aux cs (co_members (@get_co cs i)) (co_members (@get_co cs i)) (@FTI_aux cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) i) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @type_func cs (fun t : type => forall _ : @reptype cs t, Prop) (fun (t : type) (v : @reptype cs t) => if type_is_volatile t then True else tc_val' t (@repinject cs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall _ : @reptype cs t, Prop) (v : @reptype cs (Tarray t n a)) => and (@eq Z (@Zlength (@reptype cs t) (@unfold_reptype cs (Tarray t n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t) P (@unfold_reptype cs (Tarray t n a) v))) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tstruct id a)) => @struct_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @FT_aux cs (fun t : type => forall _ : @reptype cs t, Prop) id) (v : @reptype cs (Tunion id a)) => @union_value_fits_aux cs (co_members (@get_co cs id)) (co_members (@get_co cs id)) P (@unfold_reptype cs (Tunion id a) v)) (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v)) *)
apply union_value_fits_aux_spec.
Qed.

Lemma value_fits_type_changable: forall (t1 t2: type) v1 v2,
  t1 = t2 ->
  JMeq v1 v2 ->
  value_fits t1 v1 = value_fits t2 v2.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
(* Goal: @eq Prop (value_fits t1 v1) (value_fits t2 v2) *)
  subst t2.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v))) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  apply JMeq_eq in H0.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v))) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  rewrite H0.
(* Goal: @eq Prop (value_fits t1 v2) (value_fits t1 v2) *)
  reflexivity.
Qed.

Lemma default_value_fits:
  forall t, value_fits t (default_val t).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  type_induction t; try destruct f; rewrite value_fits_eq;
  try solve [simpl; try (simple_if_tac; auto); apply tc_val'_Vundef];
  rewrite default_val_eq, unfold_fold_reptype.
  + (* Tarray *)
(* Goal: and (@eq Z (@Zlength (@reptype cs t) (@list_repeat (@reptype cs t) (Z.to_nat z) (@default_val cs t))) (Z.max Z0 z)) (@Forall (@reptype cs t) (value_fits t) (@list_repeat (@reptype cs t) (Z.to_nat z) (@default_val cs t))) *)
    split.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - rewrite Zlength_list_repeat', Z2Nat_id'; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - apply Forall_list_repeat; auto.
  + (* Tstruct *)
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: @struct_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@struct_default_val cs (co_members (@get_co cs id))) *)
    apply struct_Prop_compact_prod_gen.
    - apply get_co_members_no_replicate.
    - rewrite Forall_forall in IH.
      intros; apply IH.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply in_members_field_type; auto.
  + (* Tunion *)
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    apply union_Prop_compact_sum_gen.
    - apply get_co_members_no_replicate.
    - rewrite Forall_forall in IH.
      intros; apply IH.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply in_members_field_type; auto.
Qed.

Lemma data_at_rec_value_fits: forall sh t v p,
  data_at_rec sh t v p |-- !! value_fits t v.
Proof.
  intros until p.
  revert v p; type_induction t; intros;
  rewrite value_fits_eq, data_at_rec_eq;
  try solve [normalize];
  try solve [cbv zeta; simple_if_tac; [normalize | apply mapsto_tc_val']].
  + (* Tarray *)
    eapply derives_trans; [apply array_pred_local_facts |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
      unfold at_offset.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
      instantiate (1 := fun x => value_fits t x); simpl.
      apply IH.
    - apply prop_derives.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      intros [? ?]; split; auto.
      rewrite Zlength_correct in *.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      omega.
  + (* Tstruct *)
    apply struct_pred_local_facts; [apply get_co_members_no_replicate |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    rewrite withspacer_spacer.
    unfold at_offset.
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
    rewrite Forall_forall in IH.
    specialize (IH (i, (field_type i (co_members (get_co id))))).
    spec IH; [apply in_members_field_type; auto |].
    eapply derives_trans; [apply sepcon_derives; [apply derives_refl | apply IH] |].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite sepcon_comm; apply derives_left_sepcon_right_corable; auto.
  + (* Tunion *)
    apply union_pred_local_facts; [apply get_co_members_no_replicate |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    rewrite withspacer_spacer.
    unfold at_offset.
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
    rewrite Forall_forall in IH.
    specialize (IH (i, (field_type i (co_members (get_co id))))).
    spec IH; [apply in_members_field_type; auto |].
    eapply derives_trans; [apply sepcon_derives; [apply derives_refl | apply IH] |].
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite sepcon_comm; apply derives_left_sepcon_right_corable; auto.
Qed.

Lemma data_at_rec_share_join:
  forall sh1 sh2 sh t v b ofs,
    sepalg.join sh1 sh2 sh ->
   data_at_rec sh1 t v (Vptr b ofs) * data_at_rec sh2 t v (Vptr b ofs) = data_at_rec sh t v (Vptr b ofs).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  revert v ofs; pattern t; type_induction t; intros;
  rewrite !data_at_rec_eq;
    try solve [simple_if_tac;
        [ apply memory_block_share_join; auto
        | apply mapsto_share_join; auto]];
    try solve [normalize].
  + (* Tarray *)
    rewrite array_pred_sepcon.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    apply array_pred_ext; auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
    unfold at_offset; simpl.
    apply IH.
  + (* Tstruct *)
    rewrite struct_pred_sepcon.
    apply struct_pred_ext; [apply get_co_members_no_replicate |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
Opaque field_type field_offset.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
    simpl.
Transparent field_type field_offset.
    rewrite !withspacer_spacer.
    rewrite !spacer_memory_block by (simpl; auto).
    rewrite !sepcon_assoc, (sepcon_comm (at_offset _ _ _)), <- !sepcon_assoc.
    erewrite memory_block_share_join by eassumption.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
    rewrite sepcon_assoc; f_equal.
    unfold at_offset.
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
    rewrite Forall_forall in IH.
    pose proof H0.
    apply in_members_field_type in H0.
    rewrite sepcon_comm.
    etransitivity; [apply (IH (i, field_type i (co_members (get_co id))) H0) |].
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
    f_equal.
    apply JMeq_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    apply (@proj_compact_prod_JMeq _ _ _ (fun it => reptype (field_type (fst it) (co_members (get_co id)))) (fun it => reptype (field_type (fst it) (co_members (get_co id))))); auto.
  + rewrite union_pred_sepcon.
    apply union_pred_ext; [apply get_co_members_no_replicate | reflexivity | ].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
Opaque field_type field_offset.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
    simpl.
Transparent field_type field_offset.
    rewrite !withspacer_spacer.
    rewrite !spacer_memory_block by (simpl; auto).
    rewrite !sepcon_assoc, (sepcon_comm (data_at_rec _ _ _ _)), <- !sepcon_assoc.
    erewrite memory_block_share_join by eassumption.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
    rewrite sepcon_assoc; f_equal.
    unfold at_offset.
(* Goal: @union_Prop (co_members (@get_co cs id)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs id)))) (fun it : prod ident type => value_fits (field_type (@fst ident type it) (co_members (@get_co cs id)))) (@union_default_val cs (co_members (@get_co cs id))) *)
    cbv zeta in IH.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
    rewrite Forall_forall in IH.
    apply compact_sum_inj_in in H1.
    rewrite sepcon_comm.
    etransitivity; [apply (IH (i, field_type i (co_members (get_co id))) H1) |].
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
    f_equal.
    apply JMeq_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    apply (@proj_compact_sum_JMeq _ _ _ (fun it => reptype (field_type (fst it) (co_members (get_co id)))) (fun it => reptype (field_type (fst it) (co_members (get_co id))))); auto.
Qed.

Lemma nonreadable_memory_block_data_at_rec:
  forall sh t v b ofs
  (LEGAL_COSU: complete_legal_cosu_type t = true),
  0 <= ofs /\ ofs + sizeof t < Ptrofs.modulus ->
  align_compatible_rec cenv_cs t ofs ->
  ~ readable_share sh ->
  value_fits t v ->
  memory_block sh (sizeof t) (Vptr b (Ptrofs.repr ofs)) = data_at_rec sh t v (Vptr b (Ptrofs.repr ofs)).
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  symmetry.
  revert v ofs LEGAL_COSU H H0 H1 H2;
  pattern t; type_induction t; (* try destruct i; try destruct s; *) intros;
    try inversion LEGAL_COSU;
    rewrite value_fits_eq in H2; cbv beta zeta in H2;
    try match type of H2 with
        | context [type_is_volatile ?t] =>
            destruct (type_is_volatile t) eqn:?;
             [apply by_value_data_at_rec_volatile | apply by_value_data_at_rec_nonreachable2]; auto
        end;
    rewrite !data_at_rec_eq.
  + simpl in H, H0.
    rewrite array_pred_ext with
     (P1 := fun i _ p => memory_block sh (sizeof t)
                          (offset_val (sizeof t * i) p))
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
     (v1 := list_repeat (Z.to_nat (Z.max 0 z)) (default_val t)); auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite memory_block_array_pred; auto.
    - apply Z.le_max_l.
    - rewrite (proj1 H2).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      symmetry; apply Zlength_list_repeat; auto.
      apply Z.le_max_l.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
      rewrite at_offset_eq3.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
      unfold offset_val; solve_mod_modulus.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      unfold Znth. rewrite if_false by omega.
      rewrite Z.sub_0_r.
      assert (value_fits t (nth (Z.to_nat i) (unfold_reptype v) (default_val t))).
      {
        destruct H2.
        rewrite Forall_forall in H5.
        apply H5.
        apply nth_In.
        apply Nat2Z.inj_lt.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        rewrite <- Zlength_correct, H2, Z2Nat.id by omega.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        omega.
      }
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply IH; auto.
      * pose_size_mult cenv_cs t (0 :: i :: i + 1 :: Z.max 0 z :: nil); omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * eapply align_compatible_rec_Tarray_inv; eauto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        apply range_max0; auto.
  + rewrite struct_pred_ext with
     (P1 := fun it _ p =>
              memory_block sh
               (field_offset_next cenv_cs (fst it) (co_members (get_co id)) (co_sizeof (get_co id)) -
                  field_offset cenv_cs (fst it) (co_members (get_co id)))
               (offset_val (field_offset cenv_cs (fst it) (co_members (get_co id))) p))
     (v1 := (struct_default_val (co_members (get_co id))));
    [| apply get_co_members_no_replicate |].
    - rewrite memory_block_struct_pred.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * rewrite sizeof_Tstruct; auto.
      * apply get_co_members_nil_sizeof_0.
      * apply get_co_members_no_replicate.
      * rewrite sizeof_Tstruct in H.
        pose proof co_consistent_sizeof cenv_cs (get_co id) (get_co_consistent id).
        erewrite complete_legal_cosu_type_Tstruct in H3 by exact LEGAL_COSU.
        unfold sizeof_composite in H3.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        revert H3; pose_align_le; intros; omega.
      * rewrite sizeof_Tstruct in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
      pose proof get_co_members_no_replicate id as NO_REPLI.
      rewrite withspacer_spacer.
      simpl @fst.
      rewrite spacer_memory_block by (simpl; auto).
      rewrite at_offset_eq3.
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
      unfold offset_val; solve_mod_modulus.
      unfold struct_default_val.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
      rewrite Forall_forall in IH.
      specialize (IH (i, field_type i (co_members (get_co id)))).
      spec IH; [apply in_members_field_type; auto |].
      unfold snd in IH.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply struct_Prop_proj with (i := i) (d:= d0) in H2; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      rewrite IH; auto.
      * rewrite Z.add_assoc, sepcon_comm, <- memory_block_split by (pose_field; omega).
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
        f_equal; omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * apply complete_legal_cosu_type_field_type; auto.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
      * simpl fst. pose_field; omega.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      * eapply align_compatible_rec_Tstruct_inv'; eauto.
  + assert (co_members (get_co id) = nil \/ co_members (get_co id) <> nil)
      by (clear; destruct (co_members (get_co id)); [left | right]; congruence).
    destruct H3.
    - rewrite sizeof_Tunion.
      rewrite (get_co_members_nil_sizeof_0 _ H3).
      forget (unfold_reptype v) as v'; simpl in v'.
      generalize (unfold_reptype (default_val (Tunion id a)));
      clear H2; revert v'; rewrite H3 in *;
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      intros.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
      simpl.
      rewrite memory_block_zero.
      normalize.
    - rewrite union_pred_ext with
       (P1 := fun it _ => memory_block sh (co_sizeof (get_co id)))
       (v1 := (unfold_reptype v));
      [| apply get_co_members_no_replicate | reflexivity |].
      * rewrite memory_block_union_pred by (apply get_co_members_nil_sizeof_0).
        rewrite sizeof_Tunion.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      * intros.
        pose proof get_co_members_no_replicate id as NO_REPLI.
        pose proof @compact_sum_inj_in _ _ (co_members (get_co id)) _ _ _ H6.
        apply in_map with (f := fst) in H7; unfold fst in H7.
        rewrite withspacer_spacer.
        simpl @fst.
        rewrite spacer_memory_block by (simpl; auto).
(* Goal: align_compatible_rec (@cenv_cs cs) t (Ptrofs.unsigned (Ptrofs.repr ofs)) *)
        unfold offset_val; solve_mod_modulus.
(* Goal: forall (i : ident) (_ : in_members i (co_members (@get_co cs id))), value_fits (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id))) (@default_val cs (field_type (@fst ident type (@pair ident type i (field_type i (co_members (@get_co cs id))))) (co_members (@get_co cs id)))) *)
        rewrite Forall_forall in IH.
        specialize (IH (i, field_type i (co_members (get_co id)))).
        spec IH; [apply in_members_field_type; auto |].
        unfold snd in IH.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        apply union_Prop_proj with (i := i) (d := d0) in H2; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        rewrite IH; auto.
        { rewrite sepcon_comm, <- memory_block_split by (pose_field; omega).
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          f_equal; f_equal; omega.
        } {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          apply complete_legal_cosu_type_field_type; auto.
        } {
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
          simpl fst; pose_field; omega.
        } {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
          eapply align_compatible_rec_Tunion_inv'; eauto.
        }
Qed.

(*
Lemma f_equal_Int_repr:
  forall i j, i=j -> Int.repr i = Int.repr j.
Proof. intros; congruence. Qed.

Lemma sizeof_Tarray:
  forall t (n:Z) a, n >= 0 ->
      sizeof (Tarray t n a) = (sizeof t * n)%Z.
Proof.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
intros; simpl. rewrite Z.max_r; omega.
Qed.

Lemma data_at_Tarray_ext_derives: forall sh t n a v v',
  (forall i, 0 <= i < n ->
     data_at sh t (Znth i v (default_val _)) |-- data_at sh t (Znth i v' (default_val _))) ->
  data_at sh (Tarray t n a) v |-- data_at sh (Tarray t n a) v'.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  unfold data_at.
  simpl; intro p.
  unfold array_at'.
  normalize.
  apply rangespec_ext_derives.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  rewrite !Z.add_0_l.
  rewrite !Z.sub_0_r.
  assert (legal_alignas_type t = true).
  {
    unfold legal_alignas_type in H2.
    simpl in H2.
    rewrite andb_true_iff in H2.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    tauto.
  }
  assert (alignof t | sizeof t * i).
  {
    apply Z.divide_mul_l.
    apply legal_alignas_sizeof_alignof_compat, H5.
  }
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  rewrite !data_at_rec_at_offset with (pos := (sizeof t * i)%Z) by auto.
  rewrite !at_offset_eq by (rewrite <- data_at_rec_offset_zero; reflexivity).
  assert (legal_nested_field (Tarray t n a) (ArraySubsc i :: nil)) by solve_legal_nested_field.
  pose proof size_compatible_nested_field _ (ArraySubsc i :: nil) _ H7 H0.
  unfold nested_field_type2, nested_field_offset2 in H8; simpl in H8.
  pose proof align_compatible_nested_field _ (ArraySubsc i :: nil) _ H7 H2 H1.
  unfold nested_field_type2, nested_field_offset2 in H9; simpl in H9.
  simpl in H8, H9.
  specialize (H i H4 (offset_val (Int.repr (sizeof t * i)) p)).
  unfold data_at in H.
  simpl in H.
  normalize in H.
Qed.

Lemma data_at_Tarray_ext: forall sh t n a v v',
  (forall i, 0 <= i < n ->
    data_at sh t (Znth i v (default_val _)) =
      data_at sh t (Znth i v' (default_val _))) ->
  data_at sh (Tarray t n a) v = data_at sh (Tarray t n a) v'.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  intros.
  apply pred_ext; apply data_at_Tarray_ext_derives; auto;
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
  intros; rewrite H by auto; auto.
Qed.

*)

End CENV.

Lemma data_at_rec_change_composite {cs_from cs_to} {CCE: change_composite_env cs_from cs_to}: forall (sh: Share.t) (t: type) v1 v2,
  JMeq v1 v2 ->
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  @data_at_rec cs_from sh t v1 = @data_at_rec cs_to sh t v2.
Proof.
  intros sh t.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
  type_induction t; intros.
  + rewrite !data_at_rec_eq; auto.
  + rewrite !data_at_rec_eq.
    change val in v1, v2.
    apply JMeq_eq in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    subst; auto.
  + rewrite !data_at_rec_eq.
    change val in v1, v2.
    apply JMeq_eq in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    subst; auto.
  + rewrite !data_at_rec_eq.
    change val in v1, v2.
    apply JMeq_eq in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    subst; auto.
  + rewrite !data_at_rec_eq.
    change val in v1, v2.
    apply JMeq_eq in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    subst; auto.
  + (* Tarray *)
    rewrite !data_at_rec_eq.
    extensionality p.
    assert (JMeq (unfold_reptype v1) (unfold_reptype v2)).
    {
      eapply JMeq_trans; [| eapply JMeq_trans; [exact H |]].
      + apply (unfold_reptype_JMeq (Tarray t z a) v1).
      + apply JMeq_sym, (unfold_reptype_JMeq (Tarray t z a) v2).
    }
    apply array_pred_ext.
    - apply list_func_JMeq; [apply reptype_change_composite; auto | auto].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    - intros.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      rewrite (IH (Znth (i - 0) (unfold_reptype v1)) (Znth (i - 0) (unfold_reptype v2))); auto.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
      * f_equal.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
        f_equal.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        apply sizeof_change_composite; auto.
      *
        pose (Znthx (A: Type) (i: Z) (al: list A) (d: A) := @Znth A d i al).
        change  (@Znth (@reptype cs_from t) (@Inhabitant_reptype cs_from t) (i - 0)
                                     (@unfold_reptype cs_from (Tarray t z a) v1))
       with (Znthx (@reptype cs_from t) (i-0) (@unfold_reptype cs_from (Tarray t z a) v1)(@Inhabitant_reptype cs_from t)).
        change  (@Znth (@reptype cs_to t) (@Inhabitant_reptype cs_to t) (i - 0)
                                     (@unfold_reptype cs_to (Tarray t z a) v2))
       with (Znthx (@reptype cs_to t) (i-0) (@unfold_reptype cs_to (Tarray t z a) v2)(@Inhabitant_reptype cs_to t)).
       change (@Znthx (@reptype cs_from t) (i - 0)) 
     with ((fun X: Type => @Znthx X (i - 0)) (@reptype cs_from t)).
        change (@Znthx (@reptype cs_to t) (i - 0)) 
          with ((fun X: Type => @Znthx X (i - 0)) (@reptype cs_to t)).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply @list_func_JMeq'; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply default_val_change_composite; auto.
  + rewrite !data_at_rec_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    auto.
  + (* Tstruct *)
    rewrite !data_at_rec_eq.
    extensionality p.
    assert (JMeq (unfold_reptype v1) (unfold_reptype v2)).
    {
      eapply JMeq_trans; [| eapply JMeq_trans; [exact H |]].
      + apply (unfold_reptype_JMeq (Tstruct _ _) v1).
      + apply JMeq_sym, (unfold_reptype_JMeq (Tstruct _ _) v2).
    }
    revert H1; clear H.
    forget (unfold_reptype v1) as v1'.
    forget (unfold_reptype v2) as v2'.
    clear v1 v2.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    simpl in v1', v2', H1.
    unfold reptype_structlist in *.
    revert v1' H1.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite co_members_get_co_change_composite in * by auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    pose proof (fun i => field_offset_change_composite _ i H0) as HH0.
    pose proof (fun i => field_offset_next_change_composite _ i H0) as HH1.
    apply members_spec_change_composite in H0.
    apply struct_pred_ext; [apply get_co_members_no_replicate |].
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    f_equal; [f_equal | | f_equal ]; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - apply sizeof_change_composite; auto.
      rewrite Forall_forall in H0.
      apply H0.
      apply in_members_field_type.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      auto.
    - clear HH0 HH1.
      simpl fst in *.
      revert d0 d1 v1' v2' IH H0 H1.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      generalize (co_members (get_co id)) at 1 2 3 5 7 8 9 10 11 12 13 15 17 19 21 23 24 26; intros.
      pose proof in_members_field_type _ _ H.
      rewrite Forall_forall in IH, H0.
      specialize (IH _ H2); pose proof (H0 _ H2).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply IH; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply (@proj_struct_JMeq i (co_members (@get_co cs_to id)) (fun it : ident * type => @reptype cs_from (field_type (@fst ident type it) m)) (fun it : ident * type => @reptype cs_to (field_type (@fst ident type it) m))); auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      * intros. 
        rewrite reptype_change_composite; [reflexivity |].
        apply H0.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        apply in_members_field_type; auto.
      * apply get_co_members_no_replicate.
  + (* Tunion *)
    rewrite !data_at_rec_eq.
    extensionality p.
    assert (JMeq (unfold_reptype v1) (unfold_reptype v2)).
    {
      eapply JMeq_trans; [| eapply JMeq_trans; [exact H |]].
      + apply (unfold_reptype_JMeq (Tunion _ _) v1).
      + apply JMeq_sym, (unfold_reptype_JMeq (Tunion _ _) v2).
    }
    revert H1; clear H.
    forget (unfold_reptype v1) as v1'.
    forget (unfold_reptype v2) as v2'.
    clear v1 v2.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    simpl in v1', v2', H1.
    unfold reptype_structlist in *.
    revert v1' H1.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    rewrite co_members_get_co_change_composite in * by auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
    pose proof (fun i => field_offset_change_composite _ i H0) as HH0.
    pose proof (fun i => field_offset_next_change_composite _ i H0) as HH1.
    pose proof H0 as H0'.
    apply members_spec_change_composite in H0.
    apply union_pred_ext.
(* Goal: @eq bool (members_no_replicate (co_members (@get_co cs id))) true *)
    { apply get_co_members_no_replicate. }
    {
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply members_union_inj_JMeq; auto.
(* Goal: @eq bool (members_no_replicate (co_members (@get_co cs id))) true *)
      2: apply get_co_members_no_replicate.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      intros.
      rewrite reptype_change_composite; [reflexivity |].
      apply in_members_field_type in H.
      rewrite Forall_forall in H0.
      apply (H0 _ H).
    }
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
    intros.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
    f_equal.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
    - apply sizeof_change_composite; auto.
      rewrite Forall_forall in H0.
      apply H0.
      apply in_members_field_type.
      apply compact_sum_inj_in in H.
      apply (in_map fst) in H.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      auto.
    - apply co_sizeof_get_co_change_composite.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      auto.
    - clear HH0 HH1.
      simpl fst in *.
      revert d0 d1 v1' v2' IH H0 H1 H H2.
      unfold reptype_unionlist.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      generalize (co_members (get_co id)) at 1 2 3 5 7 8 9 10 11 12 13 15 17 19 22 25 27 29 30 32; intros.
      apply compact_sum_inj_in in H2.
      apply (in_map fst) in H2.
      apply in_members_field_type in H2.
      rewrite Forall_forall in IH, H0.
      specialize (IH _ H2); pose proof (H0 _ H2).
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply IH; auto.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
      apply (@proj_union_JMeq i (co_members (@get_co cs_to id)) (fun it : ident * type => @reptype cs_from (field_type (@fst ident type it) m)) (fun it : ident * type => @reptype cs_to (field_type (@fst ident type it) m))); auto.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
      * intros.
        rewrite reptype_change_composite; [reflexivity |].
        apply H0.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
        apply in_members_field_type; auto.
      * apply get_co_members_no_replicate.
Qed.

(**** tactics for value_fits  ****)

Lemma value_fits_Tstruct:
  forall {cs: compspecs} t (v: reptype t) i a m v2 r,
  t = Tstruct i a ->
  m = co_members (get_co i)  ->
  JMeq (@unfold_reptype cs t v) v2 ->
  r =struct_Prop m
          (fun it => value_fits (field_type (fst it) m))  v2 ->
  value_fits t v = r.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros.
(* Goal: @eq Prop (@value_fits cs t v) r *)
subst.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
rewrite value_fits_eq; simpl.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
f_equal.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
apply JMeq_eq in H1. auto.
Qed.

Lemma value_fits_Tunion:
  forall {cs: compspecs} t (v: reptype t) i a m v2 r,
  t = Tunion i a ->
  m = co_members (get_co i)  ->
  JMeq (@unfold_reptype cs t v) v2 ->
  r =union_Prop m
          (fun it => value_fits (field_type (fst it) m))  v2 ->
  value_fits t v = r.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros.
(* Goal: @eq Prop (@value_fits cs t v) r *)
subst.
(* Goal: @eq A (@nth A (Z.to_nat n) (@nil A) d) (@default A d) *)
rewrite value_fits_eq; simpl.
(* Goal: @eq Prop (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (@unfold_reptype cs (Tunion i a) v)) (@union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) (fun it : prod ident type => @value_fits cs match Ctypes.field_type (@fst ident type it) (co_members (@get_co cs i)) with | Errors.OK t => t | Errors.Error e => Tvoid end) v2) *)
f_equal.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
apply JMeq_eq in H1. auto.
Qed.

Lemma value_fits_by_value_defined:
  forall {cs: compspecs} t t' v r,
   type_is_by_value t = true ->
   repinject t v <> Vundef  ->
   t = t' ->
   (r = if type_is_volatile t' then True
       else tc_val t' (repinject t v)) ->
   value_fits t v = r.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros. subst t' r.
(* Goal: @eq Prop (@value_fits cs (Tarray t' n a) v) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
rewrite value_fits_eq.
(* Goal: @eq Prop (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => let t0 := Tvoid in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tint i s a => let t0 := Tint i s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tlong s a => let t0 := Tlong s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tfloat f a => let t0 := Tfloat f a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tpointer t a => let t0 := Tpointer t a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v0)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v0)) | Tfunction t t1 c => let t0 := Tfunction t t1 c in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) (if type_is_volatile t then True else tc_val' t (@repinject cs t v)) *)
unfold tc_val'.
destruct t; inv H;
 (simple_if_tac; auto; apply prop_ext; intuition).
Qed.

Lemma value_fits_by_value_Vundef:
  forall {cs: compspecs} t v,
   type_is_by_value t = true ->
   repinject t v = Vundef  ->
   value_fits t v = True.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros.
(* Goal: @eq Prop (@value_fits cs (Tarray t' n a) v) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
rewrite value_fits_eq.
(* Goal: @eq Prop (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => let t0 := Tvoid in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tint i s a => let t0 := Tint i s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tlong s a => let t0 := Tlong s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tfloat f a => let t0 := Tfloat f a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tpointer t a => let t0 := Tpointer t a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v0)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v0)) | Tfunction t t1 c => let t0 := Tfunction t t1 c in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) (if type_is_volatile t then True else tc_val' t (@repinject cs t v)) *)
unfold tc_val'.
destruct t; inv H;
 (simple_if_tac; auto; auto; apply prop_ext; intuition).
Qed.

Lemma value_fits_by_value:
  forall {cs: compspecs} t t' v r,
   type_is_by_value t = true ->
   t = t' ->
   (r = if type_is_volatile t then True
       else tc_val' t' (repinject t v)) ->
   value_fits t v = r.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros. subst r t'.
(* Goal: @eq Prop (@value_fits cs (Tarray t' n a) v) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
rewrite value_fits_eq.
(* Goal: @eq Prop (match t as t0 return (forall _ : @reptype cs t0, Prop) with | Tvoid => let t0 := Tvoid in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tint i s a => let t0 := Tint i s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tlong s a => let t0 := Tlong s a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tfloat f a => let t0 := Tfloat f a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tpointer t a => let t0 := Tpointer t a in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tarray t' n a => fun v0 : @reptype cs (Tarray t' n a) => and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v0)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v0)) | Tfunction t t1 c => let t0 := Tfunction t t1 c in fun v0 : @reptype cs t0 => if type_is_volatile t0 then True else tc_val' t0 (@repinject cs t0 v0) | Tstruct i a => fun v0 : @reptype cs (Tstruct i a) => @struct_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tstruct i a) v0) | Tunion i a => fun v0 : @reptype cs (Tunion i a) => @union_Prop (co_members (@get_co cs i)) (fun it : prod ident type => @reptype cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (fun it : prod ident type => @value_fits cs (field_type (@fst ident type it) (co_members (@get_co cs i)))) (@unfold_reptype cs (Tunion i a) v0) end v) (if type_is_volatile t then True else tc_val' t (@repinject cs t v)) *)
unfold tc_val'.
destruct t; inv H;
 (simple_if_tac; auto; apply prop_ext; intuition).
Qed.

Lemma value_fits_Tarray:
  forall {cs: compspecs} t (v: reptype t) t' n a
    (v' : list (reptype t')) r,
  t = (Tarray t' n a) ->
  JMeq (unfold_reptype v) v' ->
  n >= 0 ->
  r = (Zlength v' = n /\ Forall (value_fits t') v') ->
  value_fits t v =r.
Proof.
(* Goal: forall (cs : compspecs) (t : type) (v : @reptype cs t) (t' : type) (n : Z) (a : attr) (v' : list (@reptype cs t')) (r : Prop) (_ : @eq type t (Tarray t' n a)) (_ : @JMeq match t with | Tvoid => unit | Tint i s a0 => val | Tlong s a0 => val | Tfloat f a0 => val | Tpointer t0 a0 => val | Tarray t0 z a0 => list (@reptype cs t0) | Tfunction t0 t1 c => unit | Tstruct id a0 => @reptype_structlist cs (co_members (@get_co cs id)) | Tunion id a0 => @reptype_unionlist cs (co_members (@get_co cs id)) end (@unfold_reptype cs t v) (list (@reptype cs t')) v') (_ : Z.ge n Z0) (_ : @eq Prop r (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v'))), @eq Prop (@value_fits cs t v) r *)
intros.
(* Goal: @eq Prop (@value_fits cs t v) r *)
subst. rewrite value_fits_eq.
(* Goal: @eq Prop (and (@eq Z (@Zlength (@reptype cs t') (@unfold_reptype cs (Tarray t' n a) v)) (Z.max Z0 n)) (@Forall (@reptype cs t') (@value_fits cs t') (@unfold_reptype cs (Tarray t' n a) v))) (and (@eq Z (@Zlength (@reptype cs t') v') n) (@Forall (@reptype cs t') (@value_fits cs t') v')) *)
apply JMeq_eq in H0. rewrite H0.
(* Goal: iff (and (Z.le Z0 x) (Z.lt x z)) (and (Z.le Z0 x) (Z.lt x z)) *)
rewrite Z.max_r by omega. auto.
Qed.

Ltac cleanup_unfold_reptype :=
    match goal with |- JMeq (unfold_reptype ?A) _ =>
                 instantiate (1:=A); apply JMeq_refl
    end.

Ltac simplify_value_fits' :=
first
 [erewrite value_fits_Tstruct;
    [ | reflexivity
    | simpl; reflexivity
    | cleanup_unfold_reptype
    | simpl; reflexivity]
 |erewrite value_fits_Tarray;
    [ | reflexivity
    | cleanup_unfold_reptype
    | repeat subst_any; try computable; omega
    | simpl; reflexivity
    ]
 | erewrite value_fits_by_value_defined;
   [ | reflexivity
   | repeat subst_any; clear; simpl; intro; discriminate
   | simpl; lazy beta iota zeta delta [field_type]; simpl; reflexivity
   | simpl; reflexivity
   ]
 | rewrite value_fits_by_value_Vundef;
   [ | reflexivity | reflexivity
   ]
 | erewrite value_fits_by_value;
   [ | reflexivity
   | simpl; lazy beta iota zeta delta [field_type]; simpl; reflexivity
   | simpl; reflexivity
   ]
 ];
 cbv beta;
 repeat match goal with |- context [@reptype ?cs ?t] =>
   change (@reptype cs t) with val
 end.

Tactic Notation "simplify_value_fits" :=
  simplify_value_fits'.

Tactic Notation "simplify_value_fits" "in" hyp(H) :=
  match type of H with ?A =>
  let a := fresh "a" in set (a:=A) in H;
   let H1 := fresh in assert (H1: a = A) by (apply eq_refl);
   clearbody a;
   match goal with |- ?B =>
    let BB := fresh "BB" in set (BB:=B);
   revert H1; simplify_value_fits'; intro H1; subst a; subst BB
  end
 end.

Tactic Notation "simplify_value_fits" "in" "*" :=
repeat match goal with
 | H: context [value_fits _ _ _] |- _ =>
  simplify_value_fits in H
end;
 repeat simplify_value_fits'.

(*** end tactics for value_fits ***)