Require Import VST.veric.juicy_base.
Require Import VST.msl.normalize.
Require Import VST.veric.juicy_mem VST.veric.juicy_mem_lemmas VST.veric.juicy_mem_ops.
Require Import VST.veric.res_predicates.
Require Import VST.veric.extend_tc.
Require Import VST.veric.Clight_seplog.
Require Import VST.veric.Clight_assert_lemmas.
Require Import VST.veric.Clight_new.
Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.expr_lemmas.
Require Import VST.veric.semax.
Require Import VST.veric.semax_lemmas.
Require Import VST.veric.Clight_lemmas.

Lemma closed_wrt_modvars_switch:
  forall a sl n F,
  closed_wrt_modvars (Sswitch a sl) F ->
  closed_wrt_modvars (seq_of_labeled_statement (select_switch n sl)) F.
Proof.
(* Goal: forall (a : expr) (sl : labeled_statements) (n : Z) (F : assert) (_ : closed_wrt_modvars (Sswitch a sl) F), closed_wrt_modvars (seq_of_labeled_statement (select_switch n sl)) F *)
unfold closed_wrt_modvars, modifiedvars.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @closed_wrt_vars mpred (fun id : ident => @isSome unit (@PTree.get unit id (modifiedvars' (seq_of_labeled_statement (select_switch n sl)) idset0))) F *)
intros rho te' H0; apply H.
(* Goal: forall i : ident, or (@isSome unit (@PTree.get unit i (modifiedvars' (Sswitch a sl) idset0))) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
intros; specialize (H0 i).
(* Goal: or (@isSome unit (@PTree.get unit i (modifiedvars' (Sswitch a sl) idset0))) (@eq (option val) (@Map.get val (te_of rho) i) (@Map.get val te' i)) *)
destruct H0; auto;left.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (Sswitch a sl) idset0)) *)
clear - H0.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement LSnil) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement (LScons o s sl)) s0)) *)
simpl in *.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl idset0)) *)
forget idset0 as s.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
assert (isSome (modifiedvars' (seq_of_labeled_statement sl) s) ! i). {
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
  unfold select_switch in *.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
  destruct (select_switch_case n sl) eqn:?.
 *
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
  revert l Heqo s H0; induction sl ;intros. inv Heqo.
(* Goal: @derives nat ag_nat (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (@seplog.sepcon assert (@seplog.LiftNatDed environ mpred (@alg_seplog.algNatDed rmap ag_rmap)) (@seplog.LiftSepLog environ mpred (@alg_seplog.algNatDed rmap ag_rmap) (@alg_seplog.algSepLog rmap ag_rmap Join_rmap Perm_rmap Sep_rmap Age_rmap)) (proj_ret_assert R ek' vl') F rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (@seplog.sepcon assert (@seplog.LiftNatDed environ mpred (@alg_seplog.algNatDed rmap ag_rmap)) (@seplog.LiftSepLog environ mpred (@alg_seplog.algNatDed rmap ag_rmap) (@alg_seplog.algSepLog rmap ag_rmap Join_rmap Perm_rmap Sep_rmap Age_rmap)) (proj_ret_assert (switch_ret_assert R) ek vl) F rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
  simpl. simpl in Heqo. destruct o. destruct (zeq z n).
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
  inv Heqo; subst. simpl in H0. auto.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
  specialize (IHsl _ Heqo _ H0).
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  rewrite modifiedvars'_union; right; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  rewrite modifiedvars'_union; right; eauto.
 *
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
  revert sl Heqo s H0; induction sl; intros.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement LSnil) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement (LScons o s sl)) s0)) *)
  simpl in *. auto.
  simpl in Heqo, H0|- *.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
  destruct o.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
  destruct (zeq z n). inv Heqo.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  rewrite modifiedvars'_union; right; eauto.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' s (modifiedvars' (seq_of_labeled_statement sl) s0))) *)
  simpl in H0. auto.
}
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
 clear - H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 revert s H; induction sl; simpl; intros; auto.
 rewrite modifiedvars'_union in H|-*.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 destruct H;[left|right]; auto.
Qed.
(*
Lemma typecheck_environ_join_switch2:
   forall sl Delta rho,
    typecheck_environ Delta rho ->
    typecheck_environ (join_tycon_labeled sl Delta) rho.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
 intros.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 induction sl; simpl; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 apply typecheck_environ_join2 with Delta; auto.
apply tycontext_evolve_update_tycon.
 clear.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 induction sl; simpl; auto.
apply tycontext_evolve_refl.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply tycontext_evolve_join; auto.
apply tycontext_evolve_update_tycon.
Qed.

Lemma typecheck_environ_join_switch1:
  forall n sl rho Delta,
    typecheck_environ
      (update_tycon Delta (seq_of_labeled_statement (select_switch n sl))) rho ->
    typecheck_environ (join_tycon_labeled sl Delta) rho.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
 intros.
 unfold select_switch in H.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
 destruct (select_switch_case n sl) eqn:?.
 apply typecheck_environ_update in H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 apply typecheck_environ_join_switch2; auto.
 apply typecheck_environ_update in H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 apply typecheck_environ_join_switch2; auto.
Qed.
*) 

Lemma frame_tc_expr:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {CS: compspecs} (Q F: mpred) Delta e rho,
  Q |-- tc_expr Delta e rho ->
  Q * F |-- tc_expr Delta e rho.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q F) (@tc_expr CS Delta e rho) *)
eapply derives_trans; [apply sepcon_derives; [apply H | apply derives_refl ] | ].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@tc_expr CS Delta e rho) F) (@tc_expr CS Delta e rho) *)
apply extend_sepcon; apply extend_tc_expr.
Qed.

Lemma subp_trans':
  forall A (NA: ageable A) (P Q R: pred A) w,  
    app_pred (P >=> Q) w ->
    app_pred (Q >=> R) w -> 
    app_pred (P >=> R) w.
Proof.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 repeat intro.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 eapply H0; eauto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 eapply H; eauto.
Qed.

Lemma prop_subp:
   forall A (NA: ageable A) (P Q: Prop) (w: nat),
    (P -> Q) -> app_pred (!! P >=> !! Q)  w.
Proof.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
repeat intro. apply H. apply H2.
Qed.

Lemma andp_subp'_right:
  forall A (NA: ageable A) (P Q R: pred A) w,  
    app_pred (P >=> Q) w ->
    app_pred (P >=> R) w -> 
    app_pred (P >=> Q && R) w.
Proof.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
repeat intro.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
split. eapply H; eauto. eapply H0; eauto.
Qed.

Lemma prop_true_imp:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {A} {agA: ageable A} (P: Prop) (Q: pred A),
   P ->   (!! P --> Q)%pred = Q.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
apply pred_ext.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
intros ? ?. apply H0; auto.
(* Goal: @derives A agA P (@imp A agA Q R) *)
intros ? ? ? ? ?.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply pred_nec_hereditary; eauto.
Qed.

Lemma prop_imp_right: forall A (agA: ageable A) (P: Prop) (Q R: pred A),
   (P -> (Q |-- R)) ->
   Q |-- !! P --> R.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA Q (@imp A agA (@prop A agA P) R) *)
intros w ? ? ? ?.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply H; auto. eapply pred_nec_hereditary; eauto.
Qed.

(*Moved to semax_lemmas
Lemma semax_eq:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
 forall {Espec: OracleKind} {CS: compspecs} Delta P c R,
  semax Espec Delta P c R = 
  (TT |-- (ALL psi : genv,
         ALL Delta' : tycontext,
         !! (tycontext_sub Delta Delta' /\ genv_cenv psi = cenv_cs) -->
         believe Espec Delta' psi Delta' -->
         ALL k : cont ,
         ALL F : assert ,
         !! closed_wrt_modvars c F &&
         rguard Espec psi (exit_tycon c Delta') (frame_ret_assert R F) k -->
         guard Espec psi Delta' (fun rho : environ => F rho * P rho) (Kseq c :: k))).
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
extensionality w.
rewrite semax_fold_unfold.
apply prop_ext; intuition.
Qed.*)

Lemma imp_right:
 forall A (agA: ageable A) (P Q R : pred A),
  P && Q |-- R ->
  P |-- Q --> R.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA P (@imp A agA Q R) *)
intros ? ? ? ? ?.
(* Goal: @app_pred nat ag_nat Q (@level A agA a) *)
apply H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
split; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply pred_nec_hereditary; eauto.
Qed.

Lemma prop_andp_subp':
  forall (A : Type) (agA : ageable A) (P : Prop) (S: pred nat) (Q R : pred A),
  (P -> S |-- Q >=> R)%pred
  ->  (S  |--  !! P && Q >=> R)%pred.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives nat ag_nat S (@fash A agA (@imp A agA (@andp A agA (@prop A agA P) Q) R)) *)
intros ? ? ? ? ? ? [? ?].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply H; eauto.
Qed.

(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
Lemma tc_expr_sound {CS: compspecs}:
 forall Delta e rho, typecheck_environ Delta rho -> 
     tc_expr Delta e rho |-- !! tc_val (typeof e) (eval_expr e rho).
Proof.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
repeat intro.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply typecheck_expr_sound; eauto.
Qed.

(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
Lemma unfash_allp:  forall {A} {agA: ageable A} {B} (f: B -> pred nat),
  @unfash _ agA (allp f) = allp (fun x:B => unfash (f x)).
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
apply pred_ext.
(* Goal: @app_pred A NA (@imp A NA P Q) a *)
intros ? ? ?.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
specialize (H b). auto.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
repeat intro. apply (H b).
Qed.

(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
Lemma fash_TT: forall {A} {agA: ageable A}, @unfash A agA TT = TT.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@TT nat ag_nat)) (@TT A agA) *)
apply pred_ext; intros ? ?; apply I.
Qed.

Lemma allp_andp: 
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {A} {NA: ageable A} {B: Type} (b0: B) (P: B -> pred A) (Q: pred A),
   (allp P && Q = allp (fun x => P x && Q))%pred.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
apply pred_ext.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
intros ? [? ?] b. split; auto.
(* Goal: @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros ? ?.
(* Goal: @app_pred A NA (@andp A NA (@allp A NA B P) Q) a *)
split.
(* Goal: @app_pred A NA (P b) a *)
(* Goal: @app_pred A NA Q a *)
intro b. apply (H b).
(* Goal: @app_pred A NA Q a *)
apply (H b0).
Qed.

Lemma unfash_prop_imp:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {A} {agA: ageable A} (P: Prop) (Q: pred nat),
  (@unfash _ agA (prop P --> Q) = prop P --> @unfash _ agA Q)%pred.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply pred_ext; repeat intro.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply H; auto. apply necR_level'; auto.
(* Goal: @app_pred nat ag_nat Q a' *)
hnf in H.
(* Goal: @app_pred nat ag_nat Q a' *)
specialize (H a (necR_refl _) H1).
(* Goal: @app_pred nat ag_nat Q a' *)
eapply pred_nec_hereditary; try apply H0.
(* Goal: @app_pred nat ag_nat Q (@level A agA a) *)
apply H.
Qed.

Import age_to.

Lemma unfash_imp:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {A} {NA: ageable A} (P Q: pred nat),
  (@unfash A _ (P --> Q) = (@unfash A _ P) --> @unfash A _ Q)%pred.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply pred_ext; repeat intro.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply H; auto. apply necR_level'; auto.
(* Goal: @app_pred nat ag_nat Q a' *)
specialize (H (age_to a' a)).
(* Goal: @app_pred nat ag_nat Q a' *)
spec H.
(* Goal: @necR A NA a (@age_to a' A NA a) *)
(* Goal: @app_pred nat ag_nat Q a' *)
apply age_to_necR.
(* Goal: @app_pred nat ag_nat Q a' *)
spec H.
(* Goal: @app_pred A NA (@unfash A NA P) (@age_to a' A NA a) *)
(* Goal: @app_pred nat ag_nat Q a' *)
do 3 red. 
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
rewrite level_age_to; auto.
(* Goal: le a' (@level A NA a) *)
apply necR_level in H0. apply H0.
(* Goal: @app_pred A NA Q a' *)
do 3 red in H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
rewrite level_age_to in H; auto.
(* Goal: le a' (@level A NA a) *)
apply necR_level in H0.
(* Goal: le a' (@level A NA a) *)
apply H0.
Qed.

(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
Lemma unfash_andp:  forall {A} {agA: ageable A} (P Q: pred nat),
  (@unfash A agA (andp P Q) = andp (@unfash A agA P) (@unfash A agA Q)).
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @eq (@pred A agA) (@unfash A agA (@andp nat ag_nat P Q)) (@andp A agA (@unfash A agA P) (@unfash A agA Q)) *)
apply pred_ext.
(* Goal: @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros ? ?.
(* Goal: @app_pred A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) a *)
(* Goal: @derives A agA (@andp A agA (@unfash A agA P) (@unfash A agA Q)) (@unfash A agA (@andp nat ag_nat P Q)) *)
destruct H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
split; auto.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) Q *)
intros ? [? ?].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
split; auto.
Qed.

Lemma andp_imp_e:
  forall (A : Type) (agA : ageable A) (P Q : pred A),
   P && (P --> Q) |-- Q.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) Q *)
intros ? [? ?].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply H0; auto.
Qed.

Lemma andp_imp_e':
  forall (A : Type) (agA : ageable A) (P Q : pred A),
   P && (P --> Q) |-- P && Q.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) (@andp A agA P Q) *)
apply andp_right.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply andp_left1; auto.
(* Goal: @derives A agA (@andp A agA P (@imp A agA P Q)) Q *)
intros ? [? ?].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply H0; auto.
Qed.

Lemma switch_rguard:
 forall (Espec : OracleKind)
  (R : ret_assert)
  (psi : genv)
  (F : assert)
  (Delta' : tycontext)
  (k : cont),
 rguard Espec psi Delta'
        (frame_ret_assert R F) k |--
(rguard Espec psi  Delta'
   (frame_ret_assert (switch_ret_assert R) F) 
   (Kswitch :: k)).
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives nat ag_nat (rguard Espec psi Delta' (frame_ret_assert R F) k) (rguard Espec psi Delta' (frame_ret_assert (switch_ret_assert R) F) (@cons cont' Kswitch k)) *)
unfold rguard.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl) (current_function (@cons cont' Kswitch k)) (exit_cont ek vl (@cons cont' Kswitch k))))) *)
apply allp_right; intro ek.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl) (current_function (@cons cont' Kswitch k)) (exit_cont ek vl (@cons cont' Kswitch k)))) *)
apply allp_right; intro vl.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (_guard Espec psi Delta' (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl) (current_function (@cons cont' Kswitch k)) (exit_cont ek vl (@cons cont' Kswitch k))) *)
apply allp_right; intro tx'.
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho)))) *)
apply allp_right; intro vx'.
 pose (ek' := match ek with 
                    | EK_normal => EK_normal
                    | EK_break => EK_normal
                    | EK_continue => EK_continue
                    | EK_return => EK_return
                    end).
 pose (vl' := match ek with 
                    | EK_normal => None
                    | EK_break => None
                    | EK_continue => None
                    | EK_return => vl
                    end).
(* Goal: @derives nat ag_nat (@allp nat ag_nat exitkind (fun ek : exitkind => @allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek vl) (current_function k) (exit_cont ek vl k)))) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 apply allp_left with ek'.
(* Goal: @derives nat ag_nat (@allp nat ag_nat (option val) (fun vl : option val => _guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek' vl) (current_function k) (exit_cont ek' vl k))) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 apply allp_left with vl'.
(* Goal: @derives nat ag_nat (_guard Espec psi Delta' (proj_ret_assert (frame_ret_assert R F) ek' vl') (current_function k) (exit_cont ek' vl' k)) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 apply allp_left with tx'.
(* Goal: @derives nat ag_nat (@allp nat ag_nat env (fun vx : env => let rho := construct_rho (filter_genv psi) vx tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert R F) ek' vl' rho)) (funassert Delta' rho)) (assert_safe Espec psi vx tx' (exit_cont ek' vl' k) rho)))) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 apply allp_left with vx'.
(* Goal: @derives nat ag_nat (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert R F) ek' vl' rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 simpl current_function.
 set (rho' := construct_rho (filter_genv psi) vx' tx') in *.
(* Goal: @derives nat ag_nat (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert R F) ek' vl' rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 forget (funassert Delta' rho') as FDR.
(* Goal: @derives nat ag_nat (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert R F) ek' vl' rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 rewrite !proj_frame_ret_assert.
(* Goal: @derives nat ag_nat (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (@seplog.sepcon assert (@seplog.LiftNatDed environ mpred (@alg_seplog.algNatDed rmap ag_rmap)) (@seplog.LiftSepLog environ mpred (@alg_seplog.algNatDed rmap ag_rmap) (@alg_seplog.algSepLog rmap ag_rmap Join_rmap Perm_rmap Sep_rmap Age_rmap)) (proj_ret_assert R ek' vl') F rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := rho' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (@seplog.sepcon assert (@seplog.LiftNatDed environ mpred (@alg_seplog.algNatDed rmap ag_rmap)) (@seplog.LiftSepLog environ mpred (@alg_seplog.algNatDed rmap ag_rmap) (@alg_seplog.algSepLog rmap ag_rmap Join_rmap Perm_rmap Sep_rmap Age_rmap)) (proj_ret_assert (switch_ret_assert R) ek vl) F rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
 simpl.
(* Goal: @derives nat ag_nat (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (proj_ret_assert R ek' vl' rho') (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho'))) (@fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (proj_ret_assert (switch_ret_assert R) ek vl rho') (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho'))) *)
 apply fash_derives.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 destruct R as [?R ?R ?R ?R]; destruct ek; subst ek' vl'; simpl; auto.
(* Goal: @derives rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (R rho') (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' k rho')) (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@prop rmap ag_rmap False) (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' (@cons cont' Kswitch k) rho')) *)
 apply imp_right. normalize.
Qed.

Lemma unfash_fash_imp:
  forall A (NA: ageable A) P Q,
  @unfash A _ (# (P --> Q)) |-- P --> Q.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
(* Goal: @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros ? ?.
(* Goal: @app_pred A NA (@imp A NA P Q) a *)
intros ? ? ?.
(* Goal: @app_pred A NA Q a' *)
do 3 red in H.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply (H a'); auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply necR_level; auto.
Qed.

Lemma assert_safe_step_nostore:
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {cs: compspecs} Espec psi vx vx2 tx tx2 k1 k2 Delta e rho,
  (forall jm jm', age1 jm = Some jm' ->
    app_pred (tc_expr Delta e rho) (m_phi jm) ->
     cl_step psi (State vx tx k1)
      (m_dry jm) (State vx2 tx2 k2) (m_dry jm)) ->
  assert_safe Espec psi vx2 tx2 k2 (construct_rho (filter_genv psi) vx2 tx2)
 && tc_expr Delta e rho
|-- assert_safe Espec psi vx tx k1 (construct_rho (filter_genv psi) vx tx).
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
intros w [Hw Hw'] ? J.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eexists; split; eauto; eexists; repeat split; eauto.
intros ora jm Hora ? ?. subst.
destruct (level (m_phi jm)) eqn:?.
constructor.
destruct (levelS_age1 _ _ Heqn) as [phi' H1].
destruct (can_age1_juicy_mem _ _ H1) as [jm' H9].
clear phi' H1.
econstructor 2 with (m' := jm').
econstructor.
rewrite <- (age_jm_dry H9).
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply (H _ _ H9); auto.
(* Goal: @app_pred A NA (@andp A NA (@allp A NA B P) Q) a *)
split.
apply age1_resource_decay; assumption.
split; [apply age_level; assumption|].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply age1_ghost_of, age_jm_phi; auto.
pose  proof (age_level _ _ H9).
rewrite <- level_juice_level_phi in Heqn.
rewrite Heqn in H1.
inv H1. clear Heqn.
eapply pred_hereditary in Hw;
  [ | instantiate (1:= (m_phi jm')); apply age_jm_phi; auto].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply assert_safe_jsafe; auto.
Qed.

Lemma semax_switch: 
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {CS: compspecs} Espec Delta (Q: assert) a sl R,
     is_int_type (typeof a) = true ->
     (forall rho, Q rho |-- tc_expr Delta a rho) ->
     (forall n,
     semax Espec Delta (fun rho => andp (prop (eval_expr a rho = Vint n)) (Q rho))
               (seq_of_labeled_statement (select_switch (Int.unsigned n) sl))
               (switch_ret_assert R)) ->
     semax Espec Delta Q (Sswitch a sl) R.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
rewrite semax_eq.
apply allp_right; intro psi.
apply allp_right; intro Delta'.
apply prop_imp_right; intros [TS HGG].
(* Goal: @derives rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (R rho') (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' k rho')) (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@prop rmap ag_rmap False) (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' (@cons cont' Kswitch k) rho')) *)
apply imp_right.
rewrite TT_and.
apply allp_right; intro k.
apply allp_right; intro F.
(* Goal: @derives rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (R rho') (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' k rho')) (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho')) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@prop rmap ag_rmap False) (F rho'))) (funassert Delta' rho')) (assert_safe Espec psi vx' tx' (@cons cont' Kswitch k) rho')) *)
apply imp_right.
rewrite <- andp_assoc;
 rewrite (andp_comm (believe _ _ _ _));
 rewrite andp_assoc;
 apply prop_andp_left; intro.
unfold guard, _guard.
apply allp_right; intro tx.
apply allp_right; intro vx.
rewrite andp_assoc.
apply prop_andp_subp'; intros [H4 H4'].
set (rho := construct_rho (filter_genv psi) vx tx) in *.
specialize (H0 rho).
apply frame_tc_expr with (F0 := F rho) in  H0.
rewrite sepcon_comm in H0.
apply subp_i1.
eapply derives_trans.
 apply andp_derives; [apply derives_refl | ].
 apply andp_derives; [ | apply derives_refl].
 apply andp_right; [ apply derives_refl | ].
 eapply derives_trans; [apply H0 | ].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 eapply tc_expr_sound; eauto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
 eapply typecheck_environ_sub; eauto.
rewrite andp_comm.
rewrite (andp_comm (_ * _)).
rewrite !andp_assoc.
apply derives_extract_prop; intro H0'.
destruct (typeof a) eqn:?; inv H.
destruct (eval_expr a rho) as [ | n | | | |] eqn:?;  try contradiction H0'.
specialize (H1 n).
rewrite semax_eq in H1.
match goal with |- ?A |-- _ => rewrite <- (TT_and A) end.
eapply derives_trans; [apply andp_derives; [ | apply derives_refl] | ].
eapply derives_trans; [ | apply @unfash_derives; apply H1].
rewrite fash_TT.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
auto.
clear H1.
rewrite unfash_allp. rewrite (allp_andp psi). apply allp_left with psi.
rewrite unfash_allp. rewrite (allp_andp Delta'). apply allp_left with Delta'.
rewrite unfash_prop_imp.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
rewrite prop_true_imp by auto.
rewrite unfash_imp.
rewrite unfash_andp.
rewrite (andp_comm (sepcon _ _)).
rewrite (andp_comm (funassert _ _)).
rewrite <- !andp_assoc.
eapply derives_trans.
apply andp_derives; [ | apply derives_refl].
apply andp_derives; [ | apply derives_refl].
apply andp_derives; [ | apply derives_refl].
rewrite andp_comm.
apply andp_imp_e.
rewrite unfash_allp. rewrite !(allp_andp (Kswitch :: k)). apply allp_left with (Kswitch :: k).
rewrite unfash_allp. rewrite !(allp_andp F). apply allp_left with F.
rewrite prop_true_andp 
  by (eapply closed_wrt_modvars_switch with (n:= Int.unsigned n); eauto).
eapply derives_trans.
apply andp_derives; [ | apply derives_refl].
apply andp_derives; [ | apply derives_refl].
apply andp_derives; [apply derives_refl | ].
eapply unfash_derives.
apply switch_rguard.
eapply derives_trans.
apply andp_derives; [ | apply derives_refl].
apply andp_derives; [ | apply derives_refl].
rewrite unfash_imp.
rewrite andp_comm.
apply andp_imp_e.
unfold guard, _guard.
rewrite unfash_allp. rewrite !(allp_andp tx). apply allp_left with tx.
rewrite unfash_allp. rewrite !(allp_andp vx). apply allp_left with vx.
fold rho.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
rewrite (prop_true_andp (_ = _)) by auto.
eapply derives_trans.
apply andp_derives; [apply derives_refl | ].
apply andp_right; apply derives_refl.
rewrite !andp_assoc.
rewrite (andp_comm (sepcon _ _)).
rewrite <- (andp_assoc (funassert _ _)).
forget (funassert Delta' rho && (F rho * Q rho))%pred as FQ.
(* Goal: @derives nat ag_nat (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function k) rho)) (proj_ret_assert (frame_ret_assert R F) ek' vl' rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek' vl' k) rho))) (let rho := construct_rho (filter_genv psi) vx' tx' in @fash rmap ag_rmap (@imp rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (guard_environ Delta' (current_function (@cons cont' Kswitch k)) rho)) (proj_ret_assert (frame_ret_assert (switch_ret_assert R) F) ek vl rho)) (funassert Delta' rho)) (assert_safe Espec psi vx' tx' (exit_cont ek vl (@cons cont' Kswitch k)) rho))) *)
simpl current_function.
rewrite prop_true_andp by (split; auto).
rewrite <- andp_assoc.
eapply derives_trans.
apply andp_derives; [ | apply H0].
apply andp_derives; [ | apply derives_refl].
apply unfash_fash_imp.
eapply derives_trans.
apply andp_derives; [ | apply derives_refl].
rewrite andp_comm. apply andp_imp_e.
eapply typecheck_environ_sub in H4; try eassumption.
clear - H4 HGG Heqv Heqt.
apply assert_safe_step_nostore.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
econstructor.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply eval_expr_relate; eauto.
fold rho.
rewrite Heqv, Heqt.
reflexivity.
Qed.

Lemma semax_switch_orig: 
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
  forall {CS: compspecs} Espec Delta (Q: assert) a sl R,
     is_int_type (typeof a) = true ->
     (forall rho, Q rho |-- tc_expr Delta a rho) ->
     (forall n,
     semax Espec Delta (fun rho => andp (prop (eval_expr a rho = Vint n)) (Q rho))
               (seq_of_labeled_statement (select_switch (Int.unsigned n) sl))
               (switch_ret_assert R)) ->
     semax Espec Delta Q (Sswitch a sl) R.
Proof.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
rewrite semax_unfold.
(* Goal: forall (A : Type) (NA : ageable A) (P Q : @pred A NA), @derives A NA (@unfash A NA (@fash A NA (@imp A NA P Q))) (@imp A NA P Q) *)
intros.
unfold guard.
intros tx vx.
set (rho := construct_rho (filter_genv psi) vx tx) in *.
specialize (H0 rho).
apply frame_tc_expr with (F0 := F rho) in  H0.
intros w' Hw' w'' Hw'' [[[H4 H4'] H5] H6].
rewrite sepcon_comm in H0; specialize (H0 _ H5).
assert (H0' := typecheck_expr_sound _ _ _ _ (typecheck_environ_sub _ _ TS _ H4) H0).
destruct (typeof a) eqn:?; inv H.
destruct (eval_expr a rho) as [ | n | | | |] eqn:?;  try contradiction H0'.
specialize (H1 n).
rewrite semax_unfold in H1.
specialize (H1 psi Delta' w TS HGG Prog_OK (Kswitch :: k) F).
specialize (H1 (closed_wrt_modvars_switch _ _ _ _ H2)); clear H2.
set (c := seq_of_labeled_statement (select_switch (Int.unsigned n) sl)) in *.
spec H1.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
{ eapply switch_rguard; eauto. }
specialize (H1 tx vx w' Hw' _ Hw'').
spec H1.
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars' (seq_of_labeled_statement sl) s)) *)
(* Goal: @isSome unit (@PTree.get unit i (modifiedvars_ls sl s)) *)
{ clear H1.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  split; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  split; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  do 3 red. split; auto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
  fold rho. rewrite prop_true_andp by auto. auto. }
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
intros ? J; eexists; split; eauto; repeat eexists; auto.
intros ora jm Hora H7 H8. subst; clear H7.
destruct (level (m_phi jm)) eqn:?.
constructor.
destruct (levelS_age1 _ _ Heqn0) as [phi' ?].
destruct (can_age1_juicy_mem _ _ H) as [jm' H9].
clear phi' H.
econstructor 2 with (m' := jm').
econstructor.
rewrite <- (age_jm_dry H9).
econstructor.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply eval_expr_relate; eauto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply tc_expr_sub; eauto.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
eapply typecheck_environ_sub; eauto.
fold rho. rewrite Heqv, Heqt.
reflexivity.
(* Goal: @app_pred A NA (@andp A NA (@allp A NA B P) Q) a *)
split.
apply age1_resource_decay; assumption.
split; [apply age_level; assumption|].
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply age1_ghost_of, age_jm_phi; auto.

pose  proof (age_level _ _ H9).
rewrite <- level_juice_level_phi in Heqn0.
rewrite Heqn0 in H.
inv H. clear Heqn0.
eapply assert_safe_jsafe, pred_hereditary, H1.
(* Goal: @app_pred A agA (@unfash A agA (f b)) a *)
(* Goal: @derives A agA (@allp A agA B (fun x : B => @unfash A agA (f x))) (@unfash A agA (@allp nat ag_nat B f)) *)
apply age_jm_phi; auto.
Qed.
