(* TODO: remove this file *)
Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.nested_field_lemmas.
Require Import VST.floyd.mapsto_memory_block.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.proj_reptype_lemmas.
Require Import VST.floyd.data_at_rec_lemmas.
Require Import VST.floyd.field_at.
Require Import VST.floyd.entailer.
Require Import VST.floyd.closed_lemmas.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import VST.floyd.sublist.

Local Open Scope logic.

Section STRONGER.

Context {cs: compspecs}.

(* Goal: Z.le (Z.add (Z.mul (@sizeof (@cenv_cs cs) t0) i) (@sizeof (@cenv_cs cs) t0)) (Z.mul (@sizeof (@cenv_cs cs) t0) n) *)
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
Definition stronger {t: type} (v v': reptype t) : Prop :=
  forall sh, data_at sh t v |-- data_at sh t v'.

Definition data_equal {t} v1 v2 := forall sh, data_at sh t v1 = data_at sh t v2.

Notation "X '>>>' Y" := (stronger X Y) (at level 60, no associativity).
Notation "X '===' Y" := (data_equal X Y) (at level 60, no associativity).

Lemma stronger_refl: forall t (v: reptype t), v >>> v.
Proof.
(* Goal: forall (t : type) (v : @reptype cs t), @stronger t v v *)
  intros t v sh p.
(* Goal: @data_equal t2 v0 v1 *)
  auto.
Qed.

Lemma stronger_JMeq:
  forall t t' a a' b b',
    t=t' ->
    @JMeq (reptype t) a (reptype t') a' ->
    @JMeq (reptype t) b (reptype t') b' ->
    a >>> b -> a' >>> b'.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
intros. subst t'.
(* Goal: @data_equal t a' b' *)
apply JMeq_eq in H0. apply JMeq_eq in H1.
(* Goal: @data_equal t2 v0 v1 *)
subst; auto.
Qed.

(* Goal: Z.le (Z.add (Z.mul (@sizeof (@cenv_cs cs) t0) i) (@sizeof (@cenv_cs cs) t0)) (Z.mul (@sizeof (@cenv_cs cs) t0) n) *)
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
Lemma eq_rect_r_stronger: forall {t1 t2} v0 v1 (H: t1 = t2),
  v0 >>> v1 ->
  eq_rect_r reptype v0 H >>> eq_rect_r reptype v1 H.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t1 (@eq_rect_r type t2 (@reptype cs) v0 t1 H) (@eq_rect_r type t2 (@reptype cs) v1 t1 H) *)
  generalize H.
(* Goal: @data_equal t v v' *)
  subst.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t2 (@eq_rect_r type t2 (@reptype cs) v0 t2 H) (@eq_rect_r type t2 (@reptype cs) v1 t2 H) *)
  unfold eq_rect_r.
(* Goal: @data_equal t2 (@eq_rect type t2 (fun y : type => @reptype cs y) v0 t2 (@eq_sym type t2 t2 H)) (@eq_rect type t2 (fun y : type => @reptype cs y) v1 t2 (@eq_sym type t2 t2 H)) *)
  rewrite <- !eq_rect_eq.
(* Goal: @data_equal t2 v0 v1 *)
  auto.
Qed.
(*
Lemma stronger_data_at_rec_derives: forall sh t v0 v1 pos p,
  legal_alignas_type t = true ->
  (alignof t | pos) ->
  v0 >>> v1 ->
  field_compatible t nil (offset_val (Int.repr pos) p) ->
  data_at_rec sh type_id_env.empty_ti t pos v0 p |--
    data_at_rec sh type_id_env.empty_ti t pos v1 p.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  specialize (H1 sh (offset_val (Int.repr pos) p)).
  unfold data_at in H1.
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0)) *)
  simpl in H1.
  unfold field_compatible in H2.
  destruct H2 as [? [? [? [? [? ?]]]]].
  normalize in H1.
(* Goal: @data_equal t2 v0 v1 *)
  rewrite !data_at_rec_at_offset' with (pos := pos) by auto.
  rewrite !at_offset'_eq by (rewrite <- data_at_rec_offset_zero; reflexivity).
  exact H1.
Qed.
*)
(*
Lemma stronger_data_at_rec_nested_field_derives: forall sh t gfs t0 v0 v1 p,
  legal_alignas_type t = true ->
  nested_field_type2 t gfs = t0 ->
  legal_nested_field t gfs ->
  v0 >>> v1 ->
  size_compatible t p ->
  align_compatible t p ->
  data_at_rec sh type_id_env.empty_ti t0 (nested_field_offset2 t gfs) v0 p |--
    data_at_rec sh type_id_env.empty_ti t0 (nested_field_offset2 t gfs) v1 p.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t2 v0 v1 *)
  apply stronger_data_at_rec_derives; auto.
  + rewrite <- H0.
(* Goal: @data_equal t2 v0 v1 *)
    apply nested_field_type2_nest_pred; auto.
  + rewrite <- H0.
(* Goal: @data_equal t2 v0 v1 *)
    apply nested_field_offset2_type2_divide; auto.
  + rewrite <- H0.
(* Goal: @data_equal t2 v0 v1 *)
    apply size_compatible_nested_field; auto.
  + rewrite <- H0.
(* Goal: @data_equal t2 v0 v1 *)
    apply align_compatible_nested_field; auto.
Qed.
*)

Lemma stronger_trans: forall t (v0 v1 v2: reptype t),
  v0 >>> v1 -> v1 >>> v2 -> v0 >>> v2.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  intro sh.
  eapply derives_trans.
(* Goal: @derives mpred Nveric (@data_at cs sh (@nested_field_type cs t gfs) v0 (@field_address cs t gfs p)) (@data_at cs sh (@nested_field_type cs t gfs) v1 (@field_address cs t gfs p)) *)
  apply H.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  apply H0.
Qed.

Lemma field_at_stronger: forall sh t gfs v0 v1,
  v0 >>> v1 ->
  field_at sh t gfs v0 |-- field_at sh t gfs v1.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @derives (forall _ : val, mpred) (@LiftNatDed val mpred Nveric) (@field_at cs sh t gfs v0) (@field_at cs sh t gfs v1) *)
  intros p.
(* Goal: @derives mpred Nveric (@field_at cs sh t gfs v0 p) (@field_at cs sh t gfs v1 p) *)
  rewrite !field_at_data_at by exact H.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
  simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) *)
  normalize.
(* Goal: @derives mpred Nveric (@data_at cs sh (@nested_field_type cs t gfs) v0 (@field_address cs t gfs p)) (@data_at cs sh (@nested_field_type cs t gfs) v1 (@field_address cs t gfs p)) *)
  apply H.
Qed.

Lemma stronger_array_ext: forall t0 n a (v0 v1: reptype (Tarray t0 n a)),
 Zlength (unfold_reptype v0) = Zlength (unfold_reptype v1) ->
  (forall i, 0 <= i < n -> Znth i (unfold_reptype v0)  >>> Znth i (unfold_reptype v1)) ->
  v0 >>> v1.
Proof.
(* Goal: forall (t0 : type) (n : Z) (a : attr) (v0 v1 : @reptype cs (Tarray t0 n a)) (_ : @eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1))) (_ : forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1))), @stronger (Tarray t0 n a) v0 v1 *)
  intros; intros sh p.
(* Goal: @derives mpred Nveric (@data_at cs sh t v p) (@data_at cs sh t (@default_val cs t) p) *)
  unfold data_at.
(* Goal: @derives mpred Nveric (@field_at cs sh (Tarray t0 n a) (@nil gfield) v0 p) (@field_at cs sh (Tarray t0 n a) (@nil gfield) v1 p) *)
  destruct (zle n 0).
*
(* Goal: @derives mpred Nveric (@field_at cs sh (Tarray t0 n a) (@nil gfield) v0 p) (@field_at cs sh (Tarray t0 n a) (@nil gfield) v1 p) *)
  unfold field_at.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible cs (Tarray t0 n a) (@nil gfield) p)) (at_offset (@data_at_rec cs sh (@nested_field_type cs (Tarray t0 n a) (@nil gfield)) v0) (@nested_field_offset cs (Tarray t0 n a) (@nil gfield)) p)) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible cs (Tarray t0 n a) (@nil gfield) p)) (at_offset (@data_at_rec cs sh (@nested_field_type cs (Tarray t0 n a) (@nil gfield)) v1) (@nested_field_offset cs (Tarray t0 n a) (@nil gfield)) p)) *)
  entailer.
(* Goal: @derives mpred Nveric (at_offset (@data_at_rec cs sh (@nested_field_type cs (Tarray t0 n a) (@nil gfield)) v0) (@nested_field_offset cs (Tarray t0 n a) (@nil gfield)) p) (at_offset (@data_at_rec cs sh (@nested_field_type cs (Tarray t0 n a) (@nil gfield)) v1) (@nested_field_offset cs (Tarray t0 n a) (@nil gfield)) p) *)
  apply derives_refl'.
(* Goal: @eq mpred (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) Z0)) (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) Z0)) *)
  f_equal.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
  unfold nested_field_type; simpl.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh (Tarray t0 n a) v0 (offset_val Z0 p)) (@data_at_rec cs sh (Tarray t0 n a) v1 (offset_val Z0 p)) *)
  rewrite !data_at_rec_eq.
(* Goal: @eq (forall _ : val, mpred) (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v0)) (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v1)) *)
  rewrite Z.max_l by omega.
(* Goal: @derives mpred Nveric (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v0) (offset_val Z0 p)) (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v1) (offset_val Z0 p)) *)
  unfold aggregate_pred.aggregate_pred.array_pred.
(* Goal: @derives mpred Nveric (@aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v0) (offset_val Z0 p)) (@aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v1) (offset_val Z0 p)) *)
  unfold aggregate_pred.array_pred.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
  simpl.
(* Goal: @eq (forall _ : val, mpred) (fun _ : val => @andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) Z0)) (@emp mpred Nveric Sveric)) (fun _ : val => @andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) Z0)) (@emp mpred Nveric Sveric)) *)
  extensionality Vundef.
(* Goal: @eq mpred (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) Z0)) (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) Z0)) *)
  f_equal. f_equal.
(* Goal: @eq Prop (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) Z0) (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) Z0) *)
  change (unfold_reptype v0) with v0.
(* Goal: @eq Prop (@eq Z (@Zlength (@reptype cs t0) v0) Z0) (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) Z0) *)
  change (unfold_reptype v1) with v1.
(* Goal: @data_equal t2 v0 v1 *)
  rewrite H. auto.
*
(* Goal: @derives mpred Nveric (@field_at cs sh (Tarray t0 n a) (@nil gfield) v0 p) (@field_at cs sh (Tarray t0 n a) (@nil gfield) v1 p) *)
  assert_PROP (Zlength (unfold_reptype v0) = n). {
(* Goal: @data_equal t2 v0 v1 *)
     entailer!. destruct H2 as [? _]. rewrite Z.max_r in H2 by omega. auto.
  }
(* Goal: @derives mpred Nveric (@field_at cs sh (Tarray t0 n a) (@nil gfield) v0 p) (@field_at cs sh (Tarray t0 n a) (@nil gfield) v1 p) *)
  rewrite H1 in H. symmetry in H.
(* Goal: @derives mpred Nveric (@field_at cs sh (Tarray t0 n a) (@nil gfield) v0 p) (@field_at cs sh (Tarray t0 n a) (@nil gfield) v1 p) *)
  unfold field_at.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) *)
  normalize.
(* Goal: @derives mpred Nveric (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
  unfold at_offset.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
  unfold nested_field_offset, nested_field_type;   simpl.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh (Tarray t0 n a) v0 (offset_val Z0 p)) (@data_at_rec cs sh (Tarray t0 n a) v1 (offset_val Z0 p)) *)
  rewrite !data_at_rec_eq.
(* Goal: @derives mpred Nveric (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v0) (offset_val Z0 p)) (@aggregate_pred.aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v1) (offset_val Z0 p)) *)
  unfold aggregate_pred.aggregate_pred.array_pred.
(* Goal: @derives mpred Nveric (@aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v0) (offset_val Z0 p)) (@aggregate_pred.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 cs sh t0 v) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@unfold_reptype cs (Tarray t0 n a) v1) (offset_val Z0 p)) *)
  unfold aggregate_pred.array_pred.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) (Z.sub (Z.max Z0 n) Z0))) (aggregate_pred.rangespec Z0 (Z.to_nat (Z.sub (Z.max Z0 n) Z0)) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) (Z.sub (Z.max Z0 n) Z0))) (aggregate_pred.rangespec Z0 (Z.to_nat (Z.sub (Z.max Z0 n) Z0)) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) *)
  rewrite Z.max_r by omega. rewrite Z.sub_0_r.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) *)
  normalize.
(* Goal: @derives mpred Nveric (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) p) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) p) *)
  apply aggregate_pred.rangespec_ext_derives.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @derives mpred Nveric (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
  unfold at_offset.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  rewrite Z.sub_0_r.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  rewrite Z2Nat.id in H3 by omega. rewrite Z.add_0_l in H3.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  specialize (H0 _ H3 sh).
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  unfold data_at, field_at in H0.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  simpl in H0.
  specialize (H0 (offset_val (sizeof t0 * i) p)).
  assert (field_compatible t0 nil (offset_val (sizeof t0 * i) p)). {
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
   destruct (zle (sizeof t0) 0).
  - assert (sizeof t0 = 0) by (pose proof (sizeof_pos t0); omega).
(* Goal: Z.lt (Z.add (Ptrofs.unsigned (Ptrofs.add i0 (Ptrofs.repr Z0))) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
(* Goal: @align_compatible cs t0 (offset_val Z0 (Vptr b i0)) *)
     rewrite H4. rewrite Z.mul_0_l.
     clear - H2 H4 H3.
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
    destruct H2 as [? [? [? [? ?]]]].
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
    destruct p; try contradiction.
(* Goal: @data_equal t2 v0 v1 *)
    split3; [ | | split3]; auto.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
    red. simpl. rewrite H4. rewrite Z.add_0_r.
(* Goal: Z.lt (Ptrofs.unsigned (Ptrofs.add i0 (Ptrofs.repr Z0))) Ptrofs.modulus *)
(* Goal: @align_compatible cs t0 (offset_val Z0 (Vptr b i0)) *)
    red in H1. simpl in H1. rewrite H4 in H1. rewrite Z.mul_0_l in H1.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Ptrofs.unsigned (Ptrofs.add i0 (Ptrofs.repr Z0))) *)
    rewrite Ptrofs.add_zero. omega.
(* Goal: @data_equal t2 v0 v1 *)
   red in H2|-*. apply align_compatible_rec_Tarray_inv with (i:=i) in H2; auto.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
   rewrite H4 in H2. rewrite Z.mul_0_l, Z.add_0_r in H2. simpl.
(* Goal: @data_equal t2 v0 v1 *)
    rewrite Ptrofs.add_zero. auto.
   -
    clear - H2 H3 g0.
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
    destruct H2 as [? [? [? [? ?]]]].
    assert (H5: 0 <= sizeof t0 * i < sizeof t0 * n). {
      replace 0 with (sizeof t0 * 0)%Z by (rewrite Z.mul_0_r; auto).
(* Goal: and (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) Z0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (Z.lt (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Z.mul (@sizeof (@cenv_cs cs) t0) n)) *)
      pose proof (sizeof_pos t0).
(* Goal: and (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) Z0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (Z.lt (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Z.mul (@sizeof (@cenv_cs cs) t0) n)) *)
      split.
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
      apply Zmult_le_compat_l; omega.
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
      apply Zmult_lt_compat_l; omega.
    }
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
    hnf in H1. destruct p; try contradiction.
(* Goal: @field_compatible cs t0 (@nil gfield) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0)) *)
    simpl in H1. rewrite Z.max_r in H1 by omega.
(* Goal: @data_equal t2 v0 v1 *)
    split3; [ | | split3]; auto.
   +
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
    red. simpl.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Ptrofs.unsigned (Ptrofs.add i0 (Ptrofs.repr (Z.mul (@sizeof (@cenv_cs cs) t0) i)))) *)
    rewrite Ptrofs.add_unsigned.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Ptrofs.unsigned (Ptrofs.repr (Z.add (Ptrofs.unsigned i0) (Ptrofs.unsigned (Ptrofs.repr (Z.mul (@sizeof (@cenv_cs cs) t0) i)))))) *)
    pose proof (Ptrofs.unsigned_range i0).
    rewrite (Ptrofs.unsigned_repr (_*_))
      by (change (Ptrofs.max_unsigned) with (Ptrofs.modulus - 1); omega).
    rewrite (Ptrofs.unsigned_repr)
      by (change (Ptrofs.max_unsigned) with (Ptrofs.modulus - 1); omega).
    assert (sizeof t0 * i + sizeof t0 <= sizeof t0 * n). {
       rewrite <- (Z.mul_1_r (sizeof t0)) at 2.
       rewrite <- Z.mul_add_distr_l.
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
      apply Zmult_le_compat_l; omega.
    }
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
    omega.
    +
(* Goal: @data_equal t2 v0 v1 *)
     red in H2. apply align_compatible_rec_Tarray_inv with (i:=i) in H2; auto.
(* Goal: @align_compatible cs t0 (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0)) *)
     unfold offset_val. 
(* Goal: @align_compatible cs t0 (Vptr b (Ptrofs.add i0 (Ptrofs.repr (Z.mul (@sizeof (@cenv_cs cs) t0) i)))) *)
     red.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Ptrofs.unsigned (Ptrofs.add i0 (Ptrofs.repr (Z.mul (@sizeof (@cenv_cs cs) t0) i)))) *)
     rewrite Ptrofs.add_unsigned.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Ptrofs.unsigned (Ptrofs.repr (Z.add (Ptrofs.unsigned i0) (Ptrofs.unsigned (Ptrofs.repr (Z.mul (@sizeof (@cenv_cs cs) t0) i)))))) *)
    pose proof (Ptrofs.unsigned_range i0).
    rewrite (Ptrofs.unsigned_repr (_*_))
      by (change (Ptrofs.max_unsigned) with (Ptrofs.modulus - 1); omega).
    rewrite (Ptrofs.unsigned_repr)
      by (change (Ptrofs.max_unsigned) with (Ptrofs.modulus - 1); omega).
(* Goal: @data_equal t2 v0 v1 *)
    auto.
  }
(* Goal: @data_equal t2 v0 v1 *)
  rewrite !prop_true_andp in H0 by auto.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  unfold at_offset in H0.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  unfold nested_field_offset, nested_field_type in H0;   simpl in H0.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  rewrite !offset_offset_val in H0.
(* Goal: @derives mpred Nveric (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) p)) *)
  rewrite Z.add_0_r in H0. apply H0.
Qed.

Lemma stronger_default_val: forall t v, v >>> default_val t.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @stronger t v (@default_val cs t) *)
  intros sh p.
(* Goal: @derives mpred Nveric (@data_at cs sh t v p) (@data_at cs sh t (@default_val cs t) p) *)
  unfold data_at.
(* Goal: @derives mpred Nveric (@field_at cs sh t (@nil gfield) v p) (@field_at cs sh t (@nil gfield) (@default_val cs t) p) *)
  apply field_at_field_at_.
Qed.

Lemma stronger_proj_reptype: forall t v1 v2,
  (v1 >>> v2) <->
  (forall gfs, legal_nested_field t gfs -> type_is_by_value (nested_field_type t gfs) = true ->
   proj_reptype t gfs v1 >>> proj_reptype t gfs v2).
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
intros.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
split; intros.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
hnf; intros.
specialize (H sh).
unfold data_at in *.
intro p.
unfold field_at in *.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v0)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) (@andp mpred Nveric (@prop mpred Nveric (@eq Z (@Zlength (@reptype cs t0) (@unfold_reptype cs (Tarray t0 n a) v1)) n)) (aggregate_pred.rangespec Z0 (Z.to_nat n) (fun i : Z => at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (offset_val Z0 p))) *)
normalize.
(* Goal: @derives mpred Nveric (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v0))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) (at_offset (@data_at_rec cs sh t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) (Z.sub i Z0) (@unfold_reptype cs (Tarray t0 n a) v1))) (Z.mul (@sizeof (@cenv_cs cs) t0) i) p) *)
unfold at_offset.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
unfold nested_field_type at 1 4. simpl.
(* Goal: match offset_val (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Vptr b i0) with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus end *)
unfold nested_field_offset; simpl.
unfold nested_field_offset in H; simpl in H.
unfold at_offset in H.
unfold nested_field_type in H; simpl in H.
Abort.  (* probably true, but not needed *)

(* Goal: Z.le (Z.add (Z.mul (@sizeof (@cenv_cs cs) t0) i) (@sizeof (@cenv_cs cs) t0)) (Z.mul (@sizeof (@cenv_cs cs) t0) n) *)
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
Lemma data_equal_stronger: forall {t} (v1 v2: reptype t), (v1 === v2) <-> (v1 >>> v2) /\ (v2 >>> v1).
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: iff (@data_equal t v1 v2) (and (@stronger t v1 v2) (@stronger t v2 v1)) *)
  split; intro.
(* Goal: @data_equal t2 v0 v1 *)
  + split; intro sh; rewrite H; auto.
  + destruct H.
(* Goal: @data_equal t v1 v2 *)
    intro sh; apply pred_ext; [apply H | apply H0].
Qed.

Lemma data_equal_JMeq:
  forall t t' a a' b b',
    t=t' ->
    @JMeq (reptype t) a (reptype t') a' ->
    @JMeq (reptype t) b (reptype t') b' ->
    a === b -> a' === b'.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
intros. subst t'.
(* Goal: @data_equal t a' b' *)
apply JMeq_eq in H0. apply JMeq_eq in H1.
(* Goal: @data_equal t2 v0 v1 *)
subst; auto.
Qed.

(* Goal: Z.le (Z.add (Z.mul (@sizeof (@cenv_cs cs) t0) i) (@sizeof (@cenv_cs cs) t0)) (Z.mul (@sizeof (@cenv_cs cs) t0) n) *)
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
Lemma eq_rect_r_data_equal: forall {t1 t2} v0 v1 (H: t1 = t2),
  v0 === v1 ->
  eq_rect_r reptype v0 H === eq_rect_r reptype v1 H.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t1 (@eq_rect_r type t2 (@reptype cs) v0 t1 H) (@eq_rect_r type t2 (@reptype cs) v1 t1 H) *)
  generalize H.
(* Goal: @data_equal t v v' *)
  subst.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t2 (@eq_rect_r type t2 (@reptype cs) v0 t2 H) (@eq_rect_r type t2 (@reptype cs) v1 t2 H) *)
  unfold eq_rect_r.
(* Goal: @data_equal t2 (@eq_rect type t2 (fun y : type => @reptype cs y) v0 t2 (@eq_sym type t2 t2 H)) (@eq_rect type t2 (fun y : type => @reptype cs y) v1 t2 (@eq_sym type t2 t2 H)) *)
  rewrite <- !eq_rect_eq.
(* Goal: @data_equal t2 v0 v1 *)
  auto.
Qed.

Instance Equiv_data_equal t: Equivalence (@data_equal t).
Proof.
(* Goal: and (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) Z0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (Z.lt (Z.mul (@sizeof (@cenv_cs cs) t0) i) (Z.mul (@sizeof (@cenv_cs cs) t0) n)) *)
  unfold data_equal; split.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  + intro; intros.
(* Goal: @data_equal t v' v' *)
    reflexivity.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  + intro; intros.
(* Goal: @data_equal t v' v' *)
    rewrite H; reflexivity.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  + intro; intros.
(* Goal: @data_equal t v' v' *)
    rewrite H, H0; reflexivity.
Defined.

Lemma data_equal_refl': forall t (v v': reptype t), v = v' -> v === v'.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros. subst. reflexivity.
Qed.

Lemma field_at_data_equal: forall sh t gfs v0 v1,
  v0 === v1 ->
  field_at sh t gfs v0 = field_at sh t gfs v1.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @eq (forall _ : val, mpred) (@field_at cs sh t gfs v0) (@field_at cs sh t gfs v1) *)
  destruct (data_equal_stronger v0 v1) as [? _].
(* Goal: @eq (forall _ : val, mpred) (@field_at cs sh t gfs v0) (@field_at cs sh t gfs v1) *)
  spec H0; [auto |].
(* Goal: @data_equal t2 v0 v1 *)
  apply pred_ext; apply field_at_stronger; tauto.
Qed.

Instance Proper_field_at: forall sh t gfs,
  Proper ((@data_equal _) ==> eq) (field_at sh t gfs).
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intro; intros.
(* Goal: @data_equal t2 v0 v1 *)
  apply field_at_data_equal; auto.
Defined.

Lemma data_equal_array_ext: forall t0 n a (v0 v1: reptype (Tarray t0 n a)),
 Zlength (unfold_reptype v0) = Zlength (unfold_reptype v1) ->
  (forall i, 0 <= i < n ->
     Znth i (unfold_reptype v0) === Znth i (unfold_reptype v1)) ->
  v0 === v1.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: @data_equal t2 v0 v1 *)
  apply data_equal_stronger; split; apply stronger_array_ext; auto.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  + intros.
(* Goal: @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
    specialize (H0 i H1).
    destruct (data_equal_stronger
                      (Znth i (unfold_reptype v0))
                      (Znth i (unfold_reptype v1))) as [? _].
(* Goal: @data_equal t2 v0 v1 *)
    tauto.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  + intros.
(* Goal: @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
    specialize (H0 i H1).
    destruct (data_equal_stronger
                      (Znth i (unfold_reptype v0))
                      (Znth i (unfold_reptype v1))) as [? _].
(* Goal: @data_equal t2 v0 v1 *)
    tauto.
Qed.

(*
Lemma data_equal_zl_equiv: forall t n a (v v': reptype (Tarray t n a)),
  zl_equiv (unfold_reptype v) (unfold_reptype v') ->
  @data_equal (Tarray t n a) v v'.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  apply data_equal_array_ext.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  specialize (H i H0).
(* Goal: @eq Prop (@eq Z (@Zlength (@reptype cs t0) v0) Z0) (@eq Z (@Zlength (@reptype cs t0) v1) Z0) *)
  rewrite H.
(* Goal: @data_equal t v' v' *)
  reflexivity.
Qed.

Lemma data_equal_zl_equiv': forall t n a v v',
  zl_equiv v v' ->
  @fold_reptype _ _ (Tarray t n a) v === @fold_reptype _ _ (Tarray t n a) v'.
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  apply data_equal_zl_equiv.
  rewrite !unfold_fold_reptype.
(* Goal: @data_equal t2 v0 v1 *)
  auto.
Qed.

Instance Proper_fold_reptype_array: forall t n a,
  Proper ((@zl_equiv (reptype t) (default_val _) (list_zlist _ _) 0 n)
               ==> (@data_equal (Tarray t n a))) (@fold_reptype _ _ (Tarray t n a)).
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intro; intros.
  apply data_equal_zl_equiv'.
(* Goal: @data_equal t2 v0 v1 *)
  auto.
Defined.
*)

Lemma data_equal_proj_reptype: forall t v1 v2,
  (v1 === v2) <->
  (forall gfs, legal_nested_field t gfs -> type_is_by_value (nested_field_type t gfs) = true ->
   proj_reptype t gfs v1 === proj_reptype t gfs v2).
Proof.
(* Goal: forall (i : Z) (_ : and (Z.le Z0 i) (Z.lt i n)), @stronger t0 (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v1)) (@Znth (@reptype cs t0) (@Inhabitant_reptype cs t0) i (@unfold_reptype cs (Tarray t0 n a) v0)) *)
  intros.
  rewrite data_equal_stronger.
  assert ((forall gfs : list gfield,
    legal_nested_field t gfs ->
    type_is_by_value (nested_field_type t gfs) = true ->
    proj_reptype t gfs v1 === proj_reptype t gfs v2) <->
    (forall gfs : list gfield,
    legal_nested_field t gfs ->
    type_is_by_value (nested_field_type t gfs) = true ->
    proj_reptype t gfs v1 >>> proj_reptype t gfs v2) /\
    (forall gfs : list gfield,
    legal_nested_field t gfs ->
    type_is_by_value (nested_field_type t gfs) = true ->
    proj_reptype t gfs v2 >>> proj_reptype t gfs v1)).
(* Goal: Z.le (Z.add (Z.mul (@sizeof (@cenv_cs cs) t0) i) (@sizeof (@cenv_cs cs) t0)) (Z.mul (@sizeof (@cenv_cs cs) t0) n) *)
(* Goal: Z.lt (Z.add (Z.add (Ptrofs.unsigned i0) (Z.mul (@sizeof (@cenv_cs cs) t0) i)) (@sizeof (@cenv_cs cs) t0)) Ptrofs.modulus *)
  {
    split; intros; [split; intros |].
    + specialize (H gfs H0 H1).
      rewrite data_equal_stronger in H.
(* Goal: @data_equal t2 v0 v1 *)
      tauto.
    + specialize (H gfs H0 H1).
      rewrite data_equal_stronger in H.
(* Goal: @data_equal t2 v0 v1 *)
      tauto.
(* Goal: @data_equal t2 v0 v1 *)
    + rewrite data_equal_stronger; split; apply H; auto.
  }
(*  pose proof stronger_proj_reptype t v1 v2.
  pose proof stronger_proj_reptype t v2 v1.
(* Goal: @data_equal t2 v0 v1 *)
  tauto.
*)
Abort.  (* not needed *)

End STRONGER.

Module DataCmpNotations.
  Notation "X '>>>' Y" := (stronger X Y) (at level 60, no associativity).
  Notation "X '===' Y" := (data_equal X Y) (at level 60, no associativity).
End DataCmpNotations.

Global Existing Instance Equiv_data_equal.
(*Global Existing Instance Proper_fold_reptype_array.*)
Global Existing Instance Proper_field_at.