From compcert Require Export Clightdefs.
Require Export VST.veric.SeparationLogic.
Require Export VST.msl.Extensionality.
Require Export compcert.lib.Coqlib.
Require Export VST.msl.Coqlib2 VST.veric.coqlib4 VST.floyd.coqlib3.
Require Import VST.floyd.val_lemmas.
Local Open Scope logic.

Ltac _destruct_var_types i Heq_vt Heq_ve t b ::=
  let HH := fresh "H" in
  match goal with
  | H: typecheck_var_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_var_types___instead _ _ H i as HH
  | H: typecheck_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_var_types___instead _ _ (proj1 (proj2 H)) i as HH
  | H: tc_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_var_types___instead _ _ (proj1 (proj2 H)) i as HH
  end;
  match type of HH with
  | match ?o with _ => _ end =>
      match goal with
      | H: o = Some _ |- _ =>
          rewrite H in HH
      | H: Some _ = o |- _ =>
          rewrite <- H in HH
      | H: o = None |- _ =>
          rewrite H in HH
      | H: None = o |- _ =>
          rewrite <- H in HH
      | _ =>
          let HH' := fresh "H" in
          pose proof eq_refl o as HH';
          destruct o as [t |] in HH, HH' at 2;
          pose proof HH' as Heq_vt; clear HH'
      end
  end;
  match type of HH with
  | ex _ =>
      pose proof HH as [b Heq_ve]
  | _ =>
      pose proof HH as Heq_ve
  end;
  clear HH.

Ltac _destruct_glob_types i Heq_gt Heq_ge t b ::=
  let HH := fresh "H" in
  match goal with
  | H: typecheck_glob_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_glob_types___instead _ _ H i as HH
  | H: typecheck_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_glob_types___instead _ _ (proj2 (proj2 H)) i as HH
  | H: tc_environ _ _ |- _ =>
      pose proof WARNING___________you_should_use_tactic___destruct_glob_types___instead _ _ (proj2 (proj2 H)) i as HH
  end;
  match type of HH with
  | match ?o with _ => _ end =>
      match goal with
      | H: o = Some _ |- _ =>
          rewrite H in HH
      | H: Some _ = o |- _ =>
          rewrite <- H in HH
      | H: o = None |- _ =>
          rewrite H in HH
      | H: None = o |- _ =>
          rewrite <- H in HH
      | _ =>
          let HH' := fresh "H" in
          pose proof eq_refl o as HH';
          destruct o as [t |] in HH, HH' at 2;
          pose proof HH' as Heq_gt; clear HH'
      end
  end;
  match type of HH with
  | ex _ =>
      pose proof HH as [b Heq_ge]
  | _ =>
      idtac
  end;
  clear HH.

(* no "semax" in this file, just assertions. *)
Global Transparent Int.repr.
Global Transparent Ptrofs.repr.

Definition loop1x_ret_assert (Inv : environ -> mpred) (R : ret_assert) :=
  {| RA_normal := Inv; RA_break := FF; RA_continue := Inv; RA_return := R.(RA_return) |}.

Lemma loop1x_ret_assert_EK_normal:
 forall Inv R, RA_normal (loop1x_ret_assert Inv R) = Inv.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite loop1x_ret_assert_EK_normal: ret_assert.


Definition loop1y_ret_assert (Inv : environ -> mpred) :=
  {| RA_normal := Inv; RA_break := FF; RA_continue := Inv; RA_return := FF |}.

Definition for_ret_assert (I: environ->mpred) (Post: ret_assert) :=
 match Post with 
  {| RA_normal := _; RA_break := _; RA_continue := _; RA_return := r |} =>
  {| RA_normal := I; RA_break := FF; RA_continue := I; RA_return := r |}
 end.

Ltac simpl_ret_assert := 
 cbn [RA_normal RA_break RA_continue RA_return 
      normal_ret_assert overridePost loop1_ret_assert
      loop2_ret_assert function_body_ret_assert frame_ret_assert
      switch_ret_assert loop1x_ret_assert loop1y_ret_assert
      for_ret_assert loop_nocontinue_ret_assert].

Lemma RA_normal_loop2_ret_assert: (* MOVE TO assert_lemmas *)
  forall Inv R, RA_normal (loop2_ret_assert Inv R) = Inv.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. destruct R; reflexivity. Qed.
Hint Rewrite RA_normal_loop2_ret_assert : ret_assert.

Lemma liftTrue: forall rho, `True rho.
Proof. intro. unfold_lift; apply Coq.Init.Logic.I. Qed.
Hint Resolve liftTrue.

Lemma overridePost_normal:
  forall P Q, overridePost P (normal_ret_assert Q) = normal_ret_assert P.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
reflexivity.
Qed.

Lemma frame_normal:
  forall P F,
   frame_ret_assert (normal_ret_assert P) F = normal_ret_assert (P * F).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq ret_assert (frame_ret_assert (normal_ret_assert P) F) (normal_ret_assert (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P F)) *)
unfold normal_ret_assert; simpl.
(* Goal: @eq ret_assert (Build_ret_assert (fun rho : environ => @sepcon mpred Nveric Sveric (Q rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (RA_normal rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (@prop mpred Nveric False) (F rho)) (fun (vl : option val) (rho : environ) => @sepcon mpred Nveric Sveric (RA_return vl rho) (F rho))) (Build_ret_assert (fun rho : environ => @sepcon mpred Nveric Sveric (Q rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (RA_normal rho) (F rho)) (fun _ : environ => @prop mpred Nveric False) (fun (vl : option val) (rho : environ) => @sepcon mpred Nveric Sveric (RA_return vl rho) (F rho))) *)
f_equal; try solve [extensionality rho; normalize].
(* Goal: @eq (forall (_ : option val) (_ : environ), mpred) (fun (_ : option val) (rho : environ) => @sepcon mpred Nveric Sveric (@prop mpred Nveric False) (F rho)) (fun (_ : option val) (_ : environ) => @prop mpred Nveric False) *)
extensionality vl rho; normalize.
Qed.

Lemma frame_for1:
  forall Q R F,
   frame_ret_assert (loop1_ret_assert Q R) F =
   loop1_ret_assert (Q * F) (frame_ret_assert R F).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq ret_assert (frame_ret_assert (loop1_ret_assert Q R) F) (loop1_ret_assert (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) Q F) (frame_ret_assert R F)) *)
destruct R; simpl; normalize.
Qed.

Lemma frame_loop1:
  forall Q R F,
   frame_ret_assert (loop2_ret_assert Q R) F =
   loop2_ret_assert (Q * F) (frame_ret_assert R F).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq ret_assert (frame_ret_assert (loop2_ret_assert Q R) F) (loop2_ret_assert (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) Q F) (frame_ret_assert R F)) *)
destruct R; simpl.
(* Goal: @eq ret_assert (Build_ret_assert (fun rho : environ => @sepcon mpred Nveric Sveric (Q rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (RA_normal rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (@prop mpred Nveric False) (F rho)) (fun (vl : option val) (rho : environ) => @sepcon mpred Nveric Sveric (RA_return vl rho) (F rho))) (Build_ret_assert (fun rho : environ => @sepcon mpred Nveric Sveric (Q rho) (F rho)) (fun rho : environ => @sepcon mpred Nveric Sveric (RA_normal rho) (F rho)) (fun _ : environ => @prop mpred Nveric False) (fun (vl : option val) (rho : environ) => @sepcon mpred Nveric Sveric (RA_return vl rho) (F rho))) *)
f_equal; try solve [extensionality rho; normalize].
Qed.


Hint Rewrite frame_normal frame_for1 frame_loop1
                 overridePost_normal: ret_assert.
Hint Resolve @TT_right.

Lemma overridePost_overridePost:
 forall P Q R, overridePost P (overridePost Q R) = overridePost P R.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
destruct R; reflexivity.
Qed.
Hint Rewrite overridePost_overridePost : ret_assert.

Lemma overridePost_normal':
  forall P R, RA_normal (overridePost P R) = P.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
 intros. destruct R; reflexivity. 
Qed.
Hint Rewrite overridePost_normal' : ret_assert.

Lemma liftx_id:
    forall {T} e, @liftx (Tarrow T (LiftEnviron T)) (fun v => v) e = e.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
 intros. extensionality rho; simpl; auto.
Qed.
Hint Rewrite @liftx_id : norm2.

Lemma liftx3_liftx2:
 forall {A1 A2 A3 B} f (x: A1),
  @liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f (@liftx (LiftEnviron A1) x) =
  @liftx (Tarrow A2 (Tarrow A3 (LiftEnviron B))) (f x).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.

Lemma liftx2_liftx1:
 forall {A1 A2 B} f (x: A1),
  @liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f (@liftx (LiftEnviron A1) x) =
  @liftx (Tarrow A2 (LiftEnviron B)) (f x).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.

Lemma liftx1_liftx0:
  forall {A1 B} f (x: A1),
  @liftx (Tarrow A1 (LiftEnviron B)) f (@liftx (LiftEnviron A1) x) =
  @liftx (LiftEnviron B) (f x).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.

Hint Rewrite @liftx3_liftx2 @liftx2_liftx1 @liftx1_liftx0 : norm2.

Lemma lift1_lift0:
 forall {A1 B} (f: A1 -> B) (x: A1), lift1 f (lift0 x) = lift0 (f x).
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
intros. extensionality rho; reflexivity.
Qed.
Hint Rewrite @lift1_lift0 : norm2.

Lemma const_liftx0:
  forall B (P: B), (fun _ : environ => P) = `P.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite const_liftx0 : norm2.

Lemma lift_identity:
  forall A f, `(fun v: A => v) f = f.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. intros. reflexivity. Qed.
Hint Rewrite lift_identity : norm2.

Lemma tc_eval_gvar_zero:
  forall Delta t i rho, tc_environ Delta rho ->
            (var_types Delta) ! i = None ->
            (glob_types Delta) ! i = Some t ->
            exists b, eval_var i t rho = Vptr b Ptrofs.zero.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
 intros. unfold eval_var; simpl.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 destruct_var_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 destruct_glob_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 rewrite Heqo0, Heqo1.
(* Goal: @ex block (fun b0 : block => and (@eq val (Vptr b Ptrofs.zero) (Vptr b0 Ptrofs.zero)) (@eq (option block) (@Some block b) (@Some block b0))) *)
 eauto.
Qed.

Lemma tc_eval_gvar_i:
  forall Delta t i rho, tc_environ Delta rho ->
            (var_types Delta) ! i = None ->
            (glob_types Delta) ! i = Some t ->
             tc_val (Tpointer t noattr) (eval_var i t rho).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
 intros.
(* Goal: tc_val (Tpointer t noattr) (eval_var i t rho) *)
 red.
(* Goal: (if eqb_type (Tpointer t noattr) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (eval_var i t rho) *)
 destruct (tc_eval_gvar_zero _ _ _ _ H H0 H1) as [b ?].
(* Goal: (if eqb_type (Tpointer t noattr) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) (eval_var i t rho) *)
 rewrite H2.  destruct (eqb_type _ _); apply Coq.Init.Logic.I.
Qed.

Lemma local_lift2_and: forall P Q, local (`and P Q) =
        local P && local Q.
(* Goal: forall (P : forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (Q : forall _ : lift_S (LiftEnviron Prop), Prop), @eq (forall _ : environ, mpred) (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and P Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local P) (local Q)) *)
Proof. intros; extensionality rho. unfold local; super_unfold_lift.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @eq mpred (@prop mpred Nveric (and (P rho) (Q rho))) (@andp mpred Nveric (@prop mpred Nveric (P rho)) (@prop mpred Nveric (Q rho))) *)
 apply pred_ext; normalize. destruct H; normalize.
Qed.
Hint Rewrite local_lift2_and : norm2.

Lemma subst_TT {A}{NA: NatDed A}: forall i v, subst i v TT = TT.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
intros. extensionality rho; reflexivity.
Qed.

Lemma subst_FF {A}{NA: NatDed A}: forall i v, subst i v FF = FF.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
intros. extensionality rho; reflexivity.
Qed.
Hint Rewrite @subst_TT @subst_FF: subst.
Hint Rewrite (@subst_TT mpred Nveric) (@subst_FF mpred Nveric): subst.

Lemma subst_sepcon: forall i v (P Q: environ->mpred),
  subst i v (P * Q) = (subst i v P * subst i v Q).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite subst_sepcon : subst.

Lemma subst_wand: forall i v (P Q: environ->mpred),
  subst i v (P -* Q) = (subst i v P -* subst i v Q).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite subst_wand : subst.

Lemma subst_exp:
  forall (A B: Type) (NA : NatDed A) (a : ident) (v : environ -> val) (P: B -> environ -> A),
    subst a v (EX b: B, P b) = EX b: B, subst a v (P b).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. intros; reflexivity. Qed.

Lemma env_set_env_set: forall id v1 v2 rho, env_set (env_set rho id v1) id v2 = env_set rho id v2.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @eq environ (env_set (env_set rho i (v1 rho)) i (v (env_set rho i (v1 rho)))) (env_set rho i (v (env_set rho i (v1 rho)))) *)
  unfold env_set.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  f_equal.
(* Goal: @eq (Map.t val) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho))))) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) *)
  apply Map.ext. intro j.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  destruct (eq_dec id j). subst. repeat rewrite Map.gss. f_equal.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
  simpl.
(* Goal: @eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (@Map.set val i (v1 rho) (te_of rho))) j) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) j) *)
  repeat rewrite Map.gso by auto. auto.
Qed.

Lemma env_set_eval_id: forall id rho Delta t,
  tc_environ Delta rho ->
  (temp_types Delta) ! id = Some t ->
  env_set rho id (eval_id id rho) = rho.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @eq environ (env_set rho id (eval_id id rho)) rho *)
  destruct H as [? _].
(* Goal: @eq environ (env_set rho id (eval_id id rho)) rho *)
  specialize (H _ _ H0).
(* Goal: @eq environ (env_set rho id (eval_id id rho)) rho *)
  destruct H as [? [? ?]].
(* Goal: @eq environ (env_set rho id (eval_id id rho)) rho *)
  unfold eval_id, env_set, force_val.
(* Goal: tc_environ Delta (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v rho) (te_of rho))) *)
  destruct rho; simpl in *.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  f_equal.
(* Goal: @eq (Map.t val) (@Map.set val id match @Map.get val te id with | Some v' => v' | None => Vundef end te) te *)
  rewrite H.
(* Goal: @eq (Map.t val) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho))))) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) *)
  apply Map.ext.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @eq (option val) (@Map.get val (@Map.set val id x te) x0) (@Map.get val te x0) *)
  destruct (Pos.eq_dec id x0).
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  - subst.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    rewrite Map.gss; auto.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  - rewrite Map.gso; auto.
Qed.

Lemma resubst: forall {A} i (v v1: val) (e: environ -> A), subst i (`v1) (subst i `(v) e) = subst i `(v) e.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
 intros. extensionality rho. unfold subst.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 f_equal.
(* Goal: @eq environ (env_set (env_set rho i (v1 rho)) i (v (env_set rho i (v1 rho)))) (env_set rho i (v (env_set rho i (v1 rho)))) *)
 unfold env_set.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 f_equal.
(* Goal: @eq (Map.t val) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho))))) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) *)
 apply Map.ext. intro j.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 destruct (eq_dec i j). subst. repeat rewrite Map.gss. f_equal.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
 simpl.
(* Goal: @eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (@Map.set val i (v1 rho) (te_of rho))) j) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) j) *)
 repeat rewrite Map.gso by auto. auto.
Qed.

(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite @resubst : subst.

Lemma resubst_full: forall {A} i (v: environ -> val) v1 (e: environ -> A), subst i v1 (subst i v e) = subst i (subst i v1 v) e.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  extensionality rho. unfold subst.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 f_equal.
(* Goal: @eq environ (env_set (env_set rho i (v1 rho)) i (v (env_set rho i (v1 rho)))) (env_set rho i (v (env_set rho i (v1 rho)))) *)
 unfold env_set.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 f_equal.
(* Goal: @eq (Map.t val) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho))))) (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) *)
 apply Map.ext. intro j.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
 destruct (eq_dec i j). subst. repeat rewrite Map.gss. f_equal.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
 simpl.
(* Goal: @eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (@Map.set val i (v1 rho) (te_of rho))) j) (@Map.get val (@Map.set val i (v (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v1 rho) (te_of rho)))) (te_of rho)) j) *)
 repeat rewrite Map.gso by auto. auto.
Qed.

Lemma subst_ewand: forall i v (P Q: environ->mpred),
  subst i v (ewand P Q) = ewand (subst i v P) (subst i v Q).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite subst_ewand : subst.

Lemma subst_andp {A}{NA: NatDed A}:
  forall id v (P Q: environ-> A), subst id v (P && Q) = subst id v P && subst id v Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
extensionality rho; unfold subst; simpl.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
auto.
Qed.

Lemma subst_prop {A}{NA: NatDed A}: forall i v P,
    subst i v (prop P) = prop P.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
intros; reflexivity.
Qed.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite @subst_andp subst_prop : subst.

Lemma eval_expr_Econst_int: forall {cs: compspecs}  i t, eval_expr (Econst_int i t) = `(Vint i).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite @eval_expr_Econst_int : eval.

Lemma subst_eval_var:
  forall id v id' t, subst id v (eval_var id' t) = eval_var id' t.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros. unfold subst, eval_var. extensionality rho.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl. auto.
Qed.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite subst_eval_var : subst.

Lemma subst_local: forall id v P,
  subst id v (local P) = local (subst id v P).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite subst_local : subst.

Lemma eval_lvalue_Ederef:
  forall {cs: compspecs}  e t, eval_lvalue (Ederef e t) = eval_expr e.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite @eval_lvalue_Ederef : eval.

Lemma local_lift0_True:     local (`True) = TT.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite local_lift0_True : norm2.

Lemma overridePost_EK_return:
  forall Q P, RA_return (overridePost Q P) = RA_return P.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
 destruct P; reflexivity.
Qed.
Hint Rewrite overridePost_EK_return : ret_assert.

Lemma frame_ret_assert_emp:
  forall P, frame_ret_assert P emp = P.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
Proof. intros.
(* Goal: @eq ret_assert (frame_ret_assert P (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric))) P *)
 destruct P; simpl; f_equal; extensionality; try extensionality; normalize.
Qed.

(*Hint Rewrite frame_ret_assert_emp : ret_assert.*)

Lemma frame_ret_assert_EK_return:
 forall P Q vl, RA_return (frame_ret_assert P Q) vl =  RA_return P vl * Q.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
 destruct P; simpl; reflexivity.
Qed.
Hint Rewrite frame_ret_assert_EK_return : ret_assert.

Lemma function_body_ret_assert_EK_return:
  forall t P vl, RA_return (function_body_ret_assert t P) vl = bind_ret vl t P.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite function_body_ret_assert_EK_return : ret_assert.

Lemma bind_ret1_unfold:
  forall v t Q, bind_ret (Some v) t Q = !!tc_val t v && `Q (make_args (ret_temp :: nil)(v::nil)).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite bind_ret1_unfold : norm2.

Lemma bind_ret1_unfold':
  forall v t Q rho,
  bind_ret (Some v) t Q rho = !!(tc_val t v) && Q (make_args (ret_temp::nil)(v::nil) rho).
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
 intros. reflexivity.
Qed.
Hint Rewrite bind_ret1_unfold' : norm2.  (* put this in AFTER the unprimed version, for higher priority *)

Lemma normal_ret_assert_elim:
 forall P, RA_normal (normal_ret_assert P) = P.
Proof.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
reflexivity.
Qed.

Lemma overridePost_EK_break:
 forall P Q, RA_break (overridePost P Q) = RA_break Q.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. destruct Q; reflexivity.
Qed.

Lemma loop1_ret_assert_EK_break:
 forall P Q, RA_break (loop1_ret_assert P Q) = RA_normal Q.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. destruct Q;   reflexivity.
Qed.

Hint Rewrite overridePost_EK_break loop1_ret_assert_EK_break
  normal_ret_assert_elim : ret_assert.

Lemma loop1_ret_assert_normal:
  forall P Q, RA_normal (loop1_ret_assert P Q) = P.
Proof. 
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
  destruct Q; reflexivity.
Qed.
Hint Rewrite loop1_ret_assert_normal: ret_assert.

Lemma unfold_make_args': forall fsig args rho,
    make_args' fsig args rho = make_args (map (@fst _ _) (fst fsig)) (args rho) rho.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite unfold_make_args' : norm2.
Lemma unfold_make_args_cons: forall i il v vl rho,
   make_args (i::il) (v::vl) rho = env_set (make_args il vl rho) i v.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Lemma unfold_make_args_nil: make_args nil nil = globals_only.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite unfold_make_args_cons unfold_make_args_nil : norm2.

Lemma clear_rhox:  (* replaces clear_make_args' *)
 forall (P: mpred) (f: environ -> environ),
    @liftx (Tarrow environ (LiftEnviron mpred))
                    (@liftx (LiftEnviron mpred) P) f
       = `P.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. intros. reflexivity. Qed.
Hint Rewrite clear_rhox: norm2.

Lemma eval_make_args':
  forall (Q: val -> Prop) i fsig args,
  @liftx (Tarrow environ (LiftEnviron Prop))
      (@liftx (Tarrow val (LiftEnviron Prop)) Q (eval_id i))
   (make_args' fsig args) =
  `Q (`(eval_id i) (make_args' fsig args)).
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite eval_make_args' : norm2.

Lemma eval_make_args_same:
 forall {cs: compspecs}  i t fsig t0 tl (e: expr) el,
 `(eval_id i) (make_args' ((i,t)::fsig, t0) (eval_exprlist (t::tl) (e::el))) =
   `force_val (`(sem_cast (typeof e) t) (eval_expr e)).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq (lifted (LiftEnviron val)) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i : forall _ : environ, val) (make_args' (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el)))) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i : forall _ : environ, val) (make_args' (@pair (list (prod ident type)) type fsig t0) (@eval_exprlist cs tl el))) *)
extensionality rho.
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (make_args' (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el))) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (make_args' (@pair (list (prod ident type)) type fsig t0) (@eval_exprlist cs tl el)) rho) *)
unfold make_args'.
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0))) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el) rho) rho) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type fsig t0))) (@eval_exprlist cs tl el rho) rho) rho) *)
unfold_lift.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @eq val (eval_id i (env_set (make_args (@map (prod ident type) ident (@fst ident type) fsig) (@eval_exprlist cs tl el rho) rho) j (@liftx (Tarrow (option val) (LiftEnviron val)) force_val (@liftx (Tarrow val (LiftEnviron (option val))) (sem_cast (typeof e) t') (@eval_expr cs e)) rho))) (eval_id i (make_args (@map (prod ident type) ident (@fst ident type) fsig) (@eval_exprlist cs tl el rho) rho)) *)
unfold eval_id.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val id (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
rewrite Map.gss.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0))) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el) rho) rho) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type fsig t0))) (@eval_exprlist cs tl el rho) rho) rho) *)
unfold_lift.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
reflexivity.
Qed.

Lemma eval_make_args_other:
 forall {cs: compspecs}  i j fsig t0 t t' tl (e: expr) el,
   i<>j ->
  `(eval_id i) (make_args' ((j,t)::fsig, t0) (eval_exprlist (t'::tl) (e::el))) =
   `(eval_id i) (make_args' (fsig, t0) (eval_exprlist tl el)).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros. extensionality rho.
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (make_args' (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el))) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (make_args' (@pair (list (prod ident type)) type fsig t0) (@eval_exprlist cs tl el)) rho) *)
unfold make_args'.
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0))) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el) rho) rho) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type fsig t0))) (@eval_exprlist cs tl el rho) rho) rho) *)
unfold_lift.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @eq val (eval_id i (env_set (make_args (@map (prod ident type) ident (@fst ident type) fsig) (@eval_exprlist cs tl el rho) rho) j (@liftx (Tarrow (option val) (LiftEnviron val)) force_val (@liftx (Tarrow val (LiftEnviron (option val))) (sem_cast (typeof e) t') (@eval_expr cs e)) rho))) (eval_id i (make_args (@map (prod ident type) ident (@fst ident type) fsig) (@eval_exprlist cs tl el rho) rho)) *)
unfold eval_id.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
rewrite Map.gso; auto.
Qed.

Hint Rewrite @eval_make_args_same : norm2.
Hint Rewrite @eval_make_args_other using (solve [clear; intro Hx; inversion Hx]) : norm.

Infix "oo" := Basics.compose (at level 54, right associativity).
Arguments Basics.compose {A B C} g f x / .

Lemma compose_backtick:
  forall A B C (F: B -> C) (G: A -> B) (J: environ -> A),
   `F (`G  J) = `(Basics.compose F G) J.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite compose_backtick : norm.

Lemma compose_eval_make_args_same:
  forall {cs: compspecs}  (Q: val -> Prop) i t fsig t0 tl e el,
  @liftx (Tarrow environ (LiftEnviron Prop))
      (Q oo (eval_id i)) (make_args' ((i,t)::fsig,t0) (eval_exprlist (t::tl) (e::el))) =
  `Q (`force_val (`(sem_cast (typeof e) t) (eval_expr e))).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- compose_backtick.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  f_equal. apply eval_make_args_same.
Qed.

Lemma compose_eval_make_args_other:
  forall {cs: compspecs}  Q i j fsig t0 t t' tl (e: expr) el,
   i<>j ->
    @liftx (Tarrow environ (LiftEnviron Prop))
     (Q oo (eval_id i)) (make_args' ((j,t)::fsig, t0) (eval_exprlist (t'::tl) (e::el))) =
     `Q (`(eval_id i) (make_args' (fsig, t0) (eval_exprlist tl el))).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- compose_backtick.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  f_equal. apply eval_make_args_other; auto.
Qed.

Hint Rewrite @compose_eval_make_args_same : norm.
Hint Rewrite @compose_eval_make_args_other using (solve [clear; intro Hx; inversion Hx]) : norm.

Lemma substopt_unfold {A}: forall id v, @substopt A (Some id) v = @subst A id v.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Lemma substopt_unfold_nil {A}: forall v (P:  environ -> A), substopt None v P = P.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
Hint Rewrite @substopt_unfold @substopt_unfold_nil : subst.

Lemma get_result_unfold: forall id, get_result (Some id) = get_result1 id.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Lemma get_result_None: get_result None = globals_only.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite get_result_unfold get_result_None : norm.

Lemma elim_globals_only:
  forall Delta g i t rho,
  tc_environ Delta rho /\ (var_types Delta) ! i = None /\ (glob_types Delta) ! i = Some g ->
  eval_var i t (globals_only rho) = eval_var i t rho.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @eq val (eval_var i t (globals_only rho)) (eval_var i t rho) *)
destruct H as [H [H8 H0]].
(* Goal: @eq val (eval_var i t (globals_only rho)) (eval_var i t rho) *)
unfold eval_var, globals_only.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
simpl.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
destruct_var_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
destruct_glob_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
rewrite Heqo0, Heqo1.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
auto.
Qed.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Hint Rewrite elim_globals_only using (split3; [eassumption | reflexivity.. ]) : norm.

Lemma elim_globals_only':
 forall a: mpred,
 (@liftx (Tarrow environ (LiftEnviron mpred)) (`a) globals_only) = `a.
(* Goal: forall a : mpred, @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow environ (LiftEnviron mpred)) (@liftx (LiftEnviron mpred) a) globals_only) (@liftx (LiftEnviron mpred) a) *)
Proof. reflexivity. Qed.
Hint Rewrite elim_globals_only' : norm.

Lemma globvar_eval_var:
  forall Delta rho id t,
      tc_environ Delta rho ->
     (var_types Delta) ! id = None ->
     (glob_types Delta) ! id = Some  t ->
     exists b,  eval_var id t rho = Vptr b Ptrofs.zero
            /\ Map.get (ge_of rho) id = Some b.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
(* Goal: @ex block (fun b : block => and (@eq val (eval_var id t rho) (Vptr b Ptrofs.zero)) (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) *)
unfold eval_var; simpl.
(* Goal: @ex block (fun b : block => and (@eq val match @Map.get (prod block type) (ve_of rho) id with | Some (pair b0 ty' as p) => if eqb_type t ty' then Vptr b0 Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) id with | Some b0 => Vptr b0 Ptrofs.zero | None => Vundef end end (Vptr b Ptrofs.zero)) (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) *)
destruct_var_types id.
(* Goal: @ex block (fun b : block => and (@eq val match @Map.get (prod block type) (ve_of rho) id with | Some (pair b0 ty' as p) => if eqb_type t ty' then Vptr b0 Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) id with | Some b0 => Vptr b0 Ptrofs.zero | None => Vundef end end (Vptr b Ptrofs.zero)) (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) *)
destruct_glob_types id.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
rewrite Heqo0, Heqo1.
(* Goal: @ex block (fun b0 : block => and (@eq val (Vptr b Ptrofs.zero) (Vptr b0 Ptrofs.zero)) (@eq (option block) (@Some block b) (@Some block b0))) *)
eauto.
Qed.

Lemma globvars2pred_unfold: forall gv vl rho,
    globvars2pred gv vl rho =
     andp (prop (gv = globals_of_env rho))
      (fold_right sepcon emp (map (fun idv => globvar2pred gv idv rho) vl)).
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
Proof. intros. unfold globvars2pred.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right (forall _ : environ, mpred) (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (@map (prod ident (globvar type)) (forall _ : environ, mpred) (globvar2pred gv) vl) rho)) (@andp mpred Nveric (@prop mpred Nveric (@eq globals gv (globals_of_env rho))) (@fold_right mpred mpred (@sepcon mpred Nveric Sveric) (@emp mpred Nveric Sveric) (@map (prod ident (globvar type)) mpred (fun idv : prod ident (globvar type) => globvar2pred gv idv rho) vl))) *)
  unfold lift2. f_equal.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
   induction vl; simpl; auto. normalize; f_equal; auto.
Qed.
Hint Rewrite globvars2pred_unfold : norm.

Hint Rewrite @exp_trivial : norm.

Lemma eval_var_isptr:
  forall Delta t i rho,
            tc_environ Delta rho ->
            ((var_types Delta) ! i = Some t \/
             (var_types Delta)!i = None /\
            (glob_types Delta) ! i = Some t) ->
            isptr (eval_var i t rho).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
 intros.
(* Goal: @eq val match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of (mkEnviron (ge_of rho) (Map.empty (prod block type)) (Map.empty val))) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
 unfold isptr, eval_var; simpl.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 destruct H0 as [? | [? ?]].
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 + destruct_var_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
   rewrite Heqo0.
(* Goal: match (if eqb_type t t then Vptr b Ptrofs.zero else Vundef) with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
   rewrite eqb_type_refl.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
   auto.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
 + destruct_var_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
   destruct_glob_types i.
(* Goal: match match @Map.get (prod block type) (ve_of rho) i with | Some (pair b ty' as p) => if eqb_type t ty' then Vptr b Ptrofs.zero else Vundef | None => match @Map.get block (ge_of rho) i with | Some b => Vptr b Ptrofs.zero | None => Vundef end end with | Vundef => False | Vint i => False | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => True end *)
   rewrite Heqo0, Heqo1.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
   auto.
Qed.

Lemma ENTAIL_trans:
  forall Delta P Q R,
  local (tc_environ Delta) && P |-- Q ->
  local (tc_environ Delta) && Q |-- R ->
  local (tc_environ Delta) && P |-- R.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
intros.
eapply derives_trans.
apply andp_right; [ | apply H].
apply andp_left1; apply derives_refl.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
auto.
Qed.

Lemma ENTAIL_refl:
  forall Delta P,
  local (tc_environ Delta) && P |-- P.
Proof. intros. apply andp_left2, derives_refl. Qed.

Lemma corable_andp_bupd: forall (P Q: environ -> mpred),
  corable P ->
  (P && |==> Q) |-- |==> P && Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P Q)) *)
  rewrite !(andp_comm P).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply bupd_andp2_corable; auto.
Qed.

Lemma local_andp_bupd: forall P Q,
  (local P && |==> Q) |-- |==> (local P && Q).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local P) Q)) *)
  rewrite !(andp_comm (local P)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) P) (local Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (local Q))) *)
  apply bupd_andp2_corable.
(* Goal: @corable (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftCorableSepLog' mpred Nveric Sveric CSLveric) (local Q) *)
  intro; apply corable_prop.
Qed.

Lemma bupd_andp_local: forall P Q,
  (|==> P) && local Q |-- |==> (P && local Q).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) P) (local Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (local Q))) *)
  apply bupd_andp2_corable.
(* Goal: @corable (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftCorableSepLog' mpred Nveric Sveric CSLveric) (local Q) *)
  intro; apply corable_prop.
Qed.

Lemma derives_bupd_trans: forall TC P Q R,
  local TC && P |-- |==> Q ->
  local TC && Q |-- |==> R ->
  local TC && P |-- |==> R.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) Q))) *)
  rewrite (add_andp _ _ H).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R) *)
  rewrite (andp_comm _ P), andp_assoc; apply andp_left2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  eapply derives_trans; [apply local_andp_bupd |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P')) (local (@subst Prop i v (tc_environ Delta))) *)
  rewrite (add_andp _ _ H0).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) Q) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R) *)
  rewrite (andp_comm _ Q), andp_assoc; eapply derives_trans; [apply bupd_mono, andp_left2, derives_refl |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R) *)
  eapply derives_trans; [apply bupd_mono,local_andp_bupd |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) R))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R) *)
  eapply derives_trans; [apply bupd_trans|].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) R)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) R) *)
  apply bupd_mono; solve_andp.
Qed.

Lemma derives_bupd_refl: forall TC P,
  local TC && P |-- |==> P.
Proof. intros. apply andp_left2, bupd_intro. Qed.

Lemma derives_bupd0_refl: forall TC P,
  local TC && P |-- |==> ((|> FF) || P).
Proof. intros. apply (derives_trans _ _ _ (derives_bupd_refl TC P)), bupd_mono, orp_right2, derives_refl. Qed.

Lemma derives_bupd0_trans: forall TC P Q R,
  local TC && P |-- |==> ((|> FF) || Q) ->
  local TC && Q |-- |==> ((|> FF) || R) ->
  local TC && P |-- |==> ((|> FF) || R).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) R)) *)
  eapply derives_bupd_trans; [exact H |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  rewrite andp_comm, distrib_orp_andp, !(andp_comm _ (local _)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_left.
  + eapply derives_trans; [| apply bupd_intro].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) R) *)
    apply orp_right1, andp_left2, derives_refl.
  + eapply derives_bupd_trans; [exact H0 |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    rewrite andp_comm, distrib_orp_andp, !(andp_comm _ (local _)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    apply orp_left.
    - eapply derives_trans; [| apply bupd_intro].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) R) *)
      apply orp_right1, andp_left2, derives_refl.
    - apply derives_bupd0_refl.
Qed.

Lemma derives_full_refl: forall Delta P,
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- |==> ((|> FF) || P).
Proof. intros. refine (derives_trans _ _ _ _ (derives_bupd0_refl (tc_environ Delta) P)). solve_andp. Qed.

Lemma derives_full_trans: forall Delta P Q R,
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- |==> ((|> FF) || Q) ->
  local (tc_environ Delta) && (allp_fun_id Delta && Q) |-- |==> ((|> FF) || R) ->
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- |==> ((|> FF) || R).
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) R)) *)
  eapply derives_bupd0_trans; [| exact H0].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) Q))) *)
  rewrite (add_andp _ _ H).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) Q))) *)
  apply derives_trans with ((|==> |> FF || Q) && allp_fun_id Delta); [solve_andp |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) (allp_fun_id Delta)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) Q))) *)
  eapply derives_trans; [apply bupd_andp2_corable; intro; apply corable_allp_fun_id |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply bupd_mono.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q) (allp_fun_id Delta)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) Q)) *)
  rewrite distrib_orp_andp.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  apply orp_derives; solve_andp.
Qed.

Lemma derives_ENTAIL: forall TC P Q,
  P |-- Q ->
  local TC && P |-- Q.
Proof. intros. apply andp_left2, H. Qed.

Lemma ENTAIL_derives_bupd: forall TC P Q,
  local TC && P |-- Q ->
  local TC && P |-- |==> Q.
Proof. intros. apply (derives_trans _ _ _ H), bupd_intro. Qed.

Lemma derives_bupd_derives_bupd0: forall TC P Q,
  local TC && P |-- |==> Q ->
  local TC && P |-- |==> ((|> FF) || Q).
Proof. intros. apply (derives_trans _ _ _ H), bupd_mono, orp_right2, derives_refl. Qed.

Lemma derives_bupd0_derives_full: forall Delta P Q,
  local (tc_environ Delta) && P |-- |==> ((|> FF) || Q) ->
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- |==> ((|> FF) || Q).
Proof. intros. refine (derives_trans _ _ _ _ H). solve_andp. Qed.

Lemma andp_ENTAIL: forall TC P P' Q Q',
  local TC && P |-- P' ->
  local TC && Q |-- Q' ->
  local TC && (P && Q) |-- P' && Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P Q))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' Q') *)
  eapply derives_trans; [| apply andp_derives; [exact H | exact H0]].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  solve_andp.
Qed.

Lemma orp_ENTAIL: forall TC P P' Q Q',
  local TC && P |-- P' ->
  local TC && Q |-- Q' ->
  local TC && (P || Q) |-- P' || Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P Q)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' Q') *)
  rewrite andp_comm, distrib_orp_andp.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_derives; rewrite andp_comm; auto.
Qed.

Lemma sepcon_ENTAIL: forall TC P P' Q Q',
  local TC && P |-- P' ->
  local TC && Q |-- Q' ->
  local TC && (P * Q) |-- P' * Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P' Q') *)
  eapply derives_trans; [| apply sepcon_derives; [exact H | exact H0]].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) P) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) Q)) *)
  rewrite corable_andp_sepcon1, corable_sepcon_andp1 by (intro; apply corable_prop).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  solve_andp.
Qed.

Lemma wand_ENTAIL: forall TC P P' Q Q',
  local TC && P' |-- P ->
  local TC && Q |-- Q' ->
  local TC && (P -* Q) |-- P' -* Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) P') Q' *)
  eapply derives_trans; [| apply H0].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) P') (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) Q) *)
  rewrite corable_andp_sepcon1 by (intro; apply corable_prop).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) P')) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) Q) *)
  apply andp_right; [apply andp_left1, derives_refl |].
  rewrite <- corable_sepcon_andp1 by (intro; apply corable_prop).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P')) Q *)
  rewrite sepcon_comm, wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P') (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) Q) *)
  eapply derives_trans; [apply H |].
  rewrite <- wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) Q *)
  apply modus_ponens_wand.
Qed.

Lemma exp_ENTAIL: forall Delta B (P Q: B -> environ -> mpred),
  (forall x: B, local (tc_environ Delta) && P x |-- Q x) ->
  local (tc_environ Delta) && exp P |-- exp Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) B P)) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) B Q) *)
  rewrite exp_andp2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply exp_derives; auto.
Qed.

Lemma later_ENTAIL: forall Delta P Q,
  local (tc_environ Delta) && P |-- Q ->
  local (tc_environ Delta) && |> P |-- |> Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) P)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) Q) *)
  apply later_left2, H.
Qed.

Lemma andp_ENTAILL: forall Delta P P' Q Q',
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- P' ->
  local (tc_environ Delta) && (allp_fun_id Delta && Q) |-- Q' ->
  local (tc_environ Delta) && (allp_fun_id Delta && (P && Q)) |-- P' && Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P Q))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' Q') *)
  eapply derives_trans; [| apply andp_derives; [exact H | exact H0]].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  solve_andp.
Qed.

Lemma orp_ENTAILL: forall Delta P P' Q Q',
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- P' ->
  local (tc_environ Delta) && (allp_fun_id Delta && Q) |-- Q' ->
  local (tc_environ Delta) && (allp_fun_id Delta && (P || Q)) |-- P' || Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- andp_assoc in *.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P Q)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' Q') *)
  rewrite andp_comm, distrib_orp_andp.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_derives; rewrite andp_comm; auto.
Qed.

Lemma sepcon_ENTAILL: forall Delta P P' Q Q',
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- P' ->
  local (tc_environ Delta) && (allp_fun_id Delta && Q) |-- Q' ->
  local (tc_environ Delta) && (allp_fun_id Delta && (P * Q)) |-- P' * Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- andp_assoc in *.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P' Q') *)
  eapply derives_trans; [| apply sepcon_derives; [exact H | exact H0]].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) Q)) *)
  rewrite corable_andp_sepcon1, corable_sepcon_andp1 by (intro; simpl; apply corable_andp; [apply corable_prop | apply corable_allp_fun_id]).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  solve_andp.
Qed.

Lemma wand_ENTAILL: forall Delta P P' Q Q',
  local (tc_environ Delta) && (allp_fun_id Delta && P') |-- P ->
  local (tc_environ Delta) && (allp_fun_id Delta && Q) |-- Q' ->
  local (tc_environ Delta) && (allp_fun_id Delta && (P -* Q)) |-- P' -* Q'.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- andp_assoc in *.
  rewrite <- wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) P') Q' *)
  eapply derives_trans; [| apply H0].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) P') (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) Q) *)
  rewrite corable_andp_sepcon1 by (intro; simpl; apply corable_andp; [apply corable_prop | apply corable_allp_fun_id]).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) P')) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) Q) *)
  apply andp_right; [apply andp_left1, derives_refl |].
  rewrite <- corable_sepcon_andp1 by (intro; simpl; apply corable_andp; [apply corable_prop | apply corable_allp_fun_id]).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P')) Q *)
  rewrite sepcon_comm, wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P') (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q) Q) *)
  eapply derives_trans; [apply H |].
  rewrite <- wand_sepcon_adjoint.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P (@wand (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) P Q)) Q *)
  apply modus_ponens_wand.
Qed.

Lemma exp_ENTAILL: forall Delta B (P Q: B -> environ -> mpred),
  (forall x: B, local (tc_environ Delta) && (allp_fun_id Delta && P x) |-- Q x) ->
  local (tc_environ Delta) && (allp_fun_id Delta && exp P) |-- exp Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) B P))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) B Q) *)
  rewrite !exp_andp2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply exp_derives; auto.
Qed.

Lemma later_ENTAILL: forall Delta P Q,
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- Q ->
  local (tc_environ Delta) && (allp_fun_id Delta && |> P) |-- |> Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- andp_assoc in *.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) P)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) Q) *)
  apply later_left2, H.
Qed.

Lemma andp_subst_ENTAILL: forall Delta P P' Q Q' i v t,
  (temp_types Delta) ! i = Some t ->
  local (tc_environ Delta) && (allp_fun_id Delta && P') |-- local (`(tc_val' t) v) ->
  local (tc_environ Delta) && (allp_fun_id Delta && P') |-- Q' ->
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- Q ->
  local (tc_environ Delta) && (allp_fun_id Delta && (P' && subst i v P)) |-- Q' && subst i v Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' (@subst mpred i v P)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q' (@subst mpred i v Q)) *)
  apply (subst_derives i v) in H2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' (@subst mpred i v P)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q' (@subst mpred i v Q)) *)
  autorewrite with subst in H2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P' (@subst mpred i v P)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q' (@subst mpred i v Q)) *)
  eapply derives_trans; [| apply andp_derives; eassumption].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  repeat apply andp_right; try solve_andp.
  rewrite <- !andp_assoc; apply andp_left1; rewrite andp_assoc.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P')) (local (@subst Prop i v (tc_environ Delta))) *)
  rewrite (add_andp _ _ H0).
(* Goal: @eq val (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type j t) fsig) t0))) (@eval_exprlist cs (@cons type t' tl) (@cons expr e el) rho) rho) rho) (@liftx (Tarrow environ (LiftEnviron val)) (eval_id i) (fun rho : environ => make_args (@map (prod ident type) ident (@fst ident type) (@fst (list (prod ident type)) type (@pair (list (prod ident type)) type fsig t0))) (@eval_exprlist cs tl el rho) rho) rho) *)
  unfold local, lift1; unfold_lift.
(* 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 (tc_environ Delta rho)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (allp_fun_id Delta) P')) (fun rho : environ => @prop mpred Nveric (tc_val' t (v rho)))) (fun rho : environ => @prop mpred Nveric (@subst Prop i v (tc_environ Delta) rho)) *)
  intro rho; simpl; normalize; clear H0 H1 H2.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (allp_fun_id Delta rho) (P' rho)) (@prop mpred Nveric (@subst Prop i v (tc_environ Delta) rho)) *)
  apply prop_right.
(* Goal: @subst Prop i v (tc_environ Delta) rho *)
  unfold subst, env_set.
(* Goal: tc_environ Delta (mkEnviron (ge_of rho) (ve_of rho) (@Map.set val i (v rho) (te_of rho))) *)
  destruct rho; simpl in *.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  destruct H3; split; auto.
(* Goal: typecheck_temp_environ (te_of (mkEnviron ge ve (@Map.set val i (v (mkEnviron ge ve te)) te))) (temp_types Delta) *)
  clear H1; simpl in *.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  hnf; intros.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  specialize (H0 _ _ H1).
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  destruct H0 as [? [? ?]].
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  destruct (Pos.eq_dec i id).
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val i (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
  + subst.
(* Goal: @ex val (fun v0 : val => and (@eq (option val) (@Map.get val (@Map.set val id (v (mkEnviron ge ve te)) te) id) (@Some val v0)) (tc_val' ty v0)) *)
    rewrite Map.gss.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    exists (v (mkEnviron ge ve te)); split; auto.
(* Goal: tc_val' ty (v (mkEnviron ge ve te)) *)
    rewrite H in H1.
(* Goal: tc_val' ty (v (mkEnviron ge ve te)) *)
    inv H1.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    auto.
  + exists x.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    rewrite Map.gso by auto.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    auto.
Qed.

Lemma derives_bupd_bupd_left: forall TC P Q,
  local TC && P |-- |==> Q ->
  (local TC && |==> P) |-- |==> Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  eapply derives_trans; [apply local_andp_bupd |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  eapply derives_trans; [apply bupd_mono, H |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  apply bupd_trans.
Qed.

Lemma derives_bupd0_bupd0_left: forall TC P Q,
  local TC && P |-- |==> |> FF || Q ->
  (local TC && |==> |> FF || P) |-- |==> |> FF || Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply derives_bupd_bupd_left.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local TC) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  rewrite andp_comm, distrib_orp_andp, !(andp_comm _ (local _)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_left.
  + apply andp_left2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    eapply derives_trans; [| apply bupd_intro].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    apply orp_right1; auto.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  + auto.
Qed.

Lemma derives_full_bupd0_left: forall Delta P Q,
  local (tc_environ Delta) && (allp_fun_id Delta && P) |-- |==> |> FF || Q ->
  local (tc_environ Delta) && (allp_fun_id Delta && |==> |> FF || P) |-- |==> |> FF || Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
  rewrite <- andp_assoc in H |- *.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  eapply derives_trans; [apply corable_andp_bupd; intro; simpl; apply corable_andp; [apply corable_prop | apply corable_allp_fun_id] |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  eapply derives_trans; [apply bupd_mono | apply bupd_trans].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  rewrite andp_comm, distrib_orp_andp, !(andp_comm _ (_ && _)).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P)) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_left.
  + apply andp_left2.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    eapply derives_trans; [| apply bupd_intro].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
    apply orp_right1; auto.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  + auto.
Qed.

Ltac lifted_derives_L2R H :=
  eapply ENTAIL_trans; [apply H |].

Ltac ENTAIL_L2R H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply ENTAIL_trans; [apply H |]
  | _ =>
      eapply ENTAIL_trans; [apply derives_ENTAIL, H |]
  end.

Ltac derives_bupd_L2R H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_bupd_trans; [apply H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_bupd_trans; [apply ENTAIL_derives_bupd, H |]
  | _ =>
      eapply derives_bupd_trans; [apply ENTAIL_derives_bupd, derives_ENTAIL, H |]
  end.

Ltac derives_bupd0_L2R H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
      eapply derives_bupd0_trans; [apply H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_bupd0_trans; [apply derives_bupd_derives_bupd0, H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_bupd0_trans; [apply derives_bupd_derives_bupd0, ENTAIL_derives_bupd, H |]
  | _ =>
      eapply derives_bupd0_trans; [apply derives_bupd_derives_bupd0, ENTAIL_derives_bupd, derives_ENTAIL, H |]
  end.

Ltac derives_full_L2R H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ ?Delta) && (allp_fun_id ?Delta && _)) (|==> |> FF || _) =>
      eapply derives_full_trans; [apply H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
      eapply derives_full_trans; [apply derives_bupd0_derives_full, H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_full_trans; [apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, H |]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_full_trans; [apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, ENTAIL_derives_bupd, H |]
  | _ =>
      eapply derives_full_trans; [apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, ENTAIL_derives_bupd, derives_ENTAIL, H |]
  end.

Tactic Notation "derives_rewrite" "->" constr(H) :=
  match goal with
  | |- @derives (environ -> mpred) _ (local (tc_environ ?Delta) && (allp_fun_id ?Delta && _)) (|==> |> FF || _) =>
         derives_full_L2R H
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
         derives_bupd0_L2R H
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
         derives_bupd_L2R H
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
         ENTAIL_L2R H
  | |- _ =>
         lifted_derives_L2R H
  end.

Ltac lifted_derives_R2L H :=
  eapply derives_trans; [| apply H].

Ltac ENTAIL_R2L H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply ENTAIL_trans; [| apply H]
  | _ =>
      eapply ENTAIL_trans; [| apply derives_ENTAIL, H]
  end.

Ltac derives_bupd_R2L H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_bupd_trans; [| apply H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_bupd_trans; [| apply ENTAIL_derives_bupd, H]
  | _ =>
      eapply derives_bupd_trans; [| apply ENTAIL_derives_bupd, derives_ENTAIL, H]
  end.

Ltac derives_bupd0_R2L H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
      eapply derives_bupd0_trans; [| apply H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_bupd0_trans; [| apply derives_bupd_derives_bupd0, H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_bupd0_trans; [| apply derives_bupd_derives_bupd0, ENTAIL_derives_bupd, H]
  | _ =>
      eapply derives_bupd0_trans; [| apply derives_bupd_derives_bupd0, ENTAIL_derives_bupd, derives_ENTAIL, H]
  end.

Ltac derives_full_R2L H :=
  match type of H with
  | @derives (environ -> mpred) _ (local (tc_environ ?Delta) && (allp_fun_id ?Delta && _)) (|==> |> FF || _) =>
      eapply derives_bupd0_trans; [| apply H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
      eapply derives_bupd0_trans; [| apply derives_bupd0_derives_full, H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
      eapply derives_bupd0_trans; [| apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, H]
  | @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
      eapply derives_bupd0_trans; [| apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, ENTAIL_derives_bupd, H]
  | _ =>
      eapply derives_bupd0_trans; [| apply derives_bupd0_derives_full, derives_bupd_derives_bupd0, ENTAIL_derives_bupd, derives_ENTAIL, H]
  end.

Tactic Notation "derives_rewrite" "<-" constr(H) :=
  match goal with
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> |> FF || _) =>
         derives_bupd0_R2L H
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) (|==> _) =>
         derives_bupd_R2L H
  | |- @derives (environ -> mpred) _ (local (tc_environ _) && _) _ =>
         ENTAIL_R2L H
  | |- _ =>
         lifted_derives_R2L H
  end.

Ltac solve_derives_trans :=
  first [simple apply derives_full_refl | eapply derives_full_trans; [eassumption | solve_derives_trans]].

Lemma aux1_reduceR: forall P Q: environ -> mpred,
  P |-- |==> Q ->
  P |-- |==> |> FF || Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  eapply derives_trans; [exact H |].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply bupd_mono.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (allp_fun_id Delta)) P) (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@later (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftIndir environ mpred Nveric Iveric) (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric))) Q)) *)
  apply orp_right2; auto.
Qed.

Lemma aux2_reduceR: forall P Q: environ -> mpred,
  P |-- Q ->
  P |-- |==> Q.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@bupd (forall _ : environ, mpred) own.gname compcert_rmaps.RML.R.preds (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@LiftBupdSepLog environ mpred own.gname compcert_rmaps.RML.R.preds Nveric Sveric Bveric) Q) *)
  eapply derives_trans; [exact H |].
(* Goal: forall rho : environ, @liftx (LiftEnviron Prop) True rho *)
  apply bupd_intro.
Qed.

Ltac reduceR :=
  match goal with
  | |- _ |-- |==> |> FF || _ => apply aux1_reduceR
  | _ => idtac
  end;
  match goal with
  | |- _ |-- |==> _ => apply aux2_reduceR
  | _ => idtac
  end.

Lemma aux_reduceL: forall P Q R S: environ -> mpred,
  P && R |-- S ->
  P && (Q && R) |-- S.
Proof.
(* Goal: forall (P Q R S : forall _ : environ, mpred) (_ : @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) S), @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  intros.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) S *)
  eapply derives_trans; [| exact H].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) P R) *)
  solve_andp.
Qed.

Ltac reduceLL :=
  match goal with
  | |- local (tc_environ ?Delta) && (allp_fun_id ?Delta && _) |-- _ => apply aux_reduceL
  | _ => idtac
  end.

Ltac reduceL :=
  match goal with
  | |- local (tc_environ ?Delta) && (allp_fun_id ?Delta && _) |-- _ => apply aux_reduceL
  | _ => idtac
  end;
  match goal with
  | |- local (tc_environ _) && _ |-- _ => apply derives_ENTAIL
  | _ => idtac
  end.

Ltac reduce2derives :=
  reduceL; reduceR.

Ltac reduce2ENTAIL :=
  reduceLL; reduceR.
