Require Import VST.msl.log_normalize.
Require Import VST.msl.alg_seplog.
Require Export VST.veric.base.
Require Import VST.veric.rmaps.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.

Require Import VST.veric.mpred.
Require Import VST.veric.address_conflict.
Require Export VST.veric.shares.

Local Open Scope pred.

Definition func_at (f: funspec): address -> pred rmap :=
  match f with
   | mk_funspec fsig cc A P Q _ _ => pureat (SomeP (SpecTT A) (packPQ P Q)) (FUN fsig cc)
  end.

Definition func_at' (f: funspec) (loc: address) : pred rmap :=
  match f with
   | mk_funspec fsig cc _ _ _ _ _ => EX pp:_, pureat pp (FUN fsig cc) loc
  end.

Definition func_ptr (f: funspec) (v: val): mpred :=
  EX b: block, !! (v = Vptr b Ptrofs.zero) && func_at f (b, 0).

Definition NDmk_funspec (f: funsig) (cc: calling_convention)
  (A: Type) (Pre Post: A -> environ -> mpred): funspec :=
  mk_funspec f cc (rmaps.ConstType A) (fun _ => Pre) (fun _ => Post)
             (const_super_non_expansive _ _) (const_super_non_expansive _ _).

(* Definition assert: Type := environ -> pred rmap. *)

Bind Scope pred with assert.
Local Open Scope pred.

Definition closed_wrt_vars {B} (S: ident -> Prop) (F: environ -> B) : Prop :=
  forall rho te',
     (forall i, S i \/ Map.get (te_of rho) i = Map.get te' i) ->
     F rho = F (mkEnviron (ge_of rho) (ve_of rho) te').

Definition closed_wrt_lvars {B} (S: ident -> Prop) (F: environ -> B) : Prop :=
  forall rho ve',
     (forall i, S i \/ Map.get (ve_of rho) i = Map.get ve' i) ->
     F rho = F (mkEnviron (ge_of rho) ve' (te_of rho)).

Definition not_a_param (params: list (ident * type)) (i : ident) : Prop :=
  ~ In i (map (@fst _ _) params).

Definition is_a_local (vars: list (ident * type)) (i: ident) : Prop :=
  In  i (map (@fst _ _) vars) .

(* Goal: forall (FS FS' : PTree.t funspec) (rho : environ) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS) (@PTree.get funspec id FS')), @derives rmap ag_rmap (funspecs_assert FS rho) (funspecs_assert FS' rho) *)
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
Fixpoint sepcon_list {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A} {AgeA: Age_alg A}
   (p: list (pred A)) : pred A :=
 match p with nil => emp | h::t => h * sepcon_list t end.

Definition typed_true (t: type) (v: val)  : Prop := strict_bool_val v t
= Some true.

Definition typed_false (t: type)(v: val) : Prop := strict_bool_val v t =
                                                   Some false.

Definition subst {A} (x: ident) (v: val) (P: environ -> A) : environ -> A :=
  fun s => P (env_set s x v).

Lemma  subst_extens:
 forall a v P Q, (forall rho, P rho |-- Q rho) -> forall rho, subst a v P rho |-- subst a v Q rho.
Proof.
(* Goal: forall (a : ident) (v : val) (P Q : forall _ : environ, @pred rmap ag_rmap) (_ : forall rho : environ, @derives rmap ag_rmap (P rho) (Q rho)) (rho : environ), @derives rmap ag_rmap (@subst (@pred rmap ag_rmap) a v P rho) (@subst (@pred rmap ag_rmap) a v Q rho) *)
unfold subst, derives.
simpl;
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
auto.
Qed.

Lemma approx_sepcon: forall (P Q: mpred) n,
  approx n (P * Q) =
  approx n P *
  approx n Q.
Proof.
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P Q)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (approx n P) (approx n Q)) *)
  change sepcon with predicates_sl.sepcon in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) P) (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) Q) b) *)
  apply predicates_hered.pred_ext.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (lt (@level rmap ag_rmap y) n) (@app_pred rmap ag_rmap P y)) (and (lt (@level rmap ag_rmap z) n) (@app_pred rmap ag_rmap Q z))))) *)
    destruct H as [? [y [z [? [? ?]]]]].
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (lt (@level rmap ag_rmap y) n) (@app_pred rmap ag_rmap P y)) (and (lt (@level rmap ag_rmap z) n) (@app_pred rmap ag_rmap Q z))))) *)
    exists y, z; split; auto.
(* Goal: and (and (lt (@level rmap ag_rmap y) n) (@app_pred rmap ag_rmap P y)) (and (lt (@level rmap ag_rmap z) n) (@app_pred rmap ag_rmap Q z)) *)
    split; split; auto.
    - apply age_sepalg.join_level in H0.
(* Goal: lt (@level rmap ag_rmap w) n *)
      omega.
    - apply age_sepalg.join_level in H0.
(* Goal: lt (@level rmap ag_rmap w) n *)
      omega.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (@ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q z))))) *)
    destruct H as [y [z [? [[? ?] [? ?]]]]].
(* Goal: and (lt (@level rmap ag_rmap w) n) (@ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q z))))) *)
    split.
    - apply age_sepalg.join_level in H.
(* Goal: lt (@level rmap ag_rmap w) n *)
      omega.
    - exists y, z.
(* Goal: and (@join rmap Join_rmap y z w) (and (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q z)) *)
      split; [| split]; auto.
Qed.

Lemma approx_andp: forall (P Q: mpred) n,
  approx n (P && Q) =
  approx n P &&
  approx n Q.
Proof.
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@andp rmap ag_rmap P Q)) (@andp rmap ag_rmap (approx n P) (approx n Q)) *)
  change andp with (@predicates_hered.andp compcert_rmaps.RML.R.rmap _) in *.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) P) (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) Q) b) *)
  apply predicates_hered.pred_ext.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (and (@app_pred rmap ag_rmap P w) (@app_pred rmap ag_rmap Q w)) *)
    tauto.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (and (@app_pred rmap ag_rmap P w) (@app_pred rmap ag_rmap Q w)) *)
    tauto.
Qed.

Lemma approx_exp: forall A (P: A -> mpred) n,
  approx n (exp P) =
  EX a: A, approx n (P a).
Proof.
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
  intros.
(*  change (@exp _ Nveric A) with (@predicates_hered.exp compcert_rmaps.RML.R.rmap _ A) in *. *)
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) P) (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) Q) b) *)
  apply predicates_hered.pred_ext.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (forall b : A, @app_pred rmap ag_rmap (P b) w) *)
    firstorder.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (forall b : A, @app_pred rmap ag_rmap (P b) w) *)
    firstorder.
Qed.

Lemma approx_allp: forall A (P: A -> mpred) n,
  A ->
  approx n (allp P) =
  ALL a: A, approx n (P a).
Proof.
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) P) (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) Q) b) *)
  apply predicates_hered.pred_ext.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (forall b : A, @app_pred rmap ag_rmap (P b) w) *)
    firstorder.
  + intros w ?.
(* Goal: @app_pred rmap ag_rmap (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) w *)
    simpl in *.
(* Goal: and (lt (@level rmap ag_rmap w) n) (forall b : A, @app_pred rmap ag_rmap (P b) w) *)
    firstorder.
Qed.

Lemma approx_jam {B: Type} {S': B -> Prop} (S: forall l, {S' l}+{~ S' l}) (P Q: B -> mpred) n (b : B) :
  approx n (jam S P Q b) =
  jam S (approx n oo P) (approx n oo Q) b.
Proof.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S P Q b)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap B S' S (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) P) (@compose B (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) Q) b) *)
  apply predicates_hered.pred_ext.
  + intros w ?. simpl in *. if_tac; firstorder.
  + intros w ?. simpl in *. if_tac; firstorder.
Qed.

Lemma approx_func_ptr: forall (A: Type) fsig0 cc (P Q: A -> environ -> mpred) (v: val) (n: nat),
  approx n (func_ptr (NDmk_funspec fsig0 cc A P Q) v) = approx n (func_ptr (NDmk_funspec fsig0 cc A (fun a rho => approx n (P a rho)) (fun a rho => approx n (Q a rho))) v).
Proof.
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (func_ptr (NDmk_funspec fsig0 cc A P Q) v)) (approx n (func_ptr (NDmk_funspec fsig0 cc A (fun (a : A) (rho : environ) => approx n (P a rho)) (fun (a : A) (rho : environ) => approx n (Q a rho))) v)) *)
  unfold func_ptr.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@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 (NDmk_funspec fsig0 cc A P Q) (@pair block Z b Z0))))) (approx n (@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 (NDmk_funspec fsig0 cc A (fun (a : A) (rho : environ) => approx n (P a rho)) (fun (a : A) (rho : environ) => approx n (Q a rho))) (@pair block Z b Z0))))) *)
  rewrite !approx_exp; f_equal; extensionality b.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v (Vptr b Ptrofs.zero))) (func_at (NDmk_funspec fsig0 cc A P Q) (@pair block Z b Z0)))) (approx n (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v (Vptr b Ptrofs.zero))) (func_at (NDmk_funspec fsig0 cc A (fun (a : A) (rho : environ) => approx n (P a rho)) (fun (a : A) (rho : environ) => approx n (Q a rho))) (@pair block Z b Z0)))) *)
  rewrite !approx_andp; f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (func_at (NDmk_funspec fsig0 cc A P Q) (@pair block Z b Z0))) (approx n (func_at (NDmk_funspec fsig0 cc A (fun (a : A) (rho : environ) => approx n (P a rho)) (fun (a : A) (rho : environ) => approx n (Q a rho))) (@pair block Z b Z0))) *)
  unfold func_at, NDmk_funspec.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q))) (FUN fsig0 cc) (@pair block Z b Z0))) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)))) (FUN fsig0 cc) (@pair block Z b Z0))) *)
  simpl.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q))) (FUN fsig0 cc) (@pair block Z b Z0))) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)))) (FUN fsig0 cc) (@pair block Z b Z0))) *)
  apply pred_ext; intros w; simpl; intros [? ?]; split; auto.
  + rewrite H0.
(* Goal: @eq preds (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1))) (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1))) *)
    f_equal.
(* Goal: @eq preds (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1))) (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1))) *)
    f_equal.
(* Goal: @eq (forall (_ : list Type) (_ : A) (_ : bool) (_ : environ), @pred rmap ag_rmap) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1)) *)
    extensionality ts a.
(* Goal: @eq (forall (_ : bool) (_ : environ), @pred rmap ag_rmap) (fun (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)) ts a a0 a1)) (fun (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) ts a a0 a1)) *)
    extensionality prepost rho.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q))) (FUN fsig0 cc) (@pair block Z b Z0))) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)))) (FUN fsig0 cc) (@pair block Z b Z0))) *)
    unfold packPQ; destruct prepost; simpl.
    - change (approx (level w) (approx n (P a rho))) with
        ((approx (level w) oo (approx n)) (P a rho)).
(* Goal: lt (@level rmap ag_rmap w) n *)
      rewrite approx_oo_approx' by omega.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
      auto.
    - change (approx (level w) (approx n (Q a rho))) with
        ((approx (level w) oo (approx n)) (Q a rho)).
(* Goal: lt (@level rmap ag_rmap w) n *)
      rewrite approx_oo_approx' by omega.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
      auto.
  + rewrite H0.
(* Goal: @eq preds (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1))) (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1))) *)
    f_equal.
(* Goal: @eq preds (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1))) (SomeP (SpecTT (ConstType A)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1))) *)
    f_equal.
(* Goal: @eq (forall (_ : list Type) (_ : A) (_ : bool) (_ : environ), @pred rmap ag_rmap) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (P a2 rho)) (fun (_ : list Type) (a2 : A) (rho : environ) => approx n (Q a2 rho)) i a a0 a1)) (fun (i : list Type) (a : A) (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) i a a0 a1)) *)
    extensionality ts a.
(* Goal: @eq (forall (_ : bool) (_ : environ), @pred rmap ag_rmap) (fun (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)) ts a a0 a1)) (fun (a0 : bool) (a1 : environ) => approx (@level rmap ag_rmap w) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q) ts a a0 a1)) *)
    extensionality prepost rho.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun _ : list Type => P) (fun _ : list Type => Q))) (FUN fsig0 cc) (@pair block Z b Z0))) (approx n (pureat (SomeP (SpecTT (ConstType A)) (@packPQ (ConstType A) (fun (_ : list Type) (a : A) (rho : environ) => approx n (P a rho)) (fun (_ : list Type) (a : A) (rho : environ) => approx n (Q a rho)))) (FUN fsig0 cc) (@pair block Z b Z0))) *)
    unfold packPQ; destruct prepost; simpl.
    - change (approx (level w) (approx n (P a rho))) with
        ((approx (level w) oo (approx n)) (P a rho)).
(* Goal: lt (@level rmap ag_rmap w) n *)
      rewrite approx_oo_approx' by omega.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
      auto.
    - change (approx (level w) (approx n (Q a rho))) with
        ((approx (level w) oo (approx n)) (Q a rho)).
(* Goal: lt (@level rmap ag_rmap w) n *)
      rewrite approx_oo_approx' by omega.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
      auto.
Qed.

Definition funspecs_assert (FunSpecs: PTree.t funspec): assert :=
 fun rho =>
   (ALL  id: ident, ALL fs:funspec,  !! (FunSpecs!id = Some fs) -->
              EX b:block,
                   !! (Map.get (ge_of rho) id = Some b) && func_at fs (b,0))
   &&
   (ALL  b: block, ALL fs:funspec, func_at' fs (b,0) -->
             EX id:ident, !! (Map.get (ge_of rho) id = Some b)
                             && !! exists fs, FunSpecs!id = Some fs).

Definition globals_only (rho: environ) : environ := (mkEnviron (ge_of rho) (Map.empty _) (Map.empty _)).

Fixpoint make_args (il: list ident) (vl: list val) (rho: environ)  :=
  match il, vl with
  | nil, nil => globals_only rho
  | i::il', v::vl' => env_set (make_args il' vl' rho) i v
   | _ , _ => rho
  end.

Lemma same_FS_funspecs_assert:
  forall FS1 FS2,
     (forall id, FS1 ! id = FS2 ! id) ->
              funspecs_assert FS1 = funspecs_assert FS2.
Proof.
assert (forall FS FS' rho,
             (forall id, FS ! id = FS' ! id) ->
             funspecs_assert FS rho |-- funspecs_assert FS' rho).
(* Goal: and (lt (@level rmap ag_rmap w) n) (@ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q z))))) *)
{ intros; intros w [? ?]; split.
  clear H1; intro id. rewrite <- (H id); auto.
  intros loc fs w' Hw' H4; destruct (H1 loc fs w' Hw' H4)  as [id H3].
  exists id; rewrite <- (H id); auto. }
(* Goal: forall (FS1 FS2 : PTree.t funspec) (_ : forall id : positive, @eq (option funspec) (@PTree.get funspec id FS1) (@PTree.get funspec id FS2)), @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
intros.
(* Goal: @eq assert (funspecs_assert FS1) (funspecs_assert FS2) *)
extensionality rho.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) (Q a rho)) (approx (@level rmap ag_rmap w) (Q a rho)) *)
apply pred_ext; apply H; intros; auto.
Qed.

Lemma funspecs_assert_rho:
  forall G rho rho', ge_of rho = ge_of rho' -> funspecs_assert G rho |-- funspecs_assert G rho'.
Proof. unfold funspecs_assert; intros. rewrite H; auto. Qed.