Require Export VST.veric.base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.
Require Import compcert.cfrontend.Ctypes.
Require Import VST.veric.mpred.
Require Import VST.veric.seplog.

Require Import VST.msl.normalize.

Local Open Scope pred.

Lemma mapsto_core_load: forall ch v sh loc m, 
  (address_mapsto ch v sh loc * TT)%pred m -> core_load ch loc v m.
Proof.
(* Goal: forall (ch : memory_chunk) (v : val) (sh : Share.t) (loc : AV.address) (m : rmap) (_ : @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v sh loc) (@TT rmap ag_rmap)) m), @app_pred rmap ag_rmap (core_load ch loc v) m *)
unfold address_mapsto, core_load.
(* Goal: forall (ch : memory_chunk) (v : val) (sh : Share.t) (loc : AV.address) (m : rmap) (_ : @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) (@TT rmap ag_rmap)) m), @app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh0 : Share.t => @ex (readable_share sh0) (fun rsh : readable_share sh0 => @eq resource (resource_at phi l') (YES sh0 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))))) m *)
intros until m; intros H.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))))) m *)
destruct H as [phi0 [phi1 [Hjoin [[bl [[[Hlen [Hdec Halign]] H] _]] ?]]]].
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))) w' *)
unfold allp, jam in *.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))))) w' *)
exists bl.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2)))) w' *)
repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun a : rmap => forall b : address, @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) b then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl b)) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) b)) a) (predicates_hered.allp_obligation_1 rmap ag_rmap address (fun l : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) l then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l)) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) l)))) m *)
hnf. intro b; specialize (H b).
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl b)) m *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
hnf in H|-*.
(* Goal: @eq Prop (if S b then @app_pred rmap ag_rmap (P b) w else @app_pred rmap ag_rmap (Q b) w) (if S b then @app_pred rmap ag_rmap (P b) (@core rmap Join_rmap Sep_rmap w) else @app_pred rmap ag_rmap (Q b) (@core rmap Join_rmap Sep_rmap w)) *)
if_tac.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl b)) m *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
hnf in H|-*.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at m b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
destruct H as [p ?].
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at m b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
apply (resource_at_join _ _ _ b) in Hjoin.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at m b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
rewrite H in Hjoin; clear H.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at m b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
repeat rewrite preds_fmap_NoneP in Hjoin.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at m b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
inv Hjoin.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (YES sh3 rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (YES sh3 rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
do 3 econstructor; try reflexivity.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (YES sh3 rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP))) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
do 2 econstructor; reflexivity.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
auto.
Qed.

Lemma nth_error_in_bounds: forall {A} (l: list A) i, (O <= i < length l)%nat
  -> exists x, nth_error l i = value x.
Proof.
(* Goal: forall (A : Type) (l : list A) (i : nat) (_ : and (le O i) (lt i (@Datatypes.length A l))), @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
intros until i; intros H.
(* Goal: @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
revert i l H.
induction i; destruct l; intros; simpl in *;
  try solve [eauto|omegaContradiction].
(* Goal: @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
apply IHi; omega.
Qed.

Lemma nth_eq_nth_error_eq: forall {A} (d: A) (l l': list A) i,
  (O <= i < length l)%nat
  -> length l = length l'
  -> nth i l d = nth i l' d
  -> nth_error l i = nth_error l' i.
Proof.
(* Goal: forall (A : Type) (d : A) (l l' : list A) (i : nat) (_ : and (le O i) (lt i (@Datatypes.length A l))) (_ : @eq nat (@Datatypes.length A l) (@Datatypes.length A l')) (_ : @eq A (@nth A i l d) (@nth A i l' d)), @eq (option A) (@nth_error A l i) (@nth_error A l' i) *)
intros until i; intros H H0 H1.
(* Goal: @eq (option A) (@nth_error A l i) (@nth_error A l' i) *)
revert i l l' H H0 H1.
induction i; destruct l; destruct l'; intros; simpl in *;
  try solve [auto|omegaContradiction].
(* Goal: @eq (option A) (@nth_error A l i) (@nth_error A l' i) *)
rewrite (IHi l l'); try solve [auto|omega].
Qed.

Lemma core_load_fun: forall ch m loc v1 v2,
   core_load ch loc v1 m -> core_load ch loc v2 m -> v1=v2.
Proof.
intros until v2; intros H H0.
(* Goal: @app_pred rmap ag_rmap (core_load ch loc v) w' *)
unfold core_load in *.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))) w' *)
unfold allp, jam in *.
destruct H as [bl [[H1 [H2 Halign]] H]].
destruct H0 as [bl' [[H3 [H4 Halign']] H0]].
cut (forall i, nth_error bl i = nth_error bl' i); [intro H5|].
cut (bl = bl'); [intro H6|].
rewrite H6 in H2.
rewrite H4 in H2.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
auto.
clear - H5.
revert bl' H5.
induction bl; destruct bl'; intros; try solve [specialize (H5 O); inv H5|auto].
(* Goal: @eq (prod nat rmap') (@pair nat rmap' n (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0))) (@pair nat rmap' n r0) *)
f_equal.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
specialize (H5 O); inv H5; auto.
apply IHbl.
intro i.
specialize (H5 (S i)).
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
auto.
intro i.
destruct loc as (b, ofs).
specialize (H (b, ofs + Z_of_nat i)).
specialize (H0 (b, ofs + Z_of_nat i)).
hnf in H, H0. if_tac in H.
* (* adr_range *)
destruct H as [sh [rsh H]].
destruct H0 as [sh' [rsh' H0]].
rewrite H0 in H.
clear H0.
simpl in *.
inversion H.
replace (ofs + Z_of_nat i - ofs) with (Z_of_nat i) in * by omega.
rewrite nat_of_Z_eq in *.
rewrite <- H3 in H1.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
apply nth_eq_nth_error_eq with (d := Undef); auto.
destruct H5 as [? [H5 H5']].
rewrite size_chunk_conv in H5'.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
omega.
* (* ~adr_range *)
cut (i >= length bl)%nat. intro Hlen.
cut (i >= length bl')%nat. intro Hlen'.
generalize (nth_error_length i bl) as H6; intro.
generalize (nth_error_length i bl') as H7; intro.
rewrite <- H6 in Hlen.
rewrite <- H7 in Hlen'.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
rewrite Hlen; rewrite Hlen'; auto.
rewrite <- H3 in H1; clear H3.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
rewrite <- H1; auto.
unfold adr_range in H5.
rewrite size_chunk_conv in H5.
rewrite <- H1 in H5.
cut ( ~(O <= i < length bl))%nat.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
omega.
intro HContra.
apply H5.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
split; auto.
cut (0 <= Z_of_nat i < Z_of_nat (length bl)). intro H6.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
2: omega.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
omega.
Qed.

Lemma extensible_core_load': forall ch loc v
  w w', extendR w w' -> core_load ch loc v w -> core_load ch loc v w'.
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
intros.
(* Goal: @app_pred rmap ag_rmap (core_load ch loc v) w' *)
unfold core_load in *.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))))) w' *)
destruct H0 as [bl ?].
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))))) w' *)
exists bl.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2)))) w' *)
destruct H0 as [[? [? Halign]] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2)))) w' *)
destruct H as [wx ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2)))) w' *)
repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2))) w' *)
unfold allp, jam in *.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun a : rmap => forall b : address, @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) b then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl b)) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) b)) a) (predicates_hered.allp_obligation_1 rmap ag_rmap address (fun l : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) l then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l) (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l)) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) l)))) w' *)
intro loc'.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) loc' then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi loc') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl loc')) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) loc')) w' *)
specialize (H2 loc').
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec loc (size_chunk ch) loc' then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi loc') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl loc')) m else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m) (res_predicates.jam_obligation_1 rmap ag_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun l' : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) bl Undef)) NoneP)))) (res_predicates.core_load_obligation_1 loc bl l')) (fun _ : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) loc')) w' *)
apply resource_at_join with (loc := loc') in H.
hnf in H2|-*.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
if_tac; auto.
hnf in H2|-*.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w' loc') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc') (@snd block Z loc))) bl Undef)) NoneP))) *)
destruct H2 as [sh [rsh H2]].
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w' loc') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc') (@snd block Z loc))) bl Undef)) NoneP))) *)
rewrite H2 in H.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
inv H; subst; eauto.
Qed.

(*
Lenb: should be moved to tycontext or some other Clight-dependent file- but is in fact dead
Definition Dbool {CS: compspecs} (Delta: tycontext) (e: Clight.expr) : assert :=
  fun rho =>  EX b: bool, !! (bool_of_valf (eval_expr e rho) = Some b).
*)
                             
Lemma assert_truth:  forall {A} `{ageable A} (P:  Prop), P -> forall (Q: pred A), Q |-- (!! P) && Q.
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
intros.
(* Goal: @derives A H Q (@andp A H (@prop A H P) Q) *)
intros st ?.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
split; auto.
Qed.

(*   Lemma assert_Val_is_true:
   forall {A} `{ageable A} (P: pred A), P |-- !!(is_true Vtrue) && P.
  Proof.  intros. apply assert_truth. apply Val_is_true_Vtrue. Qed.

Hint Resolve Val_is_true_Vtrue  @assert_Val_is_true.
*)

(****************** stuff moved from semax_prog  *****************)

Lemma rmap_unage_age:
  forall r, age (rmap_unage r) r.
Proof.
(* Goal: forall r : rmap, @age rmap ag_rmap (rmap_unage r) r *)
intros; unfold age, rmap_unage; simpl.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
case_eq (unsquash r); intros.
(* Goal: @eq (option rmap) (@age1 rmap ag_rmap (squash (@pair nat rmap' (S n) r0))) (@Some rmap r) *)
change ag_rmap with R.ag_rmap.
(* Goal: @eq (option rmap) (@age1 rmap ag_rmap (squash (@pair nat rmap' (S n) r0))) (@Some rmap r) *)
rewrite rmap_age1_eq.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
(* Goal: @eq (prod nat rmap') (@pair nat rmap' n (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0))) (@pair nat rmap' n r0) *)
f_equal.
(* Goal: @eq rmap (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0))) r *)
apply unsquash_inj.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (unsquash r) *)
rewrite H.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
(* Goal: @eq (prod nat rmap') (@pair nat rmap' n (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0))) (@pair nat rmap' n r0) *)
f_equal.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0)) r0 *)
generalize (equal_f (rmap_fmap_comp (approx (S n)) (approx (S n)) (approx n) (approx n)) r0); intro.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0)) r0 *)
unfold compose at 1 in H0.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0)) r0 *)
rewrite H0.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
rewrite approx_oo_approx'; auto.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
rewrite approx'_oo_approx; auto.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
clear - H.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
generalize (unsquash_squash n r0); intros.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
rewrite <- H in H0.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
rewrite squash_unsquash in H0.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
congruence.
Qed.

Lemma adr_range_split_lem1: forall n m r loc loc',
  r = n + m -> n >= 0 -> m >= 0 -> adr_range loc n loc' -> adr_range loc r loc'.
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
unfold adr_range; intros.
destruct loc; destruct loc'; simpl in *.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
destruct H2; split; auto.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
omega.
Qed.

Lemma adr_range_split_lem2: forall n m r loc loc',
  r = n + m -> n >= 0 -> m >= 0 -> adr_range (fst loc, snd loc + n) m loc'
  -> adr_range loc r loc'.
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
unfold adr_range; intros.
destruct loc; destruct loc'; simpl in *.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
destruct H2; split; auto.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
omega.
Qed.

Lemma adr_range_split_lem3: forall n m r loc loc',
  r = n + m -> n >= 0 -> m >= 0
  -> ~adr_range loc n loc'
  -> ~adr_range (fst loc, snd loc + n) m loc'
  -> ~adr_range loc r loc'.
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
unfold adr_range; intros.
destruct loc; destruct loc'; simpl in *.
(* Goal: not (and (@eq block b b0) (and (Z.le z z0) (Z.lt z0 (Z.add z r)))) *)
intros [c1 c2].
(* Goal: False *)
destruct (Z_lt_dec z0 (z+n)).
(* Goal: False *)
(* Goal: False *)
apply H2.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
split; auto||omega.
(* Goal: False *)
apply H3.
(* Goal: and (Z.le z z0) (Z.lt z0 (Z.add z r)) *)
split; auto||omega.
Qed.

Lemma prop_imp_i {A}{agA: ageable A}:
  forall (P: Prop) Q w, (P -> app_pred Q w) -> (!!P --> Q) w.
Proof.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
 intros. intros w' ? ?. apply H in H1. eapply pred_nec_hereditary; eauto.
Qed.

Lemma or_pred_ext {A} `{agA : ageable A}: forall P Q P' Q',
       (P <--> P') && (Q <--> Q') |--  (P || Q) <--> (P' || Q').
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
intros.
(* Goal: @derives A agA (@andp A agA (@andp A agA (@imp A agA P P') (@imp A agA P' P)) (@andp A agA (@imp A agA Q Q') (@imp A agA Q' Q))) (@andp A agA (@imp A agA (@orp A agA P Q) (@orp A agA P' Q')) (@imp A agA (@orp A agA P' Q') (@orp A agA P Q))) *)
intros w [? ?].
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@orp A agA P Q) (@orp A agA P' Q')) (@imp A agA (@orp A agA P' Q') (@orp A agA P Q))) w *)
split; intros w' ? [?|?].
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
left. destruct H; eauto.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
right. destruct H0; eauto.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
left. destruct H; eauto.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
right. destruct H0; eauto.
Qed.

Lemma corable_pureat: forall pp k loc, corable (pureat pp k loc).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
 intros. intro w.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (pureat pp k loc) w) (@app_pred rmap ag_rmap (pureat pp k loc) (@core rmap Join_rmap Sep_rmap w)) *)
 unfold pureat.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if S b then @app_pred rmap ag_rmap (P b) m else @app_pred rmap ag_rmap (Q b) m) (res_predicates.jam_obligation_1 rmap ag_rmap B S' S P Q b)) w) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if S b then @app_pred rmap ag_rmap (P b) m else @app_pred rmap ag_rmap (Q b) m) (res_predicates.jam_obligation_1 rmap ag_rmap B S' S P Q b)) (@core rmap Join_rmap Sep_rmap w)) *)
  simpl. rewrite <- core_resource_at.
(* Goal: @eq Prop (@eq resource (resource_at w loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (resource_at w loc)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
  destruct (w @ loc).
(* Goal: @eq Prop (@eq resource (NO sh n) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (NO sh n)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
(* Goal: @eq Prop (@eq resource (YES sh r k0 p) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (YES sh r k0 p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
(* Goal: @eq Prop (@eq resource (PURE k0 p) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (PURE k0 p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
  rewrite core_NO; apply prop_ext; split; intro Hx; inv Hx.
(* Goal: @eq Prop (@eq resource (YES sh r k0 p) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (YES sh r k0 p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
(* Goal: @eq Prop (@eq resource (PURE k0 p) (PURE k (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp))) (@eq resource (@core resource Join_resource Sep_resource (PURE k0 p)) (PURE k (preds_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) pp))) *)
  rewrite core_YES; apply prop_ext; split; intro Hx; inv Hx.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
  rewrite core_PURE; rewrite level_core; auto.
Qed.

Lemma corable_func_at: forall f l, corable (func_at f l).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
  intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_at f l) *)
  unfold func_at.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap match f with | mk_funspec fsig cc A P Q P_ne Q_ne => @exp rmap ag_rmap preds (fun pp : preds => pureat pp (FUN fsig cc) l) end *)
  destruct f as [fsig0 cc A P Q].
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (pureat b (FUN fsig0 cc) l) *)
  apply corable_pureat.
Qed.

Lemma corable_func_at': forall f l, corable (func_at' f l).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
  intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_at' f l) *)
  unfold func_at'.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap match f with | mk_funspec fsig cc A P Q P_ne Q_ne => @exp rmap ag_rmap preds (fun pp : preds => pureat pp (FUN fsig cc) l) end *)
  destruct f as [fsig0 cc A P Q].
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v (Vptr b Ptrofs.zero))) (func_at f (@pair block Z b Z0)))) *)
  apply corable_exp; intro.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (pureat b (FUN fsig0 cc) l) *)
  apply corable_pureat.
Qed.

Lemma corable_func_ptr : forall f v, corable (func_ptr f v).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
  intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_ptr f v) *)
  unfold func_ptr.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v (Vptr b Ptrofs.zero))) (func_at f (@pair block Z b Z0)))) *)
  apply corable_exp; intro.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
  apply corable_andp; auto.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_at b0 (@pair block Z b1 Z0)) *)
  apply corable_func_at.
Qed.

Hint Resolve corable_func_ptr.

Lemma corable_funspecs_assert:
  forall FS rho, corable (funspecs_assert FS rho).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
 intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (funspecs_assert FS rho) *)
 unfold funspecs_assert.
 repeat
 first [
   apply corable_andp|
   apply corable_exp; intro|
   apply corable_allp; intro|
   apply corable_prop|
   apply corable_imp].
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_at b0 (@pair block Z b1 Z0)) *)
 + apply corable_func_at.
 + apply corable_func_at'.
Qed.

Hint Resolve corable_funspecs_assert.

Lemma corable_jam: forall {B} {S': B -> Prop} (S: forall l, {S' l}+{~ S' l}) (P Q: B -> pred rmap),
    (forall loc, corable (P loc)) ->
    (forall loc, corable (Q loc)) ->
    forall b, corable (jam S P Q b).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b) *)
intro.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b) w) (@app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b) (@core rmap Join_rmap Sep_rmap w)) *)
unfold jam.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if S b then @app_pred rmap ag_rmap (P b) m else @app_pred rmap ag_rmap (Q b) m) (res_predicates.jam_obligation_1 rmap ag_rmap B S' S P Q b)) w) (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if S b then @app_pred rmap ag_rmap (P b) m else @app_pred rmap ag_rmap (Q b) m) (res_predicates.jam_obligation_1 rmap ag_rmap B S' S P Q b)) (@core rmap Join_rmap Sep_rmap w)) *)
simpl.
(* Goal: @eq Prop (if S b then @app_pred rmap ag_rmap (P b) w else @app_pred rmap ag_rmap (Q b) w) (if S b then @app_pred rmap ag_rmap (P b) (@core rmap Join_rmap Sep_rmap w) else @app_pred rmap ag_rmap (Q b) (@core rmap Join_rmap Sep_rmap w)) *)
if_tac.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (P b) w) (@app_pred rmap ag_rmap (P b) (@core rmap Join_rmap Sep_rmap w)) *)
(* Goal: @eq Prop (@app_pred rmap ag_rmap (Q b) w) (@app_pred rmap ag_rmap (Q b) (@core rmap Join_rmap Sep_rmap w)) *)
apply H.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (Q b) w) (@app_pred rmap ag_rmap (Q b) (@core rmap Join_rmap Sep_rmap w)) *)
apply H0.
Qed.
(*Lenb: add Hint Resolve corable_jam?*)

(*
Lemma corable_fun_assert: forall v fsig cc A P Q, corable (fun_assert v fsig cc A P Q).
Proof.
(* Goal: forall (P Q : Prop) (_ : forall _ : P, Q), @derives A H (@prop A H P) (@prop A H Q) *)
intros.
unfold fun_assert, res_predicates.fun_assert.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v (Vptr b Ptrofs.zero))) (func_at f (@pair block Z b Z0)))) *)
apply corable_exp; intro.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
apply corable_andp; auto.
unfold FUNspec.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b) *)
apply corable_allp; intro.
apply corable_jam; intro loc.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (pureat b (FUN fsig0 cc) l) *)
apply corable_pureat.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
intro w. unfold TTat. apply prop_ext; split; intros; hnf in H|-*; auto.
Qed.

Hint Resolve corable_fun_assert : normalize.
*)
Lemma prop_derives {A}{H: ageable A}:
 forall (P Q: Prop), (P -> Q) -> prop P |-- prop Q.
Proof.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) res_predicates.core_load_obligation_2) m *)
intros. intros w ?; apply H0; auto.
Qed.
