Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.

Local Open Scope logic.

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
Definition pTree_from_elements {A} (el: list (positive * A)) : PTree.t A :=
 fold_right (fun ia t => PTree.set (fst ia) (snd ia) t) (PTree.empty _) el.

Definition local_trees :=
   (PTree.t val * PTree.t (type * val) * list Prop * option globals)%type.

Definition local2ptree1 (Q: localdef)
   (T1: PTree.t val) (T2: PTree.t (type * val)) (P': list Prop) (Q': option globals)
   (f:  PTree.t val -> PTree.t (type * val) -> list Prop -> option globals -> local_trees)
   : local_trees :=
match Q with
| temp i v =>   match T1 ! i with
                | None => f (PTree.set i v T1) T2 P' Q'
                | Some v' => f T1 T2 ((v=v')::P')  Q'
                end
| lvar i t v => match T2 ! i with
                | None => f T1 (PTree.set i (t, v) T2) P' Q'
                | Some (t', vl) => f T1 T2 ((vl=v)::(t'=t)::P') Q'
                end
| gvars gv =>   match Q' with
                | None => f T1 T2 P' (Some gv)
                | Some gv' => f T1 T2 ((gv' = gv)::P') Q'
                end
end.

Fixpoint local2ptree_aux (Q: list localdef)
   (T1: PTree.t val) (T2: PTree.t (type * val)) (P': list Prop) (Q': option globals):
   local_trees :=
match Q with
| Q1 :: Qr => local2ptree1 Q1 T1 T2 P' Q' (local2ptree_aux Qr)
| nil => (T1,T2,P',Q')
end.

Definition local2ptree (Q: list localdef)
     : (PTree.t val * PTree.t (type * val) * list Prop * option globals) :=
local2ptree_aux Q PTree.Leaf PTree.Leaf nil None.

Definition CLEAR_ME {T} (x:T) := x.
Ltac hide_it z := let x := fresh "x" in set (x:=z); change z with (CLEAR_ME z) in x.
(* TODO: compare this with unfold_name method in symbolic_go_lower. *)

Ltac hnf_localdef_list A :=
  match A with
 | temp _ ?v :: ?Q' => hide_it v; hnf_localdef_list Q'
 | lvar _ ?t ?v :: ?Q' => hide_it t; hide_it v; hnf_localdef_list Q'
 | gvars ?v :: ?Q' => hide_it v; hnf_localdef_list Q'
  | ?B :: ?C => let x := eval hnf in B in change B with x; hnf_localdef_list (x::C)
  | nil => idtac
  | _ => try (is_evar A; fail 1);
            let x := eval hnf in A in (change A with x); hnf_localdef_list x
  end.

Ltac grab_gvars L := 
 match L with gvars ?A :: ?B => let x := grab_gvars B in let z := constr:(A::x) in z
                | nil => let x := constr:(@nil globals) in x
  end.

Ltac prove_local2ptree :=
 clear;
 match goal with |- local2ptree ?A = _ => hnf_localdef_list A end;
 etransitivity;
 [unfold local2ptree, local2ptree_aux; simpl;
  repeat match goal with x := CLEAR_ME _ |- _ => unfold CLEAR_ME in x; subst x end;
  reflexivity |
  repeat match goal with x := CLEAR_ME _ |- _ => unfold CLEAR_ME in x; subst x end;
  apply f_equal;
  try reflexivity;
  match goal with |- ?L = _ => let x := grab_gvars L in instantiate(1:=x); reflexivity end
 ].

Goal exists x,  local2ptree (
      temp 1%positive Vundef
   :: temp 3%positive (Vint (Int.repr (3+4)))
   :: lvar 1%positive tint (Vint (Int.repr (1 + 2)))
   :: nil) = x.
set (Three := 3). (* This definition should not be unfolded! *)
set (T := temp 1%positive Vundef). (* This should be unfolded! *)
set (Q := (*tc_env empty_tycontext :: *) nil).  (* This should be unfolded! *)
eexists.
etransitivity.
prove_local2ptree.
match goal with |- context [1+2] => idtac end.
match goal with |- context [Three] => idtac end.
Abort.

Ltac construct_local2ptree Q H :=
  let t := fresh "t" in
  evar (t: (PTree.t val * PTree.t (type * val) * list Prop * option globals)%type);
  assert (H: local2ptree Q = t); subst t;
   [ prove_local2ptree | ].

Definition LocalD (T1: PTree.t val) (T2: PTree.t (type * val)) (Q: option globals) :=
  PTree.fold (fun Q i v => temp i v :: Q) T1
  (PTree.fold (fun Q i tv => match tv with (t, v) => lvar i t v end :: Q) T2
   match Q with Some gv => (gvars gv) :: nil | None => nil end).

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
Lemma PTree_elements_set: forall {A} i (v: A) elm T,
  In elm (PTree.elements (PTree.set i v T)) ->
  elm = (i, v) \/ In elm (PTree.elements T).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: or (@eq (prod positive A) elm (@pair positive A i v)) (@In (prod positive A) elm (@PTree.elements A T)) *)
  destruct elm as [i' v'].
(* Goal: or (@eq (prod positive A) (@pair positive A i' v') (@pair positive A i v)) (@In (prod positive A) (@pair positive A i' v') (@PTree.elements A T)) *)
  apply PTree.elements_complete in H.
(* Goal: or (@eq (prod positive A) (@pair positive A i' v') (@pair positive A i v)) (@In (prod positive A) (@pair positive A i' v') (@PTree.elements A T)) *)
  destruct (ident_eq i i').
  + subst.
(* Goal: or (@eq localdef (temp i v) (temp i v0)) (@In localdef (temp i v0) (LocalD (@PTree.remove val i T1) T2 Q)) *)
    rewrite PTree.gss in H.
(* Goal: Q0 rho *)
    inversion H.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
    subst.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
    left; auto.
  + rewrite PTree.gso in H by auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    right.
(* Goal: @In (prod ident val) (@pair ident val j w) (@PTree.elements val (@PTree.set val i v T1)) *)
    apply PTree.elements_correct.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    auto.
Qed.

Lemma LocalD_sound_temp:
  forall i v T1 T2 Q,
  PTree.get i T1 = Some v -> In (temp i v) (LocalD T1 T2 Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 unfold LocalD; intros.
 forget (PTree.fold (fun Q i tv => match tv with (t, v) => lvar i t v end :: Q) T2
          match Q with Some gv => (gvars gv) :: nil | None => nil end) as Q'.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
 rewrite !PTree.fold_spec, <- !fold_left_rev_right.
(* Goal: @In localdef (lvar j t v1) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) *)
 apply PTree.elements_correct in H.
(* Goal: @In localdef (lvar j t v1) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) *)
 rewrite in_rev in H.
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@rev (prod positive val) (@PTree.elements val T1))) *)
 forget (rev (PTree.elements T1)) as L.
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end L) *)
 induction L; intros; destruct H.
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@cons (prod positive (prod type val)) a L)) *)
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@cons (prod positive (prod type val)) a L)) *)
 subst a. left. reflexivity.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
 right. apply IHL. auto.
Qed.

Lemma LocalD_sound_local:
  forall i t v T1 T2 Q,
  PTree.get i T2 = Some (t, v) ->
   In (lvar i t v) (LocalD T1 T2 Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 unfold LocalD; intros.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
 rewrite !PTree.fold_spec, <- !fold_left_rev_right.
(* Goal: @In localdef (lvar j t v1) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) *)
 apply PTree.elements_correct in H.
(* Goal: @In localdef (lvar j t v1) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) *)
 rewrite in_rev in H.
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@rev (prod positive val) (@PTree.elements val T1))) *)
 forget (rev (PTree.elements T1)) as L.
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) L) *)
 induction L; [ | right; apply IHL].
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@nil (prod positive val))) *)
 forget (rev (PTree.elements T2)) as L.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
 simpl.
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end L) *)
 induction L; intros; destruct H.
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@cons (prod positive (prod type val)) a L)) *)
(* Goal: @In localdef (lvar i t v) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@cons (prod positive (prod type val)) a L)) *)
 subst a.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop P' P) (LOCALx (@app localdef (@nil localdef) (LocalD T1 T2 Q')) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
 left; reflexivity.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
 simpl.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
 destruct a as [ia vda]; destruct vda; simpl in *; auto.
Qed.

Lemma LocalD_sound_gvars:
  forall gv T1 T2 Q,
  Q = Some gv->
  In (gvars gv) (LocalD T1 T2 Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 unfold LocalD; intros.
(* Goal: @In localdef (gvars gv) (@PTree.fold val (list localdef) (fun (Q : list localdef) (i : positive) (v : val) => @cons localdef (temp i v) Q) T1 (@PTree.fold (prod type val) (list localdef) (fun (Q : list localdef) (i : positive) (tv : prod type val) => @cons localdef (let (t, v) := tv in lvar i t v) Q) T2 match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end)) *)
 subst Q.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
 rewrite !PTree.fold_spec, <- !fold_left_rev_right.
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@rev (prod positive val) (@PTree.elements val T1))) *)
 forget (rev (PTree.elements T1)) as L.
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) L) *)
 induction L; [ | right; apply IHL].
(* Goal: @In localdef (gvars gv) (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) (@cons localdef (gvars gv) (@nil localdef)) (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@nil (prod positive val))) *)
 forget (rev (PTree.elements T2)) as L.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
 simpl.
(* Goal: iff (@In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q L)) (or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) L)))) (@In localdef q Q)) *)
 induction L.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
 simpl; auto.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
 simpl.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
 destruct a as [ia vda]; destruct vda; simpl in *; auto.
Qed.

Lemma LocalD_sound: forall q T1 T2 Q,
  (exists i v, PTree.get i T1 = Some v /\ q = temp i v) \/
  (exists i t v, PTree.get i T2 = Some (t, v) /\ q = lvar i t v) \/
  (exists gv, Q = Some gv /\ q = gvars gv) ->
  In q (LocalD T1 T2 Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
intros.
repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
apply LocalD_sound_temp; auto.
(* Goal: @In localdef (lvar x x0 x1) (LocalD T1 T2 Q) *)
(* Goal: @In localdef (gvars x) (LocalD T1 T2 (@Some globals x)) *)
apply LocalD_sound_local with (T1:=T1) (T2:=T2)(Q:=Q) in H; intuition.
(* Goal: @In localdef (gvars x) (LocalD T1 T2 (@Some globals x)) *)
apply LocalD_sound_gvars with (T1:=T1) (T2:=T2); intuition.
Qed.

Lemma LocalD_complete : forall q T1 T2 Q,
  In q (LocalD T1 T2 Q) ->
  (exists i v, PTree.get i T1 = Some v /\ q = temp i v) \/
  (exists i t v, PTree.get i T2 = Some (t, v) /\ q = lvar i t v) \/
  (exists gv, Q = Some gv /\ q = gvars gv).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef q (temp i v))))) (or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv))))) *)
  unfold LocalD in H.
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef q (temp i v))))) (or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv))))) *)
  rewrite !PTree.fold_spec, <- !fold_left_rev_right in H.
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef q (temp i v))))) (or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv))))) *)
  remember (rev (PTree.elements T1)) as L.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  simpl in H.
  change L with (nil ++ L) in HeqL.
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef q (temp i v))))) (or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv))))) *)
  forget (@nil (positive * val)) as K.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  revert K HeqL; induction L; intros.
  + right.
(* Goal: or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv)))) *)
    clear K T1 HeqL.
(* Goal: or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv)))) *)
    remember (rev (PTree.elements T2)) as L.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
    simpl in H.
    change L with (nil ++ L) in HeqL.
(* Goal: or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv)))) *)
    forget (@nil (positive * (type * val))) as K.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
    revert K HeqL; induction L; intros.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    - repeat right.
(* Goal: @ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv))) *)
      destruct Q; simpl in H; [| inv H].
(* Goal: @ex globals (fun gv : globals => and (@eq (option globals) (@Some globals g) (@Some globals gv)) (@eq localdef q (gvars gv))) *)
      destruct H; [| tauto].
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      subst; eexists; eauto.
    - assert (In a (PTree.elements T2)).
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
      { rewrite in_rev, <- HeqL. rewrite in_app. right; left; auto. }
(* Goal: or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv)))) *)
      destruct a as [i [t v]].
(* Goal: @eq (option val) (@PTree.get val j (@PTree.set val i v T1)) (@Some val w) *)
      apply PTree.elements_complete in H0.
(* Goal: or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef q (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef q (gvars gv)))) *)
      destruct H; try subst q; eauto 50.
      specialize (IHL H (K ++ (i, (t, v)) :: nil));
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      rewrite app_ass in IHL; specialize (IHL HeqL); eauto.
  + destruct H.
    - subst q.
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef (temp (@fst positive val a) (@snd positive val a)) (temp i v))))) (or (@ex positive (fun i : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i T2) (@Some (prod type val) (@pair type val t v))) (@eq localdef (temp (@fst positive val a) (@snd positive val a)) (lvar i t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef (temp (@fst positive val a) (@snd positive val a)) (gvars gv))))) *)
      assert (In a (PTree.elements T1)).
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
      { rewrite in_rev, <- HeqL. rewrite in_app. right; left; auto. }
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      destruct a as [i v]; apply PTree.elements_complete in H; eauto.
    - destruct a as [i v].
      specialize (IHL H (K ++ (i,v)::nil)).
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      rewrite app_ass in IHL; specialize (IHL HeqL); eauto.
Qed.

Lemma in_temp_aux:
  forall q L Q,
    In q (fold_right
     (fun (y : positive * val) (x : list localdef) =>
      temp (fst y) (snd y) :: x) Q L) <->
    ((exists i v, q = temp i v /\ In (i,v) L) \/ In q Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 intros.
(* Goal: iff (@In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q L)) (or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) L)))) (@In localdef q Q)) *)
 induction L.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
 simpl. intuition. destruct H0 as [? [? [? ?]]]. contradiction.
(* Goal: iff (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa))) (or (@eq localdef (temp i v) Q0) (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD T1a T2a Qa)))) *)
 intuition.
(* Goal: or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (or (@eq (prod ident val) (@pair positive val a0 b) (@pair ident val i v)) (@In (prod ident val) (@pair ident val i v) L))))) (@In localdef q Q) *)
(* Goal: or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) (@pair positive val a0 b) L))))) (@In localdef q Q) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
  destruct H0. simpl in *. subst q.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  left. eauto.
(* Goal: or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) (@pair positive val a0 b) L))))) (@In localdef q Q) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
  specialize (H H0).
(* Goal: or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) (@pair positive val a0 b) L))))) (@In localdef q Q) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
(* Goal: @In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) (@pair positive val a0 b) L)) *)
  destruct H as [[? [? [? ?]]] | ?].
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  left. exists x, x0. split; auto. right; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  right; auto.
(* Goal: or (@ex positive (fun i0 : positive => @ex type (fun t0 : type => @ex val (fun v0 : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i0 (@PTree.set (prod type val) i (@pair type val t v) T2)) (@Some (prod type val) (@pair type val t0 v0))) (@eq localdef (lvar i t v) (lvar i0 t0 v0)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef (lvar i t v) (gvars gv)))) *)
  destruct H3 as [i [v [? ?]]]. destruct H3. inv H3. left. reflexivity.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  right; apply H1. eauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  right; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  right; auto.
Qed.

Lemma LOCALx_expand_temp_var  : forall i v T1 T2 Q Q0,
  In Q0 (LocalD (PTree.set i v T1) T2 Q) <->
  In Q0 (temp i v :: LocalD (PTree.remove i T1) T2 Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros; split; intros.
  + simpl.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
    apply LocalD_complete in H.
(* Goal: Q0 rho *)
    destruct H.
    - destruct H as [i0 [v0 [? ?]]].
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
      subst.
(* Goal: or (@eq localdef (temp i v) (temp i0 v0)) (@In localdef (temp i0 v0) (LocalD (@PTree.remove val i T1) T2 Q)) *)
      destruct (ident_eq i0 i).
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
      * subst.
(* Goal: or (@eq localdef (temp i v) (temp i v0)) (@In localdef (temp i v0) (LocalD (@PTree.remove val i T1) T2 Q)) *)
        rewrite PTree.gss in H.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
        inversion H; subst.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop P' P) (LOCALx (@app localdef (@nil localdef) (LocalD T1 T2 Q')) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
        left; reflexivity.
(* Goal: or (@eq localdef (let (t, v) := vd in lvar i t v) (lvar x x0 x1)) (@In localdef (lvar x x0 x1) (LocalD T1 (@PTree.remove (prod type val) i T2) Q)) *)
      * rewrite PTree.gso in H by auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
        right.
(* Goal: @In localdef (temp i v0) (LocalD T1a T2a Qa) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef (temp i v) Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD (@PTree.set val i v T1a) T2a Qa)) R)) *)
        apply LocalD_sound_temp.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
        rewrite PTree.gro by auto. auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    - right.
(* Goal: Q0 rho *)
      destruct H.
      * destruct H as [j [t [v1 [? ?]]]]; subst Q0.
(* Goal: @In localdef Q0 (LocalD (@PTree.remove val i T1) T2 Q) *)
        unfold LocalD.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
        rewrite !PTree.fold_spec, <- !fold_left_rev_right.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
        induction (rev (PTree.elements (PTree.remove i T1))); simpl.
       ++ apply PTree.elements_correct in H. rewrite in_rev in H.
          induction  (rev (PTree.elements T2)).
         -- inv H.
         -- destruct H.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
           ** destruct a. inv H. simpl. left; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
           ** simpl. destruct a as [? ?]; simpl; repeat right; auto.
       ++ right; apply IHl.
      * unfold LocalD.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
        rewrite !PTree.fold_spec, <- !fold_left_rev_right.
(* Goal: @In localdef Q0 (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) (@fold_right (list localdef) (prod positive (prod type val)) (fun (y : prod positive (prod type val)) (x : list localdef) => @cons localdef (let (t, v) := @snd positive (prod type val) y in lvar (@fst positive (prod type val) y) t v) x) match Q with | Some gv => @cons localdef (gvars gv) (@nil localdef) | None => @nil localdef end (@rev (prod positive (prod type val)) (@PTree.elements (prod type val) T2))) (@rev (prod positive val) (@PTree.elements val (@PTree.remove val i T1)))) *)
        destruct H as [gv [? ?]]; subst Q Q0.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
        induction (rev (PTree.elements (PTree.remove i T1))); simpl.
       ++ induction (rev (PTree.elements T2)); simpl; auto.
       ++ destruct a as [? ?]; simpl; repeat right; auto.
  + destruct H.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
    - subst.
(* Goal: @In localdef (temp i v0) (LocalD T1a T2a Qa) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef (temp i v) Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD (@PTree.set val i v T1a) T2a Qa)) R)) *)
      apply LocalD_sound_temp. apply PTree.gss.
    - unfold LocalD in *.
      rewrite !PTree.fold_spec, <- !fold_left_rev_right in *.
      forget  (fold_right (fun (y : positive * (type * val)) (x : list localdef) => (let (t, v0) := snd y in lvar (fst y) t v0) :: x)
        match Q with
        | Some gv => gvars gv :: nil
        | None => nil
        end (rev (PTree.elements T2))) as JJ.
      clear - H.
(* Goal: @In localdef Q0 (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) JJ (@rev (prod positive val) (@PTree.elements val (@PTree.set val i v T1)))) *)
      rewrite in_temp_aux. rewrite in_temp_aux in H.
(* Goal: or (@ex ident (fun i0 : ident => @ex val (fun v0 : val => and (@eq localdef Q0 (temp i0 v0)) (@In (prod ident val) (@pair ident val i0 v0) (@rev (prod positive val) (@PTree.elements val (@PTree.set val i v T1))))))) (@In localdef Q0 JJ) *)
      destruct H as [[j [w [? ?]]] |?].
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      * left; exists j,w; split; auto.
        rewrite <- in_rev in *.
(* Goal: @In (prod ident val) (@pair ident val j w) (@PTree.elements val (@PTree.set val i v T1)) *)
        apply PTree.elements_correct. apply PTree.elements_complete in H0.
        clear - H0.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
        destruct (ident_eq i j); subst.
       ++ rewrite PTree.grs in H0; inv H0.
       ++ rewrite PTree.gro in H0 by auto. rewrite PTree.gso; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      * right; auto.
Qed.

Lemma In_LocalD_remove_set :
   forall q T1 i vd T2 Q,
      In q (LocalD T1 (PTree.remove i T2) Q) ->
      In q (LocalD T1 (PTree.set i vd T2) Q).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 intros.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
 apply LocalD_sound.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
 apply LocalD_complete in H.
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
*
(* Goal: or (@ex positive (fun i : positive => @ex val (fun v : val => and (@eq (option val) (@PTree.get val i T1) (@Some val v)) (@eq localdef (temp x x0) (temp i v))))) (or (@ex positive (fun i0 : positive => @ex type (fun t : type => @ex val (fun v : val => and (@eq (option (prod type val)) (@PTree.get (prod type val) i0 (@PTree.set (prod type val) i vd T2)) (@Some (prod type val) (@pair type val t v))) (@eq localdef (temp x x0) (lvar i0 t v)))))) (@ex globals (fun gv : globals => and (@eq (option globals) Q (@Some globals gv)) (@eq localdef (temp x x0) (gvars gv))))) *)
 left; eauto 50.
*
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
 right; left. exists x,x0,x1. split; auto.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
 destruct (ident_eq i x). subst. rewrite PTree.grs in H; inv H.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
 rewrite PTree.gro in H by auto; rewrite PTree.gso by auto; auto.
*
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
 repeat right. exists x; split; auto.
Qed.

Lemma LOCALx_expand_vardesc : forall i vd T1 T2 Q Q0,
  In Q0 (LocalD T1 (PTree.set i vd T2) Q) <->
  In Q0 (match vd with (t, v) => lvar i t v end :: (LocalD T1 (PTree.remove i T2) Q)).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros; split; intros.
  + simpl.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
    apply LocalD_complete in H.
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
    -
      destruct vd; simpl;
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      repeat right; apply LocalD_sound_temp; auto.
    -
(* Goal: @eq (option val) (@PTree.get val x (@PTree.remove val i T1)) (@Some val x0) *)
      destruct (ident_eq i x).
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      * subst x;   rewrite PTree.gss in H; inv H. simpl. auto.
(* Goal: or (@eq localdef (let (t, v) := vd in lvar i t v) (lvar x x0 x1)) (@In localdef (lvar x x0 x1) (LocalD T1 (@PTree.remove (prod type val) i T2) Q)) *)
      * rewrite PTree.gso in H by auto.
         destruct vd; simpl;
        repeat right; apply LocalD_sound;
        right; left;
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
        exists x,x0,x1; rewrite PTree.gro by auto; auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    - right.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      apply LocalD_sound_gvars. auto.
 +
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
   destruct vd; simpl in H; destruct H; subst.
   -
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
      apply LocalD_sound.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
      right. left. exists i,t,v; split; auto. apply PTree.gss.
   -
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      apply In_LocalD_remove_set; auto.
Qed.

Lemma LOCALx_expand_gvars: forall T1 T2 gv Q0,
  In Q0 (LocalD T1 T2 (Some gv)) <->
  In Q0 (gvars gv ::LocalD T1 T2 None).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros; split; intros.
  + simpl.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
    apply LocalD_complete in H.
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    - right.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      apply LocalD_sound_temp; auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    - right.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
      apply LocalD_sound.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      right; left; repeat econstructor; eauto.
    -
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      inv H; auto.
+
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
    destruct H. subst. apply LocalD_sound_gvars. auto.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
    apply LocalD_complete in H.
(* Goal: @In localdef Q0 (LocalD T1 T2 (@Some globals gv)) *)
    apply LocalD_sound.
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    * do 0 right; left; repeat econstructor; eauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    * do 1 right; left; repeat econstructor; eauto.
    * inv H.
Qed.

Lemma LOCALx_shuffle_derives': forall P Q Q' R,
  (forall Q0, In Q0 Q' -> In Q0 Q) ->
  PROPx P (LOCALx Q R) |-- PROPx P (LOCALx Q' R).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (PROPx P (LOCALx Q' R)) *)
  induction Q'.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
  {
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (PROPx P (LOCALx (@nil localdef) R)) *)
    unfold PROPx, LOCALx.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
    normalize.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    apply andp_left2; auto.
  }
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (PROPx P (LOCALx (@cons localdef a Q') R)) *)
  pose proof (H a (or_introl _ eq_refl)).
  rewrite <- insert_local'.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
  apply andp_right.
  + clear -H0.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (local (locald_denote a)) *)
    induction Q; [inversion H0 |].
    rewrite <- insert_local'.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a0)) (PROPx P (LOCALx Q R))) (local (locald_denote a)) *)
    simpl in H0; inversion H0.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
    - subst.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (LOCALx Q R) (local (locald_denote Qn)) *)
      apply andp_left1.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (locald_denote a)) *)
      apply derives_refl.
    - apply andp_left2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (local (locald_denote a)) *)
      apply IHQ, H.
  + apply IHQ'.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
    intros.
(* Goal: @In localdef Q0 Q *)
    apply H.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
    simpl.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    right.
(* Goal: @In localdef Q0 Q' *)
    apply H1.
Qed.

Lemma LOCALx_shuffle_derives: forall P Q Q' R,
  (forall Q0, In Q0 Q' -> In Q0 Q) ->
  PROPx P (LOCALx Q (SEPx R)) |-- PROPx P (LOCALx Q' (SEPx R)).
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
Proof. intros. apply LOCALx_shuffle_derives'. auto. Qed.

Lemma LOCALx_shuffle': forall P Q Q' R,
  (forall Q0, In Q0 Q' <-> In Q0 Q) ->
  PROPx P (LOCALx Q R) = PROPx P (LOCALx Q' R).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  apply pred_ext; apply LOCALx_shuffle_derives'; intros; apply H; auto.
Qed.

Lemma LOCALx_shuffle: forall P Q Q' R,
  (forall Q0, In Q0 Q' <-> In Q0 Q) ->
  PROPx P (LOCALx Q (SEPx R)) = PROPx P (LOCALx Q' (SEPx R)).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  apply pred_ext; apply LOCALx_shuffle_derives; intros; apply H; auto.
Qed.

Lemma LocalD_remove_empty_from_PTree1: forall i T1 T2 Q Q0,
  T1 ! i = None ->
  (In Q0 (LocalD (PTree.remove i T1) T2 Q) <-> In Q0 (LocalD T1 T2 Q)).
Proof.
  intros until Q0; intro G; split; intros;
  apply LocalD_sound; apply LocalD_complete in H;
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
             end; subst.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
   - do 0 right; left. exists x,x0; split; auto.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
      destruct (ident_eq i x). subst. rewrite PTree.grs in H; inv H.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      rewrite PTree.gro in H; auto.
   - do 1 right; left. repeat eexists. eauto.
   - do 2 right. repeat eexists.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
   - do 0 right; left. exists x,x0; split; auto.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
      destruct (ident_eq i x). subst. congruence.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      rewrite PTree.gro; auto.
   - do 1 right; left. repeat eexists. eauto.
   - do 2 right. repeat eexists.
Qed.

Lemma LocalD_remove_empty_from_PTree2: forall i T1 T2 Q Q0,
  T2 ! i = None ->
  (In Q0 (LocalD T1 (PTree.remove i T2) Q) <-> In Q0 (LocalD T1 T2 Q)).
Proof.
  intros until Q0; intro G; split; intros;
  apply LocalD_sound; apply LocalD_complete in H;
    repeat match type of H with
             | _ \/ _ => destruct H
             | ex _ => destruct H
             | _ /\ _ => destruct H
             end; subst;
   try solve [left; repeat eexists; eauto] ;
   try solve [repeat right; auto];
     try (destruct (ident_eq i x);
           [try congruence; subst x; rewrite PTree.grs in H; inv H
           | try rewrite PTree.gro in H by auto]).
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  - do 1 right; left; repeat eexists; eauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  - do 2 right; repeat eexists; eauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  - do 1 right; left; repeat eexists; rewrite PTree.gro by auto; eauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  - do 2 right; repeat eexists; rewrite PTree.gro by auto; eauto.
Qed.

Lemma nth_error_local':
  forall n P Q R (Qn: localdef),
    nth_error Q n = Some Qn ->
    PROPx P (LOCALx Q R) |-- local (locald_denote Qn).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (LOCALx Q R) (local (locald_denote Qn)) *)
apply andp_left2. apply andp_left1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
go_lowerx. normalize.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@nil localdef) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
revert Q H H0; induction n; destruct Q; intros; inv H.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
destruct H0; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
destruct H0. apply (IHn Q); auto.
Qed.

Lemma in_local': forall Q0 P Q R, In Q0 Q ->
   PROPx P (LOCALx Q R) |-- local (locald_denote Q0).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
  destruct (in_nth_error _ _ H) as [?n ?H].
  eapply nth_error_local'.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  eauto.
Qed.

Lemma local2ptree_sound_aux: forall P Q R Q0 Q1 Q2,
  Q1 && local (locald_denote Q0) = Q2 && local (locald_denote Q0) ->
  In Q0 Q ->
  Q1 && PROPx P (LOCALx Q R) = Q2 && PROPx P (LOCALx Q R).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q1 (PROPx P (LOCALx Q R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q2 (PROPx P (LOCALx Q R))) *)
  pose proof in_local' _ P _ R H0.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q1 (PROPx P (LOCALx Q R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q2 (PROPx P (LOCALx Q R))) *)
  rewrite (add_andp _ _ H1).
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q1 (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (local (locald_denote Q0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q2 (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q R)) (local (locald_denote Q0)))) *)
  rewrite (andp_comm _ (local (locald_denote Q0))).
  rewrite <- !andp_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
  f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q1 (local (locald_denote Q0))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q2 (local (locald_denote Q0))) *)
  exact H.
Qed.

Lemma LOCALx_expand_vardesc': forall P R i vd T1 T2 Q,
  PROPx P (LOCALx (LocalD T1 (PTree.set i vd T2) Q) R) =
  PROPx P (LOCALx (match vd with (t,v) => lvar i t v end :: LocalD T1 (PTree.remove i T2) Q) R).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 intros.
(* Goal: @eq (forall _ : environ, mpred) (PROPx P (LOCALx (LocalD T1 T2 (@Some globals gv)) R)) (PROPx P (LOCALx (@cons localdef (gvars gv) (LocalD T1 T2 (@None globals))) R)) *)
 apply LOCALx_shuffle'; intro.
(* Goal: iff (@In localdef Q0 (@cons localdef (let (t, v) := vd in lvar i t v) (LocalD T1 (@PTree.remove (prod type val) i T2) Q))) (@In localdef Q0 (LocalD T1 (@PTree.set (prod type val) i vd T2) Q)) *)
 symmetry; apply LOCALx_expand_vardesc.
Qed.

Lemma LOCALx_expand_gvars': forall P R gv T1 T2,
  PROPx P (LOCALx (LocalD T1 T2 (Some gv)) R) =
  PROPx P (LOCALx (gvars gv :: LocalD T1 T2 None) R).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
 intros.
(* Goal: @eq (forall _ : environ, mpred) (PROPx P (LOCALx (LocalD T1 T2 (@Some globals gv)) R)) (PROPx P (LOCALx (@cons localdef (gvars gv) (LocalD T1 T2 (@None globals))) R)) *)
 apply LOCALx_shuffle'; intro.
(* Goal: iff (@In localdef Q0 (@cons localdef (gvars gv) (LocalD T1 T2 (@None globals)))) (@In localdef Q0 (LocalD T1 T2 (@Some globals gv))) *)
 symmetry; apply LOCALx_expand_gvars.
Qed.

Lemma local_equal_lemma :
 forall i t v t' v',
  local (locald_denote (lvar i t v)) && local (locald_denote (lvar i t' v')) =
  !!(v' = v) && !!(t'=t) && local (locald_denote (lvar i t' v')).
Proof.
(* Goal: forall g g0 : globals, @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (local (locald_denote (gvars g0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq globals g0 g)) (local (locald_denote (gvars g0)))) *)
intros; extensionality rho.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
unfold local, lift1; simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
normalize. f_equal. apply prop_ext.
(* Goal: iff (and (lvar_denote i t v rho) (lvar_denote i t' v' rho)) (and (@eq type t' t) (and (lvar_denote i t' v' rho) (@eq val v' v))) *)
unfold lvar_denote.
(* Goal: iff (and (@eq globals g (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end)) (@eq globals g0 (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end))) (and (@eq globals g0 g) (@eq globals g0 (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end))) *)
split; intros [? ?].
(* Goal: and (@eq type t' t) (and match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => and (@eq type t' ty') (@eq val v' (Vptr b Ptrofs.zero)) | None => False end (@eq val v' v)) *)
(* Goal: and match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => and (@eq type t ty') (@eq val v (Vptr b Ptrofs.zero)) | None => False end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => and (@eq type t' ty') (@eq val v' (Vptr b Ptrofs.zero)) | None => False end *)
hnf in H,H0.
(* Goal: @In localdef q Q *)
(* Goal: iff (@In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) a L))) (or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) a L))))) (@In localdef q Q)) *)
destruct (Map.get (ve_of rho) i) as [[? ?] | ] eqn:H8; try contradiction.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
destruct H, H0; subst.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
repeat split; auto.
(* Goal: @In localdef q Q *)
(* Goal: iff (@In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) a L))) (or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) a L))))) (@In localdef q Q)) *)
destruct (Map.get (ve_of rho) i) as [[? ?] | ] eqn:H8; try contradiction.
(* Goal: and (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) (and (@eq type t0 t0) (@eq val (Vptr b Ptrofs.zero) (Vptr b Ptrofs.zero))) *)
(* Goal: and False False *)
destruct H0 as [[? ?] ?]; subst. subst. repeat split; auto.
(* Goal: @In localdef q Q *)
(* Goal: iff (@In localdef q (@fold_right (list localdef) (prod positive val) (fun (y : prod positive val) (x : list localdef) => @cons localdef (temp (@fst positive val y) (@snd positive val y)) x) Q (@cons (prod positive val) a L))) (or (@ex ident (fun i : ident => @ex val (fun v : val => and (@eq localdef q (temp i v)) (@In (prod ident val) (@pair ident val i v) (@cons (prod positive val) a L))))) (@In localdef q Q)) *)
destruct H0; contradiction.
Qed.

Lemma gvars_equal_lemma :
  forall g g0,
  local (locald_denote (gvars g)) && local (locald_denote (gvars g0)) = !! (g0 = g) && local (locald_denote (gvars g0)).
Proof.
(* Goal: forall g g0 : globals, @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (local (locald_denote (gvars g0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq globals g0 g)) (local (locald_denote (gvars g0)))) *)
intros; extensionality rho.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
unfold local, lift1; simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
normalize. f_equal. apply prop_ext.
(* Goal: iff (and (gvars_denote g rho) (gvars_denote g0 rho)) (and (@eq globals g0 g) (gvars_denote g0 rho)) *)
unfold gvars_denote.
(* Goal: iff (and (@eq globals g (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end)) (@eq globals g0 (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end))) (and (@eq globals g0 g) (@eq globals g0 (fun i : ident => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end))) *)
split; intros [? ?].
+
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
subst; split; auto.
+
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
subst; split; auto.
Qed.

Lemma insert_locals:
  forall P A B C,
  local (fold_right `(and) `(True) (map locald_denote A)) && PROPx P (LOCALx B C) =
  PROPx P (LOCALx (A++B) C).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) (and : forall (_ : Prop) (_ : Prop), Prop)) (@liftx (LiftEnviron Prop) (True : Prop)) (@map localdef (forall _ : environ, Prop) locald_denote A))) (PROPx P (LOCALx B C))) (PROPx P (LOCALx (@app localdef A B) C)) *)
induction A.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
extensionality rho; simpl. unfold local, lift1. rewrite prop_true_andp by auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
auto.
simpl app. rewrite <- (insert_local' a).
rewrite <- IHA.
rewrite <- andp_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
f_equal.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
extensionality rho; simpl; unfold_lift; unfold local, lift1; simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
normalize.
Qed.

Lemma LOCALx_app_swap:
  forall A B, LOCALx (A++B) = LOCALx (B++A).
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
intros.
(* Goal: @eq (forall (_ : forall _ : environ, mpred) (_ : environ), mpred) (LOCALx (@app localdef A B)) (LOCALx (@app localdef B A)) *)
extensionality R rho; unfold LOCALx.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
simpl andp. cbv beta. f_equal.
(* Goal: @eq mpred (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote (@app localdef A B))) rho) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote (@app localdef B A))) rho) *)
rewrite !map_app.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
simpl map. unfold local,lift1. f_equal.
(* Goal: @eq Prop (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@app (forall _ : environ, Prop) (@map localdef (forall _ : environ, Prop) locald_denote A) (@map localdef (forall _ : environ, Prop) locald_denote B)) rho) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@app (forall _ : environ, Prop) (@map localdef (forall _ : environ, Prop) locald_denote B) (@map localdef (forall _ : environ, Prop) locald_denote A)) rho) *)
rewrite !fold_right_and_app.
(* Goal: iff (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa))) (or (@eq localdef (temp i v) Q0) (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD T1a T2a Qa)))) *)
apply prop_ext; intuition.
Qed.

Lemma local2ptree_soundness' : forall P Q R T1a T2a Pa Qa T1 T2 P' Q',
  local2ptree_aux Q T1a T2a Pa Qa = (T1, T2, P', Q') ->
  PROPx (Pa++P) (LOCALx (Q ++ LocalD T1a T2a Qa) R)
   = PROPx (P' ++ P) (LOCALx (LocalD T1 T2 Q') R).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : forall _ : environ, mpred) (T1a : PTree.t val) (T2a : PTree.t (prod type val)) (Pa : list Prop) (Qa : option globals) (T1 : PTree.t val) (T2 : PTree.t (prod type val)) (P' : list Prop) (Q' : option globals) (_ : @eq local_trees (local2ptree_aux Q T1a T2a Pa Qa) (@pair (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (@pair (prod (PTree.t val) (PTree.t (prod type val))) (list Prop) (@pair (PTree.t val) (PTree.t (prod type val)) T1 T2) P') Q')), @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  intros until R.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  induction Q; intros.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop P' P) (LOCALx (@app localdef (@nil localdef) (LocalD T1 T2 Q')) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  simpl in H. inv H. reflexivity.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  simpl in H.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  destruct a; simpl in H.
+
    destruct (T1a ! i) eqn:H8; inv H;
    rewrite <- (IHQ _ _ _ _ _ _ _ _ H1); clear H1 IHQ.
    simpl app. rewrite <- insert_prop.
    rewrite <- insert_local'.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (temp i v))) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD T1a T2a Qa)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val v v0)) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD T1a T2a Qa)) R))) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef (temp i v) Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop Pa P) (LOCALx (@app localdef Q (LocalD (@PTree.set val i v T1a) T2a Qa)) R)) *)
    apply local2ptree_sound_aux with (Q0 := temp i v0).
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
    extensionality rho. unfold locald_denote; simpl.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
    unfold local, lift1; unfold_lift; simpl. normalize.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
    f_equal. apply prop_ext; split.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    intros [? [? [? ?]]]; subst; split; auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    intros [? [? ?]]; subst; split; auto.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    rewrite in_app; right. apply LocalD_sound_temp. auto.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
    apply LOCALx_shuffle'; intros.
(* Goal: iff (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa))) (or (@eq localdef (temp i v) Q0) (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD T1a T2a Qa)))) *)
    simpl In. rewrite !in_app. simpl In. intuition.
(* Goal: or (@eq localdef (temp i v) Q0) (or (@In localdef Q0 Q) (@In localdef Q0 (LocalD T1a T2a Qa))) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
    apply LOCALx_expand_temp_var in H0. simpl In in H0.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    destruct H0; auto. right. right.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    apply LocalD_remove_empty_from_PTree1 in H; auto.
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
    right; apply LOCALx_expand_temp_var.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
(* Goal: or (@In localdef Q0 Q) (@In localdef Q0 (LocalD (@PTree.set val i v T1a) T2a Qa)) *)
    simpl. left; auto.
    right;  apply LOCALx_expand_temp_var.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
    simpl.
(* Goal: or (@eq localdef (temp i v) Q0) (@In localdef Q0 (LocalD (@PTree.remove val i T1a) T2a Qa)) *)
    right. apply (LocalD_remove_empty_from_PTree1 i T1a T2a Qa Q0 H8). auto.
  +
    destruct (T2a ! i) as [[?t ?v] |] eqn:H8; inv H;
    rewrite <- (IHQ _ _ _ _ _ _ _ _ H1); clear H1 IHQ;
    simpl app;
     rewrite  <- ?insert_prop, <- ?insert_local', <- ?andp_assoc;
    rewrite <- !insert_locals;
    forget (local (fold_right `(and) `(True) (map locald_denote Q))) as QQ;
    destruct (T2a ! i) as [ vd |  ] eqn:H9;
    try assert (H8 := LOCALx_expand_vardesc i vd T1 T2 Q');
    inv H8.
   -
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
     rewrite <- (PTree.gsident _ _ H9) by auto.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (lvar i t v))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a Qa) R))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a (@PTree.set (prod type val) i (@pair type val t v) T2a) Qa) R)) *)
     rewrite !LOCALx_expand_vardesc'.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (@cons localdef (gvars g) (LocalD T1a T2a (@None globals))) R))) *)
     simpl app.
     rewrite  <- ?insert_prop, <- ?insert_local', <- ?andp_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
     f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (local (locald_denote (gvars g0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq globals g0 g)) QQ) (local (locald_denote (gvars g0)))) *)
     rewrite !andp_assoc.
     rewrite !(andp_comm QQ). rewrite <- !andp_assoc. f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (lvar i t v))) (local (locald_denote (lvar i t0 v0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq val v0 v)) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq type t0 t))) (local (locald_denote (lvar i t0 v0)))) *)
     apply local_equal_lemma.
  -
     rewrite !(andp_comm QQ). rewrite <- !andp_assoc. f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (lvar i t v))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a Qa) R))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a (@PTree.set (prod type val) i (@pair type val t v) T2a) Qa) R)) *)
     rewrite !LOCALx_expand_vardesc'.
     rewrite <- !insert_local'.
     rewrite LOCALx_shuffle'
       with (Q:= LocalD T1a (PTree.remove i T2a) Qa)
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
              (Q':= LocalD T1a T2a Qa); auto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    intro; symmetry; apply (LocalD_remove_empty_from_PTree2); auto.
 + destruct Qa; rewrite <- (IHQ _ _ _ _ _ _ _ _ H); clear IHQ H;
   simpl app; rewrite <- ?insert_prop; rewrite <- insert_local', <- ?andp_assoc;
   rewrite <- !insert_locals;
   forget (local (fold_right `(and) `(True) (map locald_denote Q))) as QQ.
   - rewrite LOCALx_expand_gvars'.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (@cons localdef (gvars g) (LocalD T1a T2a (@None globals))) R))) *)
     simpl app.
     rewrite  <- ?insert_prop, <- ?insert_local', <- ?andp_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
     f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (local (locald_denote (gvars g0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq globals g0 g)) QQ) (local (locald_denote (gvars g0)))) *)
     rewrite !andp_assoc.
     rewrite !(andp_comm QQ). rewrite <- !andp_assoc. f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (local (locald_denote (gvars g0)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq globals g0 g)) (local (locald_denote (gvars g0)))) *)
     apply gvars_equal_lemma.
   - rewrite LOCALx_expand_gvars'.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (PROPx (@app Prop Pa P) (LOCALx (@cons localdef (gvars g) (LocalD T1a T2a (@None globals))) R))) *)
     simpl app.
     rewrite  <- ?insert_prop, <- ?insert_local', <- ?andp_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) (PROPx (@app Prop Pa P) (LOCALx (LocalD T1a T2a (@None globals)) R))) *)
     f_equal.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote (gvars g))) QQ) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) QQ (local (locald_denote (gvars g)))) *)
     apply andp_comm.
Qed.

Lemma local2ptree_soundness  : forall P Q R T1 T2 P' Q',
  local2ptree Q = (T1, T2, P', Q') ->
  PROPx P (LOCALx Q (SEPx R)) = PROPx (P' ++ P) (LOCALx (LocalD T1 T2 Q') (SEPx R)).
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
Proof. intros. eapply local2ptree_soundness' in H.
   etransitivity; [ | apply H]. clear H.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
   simpl.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
   unfold LocalD. rewrite !PTree.fold_spec. simpl. rewrite <- app_nil_end; auto.
Qed.

Lemma local2ptree_soundness'' : forall Q T1 T2 gv,
  local2ptree Q = (T1, T2, nil, Some gv) ->
  LOCALx Q TT = LOCALx (LocalD T1 T2 (Some gv)) TT.
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
  eapply local2ptree_soundness in H.
  match goal with |- LOCALx _ ?B = _ =>
    replace B with (SEPx(TT::nil))
  end.
  instantiate (2:=@nil Prop) in H.
  simpl app in H.
  unfold PROPx in H.
  simpl fold_right in H.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  rewrite !prop_true_andp in H by auto. apply H.
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop P' P) (LOCALx (@app localdef (@nil localdef) (LocalD T1 T2 Q')) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
(* Goal: @eq (forall _ : environ, mpred) (PROPx (@app Prop Pa P) (LOCALx (@app localdef (@cons localdef a Q) (LocalD T1a T2a Qa)) R)) (PROPx (@app Prop P' P) (LOCALx (LocalD T1 T2 Q') R)) *)
  extensionality rho; unfold SEPx; simpl. rewrite sepcon_emp. reflexivity.
Qed.

Lemma local_ext: forall Q0 Q rho, In Q0 Q -> fold_right `(and) `(True) Q rho -> Q0 rho.
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) (and : forall (_ : Prop) (_ : Prop), Prop)) (@liftx (LiftEnviron Prop) (True : Prop)) Q rho *)
  induction Q.
  + inversion H.
  + destruct H.
    - subst; simpl in H0; unfold_lift in H0.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      tauto.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    - apply IHQ; auto.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) Q rho *)
      unfold_lift in H0.
(* Goal: @derives mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))) rho) (@liftx (LiftEnviron mpred) (func_ptr fs (gv id)) rho) *)
      unfold_lift.
(* Goal: @fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (fun (x x0 : forall _ : environ, Prop) (x1 : environ) => and (x x1) (x0 x1)) (fun _ : environ => True) Q rho *)
      simpl in H0.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      tauto.
Qed.

Lemma local_ext_rev: forall (Q: list (environ -> Prop)) rho, (forall Q0, In Q0 Q -> Q0 rho) -> fold_right `(and) `(True) Q rho.
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
  intros.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) (and : forall (_ : Prop) (_ : Prop), Prop)) (@liftx (LiftEnviron Prop) (True : Prop)) Q rho *)
  induction Q.
  + simpl; auto.
  + simpl.
(* Goal: @liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and a (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) Q) rho *)
    split.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
    - apply H; simpl; auto.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
    - apply IHQ; intros.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
      apply H; simpl; auto.
Qed.

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
Fixpoint explicit_cast_exprlist (et: list type) (el: list expr) {struct et} : list expr :=
 match et, el with
 | t::et', e::el' => Ecast e t :: explicit_cast_exprlist et' el'
 | _, _ => nil
 end.

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
Fixpoint force_list {A} (al: list (option A)) : option (list A) :=
 match al with
 | Some a :: al' => match force_list al' with Some bl => Some (a::bl) | _ => None end
 | nil => Some nil
 | _ => None
 end.

Lemma make_func_ptr:
 forall id (Espec: OracleKind) (CS: compspecs) Delta P Q R fs gv p c Post,
   (var_types Delta) ! id = None ->
   (glob_specs Delta) ! id = Some fs ->
   (glob_types Delta) ! id = Some (type_of_funspec fs) ->
   snd (local2ptree Q) = Some gv /\ gv id = p ->
  semax Delta (PROPx P (LOCALx Q (SEPx (func_ptr' fs p :: R)))) c Post ->
  semax Delta (PROPx P (LOCALx Q (SEPx R))) c Post.
Proof.
(* Goal: forall (id : positive) (Espec : OracleKind) (CS : compspecs) (Delta : tycontext) (P : list Prop) (Q : list localdef) (R : list mpred) (fs : funspec) (gv : globals) (p : val) (c : statement) (Post : ret_assert) (_ : @eq (option type) (@PTree.get type id (var_types Delta)) (@None type)) (_ : @eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs)) (_ : @eq (option type) (@PTree.get type id (glob_types Delta)) (@Some type (type_of_funspec fs))) (_ : and (@eq (option globals) (@snd (prod (prod (PTree.t val) (PTree.t (prod type val))) (list Prop)) (option globals) (local2ptree Q)) (@Some globals gv)) (@eq val (gv id) p)) (_ : semax CS Espec Delta (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) c Post), semax CS Espec Delta (PROPx P (LOCALx Q (SEPx R))) c Post *)
intros.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
apply (semax_fun_id id fs Delta); auto.
(* Goal: semax CS Espec Delta (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) c Post *)
eapply semax_pre; try apply H3. clear H3.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
destruct (local2ptree Q) as [[[? ?] ?] ?] eqn:?.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
simpl in H2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
destruct H2 as [H3 H2']; subst o.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
pose proof (local2ptree_soundness P Q R t t0 l _ Heqp0) as H3.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
pose proof LocalD_sound_gvars gv t t0 _ eq_refl as H2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
forget (LocalD t t0 (Some gv)) as Q'.
assert (local (tc_environ Delta) |-- fun rho => !! (Map.get (ve_of rho) id = None)) as TC.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (PROPx P (LOCALx Q (SEPx (@cons mpred (func_ptr' fs p) R)))) *)
{
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) (@liftx (LiftEnviron mpred) (func_ptr fs (gv id))) *)
  intro rho.
(* Goal: @derives mpred Nveric (local (tc_environ Delta) rho) (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) *)
  unfold local, lift1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
  normalize.
(* Goal: @eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)) *)
  destruct H4 as [_ [? _]].
(* Goal: @eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)) *)
  specialize (H4 id).
(* Goal: @eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)) *)
  rewrite H in H4.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
  destruct (Map.get (ve_of rho) id) as [[? ?] |]; auto.
(* Goal: @eq (option (prod block type)) (@Some (prod block type) (@pair block type b t1)) (@None (prod block type)) *)
  specialize (H4 t1).
(* Goal: @eq (option (prod block type)) (@Some (prod block type) (@pair block type b t1)) (@None (prod block type)) *)
  destruct H4 as [_ ?].
(* Goal: @eq (option (prod block type)) (@Some (prod block type) (@pair block type b t1)) (@None (prod block type)) *)
  specialize (H4 (ex_intro _ b eq_refl)).
(* Goal: @eq (option (prod block type)) (@Some (prod block type) (@pair block type b t1)) (@None (prod block type)) *)
  inv H4.
}
clear - H2 H2' H3 TC.
rewrite <- insert_SEP.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (@sepcon (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) (func_ptr' fs p)) (PROPx P (LOCALx Q (SEPx R)))) *)
unfold func_ptr'.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
normalize.
rewrite corable_andp_sepcon1
  by (unfold_lift; simpl; intros; apply corable_func_ptr).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@liftx (LiftEnviron mpred) (func_ptr fs p)) (@sepcon (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) (@emp mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R))))) *)
apply andp_right; [ | apply andp_left2; apply andp_left1; normalize].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (PROPx P (LOCALx Q (SEPx R))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs))))) (@liftx (LiftEnviron mpred) (func_ptr fs p)) *)
rewrite H3.
rewrite <- andp_assoc.
rewrite (add_andp _ _ (in_local _ Delta (l ++ P) _ (SEPx R) H2)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@app Prop l P) (LOCALx Q' (SEPx R)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) (@liftx (LiftEnviron mpred) (func_ptr fs p)) *)
rewrite (add_andp _ _ TC).
apply derives_trans with ((fun rho : environ => !! (Map.get (ve_of rho) id = None)) &&
local (locald_denote (gvars gv)) && (` (func_ptr fs)) (eval_var id (type_of_funspec fs))); [solve_andp |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) (@liftx (LiftEnviron mpred) (func_ptr fs p)) *)
subst p.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) (@liftx (LiftEnviron mpred) (func_ptr fs (gv id))) *)
clear.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (fun rho : environ => @prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (local (locald_denote (gvars gv)))) (@liftx (Tarrow val (LiftEnviron mpred)) (func_ptr fs) (eval_var id (type_of_funspec fs)))) (@liftx (LiftEnviron mpred) (func_ptr fs (gv id))) *)
intro rho.
(* Goal: @fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@cons (forall _ : environ, Prop) a Q) rho *)
unfold_lift. unfold local, lift1; simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (option (prod block type)) (@Map.get (prod block type) (ve_of rho) id) (@None (prod block type)))) (@prop mpred Nveric (gvars_denote gv rho))) (func_ptr fs (eval_var id (type_of_funspec fs) rho))) (func_ptr fs (gv id)) *)
normalize.
(* Goal: @derives mpred Nveric (func_ptr fs (eval_var id (type_of_funspec fs) rho)) (func_ptr fs (gv id)) *)
unfold eval_var.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get (prod block type) (ve_of rho) id with | Some (pair b ty' as p) => if eqb_type (type_of_funspec fs) ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end end) (func_ptr fs (gv id)) *)
hnf in H0.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get (prod block type) (ve_of rho) id with | Some (pair b ty' as p) => if eqb_type (type_of_funspec fs) ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end end) (func_ptr fs (gv id)) *)
subst gv.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get (prod block type) (ve_of rho) id with | Some (pair b ty' as p) => if eqb_type (type_of_funspec fs) ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
rewrite H.
(* Goal: @derives mpred Nveric (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) (func_ptr fs match @Map.get block (ge_of rho) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end) *)
auto.
Qed.
