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

Local Open Scope logic.

(*
Lemma gvar_globals_only:
  forall i v rho, gvar i v rho -> gvar i v (globals_only rho).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold gvar; intros.
unfold Map.get in *.
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (te_of (mkEnviron (ge_of rho) (ve_of rho) te')) i) *)
destruct (ve_of rho i) as [[? ?]|] eqn:?; try contradiction.
unfold globals_only.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. auto.
Qed.
Hint Resolve gvar_globals_only.
*)

Ltac safe_auto_with_closed :=
   (* won't instantiate evars by accident *)
 match goal with |- ?A =>
          solve [first [has_evar A | auto 50 with closed]]
 end.

Lemma closed_env_set:
 forall {B} i v (P: environ -> B) rho,
     closed_wrt_vars (eq i) P ->
     P (env_set rho i v) = P rho.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros. hnf in H.
(* Goal: @eq B (P (env_set rho i v)) (P rho) *)
 symmetry; destruct rho; apply H.
(* Goal: forall i0 : ident, or (@eq ident i i0) (@eq (option val) (@Map.get val (te_of (mkEnviron ge ve te)) i0) (@Map.get val (@Map.set val i v (te_of (mkEnviron ge ve te))) i0)) *)
 intros; simpl; destruct (ident_eq i i0). left; auto.
(* Goal: or (@eq ident i i0) (@eq (option val) (@Map.get val te i0) (@Map.get val (@Map.set val i v te) i0)) *)
 right; rewrite Map.gso; auto.
Qed.
Hint Rewrite @closed_env_set using safe_auto_with_closed : norm2.

Lemma subst_eval_id_eq:
 forall id v, subst id v (eval_id id) = v.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
Proof. unfold subst, eval_id; intros. extensionality rho.
(* Goal: @eq val (force_val (@Map.get val (te_of (env_set rho id (v rho))) j)) (force_val (@Map.get val (te_of rho) j)) *)
    unfold force_val, env_set; simpl. rewrite Map.gss; auto.
Qed.

Lemma subst_eval_id_neq:
  forall id v j, id<>j -> subst id v (eval_id j) = eval_id j.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
    unfold subst, eval_id; intros. extensionality rho.
(* Goal: @eq val (force_val (@Map.get val (te_of (env_set rho id (v rho))) j)) (force_val (@Map.get val (te_of rho) j)) *)
    unfold force_val, env_set; simpl. rewrite Map.gso; auto.
Qed.

Hint Rewrite subst_eval_id_eq : subst.
Hint Rewrite subst_eval_id_neq using safe_auto_with_closed : subst.

(*
Lemma subst_temp_eq:
  forall i v w, subst i `v (temp i w) = `(eq w v).
Proof.
unfold temp; intros; autorewrite with subst.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
extensionality rho; unfold_lift. reflexivity.
Qed.

Lemma subst_temp_neq:
  forall i j v w, i<>j -> subst i v (temp j w) = temp j w.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold temp; intros. autorewrite with subst.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
f_equal. apply subst_eval_id_neq; auto.
Qed.

Lemma subst_var:
   forall i j v t w,  subst i v (var j t w) = var j t w.
Proof.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
unfold var; intros; autorewrite with subst; auto.
Qed.

Hint Rewrite subst_var : subst.
Hint Rewrite subst_temp_eq : subst.
Hint Rewrite subst_temp_neq using safe_auto_with_closed : subst.
*)

Fixpoint subst_eval_expr  {cs: compspecs}  (j: ident) (v: environ -> val) (e: expr) : environ -> val :=
 match e with
 | Econst_int i ty => `(Vint i)
 | Econst_long i ty => `(Vlong i)
 | Econst_float f ty => `(Vfloat f)
 | Econst_single f ty => `(Vsingle f)
 | Etempvar id ty => if eqb_ident j id then v else eval_id id
 | Eaddrof a ty => subst_eval_lvalue j v a
 | Eunop op a ty =>  `(eval_unop op (typeof a)) (subst_eval_expr j v a)
 | Ebinop op a1 a2 ty =>
                  `(eval_binop op (typeof a1) (typeof a2)) (subst_eval_expr j v a1) (subst_eval_expr j v a2)
 | Ecast a ty => `(eval_cast (typeof a) ty) (subst_eval_expr j v a)
 | Evar id ty => eval_var id ty
 | Ederef a ty => subst_eval_expr j v a
 | Efield a i ty => `(eval_field (typeof a) i) (subst_eval_lvalue j v a)
 | Esizeof t ty => `(Vptrofs (Ptrofs.repr (sizeof t)))
 | Ealignof t ty => `(Vptrofs (Ptrofs.repr (alignof t)))
 end

 with subst_eval_lvalue {cs: compspecs} (j: ident) (v: environ -> val) (e: expr) : environ -> val :=
 match e with
 | Evar id ty => eval_var id ty
 | Ederef a ty => subst_eval_expr j v a
 | Efield a i ty => `(eval_field (typeof a) i) (subst_eval_lvalue j v a)
 | _  => `Vundef
 end.

Lemma subst_eval_expr_eq:
    forall {cs: compspecs} j v e, subst j v (eval_expr e) = subst_eval_expr j v e
with subst_eval_lvalue_eq:
    forall {cs: compspecs} j v e, subst j v (eval_lvalue e) = subst_eval_lvalue j v e.
Proof.
intros cs j v; clear subst_eval_expr_eq; induction e; intros; simpl; try auto.
unfold eqb_ident.
(* Goal: @eq (forall _ : environ, A) (fun s : environ => P (env_set s id (e s))) P *)
unfold subst, eval_id, env_set, te_of. extensionality rho.
pose proof (Pos.eqb_spec j i).
destruct H. subst. rewrite Map.gss. reflexivity.
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (@Map.set val id (e rho) (te_of rho)) i) *)
rewrite Map.gso; auto.
rewrite <- IHe; clear IHe.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
extensionality rho; unfold subst.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
reflexivity.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
extensionality rho; unfold subst.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
rewrite <- IHe1, <- IHe2; reflexivity.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
extensionality rho; unfold subst.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
rewrite <- IHe; reflexivity.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
rewrite <- subst_eval_lvalue_eq.
extensionality rho; unfold subst.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
f_equal. f_equal.

intros Delta j v; clear subst_eval_lvalue_eq; induction e; intros; simpl; try auto.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
extensionality rho; unfold subst.
rewrite <- IHe.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
f_equal.
Qed.

Hint Rewrite @subst_eval_expr_eq @subst_eval_lvalue_eq : subst.


Lemma closed_wrt_subst:
  forall {A} id e (P: environ -> A), closed_wrt_vars (eq id) P -> subst id e P = P.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq (forall _ : environ, A) (@subst A id e P) P *)
unfold subst, closed_wrt_vars in *.
(* Goal: @eq (forall _ : environ, A) (fun s : environ => P (env_set s id (e s))) P *)
extensionality rho.
(* Goal: @eq A (P (env_set rho id (e rho))) (P rho) *)
symmetry.
(* Goal: @eq A (P rho) (P (mkEnviron (ge_of rho) (ve_of rho) te')) *)
apply H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: or (@eq ident id i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (@Map.set val id (e rho) (te_of rho)) i)) *)
destruct (eq_dec id i); auto.
(* Goal: or (@eq ident id i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (@Map.set val id (e rho) (te_of rho)) i)) *)
right.
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (@Map.set val id (e rho) (te_of rho)) i) *)
rewrite Map.gso; auto.
Qed.

Lemma closed_wrt_map_subst:
   forall {A: Type} id e (Q: list (environ -> A)),
         Forall (closed_wrt_vars (eq id)) Q ->
         map (subst id e) Q = Q.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
induction Q; intros.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@nil (forall _ : environ, A))) (@nil (forall _ : environ, A)) *)
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
simpl; auto.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
inv H.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
simpl; f_equal; auto.
(* Goal: @eq (forall _ : environ, val) (@subst val j v (@eval_lvalue cs e)) (@eval_lvalue cs e) *)
apply closed_wrt_subst; auto.
Qed.
Hint Rewrite @closed_wrt_map_subst using safe_auto_with_closed : subst.
Hint Rewrite @closed_wrt_subst using safe_auto_with_closed : subst.

Lemma closed_wrt_map_subst':
   forall {A: Type} id e (Q: list (environ -> A)),
         Forall (closed_wrt_vars (eq id)) Q ->
         @map (LiftEnviron A) _ (subst id e) Q = Q.
Proof.
apply @closed_wrt_map_subst.
Qed.

(*Hint Rewrite @closed_wrt_map_subst' using safe_auto_with_closed : norm.*)
Hint Rewrite @closed_wrt_map_subst' using safe_auto_with_closed : subst.
Lemma closed_wrt_subst_eval_expr:
  forall {cs: compspecs} j v e,
   closed_wrt_vars (eq j) (eval_expr e) ->
   subst_eval_expr j v e = eval_expr e.
Proof.
(* Goal: forall (cs : compspecs) (j : ident) (v : forall _ : environ, val) (e : expr) (_ : @closed_wrt_vars val (@eq ident j) (@eval_expr cs e)), @eq (forall _ : environ, val) (@subst_eval_expr cs j v e) (@eval_expr cs e) *)
intros; rewrite <- subst_eval_expr_eq.
(* Goal: @eq (forall _ : environ, val) (@subst val j v (@eval_lvalue cs e)) (@eval_lvalue cs e) *)
apply closed_wrt_subst; auto.
Qed.
Lemma closed_wrt_subst_eval_lvalue:
  forall {cs: compspecs} j v e,
   closed_wrt_vars (eq j) (eval_lvalue e) ->
   subst_eval_lvalue j v e = eval_lvalue e.
Proof.
intros; rewrite <- subst_eval_lvalue_eq.
(* Goal: @eq (forall _ : environ, val) (@subst val j v (@eval_lvalue cs e)) (@eval_lvalue cs e) *)
apply closed_wrt_subst; auto.
Qed.
Hint Rewrite @closed_wrt_subst_eval_expr using solve [auto 50 with closed] : subst.
Hint Rewrite @closed_wrt_subst_eval_lvalue using solve [auto 50 with closed] : subst.

Hint Unfold closed_wrt_modvars : closed.

Lemma closed_wrt_local: forall S P, closed_wrt_vars S P -> closed_wrt_vars S (local P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf in H|-*; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
specialize (H _ _ H0).
(* Goal: @eq mpred (local P rho) (local P (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold local, lift1.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
f_equal; auto.
Qed.

Lemma closed_wrtl_local: forall S P, closed_wrt_lvars S P -> closed_wrt_lvars S (local P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf in H|-*; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
specialize (H _ _ H0).
(* Goal: @eq mpred (local P rho) (local P (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold local, lift1.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
f_equal; auto.
Qed.
Hint Resolve closed_wrt_local closed_wrtl_local : closed.

Lemma closed_wrt_lift0: forall {A} S (Q: A), closed_wrt_vars S (lift0 Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq A (@lift0 A Q rho) (@lift0 A Q (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold lift0; auto.
Qed.
Lemma closed_wrtl_lift0: forall {A} S (Q: A), closed_wrt_lvars S (lift0 Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq A (@lift0 A Q rho) (@lift0 A Q (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold lift0; auto.
Qed.
Hint Resolve closed_wrt_lift0 closed_wrtl_lift0 : closed.

Lemma closed_wrt_lift0C: forall {B} S (Q: B),
   closed_wrt_vars S (@liftx (LiftEnviron B) Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (LiftEnviron B) Q rho) (@liftx (LiftEnviron B) Q (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold_lift; auto.
Qed.
Lemma closed_wrtl_lift0C: forall {B} S (Q: B),
   closed_wrt_lvars S (@liftx (LiftEnviron B) Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (LiftEnviron B) Q rho) (@liftx (LiftEnviron B) Q (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold_lift; auto.
Qed.
Hint Resolve @closed_wrt_lift0C @closed_wrtl_lift0C: closed.

Lemma closed_wrt_lift1: forall {A}{B} S (f: A -> B) P,
        closed_wrt_vars S P ->
        closed_wrt_vars S (lift1 f P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
intros ? ? ?. specialize (H _ _ H0).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift1; f_equal; auto.
Qed.
Lemma closed_wrtl_lift1: forall {A}{B} S (f: A -> B) P,
        closed_wrt_lvars S P ->
        closed_wrt_lvars S (lift1 f P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
intros ? ? ?. specialize (H _ _ H0).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift1; f_equal; auto.
Qed.
Hint Resolve closed_wrt_lift1 closed_wrtl_lift1 : closed.

Lemma closed_wrt_lift1C: forall {A}{B} S (f: A -> B) P,
        closed_wrt_vars S P ->
        closed_wrt_vars S (@liftx (Tarrow A (LiftEnviron B)) f P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
intros ? ? ?. specialize (H _ _ H0).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold_lift; f_equal; auto.
Qed.
Lemma closed_wrtl_lift1C: forall {A}{B} S (f: A -> B) P,
        closed_wrt_lvars S P ->
        closed_wrt_lvars S (@liftx (Tarrow A (LiftEnviron B)) f P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
intros ? ? ?. specialize (H _ _ H0).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold_lift; f_equal; auto.
Qed.
Hint Resolve @closed_wrt_lift1C @closed_wrtl_lift1C : closed.

Lemma closed_wrt_lift2: forall {A1 A2}{B} S (f: A1 -> A2 -> B) P1 P2,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S (lift2 f P1 P2).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H1).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H1).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift2; f_equal; auto.
Qed.
Lemma closed_wrtl_lift2: forall {A1 A2}{B} S (f: A1 -> A2 -> B) P1 P2,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S (lift2 f P1 P2).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H1).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H1).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift2; f_equal; auto.
Qed.
Hint Resolve closed_wrt_lift2 closed_wrtl_lift2 : closed.

Lemma closed_wrt_lift2C: forall {A1 A2}{B} S (f: A1 -> A2 -> B) P1 P2,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H1).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H1).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold_lift; f_equal; auto.
Qed.
Lemma closed_wrtl_lift2C: forall {A1 A2}{B} S (f: A1 -> A2 -> B) P1 P2,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H1).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 rho) (@liftx (Tarrow A1 (Tarrow A2 (LiftEnviron B))) f P1 P2 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H1).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold_lift; f_equal; auto.
Qed.
Hint Resolve @closed_wrt_lift2C @closed_wrtl_lift2C : closed.

Lemma closed_wrt_lift3: forall {A1 A2 A3}{B} S (f: A1 -> A2 -> A3 -> B) P1 P2 P3,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S P3 ->
        closed_wrt_vars S (lift3 f P1 P2 P3).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H2).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift3; f_equal; auto.
Qed.
Lemma closed_wrtl_lift3: forall {A1 A2 A3}{B} S (f: A1 -> A2 -> A3 -> B) P1 P2 P3,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S P3 ->
        closed_wrt_lvars S (lift3 f P1 P2 P3).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H2).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift3; f_equal; auto.
Qed.
Hint Resolve closed_wrt_lift3 closed_wrtl_lift3 : closed.

Lemma closed_wrt_lift3C: forall {A1 A2 A3}{B} S (f: A1 -> A2 -> A3 -> B) P1 P2 P3,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S P3 ->
        closed_wrt_vars S (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H2).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift. f_equal; auto.
Qed.

Lemma closed_wrtl_lift3C: forall {A1 A2 A3}{B} S (f: A1 -> A2 -> A3 -> B) P1 P2 P3,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S P3 ->
        closed_wrt_lvars S (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H2).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (LiftEnviron B)))) f P1 P2 P3 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H2).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift. f_equal; auto.
Qed.
Hint Resolve @closed_wrt_lift3C @closed_wrtl_lift3C : closed.

Lemma closed_wrt_lift4: forall {A1 A2 A3 A4}{B} S (f: A1 -> A2 -> A3 -> A4 -> B)
       P1 P2 P3 P4,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S P3 ->
        closed_wrt_vars S P4 ->
        closed_wrt_vars S (lift4 f P1 P2 P3 P4).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H2 _ _ H3).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift4; f_equal; auto.
Qed.
Lemma closed_wrtl_lift4: forall {A1 A2 A3 A4}{B} S (f: A1 -> A2 -> A3 -> A4 -> B)
       P1 P2 P3 P4,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S P3 ->
        closed_wrt_lvars S P4 ->
        closed_wrt_lvars S (lift4 f P1 P2 P3 P4).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H2 _ _ H3).
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift4; f_equal; auto.
Qed.
Hint Resolve closed_wrt_lift4  closed_wrtl_lift4 : closed.

Lemma closed_wrt_lift4C: forall {A1 A2 A3 A4}{B} S (f: A1 -> A2 -> A3 -> A4 -> B) P1 P2 P3 P4,
        closed_wrt_vars S P1 ->
        closed_wrt_vars S P2 ->
        closed_wrt_vars S P3 ->
        closed_wrt_vars S P4 ->
        closed_wrt_vars S (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H2 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold liftx; simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift. f_equal; auto.
Qed.
Lemma closed_wrtl_lift4C: forall {A1 A2 A3 A4}{B} S (f: A1 -> A2 -> A3 -> A4 -> B) P1 P2 P3 P4,
        closed_wrt_lvars S P1 ->
        closed_wrt_lvars S P2 ->
        closed_wrt_lvars S P3 ->
        closed_wrt_lvars S P4 ->
        closed_wrt_lvars S (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H0 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H1 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H2 _ _ H3).
(* Goal: @eq B (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 rho) (@liftx (Tarrow A1 (Tarrow A2 (Tarrow A3 (Tarrow A4 (LiftEnviron B))))) f P1 P2 P3 P4 (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold liftx; simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold lift. f_equal; auto.
Qed.
Hint Resolve @closed_wrt_lift4C @closed_wrtl_lift4C : closed.

Lemma closed_wrt_const:
 forall A (P: A) S, closed_wrt_vars S (fun rho: environ => P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. auto.
Qed.
Lemma closed_wrtl_const:
 forall A (P: A) S, closed_wrt_lvars S (fun rho: environ => P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. auto.
Qed.
Hint Resolve @closed_wrt_const @closed_wrtl_const : closed.

Lemma closed_wrt_eval_var:
  forall S id t, closed_wrt_vars S (eval_var id t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold closed_wrt_vars, eval_var; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
auto.
Qed.
Hint Resolve closed_wrt_eval_var : closed.
Lemma closed_wrtl_eval_var:
  forall S id t, ~ S id -> closed_wrt_lvars S (eval_var id t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold closed_wrt_lvars, eval_var; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: @eq val match @Map.get (prod block type) (ve_of rho) id 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) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end end match @Map.get (prod block type) ve' id 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) id with | Some b => Vptr b Ptrofs.zero | None => Vundef end end *)
destruct (H0 id); [contradiction | ].
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite <- H1; auto.
Qed.
Hint Resolve closed_wrtl_eval_var : closed.

(*
Lemma closed_wrt_var:
  forall S id t v, closed_wrt_vars S (var id t v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold var; intros.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
Qed.
Hint Resolve closed_wrt_var : closed.

Lemma closed_wrtl_var:
 forall S id t v, ~ S id -> closed_wrt_lvars S (var id t v).
Proof.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
unfold var; intros; auto with closed.
Qed.
Hint Resolve closed_wrtl_var : closed.
*)

Lemma closed_wrt_lvar:
  forall S id t v, closed_wrt_vars S (locald_denote (lvar id t v)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
hnf; intros; simpl.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
destruct (Map.get (ve_of rho) id); auto.
Qed.
Hint Resolve closed_wrt_lvar : closed.

Lemma closed_wrt_gvars:
  forall S gv, closed_wrt_vars S (locald_denote (gvars gv)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
hnf; intros; simpl. reflexivity.
Qed.
Hint Resolve closed_wrt_gvars : closed.

Lemma closed_wrtl_gvars:
  forall S gv, closed_wrt_lvars S (locald_denote (gvars gv)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
hnf; intros; simpl. reflexivity.
Qed.
Hint Resolve closed_wrtl_gvars : closed.

Lemma closed_wrtl_lvar:
 forall  {cs: compspecs} S id t v,
    ~ S id -> closed_wrt_lvars S (locald_denote (lvar id t v)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
hnf; intros; simpl.
(* Goal: @eq Prop (lvar_denote id t v rho) (lvar_denote id t v (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold lvar_denote.
(* Goal: @eq Prop match @Map.get (prod block type) (ve_of rho) id with | Some (pair b ty' as p) => and (@eq type t ty') (@eq val v (Vptr b Ptrofs.zero)) | None => False end match @Map.get (prod block type) (ve_of (mkEnviron (ge_of rho) ve' (te_of rho))) id with | Some (pair b ty' as p) => and (@eq type t ty') (@eq val v (Vptr b Ptrofs.zero)) | None => False end *)
destruct (H0 id); try contradiction.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite H1; auto.
Qed.
Hint Resolve closed_wrtl_lvar : closed.

Definition expr_closed_wrt_lvars (S: ident -> Prop) (e: expr) : Prop :=
  forall (cs: compspecs) rho ve',
     (forall i, S i \/ Map.get (ve_of rho) i = Map.get ve' i) ->
     eval_expr e rho = eval_expr e (mkEnviron (ge_of rho) ve' (te_of rho)).

Definition lvalue_closed_wrt_lvars (S: ident -> Prop) (e: expr) : Prop :=
  forall (cs: compspecs) rho ve',
     (forall i, S i \/ Map.get (ve_of rho) i = Map.get ve' i) ->
     eval_lvalue e rho = eval_lvalue e (mkEnviron (ge_of rho) ve'  (te_of rho)).

Lemma closed_wrt_cmp_ptr : forall {cs: compspecs} S e1 e2 c,
  expr_closed_wrt_vars S e1 ->
  expr_closed_wrt_vars S e2 ->
  closed_wrt_vars S (`(cmp_ptr_no_mem c) (eval_expr e1) (eval_expr e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold closed_wrt_vars. intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
super_unfold_lift.
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
unfold expr_closed_wrt_vars in *.
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
specialize (H rho te' H1).
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
specialize (H0 rho te' H1).
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) ve' (te_of rho))) (@eval_expr cs e2 (mkEnviron (ge_of rho) ve' (te_of rho)))) *)
unfold cmp_ptr_no_mem. rewrite H0. rewrite H.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
reflexivity.
Qed.
Lemma closed_wrtl_cmp_ptr : forall {cs: compspecs} S e1 e2 c,
  expr_closed_wrt_lvars S e1 ->
  expr_closed_wrt_lvars S e2 ->
  closed_wrt_lvars S (`(cmp_ptr_no_mem c) (eval_expr e1) (eval_expr e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
unfold closed_wrt_lvars. intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
super_unfold_lift.
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) ve' (te_of rho))) (@eval_expr cs e2 (mkEnviron (ge_of rho) ve' (te_of rho)))) *)
unfold expr_closed_wrt_lvars in *.
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) ve' (te_of rho))) (@eval_expr cs e2 (mkEnviron (ge_of rho) ve' (te_of rho)))) *)
specialize (H cs rho ve' H1).
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) ve' (te_of rho))) (@eval_expr cs e2 (mkEnviron (ge_of rho) ve' (te_of rho)))) *)
specialize (H0 cs rho ve' H1).
(* Goal: @eq val (cmp_ptr_no_mem c (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (cmp_ptr_no_mem c (@eval_expr cs e1 (mkEnviron (ge_of rho) ve' (te_of rho))) (@eval_expr cs e2 (mkEnviron (ge_of rho) ve' (te_of rho)))) *)
unfold cmp_ptr_no_mem. rewrite H0. rewrite H.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
reflexivity.
Qed.
Hint Resolve closed_wrt_cmp_ptr closed_wrtl_cmp_ptr: closed.

Lemma closed_wrt_eval_id: forall S i,
    ~ S i -> closed_wrt_vars S (eval_id i).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq val (eval_id i rho) (eval_id i (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold eval_id, force_val.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: @eq Prop (and (@eq val v (force_val (@Map.get val (te_of rho) i))) (not (@eq val v Vundef))) (and (@eq val v (force_val (@Map.get val te' i))) (not (@eq val v Vundef))) *)
destruct (H0 i).
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (te_of (mkEnviron (ge_of rho) (ve_of rho) te')) i) *)
contradiction.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite H1; auto.
Qed.
Lemma closed_wrtl_eval_id: forall S i,
    closed_wrt_lvars S (eval_id i).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars val S (eval_id i) *)
intros ? ? ?.
(* Goal: @eq val (eval_id i rho) (eval_id i (mkEnviron (ge_of rho) ve' (te_of rho))) *)
unfold eval_id, force_val.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. auto.
Qed.
Hint Resolve closed_wrt_eval_id closed_wrtl_eval_id : closed.

Lemma closed_wrt_temp: forall S i v,
    ~ S i -> closed_wrt_vars S (locald_denote (temp i v)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; simpl; intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
unfold eval_id; simpl.
(* Goal: @eq Prop (and (@eq val v (force_val (@Map.get val (te_of rho) i))) (not (@eq val v Vundef))) (and (@eq val v (force_val (@Map.get val te' i))) (not (@eq val v Vundef))) *)
destruct (H0 i).
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (te_of (mkEnviron (ge_of rho) (ve_of rho) te')) i) *)
contradiction.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite H1; auto.
Qed.

Lemma closed_wrtl_temp: forall S i v,
    closed_wrt_lvars S (locald_denote (temp i v)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars Prop S (locald_denote (temp i v)) *)
unfold locald_denote.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
unfold eval_id; simpl. auto.
Qed.
Hint Resolve closed_wrt_temp closed_wrtl_temp : closed.

Lemma closed_wrt_get_result1 :
  forall (S: ident -> Prop) i , ~ S i -> closed_wrt_vars S (get_result1 i).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold get_result1. simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
 simpl. f_equal.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply (closed_wrt_eval_id _ _ H); auto.
Qed.
Lemma closed_wrtl_get_result1 :
  forall (S: ident -> Prop) i , closed_wrt_lvars S (get_result1 i).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold get_result1. simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
 simpl. f_equal.
Qed.
Hint Resolve closed_wrt_get_result1 closed_wrtl_get_result1 : closed.

Lemma closed_wrt_tc_FF:
 forall {cs: compspecs} S e, closed_wrt_vars S (denote_tc_assert (tc_FF e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros. hnf; intros. reflexivity.
Qed.
Lemma closed_wrtl_tc_FF:
 forall {cs: compspecs} S e, closed_wrt_lvars S (denote_tc_assert (tc_FF e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros. hnf; intros. reflexivity.
Qed.
Hint Resolve closed_wrt_tc_FF closed_wrtl_tc_FF : closed.

Lemma closed_wrt_tc_TT:
 forall {cs: compspecs} S, closed_wrt_vars S (denote_tc_assert (tc_TT)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros. hnf; intros. reflexivity.
Qed.
Lemma closed_wrtl_tc_TT:
 forall {cs: compspecs} S, closed_wrt_lvars S (denote_tc_assert (tc_TT)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros. hnf; intros. reflexivity.
Qed.
Hint Resolve closed_wrt_tc_TT closed_wrtl_tc_TT : closed.

Lemma closed_wrt_andp: forall S (P Q: environ->mpred),
  closed_wrt_vars S P -> closed_wrt_vars S Q ->
  closed_wrt_vars S (P && Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Lemma closed_wrtl_andp: forall S (P Q: environ->mpred),
  closed_wrt_lvars S P -> closed_wrt_lvars S Q ->
  closed_wrt_lvars S (P && Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Hint Resolve closed_wrt_andp closed_wrtl_andp : closed.

Lemma closed_wrt_exp: forall {A} S (P: A -> environ->mpred),
  (forall a, closed_wrt_vars S (P a)) ->
  closed_wrt_vars S (exp P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. apply exp_congr. intros a.
(* Goal: @eq mpred (P a rho) (P a (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H a).
(* Goal: @eq mpred (@liftx (Tarrow val (LiftEnviron mpred)) expr2.denote_tc_iszero (@eval_expr cs e) rho) (@liftx (Tarrow val (LiftEnviron mpred)) expr2.denote_tc_iszero (@eval_expr cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
hnf in H.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
eauto.
Qed.

Lemma closed_wrtl_exp: forall {A} S (P: A -> environ->mpred),
  (forall a, closed_wrt_lvars S (P a)) ->
  closed_wrt_lvars S (exp P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. apply exp_congr. intros a.
(* Goal: @eq mpred (P a rho) (P a (mkEnviron (ge_of rho) ve' (te_of rho))) *)
specialize (H a).
(* Goal: @eq mpred (@liftx (Tarrow val (LiftEnviron mpred)) expr2.denote_tc_iszero (@eval_expr cs e) rho) (@liftx (Tarrow val (LiftEnviron mpred)) expr2.denote_tc_iszero (@eval_expr cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
hnf in H.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
eauto.
Qed.
Hint Resolve closed_wrt_exp closed_wrtl_exp : closed.

Lemma closed_wrt_imp: forall S (P Q: environ->mpred),
  closed_wrt_vars S P -> closed_wrt_vars S Q ->
  closed_wrt_vars S (P --> Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Lemma closed_wrtl_imp: forall S (P Q: environ->mpred),
  closed_wrt_lvars S P -> closed_wrt_lvars S Q ->
  closed_wrt_lvars S (P --> Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Hint Resolve closed_wrt_imp closed_wrtl_imp : closed.

Lemma closed_wrt_sepcon: forall S (P Q: environ->mpred),
  closed_wrt_vars S P -> closed_wrt_vars S Q ->
  closed_wrt_vars S (P * Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Lemma closed_wrtl_sepcon: forall S (P Q: environ->mpred),
  closed_wrt_lvars S P -> closed_wrt_lvars S Q ->
  closed_wrt_lvars S (P * Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. f_equal; eauto.
Qed.
Hint Resolve closed_wrt_sepcon closed_wrtl_sepcon : closed.

Lemma closed_wrt_emp {A} {ND: NatDed A} {SL: SepLog A}:
  forall S, closed_wrt_vars S emp.
Proof. repeat intro. reflexivity. Qed.
Lemma closed_wrtl_emp {A} {ND: NatDed A} {SL: SepLog A}:
  forall S, closed_wrt_lvars S emp.
Proof. repeat intro. reflexivity. Qed.
Hint Resolve (@closed_wrt_emp mpred Nveric Sveric) (@closed_wrtl_emp mpred Nveric Sveric) : closed.

Lemma closed_wrt_allp: forall A S P,
  (forall x: A, closed_wrt_vars S (P x)) ->
  closed_wrt_vars S (allp P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
apply pred_ext; apply allp_right; intro x; apply (allp_left _ x);
specialize (H x rho te' H0);
apply derives_refl'; congruence.
Qed.
Lemma closed_wrtl_allp: forall A S P,
  (forall x: A, closed_wrt_lvars S (P x)) ->
  closed_wrt_lvars S (allp P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf in *; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
apply pred_ext; apply allp_right; intro x; apply (allp_left _ x);
specialize (H x rho ve' H0);
apply derives_refl'; congruence.
Qed.
Hint Resolve closed_wrt_allp closed_wrtl_allp : closed.

Lemma closed_wrt_globvars:
  forall S gv v, closed_wrt_vars S (globvars2pred gv v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (globvars2pred gv v) *)
unfold globvars2pred.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. unfold lift2. f_equal.
(* Goal: @eq mpred (@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) v) 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) v) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
induction v; simpl map; auto with closed.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
f_equal; auto.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
unfold globvar2pred; destruct a; simpl.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
destruct (gvar_volatile g) eqn:?; auto.
(* Goal: @eq mpred (init_data_list2pred (@gvar_init type g) (readonly2share (@gvar_readonly type g)) (gv i) rho) (init_data_list2pred (@gvar_init type g) (readonly2share (@gvar_readonly type g)) (gv i) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
forget (readonly2share (gvar_readonly g)) as sh.
(* Goal: @eq mpred (init_data_list2pred (@gvar_init type g) sh (gv i) rho) (init_data_list2pred (@gvar_init type g) sh (gv i) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
forget (gv i) as j.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
revert j; induction (gvar_init g); intros; simpl; f_equal; auto.
Qed.

Lemma closed_wrtl_globvars:
  forall S gv v, closed_wrt_lvars S (globvars2pred gv v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (globvars2pred gv v) *)
unfold globvars2pred.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. unfold lift2. f_equal.
(* Goal: @eq mpred (@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) v) 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) v) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
induction v; simpl map; auto with closed.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
f_equal; auto.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
unfold globvar2pred; destruct a; simpl.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
destruct (gvar_volatile g) eqn:?; auto.
(* Goal: @eq mpred (init_data_list2pred (@gvar_init type g) (readonly2share (@gvar_readonly type g)) (gv i) rho) (init_data_list2pred (@gvar_init type g) (readonly2share (@gvar_readonly type g)) (gv i) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
forget (readonly2share (gvar_readonly g)) as sh.
(* Goal: @eq mpred (init_data_list2pred (@gvar_init type g) sh (gv i) rho) (init_data_list2pred (@gvar_init type g) sh (gv i) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
forget (gv i) as j.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
revert j; induction (gvar_init g); intros; simpl; f_equal; auto.
Qed.
Hint Resolve closed_wrt_globvars closed_wrtl_globvars: closed.

Lemma closed_wrt_main_pre:
  forall prog u v S, closed_wrt_vars S (main_pre prog u v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. apply closed_wrt_globvars. Qed.
Lemma closed_wrtl_main_pre:
  forall prog u v S, closed_wrt_lvars S (main_pre prog u v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. apply closed_wrtl_globvars. Qed.
Lemma closed_wrt_main_pre_ext:
  forall {Espec : OracleKind} prog z u v S, closed_wrt_vars S (main_pre_ext prog z u v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold main_pre_ext. apply closed_wrt_sepcon; [apply closed_wrt_globvars | apply closed_wrt_const].
Qed.
Lemma closed_wrtl_main_pre_ext:
  forall {Espec : OracleKind} prog z u v S, closed_wrt_lvars S (main_pre_ext prog z u v).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold main_pre_ext. apply closed_wrtl_sepcon; [apply closed_wrtl_globvars | apply closed_wrtl_const].
Qed.
Hint Resolve closed_wrt_main_pre closed_wrtl_main_pre closed_wrt_main_pre_ext closed_wrtl_main_pre_ext : closed.

Lemma closed_wrt_not1:
  forall (i j: ident),
   i<>j ->
   not (eq i j).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars B S' f *)
hnf.
(* Goal: forall _ : @eq ident i j, False *)
intros; subst; congruence.
Qed.
Hint Resolve closed_wrt_not1 : closed.

Lemma closed_wrt_tc_andp:
  forall {cs: compspecs} S a b,
  closed_wrt_vars S (denote_tc_assert a) ->
  closed_wrt_vars S (denote_tc_assert b) ->
  closed_wrt_vars S (denote_tc_assert (tc_andp a b)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
 repeat rewrite denote_tc_assert_andp; simpl; f_equal; auto.
Qed.


Lemma closed_wrt_tc_orp:
  forall {cs: compspecs} S a b,
  closed_wrt_vars S (denote_tc_assert a) ->
  closed_wrt_vars S (denote_tc_assert b) ->
  closed_wrt_vars S (denote_tc_assert (tc_orp a b)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 repeat rewrite denote_tc_assert_orp; simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
 f_equal; auto.
Qed.

Lemma closed_wrt_tc_bool:
  forall {cs: compspecs} S b e, closed_wrt_vars S (denote_tc_assert (tc_bool b e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@nil (forall _ : environ, A))) (@nil (forall _ : environ, A)) *)
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
 destruct b; simpl; auto.
Qed.

Lemma closed_wrt_tc_int_or_ptr_type:
  forall {cs: compspecs} S t, 
  closed_wrt_vars S (denote_tc_assert (tc_int_or_ptr_type t)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: @closed_wrt_vars mpred S (@denote_tc_assert cs (tc_int_or_ptr_type t)) *)
 apply closed_wrt_tc_bool.
Qed.

Hint Resolve closed_wrt_tc_andp closed_wrt_tc_orp closed_wrt_tc_bool
              closed_wrt_tc_int_or_ptr_type : closed.

Lemma closed_wrtl_tc_andp:
  forall {cs: compspecs} S a b,
  closed_wrt_lvars S (denote_tc_assert a) ->
  closed_wrt_lvars S (denote_tc_assert b) ->
  closed_wrt_lvars S (denote_tc_assert (tc_andp a b)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
 repeat rewrite denote_tc_assert_andp; simpl; f_equal; auto.
Qed.


Lemma closed_wrtl_tc_orp:
  forall {cs: compspecs} S a b,
  closed_wrt_lvars S (denote_tc_assert a) ->
  closed_wrt_lvars S (denote_tc_assert b) ->
  closed_wrt_lvars S (denote_tc_assert (tc_orp a b)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 repeat rewrite denote_tc_assert_orp; simpl.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
 f_equal; auto.
Qed.
Lemma closed_wrtl_tc_bool:
  forall {cs: compspecs} S b e, closed_wrt_lvars S (denote_tc_assert (tc_bool b e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@nil (forall _ : environ, A))) (@nil (forall _ : environ, A)) *)
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
 destruct b; simpl; auto.
Qed.
Hint Resolve closed_wrtl_tc_andp closed_wrtl_tc_orp closed_wrtl_tc_bool : closed.

Lemma closed_wrt_tc_test_eq:
  forall {cs: compspecs} S e e',
          expr_closed_wrt_vars S e ->
          expr_closed_wrt_vars S e' ->
  closed_wrt_vars S
     (denote_tc_assert
        (tc_test_eq e e')).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_test_eq cs e e') rho) (@denote_tc_assert cs (@tc_test_eq cs e e') (mkEnviron (ge_of rho) ve' (te_of rho))) *)
rewrite !binop_lemmas2.denote_tc_assert_test_eq'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
simpl. unfold_lift. rewrite H, H0; auto.
Qed.
Lemma closed_wrtl_tc_test_eq:
  forall {cs: compspecs} S e e',
          expr_closed_wrt_lvars S e ->
          expr_closed_wrt_lvars S e' ->
  closed_wrt_lvars S
     (denote_tc_assert
        (tc_test_eq e e')).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_test_eq cs e e') rho) (@denote_tc_assert cs (@tc_test_eq cs e e') (mkEnviron (ge_of rho) ve' (te_of rho))) *)
rewrite !binop_lemmas2.denote_tc_assert_test_eq'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
simpl. unfold_lift. rewrite H, H0; auto.
Qed.
Hint Resolve  closed_wrt_tc_test_eq  closed_wrtl_tc_test_eq : closed.

Lemma closed_wrt_tc_test_order:
  forall {cs: compspecs} S e e',
          expr_closed_wrt_vars S e ->
          expr_closed_wrt_vars S e' ->
  closed_wrt_vars S
     (denote_tc_assert
        (tc_test_order e e')).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_test_order cs e e') rho) (@denote_tc_assert cs (@tc_test_order cs e e') (mkEnviron (ge_of rho) ve' (te_of rho))) *)
rewrite !binop_lemmas2.denote_tc_assert_test_order'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
simpl. unfold_lift. rewrite H, H0; auto.
Qed.
Lemma closed_wrtl_tc_test_order:
  forall {cs: compspecs} S e e',
          expr_closed_wrt_lvars S e ->
          expr_closed_wrt_lvars S e' ->
  closed_wrt_lvars S
     (denote_tc_assert
        (tc_test_order e e')).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_test_order cs e e') rho) (@denote_tc_assert cs (@tc_test_order cs e e') (mkEnviron (ge_of rho) ve' (te_of rho))) *)
rewrite !binop_lemmas2.denote_tc_assert_test_order'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
simpl. unfold_lift. rewrite H, H0; auto.
Qed.
Hint Resolve  closed_wrt_tc_test_order  closed_wrtl_tc_test_order : closed.

Lemma expr_closed_const_int:
  forall {cs: compspecs} S i t, expr_closed_wrt_vars S (Econst_int i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold expr_closed_wrt_vars. simpl; intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
super_unfold_lift. auto.
Qed.
Lemma expr_closedl_const_int:
  forall S i t, expr_closed_wrt_lvars S (Econst_int i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. unfold expr_closed_wrt_lvars. simpl; intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
super_unfold_lift. auto.
Qed.
Hint Resolve expr_closed_const_int expr_closedl_const_int : closed.


Lemma closed_wrt_tc_iszero:
  forall {cs: compspecs}  S e, expr_closed_wrt_vars S e ->
    closed_wrt_vars S (expr2.denote_tc_assert (tc_iszero e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (@expr2.denote_tc_assert cs (@tc_iszero cs e)) *)
rewrite binop_lemmas2.denote_tc_assert_iszero'.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. hnf in H. specialize (H _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
unfold_lift. rewrite <- H. auto.
Qed.
Hint Resolve closed_wrt_tc_iszero : closed.

Lemma closed_wrtl_tc_iszero:
  forall {cs: compspecs}  S e, expr_closed_wrt_lvars S e ->
    closed_wrt_lvars S (expr2.denote_tc_assert (tc_iszero e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (@expr2.denote_tc_assert cs (@tc_iszero cs e)) *)
rewrite binop_lemmas2.denote_tc_assert_iszero'.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. specialize (H _ _ _ H0).
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl. unfold_lift; simpl. rewrite <- H; auto.
Qed.
Hint Resolve closed_wrtl_tc_iszero : closed.

Lemma closed_wrt_tc_isptr:
 forall {cs: compspecs} S e,
     expr_closed_wrt_vars S e ->
     closed_wrt_vars S (denote_tc_assert (tc_isptr e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 specialize (H _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_isptr : closed.

Lemma closed_wrtl_tc_isptr:
 forall {cs: compspecs} S e,
     expr_closed_wrt_lvars S e ->
     closed_wrt_lvars S (denote_tc_assert (tc_isptr e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros. specialize (H _ _ _ H0).
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl. unfold_lift; simpl. rewrite <- H; auto.
Qed.
Hint Resolve closed_wrtl_tc_isptr : closed.

Lemma closed_wrt_tc_isint:
 forall {cs: compspecs} S e,
     expr_closed_wrt_vars S e ->
     closed_wrt_vars S (denote_tc_assert (tc_isint e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 specialize (H _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_isint : closed.

Lemma closed_wrtl_tc_isint:
 forall {cs: compspecs} S e,
     expr_closed_wrt_lvars S e ->
     closed_wrt_lvars S (denote_tc_assert (tc_isint e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (tc_islong e) rho) (@denote_tc_assert cs (tc_islong e) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
 specialize (H _ _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrtl_tc_isint : closed.

Lemma closed_wrt_tc_islong:
 forall {cs: compspecs} S e,
     expr_closed_wrt_vars S e ->
     closed_wrt_vars S (denote_tc_assert (tc_islong e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 specialize (H _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_islong : closed.

Lemma closed_wrtl_tc_islong:
 forall {cs: compspecs} S e,
     expr_closed_wrt_lvars S e ->
     closed_wrt_lvars S (denote_tc_assert (tc_islong e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (tc_islong e) rho) (@denote_tc_assert cs (tc_islong e) (mkEnviron (ge_of rho) ve' (te_of rho))) *)
 specialize (H _ _ _ H0).
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrtl_tc_islong : closed.

Lemma closed_wrt_isCastResultType:
  forall {cs: compspecs} S e t t0,
          expr_closed_wrt_vars S e ->
          closed_wrt_vars S
                 (denote_tc_assert (isCastResultType (implicit_deref t) t0 e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs (@isCastResultType cs (implicit_deref t) t0 e)) *)
rewrite expr_lemmas3.isCastR.
destruct (classify_cast (implicit_deref t) t0) eqn:?;
  simpl; auto with closed;
 try solve [destruct t0 as [ | [ | | | ] [|] | [|] | [ | ] |  | | | | ]; simpl;
                auto with closed; try reflexivity];
  auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 repeat simple_if_tac; try destruct si2; simpl; auto with closed.
(* Goal: @closed_wrt_vars mpred S (@expr2.denote_tc_assert cs (@tc_test_eq cs e (Econst_long Int64.zero (Tlong Unsigned noattr)))) *)
 apply closed_wrt_tc_test_eq; auto with closed.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros. reflexivity.
Qed.

Lemma closed_wrtl_tc_Zge:
  forall  {cs: compspecs} S e i,
   expr_closed_wrt_lvars S e ->
   closed_wrt_lvars S  (denote_tc_assert (tc_Zge e i)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. simpl. unfold_lift. rewrite (H _ _ _ H0). auto.
Qed.

Lemma closed_wrtl_tc_Zle:
  forall  {cs: compspecs} S e i,
   expr_closed_wrt_lvars S e ->
   closed_wrt_lvars S  (denote_tc_assert (tc_Zle e i)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. simpl. unfold_lift. rewrite (H _ _ _ H0). auto.
Qed.
Hint Resolve closed_wrtl_tc_Zge closed_wrtl_tc_Zle : closed.

Lemma closed_wrtl_isCastResultType:
  forall {cs: compspecs} S e t t0,
          expr_closed_wrt_lvars S e ->
          closed_wrt_lvars S
                 (denote_tc_assert (isCastResultType (implicit_deref t) t0 e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs (@isCastResultType cs (implicit_deref t) t0 e)) *)
rewrite expr_lemmas3.isCastR.

(* Goal: @closed_wrt_lvars mpred S (@expr2.denote_tc_assert cs match classify_cast (implicit_deref t) t0 with | Cop.cast_case_pointer => if eqb_type (implicit_deref t) t0 then tc_TT else if orb (andb (is_pointer_type t0) (is_pointer_type (implicit_deref t))) (if Archi.ptr64 then andb (is_long_type t0) (is_long_type (implicit_deref t)) else andb (is_int_type t0) (is_int_type (implicit_deref t))) then tc_TT else if andb (eqb_type t0 int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) (implicit_deref t)) then tc_TT else if andb (eqb_type t0 int_or_ptr_type) (is_pointer_type (implicit_deref t)) then tc_TT else if andb (eqb_type (implicit_deref t) int_or_ptr_type) (is_pointer_type t0) then tc_isptr e else if andb (eqb_type (implicit_deref t) int_or_ptr_type) ((if Archi.ptr64 then is_long_type else is_int_type) t0) then (if Archi.ptr64 then tc_islong else tc_isint) e else @tc_iszero cs e | Cop.cast_case_i2i sz2 si2 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_f2f => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_s2s => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_f2s => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_s2f => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_i2f si1 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_i2s si1 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_f2i sz2 (Signed as si2) => tc_andp (tc_Zge e Int.min_signed) (tc_Zle e Int.max_signed) | Cop.cast_case_f2i sz2 (Unsigned as si2) => tc_andp (tc_Zge e Z0) (tc_Zle e Int.max_unsigned) | Cop.cast_case_s2i sz2 (Signed as si2) => tc_andp (tc_Zge e Int.min_signed) (tc_Zle e Int.max_signed) | Cop.cast_case_s2i sz2 (Unsigned as si2) => tc_andp (tc_Zge e Z0) (tc_Zle e Int.max_unsigned) | Cop.cast_case_l2l => tc_bool (andb (is_long_type (implicit_deref t)) (is_long_type t0)) (invalid_cast_result t0 t0) | Cop.cast_case_i2l si1 => tc_andp (tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result (implicit_deref t) t0)) (if is_pointer_type t0 then @tc_iszero cs e else tc_TT) | Cop.cast_case_l2i sz2 si2 => tc_andp (tc_bool (is_long_type (implicit_deref t)) (invalid_cast_result (implicit_deref t) t0)) (if is_pointer_type t0 then @tc_iszero cs e else tc_TT) | Cop.cast_case_l2f si1 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_l2s si1 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_f2l si2 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_s2l si2 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_i2bool => if is_pointer_type (implicit_deref t) then @tc_test_eq cs e (Econst_int Int.zero (Tint I32 Unsigned noattr)) else tc_TT | Cop.cast_case_l2bool => if is_pointer_type (implicit_deref t) then @tc_test_eq cs e (Econst_long Int64.zero (Tlong Unsigned noattr)) else tc_TT | Cop.cast_case_f2bool => tc_bool (is_float_type (implicit_deref t)) (invalid_cast_result (implicit_deref t) t0) | Cop.cast_case_s2bool => tc_bool (is_single_type (implicit_deref t)) (invalid_cast_result (implicit_deref t) t0) | Cop.cast_case_struct id1 id2 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_union id1 id2 => match t0 with | Tvoid => tc_FF (invalid_cast (implicit_deref t) t0) | Tint i s a => tc_bool (is_int_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tlong s a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfloat (F32 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tfloat (F64 as f) a => tc_bool (is_anyfloat_type (implicit_deref t)) (invalid_cast_result t0 t0) | Tpointer t1 a => tc_FF (invalid_cast (implicit_deref t) t0) | Tarray t1 z a => tc_FF (invalid_cast (implicit_deref t) t0) | Tfunction t1 t2 c => tc_FF (invalid_cast (implicit_deref t) t0) | Tstruct i a => tc_FF (invalid_cast (implicit_deref t) t0) | Tunion i a => tc_FF (invalid_cast (implicit_deref t) t0) end | Cop.cast_case_void => tc_noproof | Cop.cast_case_default => tc_FF (invalid_cast (implicit_deref t) t0) end) *)
change expr2.denote_tc_assert with denote_tc_assert.
destruct (classify_cast (implicit_deref t) t0) eqn:?;
  auto with closed;
 try solve [destruct t0 as [ | [ | | | ] [|] | [|] | [ | ] |  | | | | ]; simpl;
                auto with closed; try reflexivity];
repeat simple_if_tac;  auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 try destruct si2; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs (@tc_test_eq cs e (Econst_long Int64.zero (Tlong Unsigned noattr)))) *)
 apply closed_wrtl_tc_test_eq; auto with closed.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros. reflexivity.
Qed.

Hint Resolve closed_wrt_isCastResultType closed_wrtl_isCastResultType : closed.

Lemma closed_wrt_tc_temp_id :
  forall {cs: compspecs} Delta S e id t, expr_closed_wrt_vars S e ->
                         expr_closed_wrt_vars S (Etempvar id t) ->
             closed_wrt_vars S (tc_temp_id id t Delta e).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (@tc_temp_id id t cs Delta e) *)
unfold tc_temp_id.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs (@typecheck_temp_id cs id t Delta e)) *)
unfold typecheck_temp_id.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs match @PTree.get type id (temp_types Delta) with | Some t0 => tc_andp (tc_bool (is_neutral_cast (implicit_deref t) t0) (invalid_cast t t0)) (@isCastResultType cs (implicit_deref t) t0 e) | None => tc_FF (var_not_in_tycontext Delta id) end) *)
destruct ( (temp_types Delta) ! id) eqn:?; try destruct p; simpl; auto with closed.
Qed.

Lemma closed_wrtl_tc_temp_id :
  forall {cs: compspecs} Delta S e id t, expr_closed_wrt_lvars S e ->
                         expr_closed_wrt_lvars S (Etempvar id t) ->
             closed_wrt_lvars S (tc_temp_id id t Delta e).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (@tc_temp_id id t cs Delta e) *)
unfold tc_temp_id.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs (@typecheck_temp_id cs id t Delta e)) *)
unfold typecheck_temp_id.
(* Goal: @closed_wrt_lvars mpred S (@denote_tc_assert cs match @PTree.get type id (temp_types Delta) with | Some t0 => tc_andp (tc_bool (is_neutral_cast (implicit_deref t) t0) (invalid_cast t t0)) (@isCastResultType cs (implicit_deref t) t0 e) | None => tc_FF (var_not_in_tycontext Delta id) end) *)
destruct ( (temp_types Delta) ! id) eqn:?; try destruct p; simpl; auto with closed.
Qed.

Hint Resolve closed_wrt_tc_temp_id closed_wrtl_tc_temp_id : closed.

Lemma expr_closed_tempvar:
 forall {cs: compspecs} S i t, ~ S i -> expr_closed_wrt_vars S (Etempvar i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
simpl. unfold eval_id. f_equal.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
destruct (H0 i); auto.
(* Goal: @eq (option val) (@Map.get val (te_of rho) i) (@Map.get val (te_of (mkEnviron (ge_of rho) (ve_of rho) te')) i) *)
contradiction.
Qed.
Lemma expr_closedl_tempvar:
 forall S i t, expr_closed_wrt_lvars S (Etempvar i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
simpl. unfold eval_id. f_equal.
Qed.
Hint Resolve expr_closed_tempvar expr_closedl_tempvar : closed.

Hint Extern 1 (not (@eq ident _ _)) => (let Hx := fresh in intro Hx; inversion Hx) : closed.

Lemma expr_closed_cast: forall {cs: compspecs} S e t,
     expr_closed_wrt_vars S e ->
     expr_closed_wrt_vars S (Ecast e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 destruct (H rho te' H0); auto.
Qed.
Lemma expr_closedl_cast: forall S e t,
     expr_closed_wrt_lvars S e ->
     expr_closed_wrt_lvars S (Ecast e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 destruct (H cs rho ve' H0); auto.
Qed.
Hint Resolve expr_closed_cast expr_closedl_cast : closed.

Lemma expr_closed_field: forall {cs: compspecs} S e f t,
  lvalue_closed_wrt_vars S e ->
  expr_closed_wrt_vars S (Efield e f t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_vars, expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
 f_equal.
(* Goal: @eq A (P rho) (P (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 apply H.  auto.
Qed.
Lemma expr_closedl_field: forall S e f t,
  lvalue_closed_wrt_lvars S e ->
  expr_closed_wrt_lvars S (Efield e f t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_lvars, expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
 f_equal.
(* Goal: @eq A (P rho) (P (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 apply H.  auto.
Qed.
Hint Resolve expr_closed_field expr_closedl_field : closed.

Lemma expr_closed_binop: forall {cs: compspecs} S op e1 e2 t,
     expr_closed_wrt_vars S e1 ->
     expr_closed_wrt_vars S e2 ->
     expr_closed_wrt_vars S (Ebinop op e1 e2 t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; auto.
Qed.
Lemma expr_closedl_binop: forall S op e1 e2 t,
     expr_closed_wrt_lvars S e1 ->
     expr_closed_wrt_lvars S e2 ->
     expr_closed_wrt_lvars S (Ebinop op e1 e2 t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; auto.
Qed.
Hint Resolve expr_closed_binop expr_closedl_binop : closed.

Lemma expr_closed_unop: forall {cs: compspecs} S op e t,
     expr_closed_wrt_vars S e ->
     expr_closed_wrt_vars S (Eunop op e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; auto.
Qed.
Lemma expr_closedl_unop: forall S op e t,
     expr_closed_wrt_lvars S e ->
     expr_closed_wrt_lvars S (Eunop op e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; auto.
Qed.
Hint Resolve expr_closed_unop expr_closedl_unop : closed.

Lemma closed_wrt_stackframe_of:
  forall {cs: compspecs} S f, closed_wrt_vars S (stackframe_of f).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_vars mpred S (@stackframe_of cs f) *)
unfold stackframe_of.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
induction (fn_vars f); auto.
(* Goal: @closed_wrt_vars mpred S (@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 type) (forall _ : environ, mpred) (@var_block Tsh cs) (@nil (prod ident type)))) *)
(* Goal: @closed_wrt_vars mpred S (@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 type) (forall _ : environ, mpred) (@var_block Tsh cs) (@cons (prod ident type) a l))) *)
apply closed_wrt_emp.
(* Goal: @closed_wrt_vars mpred S (@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 type) (forall _ : environ, mpred) (@var_block Tsh cs) (@cons (prod ident type) a l))) *)
apply closed_wrt_sepcon; [ | apply IHl].
(* Goal: @closed_wrt_vars mpred S (@var_block Tsh cs a) *)
clear. destruct a; unfold var_block.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. reflexivity.
Qed.
Hint Resolve closed_wrt_stackframe_of : closed.

Definition included {U} (S S': U -> Prop) := forall x, S x -> S' x.

Lemma closed_wrt_TT:
 forall  (S: ident -> Prop),
  closed_wrt_vars S (@TT (environ -> mpred) _).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf; intros. reflexivity.
Qed.
Lemma closed_wrtl_TT:
 forall  (S: ident -> Prop),
  closed_wrt_lvars S (@TT (environ -> mpred) _).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf; intros. reflexivity.
Qed.
Hint Resolve closed_wrt_TT closed_wrtl_TT : closed.

Lemma closed_wrt_subset:
  forall (S S': ident -> Prop) (H: included S' S) B (f: environ -> B),
       closed_wrt_vars S f -> closed_wrt_vars S' f.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf. intros. specialize (H0 rho te').
(* Goal: @eq B (f rho) (f (mkEnviron (ge_of rho) ve' (te_of rho))) *)
apply H0.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
intro i; destruct (H1 i); auto.
Qed.
Lemma closed_wrtl_subset:
  forall (S S': ident -> Prop) (H: included S' S) B (f: environ -> B),
       closed_wrt_lvars S f -> closed_wrt_lvars S' f.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. hnf. intros. specialize (H0 rho ve').
(* Goal: @eq B (f rho) (f (mkEnviron (ge_of rho) ve' (te_of rho))) *)
apply H0.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
intro i; destruct (H1 i); auto.
Qed.
Hint Resolve closed_wrt_subset closed_wrtl_subset : closed.

Lemma closed_wrt_Forall_subset:
  forall S S' (H: included S' S) B (f: list (environ -> B)),
 Forall (closed_wrt_vars S) f ->
 Forall (closed_wrt_vars S') f.
Proof.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@nil (forall _ : environ, A))) (@nil (forall _ : environ, A)) *)
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
induction f; simpl; auto.
(* Goal: not (not_a_param L i) *)
intro.
(* Goal: @Forall (forall _ : environ, B) (@closed_wrt_lvars B S') (@cons (forall _ : environ, B) a f) *)
inv H0.
(* Goal: @Forall (forall _ : environ, B) (@closed_wrt_lvars B S') (@cons (forall _ : environ, B) a f) *)
constructor.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply (closed_wrt_subset _ _ H). auto.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
auto.
Qed.
Lemma closed_wrtl_Forall_subset:
  forall S S' (H: included S' S) B (f: list (environ -> B)),
 Forall (closed_wrt_lvars S) f ->
 Forall (closed_wrt_lvars S') f.
Proof.
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@nil (forall _ : environ, A))) (@nil (forall _ : environ, A)) *)
(* Goal: @eq (list (forall _ : environ, A)) (@map (forall _ : environ, A) (forall _ : environ, A) (@subst A id e) (@cons (forall _ : environ, A) a Q)) (@cons (forall _ : environ, A) a Q) *)
induction f; simpl; auto.
(* Goal: not (not_a_param L i) *)
intro.
(* Goal: @Forall (forall _ : environ, B) (@closed_wrt_lvars B S') (@cons (forall _ : environ, B) a f) *)
inv H0.
(* Goal: @Forall (forall _ : environ, B) (@closed_wrt_lvars B S') (@cons (forall _ : environ, B) a f) *)
constructor.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply (closed_wrtl_subset _ _ H). auto.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
auto.
Qed.

Lemma lvalue_closed_tempvar:
 forall {cs: compspecs} S i t, ~ S i -> lvalue_closed_wrt_vars S (Etempvar i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
simpl; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
simpl. reflexivity.
Qed.
Lemma lvalue_closedl_tempvar:
 forall S i t, lvalue_closed_wrt_lvars S (Etempvar i t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
simpl; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
simpl. reflexivity.
Qed.
Hint Resolve lvalue_closed_tempvar lvalue_closedl_tempvar : closed.

Lemma expr_closed_addrof: forall {cs: compspecs} S e t,
     lvalue_closed_wrt_vars S e ->
     expr_closed_wrt_vars S (Eaddrof e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_vars, expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. apply H.  auto.
Qed.
Lemma expr_closedl_addrof: forall S e t,
     lvalue_closed_wrt_lvars S e ->
     expr_closed_wrt_lvars S (Eaddrof e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_lvars, expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. apply H.  auto.
Qed.
Hint Resolve expr_closed_addrof expr_closedl_addrof : closed.

Lemma lvalue_closed_field: forall {cs: compspecs} S e f t,
  lvalue_closed_wrt_vars S e ->
  lvalue_closed_wrt_vars S (Efield e f t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_vars, expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; apply H.  auto.
Qed.
Lemma lvalue_closedl_field: forall S e f t,
  lvalue_closed_wrt_lvars S e ->
  lvalue_closed_wrt_lvars S (Efield e f t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_lvars, expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. f_equal; apply H.  auto.
Qed.
Hint Resolve lvalue_closed_field lvalue_closedl_field : closed.

Lemma lvalue_closed_deref: forall {cs: compspecs} S e t,
  expr_closed_wrt_vars S e ->
  lvalue_closed_wrt_vars S (Ederef e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_vars, expr_closed_wrt_vars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. apply H.  auto.
Qed.
Lemma lvalue_closedl_deref: forall S e t,
  expr_closed_wrt_lvars S e ->
  lvalue_closed_wrt_lvars S (Ederef e t).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 unfold lvalue_closed_wrt_lvars, expr_closed_wrt_lvars; intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
 simpl.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 super_unfold_lift. apply H.  auto.
Qed.
Hint Resolve lvalue_closed_deref lvalue_closedl_deref: closed.

Fixpoint closed_eval_expr (j: ident) (e: expr) : bool :=
 match e with
 | Econst_int i ty => true
 | Econst_long i ty => true
 | Econst_float f ty => true
 | Econst_single f ty => true
 | Etempvar id ty => negb (eqb_ident j id)
 | Eaddrof a ty => closed_eval_lvalue j a
 | Eunop op a ty =>  closed_eval_expr j a
 | Ebinop op a1 a2 ty =>  andb (closed_eval_expr j a1) (closed_eval_expr j a2)
 | Ecast a ty => closed_eval_expr j a
 | Evar id ty => true
 | Ederef a ty => closed_eval_expr j a
 | Efield a i ty => closed_eval_lvalue j a
 | Esizeof _ _ => true
 | Ealignof _ _ => true
 end

 with closed_eval_lvalue (j: ident) (e: expr) : bool :=
 match e with
 | Evar id ty => true
 | Ederef a ty => closed_eval_expr j a
 | Efield a i ty => closed_eval_lvalue j a
 | _  => false
 end.

Lemma closed_eval_expr_e:
    forall {cs: compspecs} j e, closed_eval_expr j e = true -> closed_wrt_vars (eq j) (eval_expr e)
with closed_eval_lvalue_e:
    forall {cs: compspecs} j e, closed_eval_lvalue j e = true -> closed_wrt_vars (eq j) (eval_lvalue e).
Proof.
intros cs j e; clear closed_eval_expr_e; induction e; intros; simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
simpl in H. destruct (eqb_ident j i) eqn:?; inv H.
apply Pos.eqb_neq in Heqb. auto with closed.
simpl in H.
rewrite andb_true_iff in H. destruct H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
intros Delta j e; clear closed_eval_lvalue_e; induction e; intros; simpl; auto with closed.
Qed.

Hint Extern 2 (closed_wrt_vars (eq _) (@eval_expr _ _)) => (apply closed_eval_expr_e; reflexivity) : closed.
Hint Extern 2 (closed_wrt_vars (eq _) (@eval_lvalue _ _)) => (apply closed_eval_lvalue_e; reflexivity) : closed.

Lemma closed_wrt_eval_expr: forall {cs: compspecs} S e,
  expr_closed_wrt_vars S e ->
  closed_wrt_vars S (eval_expr e).
Proof.
(* Goal: forall (cs : compspecs) (S : forall _ : ident, Prop) (e : expr) (_ : @expr_closed_wrt_vars cs S e), @closed_wrt_vars val S (@eval_expr cs e) *)
unfold expr_closed_wrt_vars, closed_wrt_vars.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply H; auto.
Qed.
(* Hint Resolve closed_wrt_eval_expr : closed. *)

Lemma closed_wrt_lvalue: forall {cs: compspecs} S e,
  access_mode (typeof e) = By_reference ->
  closed_wrt_vars S (eval_expr e) -> closed_wrt_vars S (eval_lvalue e).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
destruct e; simpl in *; auto with closed;
unfold closed_wrt_vars in *;
intros; specialize (H0 _ _ H1); clear H1; super_unfold_lift;
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
auto.
Qed.
(* Hint Resolve closed_wrt_lvalue : closed. *)

Lemma closed_wrt_ideq: forall {cs: compspecs} a b e,
  a <> b ->
  closed_eval_expr a e = true ->
  closed_wrt_vars (eq a) (fun rho => !! (eval_id b rho = eval_expr e rho)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
simpl. f_equal.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
f_equal.
(* Goal: @eq val (eval_id b rho) (eval_id b (mkEnviron (ge_of rho) (ve_of rho) te')) *)
(* Goal: @eq val (@eval_expr cs e rho) (@eval_expr cs e (mkEnviron (ge_of rho) (ve_of rho) te')) *)
specialize (H1 b).
(* Goal: @eq val (eval_id b rho) (eval_id b (mkEnviron (ge_of rho) (ve_of rho) te')) *)
(* Goal: @eq val (@eval_expr cs e rho) (@eval_expr cs e (mkEnviron (ge_of rho) (ve_of rho) te')) *)
destruct H1; [contradiction | ].
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
unfold eval_id; simpl. rewrite H1. auto.
(* Goal: @eq val (@eval_expr cs e rho) (@eval_expr cs e (mkEnviron (ge_of rho) (ve_of rho) te')) *)
clear b H.
(* Goal: @eq val (@eval_expr cs e rho) (@eval_expr cs e (mkEnviron (ge_of rho) (ve_of rho) te')) *)
eapply closed_eval_expr_e in H0.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply H0; auto.
Qed.

Hint Extern 2 (closed_wrt_vars (eq _) _) =>
      (apply closed_wrt_ideq; [solve [let Hx := fresh in (intro Hx; inv Hx)] | reflexivity]) : closed.

Lemma closed_wrt_tc_nonzero:
 forall {cs: compspecs} S e,
     closed_wrt_vars S (eval_expr e) ->
     closed_wrt_vars S (denote_tc_assert (tc_nonzero e)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 specialize (H _ _ H0).
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nonzero cs e) rho) (@denote_tc_assert cs (@tc_nonzero cs e) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 repeat rewrite binop_lemmas2.denote_tc_assert_nonzero.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 rewrite <- H; auto.
Qed.
Hint Resolve closed_wrt_tc_nonzero : closed.

Lemma closed_wrt_binarithType:
  forall {cs: compspecs} S t1 t2 t a b,
  closed_wrt_vars S (denote_tc_assert (binarithType t1 t2 t a b)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros.
(* Goal: @closed_wrt_vars mpred S (@denote_tc_assert cs (binarithType t1 t2 t a b)) *)
 unfold binarithType.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (Cop.classify_binarith t1 t2); simpl; auto with closed.
Qed.
Hint Resolve closed_wrt_binarithType : closed.

Lemma closed_wrt_tc_samebase :
 forall {cs: compspecs} S e1 e2,
 closed_wrt_vars S (eval_expr e1) ->
 closed_wrt_vars S (eval_expr e2) ->
 closed_wrt_vars S (denote_tc_assert (tc_samebase e1 e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros;  hnf; intros. simpl. unfold_lift. f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_samebase : closed.

Lemma closed_wrt_tc_ilt:
  forall {cs: compspecs} S e n,
    closed_wrt_vars S (eval_expr e) ->
    closed_wrt_vars S (denote_tc_assert (tc_ilt e n)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros; hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_ilt cs e n) rho) (@denote_tc_assert cs (@tc_ilt cs e n) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 repeat rewrite binop_lemmas2.denote_tc_assert_ilt'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal. auto.
Qed.
Hint Resolve closed_wrt_tc_ilt : closed.

Lemma closed_wrt_tc_llt:
  forall {cs: compspecs} S e n,
    closed_wrt_vars S (eval_expr e) ->
    closed_wrt_vars S (denote_tc_assert (tc_llt e n)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros; hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_llt cs e n) rho) (@denote_tc_assert cs (@tc_llt cs e n) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 repeat rewrite binop_lemmas2.denote_tc_assert_llt'.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 simpl. unfold_lift. f_equal. auto.
Qed.
Hint Resolve closed_wrt_tc_llt : closed.

Lemma closed_wrt_tc_Zge:
  forall {cs: compspecs} S e n,
    closed_wrt_vars S (eval_expr e) ->
    closed_wrt_vars S (denote_tc_assert (tc_Zge e n)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros; hnf; intros.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
 simpl. unfold_lift; f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_Zge : closed.
Lemma closed_wrt_tc_Zle:
  forall {cs: compspecs} S e n,
    closed_wrt_vars S (eval_expr e) ->
    closed_wrt_vars S (denote_tc_assert (tc_Zle e n)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros; hnf; intros.
(* Goal: @eq mpred (denote_tc_samebase (@eval_expr cs e1 rho) (@eval_expr cs e2 rho)) (denote_tc_samebase (@eval_expr cs e1 (mkEnviron (ge_of rho) (ve_of rho) te')) (@eval_expr cs e2 (mkEnviron (ge_of rho) (ve_of rho) te'))) *)
 simpl. unfold_lift; f_equal; auto.
Qed.
Hint Resolve closed_wrt_tc_Zle : closed.

Lemma closed_wrt_replace_nth:
  forall {B} S n R (R1: environ -> B),
    closed_wrt_vars S R1 ->
    Forall (closed_wrt_vars S) R ->
    Forall (closed_wrt_vars S) (replace_nth n R R1).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
revert R H0; induction n; destruct R; simpl; intros; auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
inv H0; constructor; auto with closed.
Qed.
Hint Resolve @closed_wrt_replace_nth : closed.

Lemma closed_wrt_tc_nodivover :
 forall {cs: compspecs} S e1 e2,
 closed_wrt_vars S (eval_expr e1) ->
 closed_wrt_vars S (eval_expr e2) ->
 closed_wrt_vars S (denote_tc_assert (tc_nodivover e1 e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
 intros;  hnf; intros.
(* Goal: @eq mpred (@denote_tc_assert cs (@tc_nodivover cs e1 e2) rho) (@denote_tc_assert cs (@tc_nodivover cs e1 e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
 repeat rewrite binop_lemmas2.denote_tc_assert_nodivover.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 rewrite <- H0; auto. rewrite <- H; auto.
Qed.
Hint Resolve closed_wrt_tc_nodivover : closed.

Lemma closed_wrt_tc_nosignedover:
  forall op {CS: compspecs} S e1 e2,
  closed_wrt_vars S (eval_expr e1) ->
  closed_wrt_vars S (eval_expr e2) ->
  closed_wrt_vars S (denote_tc_assert (tc_nosignedover op e1 e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros; hnf; intros.
(* Goal: @eq mpred (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) rho) (@liftx (Tarrow val (Tarrow val (LiftEnviron mpred))) (denote_tc_nosignedover op) (@eval_expr CS e1) (@eval_expr CS e2) (mkEnviron (ge_of rho) (ve_of rho) te')) *)
simpl. unfold_lift.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite <- H; auto.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
rewrite <- H0; auto.
Qed.
Hint Resolve closed_wrt_tc_nosignedover : closed.

Lemma closed_wrt_tc_nobinover:
  forall op {CS: compspecs} S e1 e2,
  closed_wrt_vars S (eval_expr e1) ->
  closed_wrt_vars S (eval_expr e2) ->
  closed_wrt_vars S (denote_tc_assert (tc_nobinover op e1 e2)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
unfold tc_nobinover.
unfold if_expr_signed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
destruct (typeof e1); auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
destruct s; auto with closed.
destruct (eval_expr e1 any_environ); auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
destruct (eval_expr e2 any_environ); auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
all: repeat simple_if_tac; auto with closed.
destruct (eval_expr e1 any_environ); auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
destruct (eval_expr e2 any_environ); auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
all: try destruct s; repeat simple_if_tac; auto with closed.
Qed.

Hint Resolve closed_wrt_tc_nobinover : closed.

Lemma closed_wrt_tc_expr:
  forall {cs: compspecs} Delta j e, closed_eval_expr j e = true ->
             closed_wrt_vars (eq j) (tc_expr Delta e)
 with closed_wrt_tc_lvalue:
  forall {cs: compspecs} Delta j e, closed_eval_lvalue j e = true ->
             closed_wrt_vars (eq j) (tc_lvalue Delta e).
Proof.
* clear closed_wrt_tc_expr.
unfold tc_expr.
induction e; simpl; intros;
try solve [destruct t  as [ | [ | | | ] [ | ] | | [ | ] | | | | | ]; simpl; auto with closed].
+
  destruct (access_mode t);  simpl; auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
  destruct (get_var_type Delta i); simpl; auto with closed.
+
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
  destruct ((temp_types Delta) ! i); simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
  destruct (is_neutral_cast t0 t || same_base_type t0 t)%bool; simpl; auto with closed.
  clear -  H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
  hnf; intros.
  specialize (H0 i).
  pose proof (eqb_ident_spec j i).
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
  destruct (eqb_ident j i); inv H.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
  destruct H0. apply H1 in H; inv H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
  unfold denote_tc_initialized;  simpl.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
  f_equal.
  apply exists_ext; intro v.
(* Goal: @eq (prod A unit) (@pair A unit (P rho) tt) (@pair A unit (P (mkEnviron (ge_of rho) (ve_of rho) te')) tt) *)
  f_equal. rewrite H; auto.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
+ destruct (access_mode t) eqn:?H; simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
  apply closed_wrt_tc_andp; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
  apply closed_wrt_tc_isptr; auto with closed.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
  apply closed_eval_expr_e; auto.
+
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 apply closed_wrt_tc_andp; auto with closed.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 apply closed_wrt_tc_lvalue; auto.
+
 specialize (IHe H).
 apply closed_eval_expr_e in H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 repeat apply closed_wrt_tc_andp; auto with closed.
 unfold isUnOpResultType.
 destruct u;
 destruct (typeof e) as   [ | [ | | | ] [ | ] | | [ | ] | | | | | ];
   simpl; repeat apply closed_wrt_tc_andp; auto 50 with closed;
  rewrite binop_lemmas2.denote_tc_assert_test_eq';
  simpl; unfold_lift;
  hnf; intros ? ? H8; simpl;
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
  rewrite <- (H _ _ H8); auto.
+
  rewrite andb_true_iff in H. destruct H.
 specialize (IHe1 H). specialize (IHe2 H0).
 apply closed_eval_expr_e in H; apply closed_eval_expr_e in H0.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 repeat apply closed_wrt_tc_andp; auto with closed.
 unfold isBinOpResultType.
 destruct b; auto 50 with closed;
 try solve [destruct (Cop.classify_binarith (typeof e1) (typeof e2));
                try destruct s;  auto with closed];
 try solve [destruct (Cop.classify_cmp (typeof e1) (typeof e2));
                 simpl; auto 50 with closed].
 destruct (Cop.classify_add (typeof e1) (typeof e2)); auto 50 with closed.
 destruct (Cop.classify_sub (typeof e1) (typeof e2)); auto 50 with closed.
 destruct (Cop.classify_shift (typeof e1) (typeof e2)); auto 50 with closed.
 destruct (Cop.classify_shift (typeof e1) (typeof e2)); auto 50 with closed.

+
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 apply closed_wrt_tc_andp; auto with closed.
 specialize (IHe H).
 apply closed_eval_expr_e in H.
 unfold isCastResultType.
 destruct (classify_cast (typeof e) t); auto with closed;
   try solve [ destruct t as [ | [ | | | ] [ | ]| [ | ] | [ | ] | | | | | ]; auto with closed].
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
all: repeat simple_if_tac; try destruct si2; auto with closed.
(* Goal: @closed_wrt_vars mpred S (@expr2.denote_tc_assert cs (@tc_test_eq cs e (Econst_long Int64.zero (Tlong Unsigned noattr)))) *)
 apply closed_wrt_tc_test_eq; auto with closed.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
 hnf; intros; reflexivity.
(* Goal: @eq ident (@fst ident type (@pair ident type i t)) i *)
 hnf; intros; reflexivity.
+
 clear IHe.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (access_mode t); simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 repeat apply closed_wrt_tc_andp; auto with closed.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
 apply closed_wrt_tc_lvalue; auto.
 destruct (typeof e); simpl; auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (cenv_cs ! i0); simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (field_offset cenv_cs i (co_members c)); simpl; auto with closed.
*
 clear closed_wrt_tc_lvalue.
 unfold tc_lvalue.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 induction e; simpl; intros; auto with closed.
 +
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (get_var_type Delta i); simpl; auto with closed.
 +
 specialize (closed_wrt_tc_expr cs Delta _ _ H).
 apply closed_eval_expr_e in H.
 auto 50 with closed.
 +
 specialize (IHe H).
 apply closed_eval_lvalue_e  in H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 repeat apply closed_wrt_tc_andp; auto with closed.
 destruct (typeof e); simpl; auto with closed;
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (cenv_cs ! i0); simpl; auto with closed.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
 destruct (field_offset cenv_cs i (co_members c)); simpl; auto with closed.
Qed.

Hint Resolve closed_wrt_tc_expr : closed.
Hint Resolve closed_wrt_tc_lvalue : closed.


Lemma closed_wrt_lift1':
      forall (A B : Type) (S : ident -> Prop) (f : A -> B)
         (P : environ -> A),
       closed_wrt_vars S P -> closed_wrt_vars S (`f P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_vars B S (@liftx (Tarrow A (LiftEnviron B)) f P) *)
apply closed_wrt_lift1.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. simpl. f_equal.
(* Goal: @eq A (P rho) (P (mkEnviron (ge_of rho) (ve_of rho) te')) *)
apply H. auto.
Qed.
Hint Resolve closed_wrt_lift1' : closed.

Lemma closed_wrt_Econst_int:
  forall {cs: compspecs} S i t, closed_wrt_vars S (eval_expr (Econst_int i t)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
simpl; intros.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
Qed.
Hint Resolve closed_wrt_Econst_int : closed.

Lemma closed_wrt_PROPx:
 forall S P Q, closed_wrt_vars S Q -> closed_wrt_vars S (PROPx P Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply closed_wrt_andp; auto.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. reflexivity.
Qed.
Lemma closed_wrtl_PROPx:
 forall S P Q, closed_wrt_lvars S Q -> closed_wrt_lvars S (PROPx P Q).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply closed_wrtl_andp; auto.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
hnf; intros. reflexivity.
Qed.
Hint Resolve closed_wrt_PROPx closed_wrtl_PROPx: closed.


Lemma closed_wrt_LOCALx:
 forall S Q R, Forall (closed_wrt_vars S) (map locald_denote Q) ->
                    closed_wrt_vars S R ->
                    closed_wrt_vars S (LOCALx Q R).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply closed_wrt_andp; auto.
(* Goal: @closed_wrt_lvars mpred S (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) *)
clear - H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
induction Q; simpl; intros.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
(* Goal: @closed_wrt_lvars mpred S (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote a) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
normalize. autorewrite with norm1 norm2; normalize.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
inv H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
apply closed_wrt_andp; auto with closed.
Qed.


Lemma closed_wrtl_LOCALx:
 forall S Q R, Forall (closed_wrt_lvars S) (map locald_denote Q) ->
                    closed_wrt_lvars S R ->
                    closed_wrt_lvars S (LOCALx Q R).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply closed_wrtl_andp; auto.
(* Goal: @closed_wrt_lvars mpred S (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) *)
clear - H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
induction Q; simpl; intros.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
(* Goal: @closed_wrt_lvars mpred S (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote a) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
normalize. autorewrite with norm1 norm2; normalize.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
inv H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
apply closed_wrtl_andp; auto with closed.
Qed.
(*
Lemma closed_wrt_LOCALx:
 forall S Q R, Forall (fun q => closed_wrt_vars S (local q)) Q ->
                    closed_wrt_vars S R ->
                    closed_wrt_vars S (LOCALx Q R).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
apply closed_wrt_andp; auto.
(* Goal: @closed_wrt_lvars mpred S (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) *)
clear - H.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
induction Q; simpl; intros.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
(* Goal: @closed_wrt_lvars mpred S (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote a) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
normalize.
(* Goal: @closed_wrt_lvars mpred S (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (locald_denote a)) (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)))) *)
inv H.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
apply closed_wrt_andp; auto with closed.
Qed.
*)

Hint Resolve closed_wrt_LOCALx closed_wrtl_LOCALx: closed.

Lemma closed_wrt_SEPx: forall S P,
     closed_wrt_vars S (SEPx P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (SEPx P) *)
unfold SEPx.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
Qed.

Lemma closed_wrtl_SEPx: forall S P,
     closed_wrt_lvars S (SEPx P).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: @closed_wrt_lvars mpred S (SEPx P) *)
unfold SEPx.
(* Goal: @closed_wrt_lvars mpred S (fun _ : environ => fold_right_sepcon P) *)
auto with closed.
Qed.
Hint Resolve closed_wrt_SEPx closed_wrtl_SEPx: closed.

Lemma not_not_a_param_i:
  forall (L: list (ident * type)) i,
   In i (map (@fst _ _) L) ->
   ~ not_a_param L i.
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
intro. apply H0; auto.
Qed.
Hint Resolve not_not_a_param_i : closed.

Lemma in_map_fst1:
 forall (i: ident) (t: type) L,
   In i (map (@fst _ _) ((i,t)::L)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros. left. reflexivity.
Qed.
Hint Resolve in_map_fst1 : closed.

Lemma in_map_fst2:
 forall (i: ident) a (L: list (ident*type)),
   In i (map (@fst _ _) L) ->
   In i (map (@fst _ _) (a::L)).
Proof.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
intros; right; auto.
Qed.
Hint Resolve in_map_fst2 : closed.

Ltac precondition_closed :=
 match goal with |- precondition_closed _ _ => idtac end;
 let x := fresh "x" in intro x;
 split;
  repeat match goal with
          | |- closed_wrt_vars _ (let (y,z) := ?x in _) => is_var x; destruct x
          | |- closed_wrt_lvars _ (let (y,z) := ?x in _) => is_var x; destruct x
          end;
  [simpl not_a_param; auto 50 with closed
  | simpl is_a_local; auto 50 with closed ].

Lemma Forall_map_cons:
  forall {A B} (F: A -> Prop) (g: B -> A) b bl,
  F (g b) -> Forall F (map g bl) ->
  Forall F (map g (b::bl)).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
constructor; auto.
Qed.

Lemma Forall_map_nil:
  forall {A B} (F: A -> Prop) (g: B -> A),
  Forall F (map g nil).
Proof.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (g : forall _ : B, A), @Forall A F (@map B A g (@nil B)) *)
simpl.
(* Goal: forall (A B : Type) (F : forall _ : A, Prop) (_ : forall _ : B, A), @Forall A F (@nil A) *)
intros.
(* Goal: forall i : ident, or (S i) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
constructor; auto.
Qed.
Hint Resolve @Forall_map_cons @Forall_map_nil : closed.
Hint Resolve Forall_cons Forall_nil : closed.
