Require Export VST.veric.base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.Clight_seplog.
Require Export VST.veric.assert_lemmas.

Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.extend_tc.

Local Open Scope pred.

Lemma corable_funassert:
  forall G rho, corable (funassert G rho).
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros. eapply corable_funspecs_assert.
Qed.

Hint Resolve corable_funassert.

Definition allp_fun_id (Delta : tycontext) (rho : environ): pred rmap :=
(ALL id : ident ,
 (ALL fs : funspec ,
  !! ((glob_specs Delta) ! id = Some fs) -->
  (EX b : block, !! (Map.get (ge_of rho) id = Some b) && func_at fs (b, 0)))).

Lemma corable_allp_fun_id: forall Delta rho,
  corable (allp_fun_id Delta rho).
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (allp_fun_id Delta rho) *)
  apply corable_allp; intros id.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@allp rmap ag_rmap funspec (fun fs : funspec => @imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0)))))) *)
  apply corable_allp; intros fs.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))))) *)
  apply corable_imp; [apply corable_prop |].
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0)))) *)
  apply corable_exp; intros b.
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))) *)
  apply corable_andp; [apply corable_prop |].
(* Goal: @corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (func_at fs (@pair block Z b Z0)) *)
  apply corable_func_at.
Qed.
  
Lemma allp_fun_id_sub: forall Delta Delta' rho,
  tycontext_sub Delta Delta' ->
  allp_fun_id Delta' rho |-- allp_fun_id Delta rho.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros.
(* Goal: @derives rmap ag_rmap (allp_fun_id Delta' rho) (allp_fun_id Delta rho) *)
  unfold allp_fun_id.
(* Goal: @derives rmap ag_rmap (@allp rmap ag_rmap ident (fun id : ident => @allp rmap ag_rmap funspec (fun fs : funspec => @imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))))))) (@allp rmap ag_rmap ident (fun id : ident => @allp rmap ag_rmap funspec (fun fs : funspec => @imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))))))) *)
  apply allp_derives; intros id.
(* Goal: @derives rmap ag_rmap (@allp rmap ag_rmap funspec (fun fs : funspec => @imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0)))))) (@allp rmap ag_rmap funspec (fun fs : funspec => @imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0)))))) *)
  apply allp_derives; intros fs.
(* Goal: @derives rmap ag_rmap (@imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))))) (@imp rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@exp rmap ag_rmap block (fun b : block => @andp rmap ag_rmap (@prop rmap ag_rmap (@eq (option block) (@Map.get block (ge_of rho) id) (@Some block b))) (func_at fs (@pair block Z b Z0))))) *)
  apply imp_derives; auto.
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta)) (@Some funspec fs))) (@prop rmap ag_rmap (@eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs))) *)
  intros ? ?; simpl in *.
(* Goal: @eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs) *)
  destruct H as [_ [_ [_ [_ [? _]]]]].
(* Goal: (let (a, _) := @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 rho in a) w *)
  specialize (H id).
(* Goal: @eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs) *)
  hnf in H.
(* Goal: and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho)))) *)
  rewrite H0 in H.
(* Goal: @eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs) *)
  destruct ((glob_specs Delta') ! id); [| tauto].
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  auto.
Qed.

Lemma funassert_allp_fun_id_sub: forall Delta Delta' rho,
  tycontext_sub Delta Delta' ->
  funassert Delta' rho |-- allp_fun_id Delta rho.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros.
(* Goal: @derives rmap ag_rmap (funassert Delta' rho) (allp_fun_id Delta rho) *)
  apply andp_left1.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  apply allp_fun_id_sub; auto.
Qed.
(*
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
Lemma corable_jam: forall {B} {S': B -> Prop} (S: forall l, {S' l}+{~ S' l}) (P Q: B -> pred rmap),
    (forall loc, corable (P loc)) ->
    (forall loc, corable (Q loc)) ->
    forall b, corable (jam S P Q b).
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
intros.
intro.
unfold jam.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta (@cons type a e) (@cons expr e0 t)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta' (@cons type a e) (@cons expr e0 t)) rho) w *)
simpl.
if_tac.
apply H.
apply H0.
Qed.
*)
Lemma prop_derives {A}{H: ageable A}:
 forall (P Q: Prop), (P -> Q) -> prop P |-- prop Q.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
intros. intros w ?; apply H0; auto.
Qed.

Section STABILITY.
Variable CS: compspecs.
Variables Delta Delta': tycontext.
Hypothesis extends: tycontext_sub Delta Delta'.

Lemma tc_bool_e_sub: forall b b' err rho phi,
  (b = true -> b' = true) ->
  denote_tc_assert (tc_bool b err) rho phi ->
  denote_tc_assert (tc_bool b' err) rho phi.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b' err) rho) phi *)
  destruct b.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + specialize (H eq_refl); subst.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool true err) rho) phi *)
    simpl; exact I.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + inversion H0.
Qed.

Lemma tc_bool_e_i:
  forall b c rho phi,
   b = true ->
  app_pred (denote_tc_assert (tc_bool b c) rho) phi.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
intros.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b c) rho) phi *)
subst. apply I.
Qed.

Lemma tc_expr_lvalue_sub: forall rho,
  typecheck_environ Delta rho ->
  forall e,
    tc_expr Delta e rho |-- tc_expr Delta' e rho /\
    tc_lvalue Delta e rho |-- tc_lvalue Delta' e rho.
Proof.
(* Goal: forall (id : positive) (t : type) (v : forall _ : environ, val) (rho : environ), @derives rmap ag_rmap (tc_temp_id_load id t Delta v rho) (tc_temp_id_load id t Delta' v rho) *)
  rename extends into H.
(* Goal: forall (rho : environ) (_ : typecheck_environ Delta rho) (e : expr), and (@derives rmap ag_rmap (@tc_expr CS Delta e rho) (@tc_expr CS Delta' e rho)) (@derives rmap ag_rmap (@tc_lvalue CS Delta e rho) (@tc_lvalue CS Delta' e rho)) *)
  intros rho HHH.
  induction e; unfold tc_expr, tc_lvalue; split; intro w; unfold prop;
  simpl; auto;
  try solve [destruct t as [  | [| | |] |  | [|] | | | | |]; auto].
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
* destruct (access_mode t) eqn:?; auto.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta i) end rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta' i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  destruct (get_var_type Delta i) eqn:?; [ | contradiction].
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool (eqb_type t t0) (mismatch_context_type t t0)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta' i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  destruct H as [_ [? [_ [? _]]]].
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool (eqb_type t t0) (mismatch_context_type t t0)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta' i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  assert (H8: get_var_type Delta' i = Some t0); [ | rewrite H8; unfold tc_bool; simple_if_tac; auto].
  unfold get_var_type in *. rewrite <- H.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  destruct ((var_types Delta)!i); auto.
(* Goal: @eq (option type) match @PTree.get type i (glob_types Delta') with | Some g => @Some type g | None => @None type end (@Some type t0) *)
  destruct ((glob_types Delta) ! i) eqn:?; inv Heqo.
(* Goal: @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  specialize (H0 i). hnf in H0. rewrite Heqo0 in H0. rewrite H0.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  auto.
* destruct (get_var_type Delta i) eqn:?; [ | contradiction].
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool (eqb_type t t0) (mismatch_context_type t t0)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta' i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  destruct H as [_ [? [_ [? _]]]].
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool (eqb_type t t0) (mismatch_context_type t t0)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match get_var_type Delta' i with | Some ty' => tc_bool (eqb_type t ty') (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  assert (H8: get_var_type Delta' i = Some t0); [ | rewrite H8; unfold tc_bool; simple_if_tac; auto].
  unfold get_var_type in *. rewrite <- H.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  destruct ((var_types Delta)!i); auto.
(* Goal: @eq (option type) match @PTree.get type i (glob_types Delta') with | Some g => @Some type g | None => @None type end (@Some type t0) *)
  destruct ((glob_types Delta) ! i) eqn:?; inv Heqo.
(* Goal: @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  specialize (H0 i). hnf in H0. rewrite Heqo0 in H0. rewrite H0.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  auto.
* destruct ((temp_types Delta)!i) as [? |] eqn:H1; [ | contradiction].
(* Goal: @eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs) *)
  destruct H as [H _]. specialize (H i); hnf in H. rewrite H1 in H.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (if orb (is_neutral_cast t0 t) (same_base_type t0 t) then tc_initialized i t0 else tc_FF (mismatch_context_type t t0)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS match @PTree.get type i (temp_types Delta') with | Some ty' => if orb (is_neutral_cast ty' t) (same_base_type ty' t) then tc_initialized i ty' else tc_FF (mismatch_context_type t ty') | None => tc_FF (var_not_in_tycontext Delta' i) end rho) w *)
  destruct ((temp_types Delta')!i) as [? |] eqn:H2; [ | contradiction].
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  simpl @fst; simpl @snd. subst t1; auto.
* destruct (access_mode t) eqn:?H; intro HH; try inversion HH.
  rewrite !denote_tc_assert_andp in HH |- *.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w *)
  destruct HH as [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w *)
  destruct IHe as [? _].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w *)
  repeat split.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + unfold tc_expr in H1.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) w *)
    apply (H4 w).
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta (@cons type a e) (@cons expr e0 t)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta' (@cons type a e) (@cons expr e0 t)) rho) w *)
    simpl.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
    tauto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + unfold tc_bool in H2 |- *; simple_if_tac; tauto.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + pose proof (H4 w H1).
    simpl in H3 |- *.
(* Goal: isptr (@expr.eval_expr CS e rho) *)
    unfold_lift in H3; unfold_lift.
(* Goal: isptr (@expr.eval_expr CS e rho) *)
    exact H3.
* destruct IHe.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp (tc_andp (@typecheck_expr CS Delta e0) (@isCastResultType CS (typeof e0) a e0)) (@typecheck_exprlist CS Delta e t)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp (tc_andp (@typecheck_expr CS Delta' e0) (@isCastResultType CS (typeof e0) a e0)) (@typecheck_exprlist CS Delta' e t)) rho) w *)
  repeat rewrite denote_tc_assert_andp.
(* Goal: forall _ : @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w, @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w *)
  intros [[? ?] ?].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e) rho) (@denote_tc_assert CS (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) rho)) (@denote_tc_assert CS (tc_isptr e) rho)) w *)
  repeat split.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + unfold tc_expr in H0.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
    apply (H0 w); unfold prop; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + unfold tc_bool in *; simple_if_tac; tauto.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
  + pose proof (H0 w H2).
    simpl in H4 |- *.
(* Goal: isptr (@expr.eval_expr CS e rho) *)
    unfold_lift in H4; unfold_lift.
(* Goal: isptr (@expr.eval_expr CS e rho) *)
    exact H4.
* repeat rewrite denote_tc_assert_andp; intros [? ?]; repeat split.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe. apply (H3 w); auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + unfold tc_bool in *; simple_if_tac; tauto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
* repeat rewrite denote_tc_assert_andp; intros [? ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  destruct IHe. apply (H2 w); auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
* repeat rewrite denote_tc_assert_andp; intros [[? ?] ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe1 as [H8 _]; apply (H8 w); auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe2 as [H8 _]; apply (H8 w); auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
* repeat rewrite denote_tc_assert_andp; intros [? ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe as [H8 _]; apply (H8 w); auto.
* destruct (access_mode t) eqn:?; try solve [intro HH; inv HH].
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  repeat rewrite denote_tc_assert_andp. intros [? ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe. apply (H3 w); auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
* repeat rewrite denote_tc_assert_andp; intros [? ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + destruct IHe as [_ H8]; apply (H8 w); auto.
Qed.

Lemma tc_expr_sub:
    forall e rho, typecheck_environ Delta rho -> tc_expr Delta e rho |-- tc_expr Delta' e rho.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
Proof. intros. apply tc_expr_lvalue_sub; auto. Qed.

Lemma tc_lvalue_sub:
    forall e rho, typecheck_environ Delta rho -> tc_lvalue Delta e rho |-- tc_lvalue Delta' e rho.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
Proof. intros. apply tc_expr_lvalue_sub; auto. Qed.

Lemma tc_temp_id_sub:
    forall id t e rho,
   tc_temp_id id t Delta e rho |-- tc_temp_id id t Delta' e rho.
Proof.
(* Goal: forall (id : positive) (t : type) (v : forall _ : environ, val) (rho : environ), @derives rmap ag_rmap (tc_temp_id_load id t Delta v rho) (tc_temp_id_load id t Delta' v rho) *)
rename extends into H.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
unfold tc_temp_id; intros.
(* Goal: @derives rmap ag_rmap (@denote_tc_assert CS (@typecheck_temp_id CS id t Delta e) rho) (@denote_tc_assert CS (@typecheck_temp_id CS id t Delta' e) rho) *)
unfold typecheck_temp_id.
intros w ?.  hnf in H0|-*.
(* Goal: (let (a, _) := @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 rho in a) w *)
destruct H as [? _]. specialize (H id).
(* Goal: (let (a, _) := @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 rho in a) w *)
destruct ((temp_types Delta)! id); try contradiction.
(* Goal: and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho)))) *)
destruct ((temp_types Delta')! id); try contradiction.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_bool b c) rho) phi *)
destruct H; subst.
rewrite !denote_tc_assert_andp in H0 |- *.
(* Goal: (let (a, _) := @andp rmap ag_rmap (@denote_tc_assert CS (tc_bool (is_neutral_cast (implicit_deref t) t0) (invalid_cast t t0)) rho) (@denote_tc_assert CS (@isCastResultType CS (implicit_deref t) t0 e) rho) in a) w *)
split.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
+ eapply tc_bool_e_sub; [| exact (proj1 H0)].
(* Goal: forall _ : @eq bool (is_neutral_cast (implicit_deref t) t0) true, @eq bool (is_neutral_cast (implicit_deref t) t0) true *)
  exact (fun x => x).
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_expr CS Delta' e0) rho) w *)
+ destruct H0 as [? _].
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@isCastResultType CS (implicit_deref t) t0 e) rho) w *)
  apply tc_bool_e in H.
(* Goal: @app_pred rmap ag_rmap (@denote_tc_assert CS (@isCastResultType CS (implicit_deref t) t0 e) rho) w *)
  eapply neutral_isCastResultType.
(* Goal: @eq bool (is_neutral_cast (implicit_deref t) t0) true *)
  exact H.
Qed.

Lemma tc_temp_id_load_sub:
   forall id t v rho,
   tc_temp_id_load id t Delta v rho |--    tc_temp_id_load id t Delta' v rho.
Proof.
(* Goal: forall (id : positive) (t : type) (v : forall _ : environ, val) (rho : environ), @derives rmap ag_rmap (tc_temp_id_load id t Delta v rho) (tc_temp_id_load id t Delta' v rho) *)
rename extends into H.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
unfold tc_temp_id_load; simpl; intros.
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (@ex type (fun tto : type => and (@eq (option type) (@PTree.get type id (temp_types Delta)) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho))))))) (@prop rmap ag_rmap (@ex type (fun tto : type => and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho))))))) *)
intros w [tto [? ?]]; exists tto.
(* Goal: and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho)))) *)
destruct H as [H _].
(* Goal: @eq (option funspec) (@PTree.get funspec id (glob_specs Delta')) (@Some funspec fs) *)
specialize (H id); hnf in H.
(* Goal: and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho)))) *)
rewrite H0 in H.
(* Goal: and (@eq (option type) (@PTree.get type id (temp_types Delta')) (@Some type tto)) (tc_val tto (force_val (Clight_Cop2.sem_cast t tto (v rho)))) *)
destruct ((temp_types Delta')! id); try contradiction.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
destruct H; subst; auto.
Qed.

Lemma tc_exprlist_sub:
  forall e t rho, typecheck_environ Delta rho -> tc_exprlist Delta e t rho |-- tc_exprlist Delta' e t rho.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
  intros.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  revert t; induction e; destruct t;  simpl; auto.
(* Goal: @derives rmap ag_rmap (@tc_exprlist CS Delta (@cons type a e) (@cons expr e0 t) rho) (@tc_exprlist CS Delta' (@cons type a e) (@cons expr e0 t) rho) *)
  specialize (IHe t).
(* Goal: @derives rmap ag_rmap (@tc_exprlist CS Delta (@cons type a e) (@cons expr e0 t) rho) (@tc_exprlist CS Delta' (@cons type a e) (@cons expr e0 t) rho) *)
  unfold tc_exprlist.
(* Goal: @derives rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta (@cons type a e) (@cons expr e0 t)) rho) (@denote_tc_assert CS (@typecheck_exprlist CS Delta' (@cons type a e) (@cons expr e0 t)) rho) *)
  intro w; unfold prop.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta (@cons type a e) (@cons expr e0 t)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS (@typecheck_exprlist CS Delta' (@cons type a e) (@cons expr e0 t)) rho) w *)
  simpl.
(* Goal: forall _ : @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp (tc_andp (@typecheck_expr CS Delta e0) (@isCastResultType CS (typeof e0) a e0)) (@typecheck_exprlist CS Delta e t)) rho) w, @app_pred rmap ag_rmap (@denote_tc_assert CS (tc_andp (tc_andp (@typecheck_expr CS Delta' e0) (@isCastResultType CS (typeof e0) a e0)) (@typecheck_exprlist CS Delta' e t)) rho) w *)
  repeat rewrite denote_tc_assert_andp.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  intros [[? ?] ?]; repeat split; auto.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
  + apply (tc_expr_sub _ _ H w H0); auto.
Qed.

Definition typeof_temp (Delta: tycontext) (id: ident) : option type :=
 match (temp_types Delta) ! id with
 | Some t => Some t
 | None => None
 end.

Lemma typeof_temp_sub:
   forall i t,
    typeof_temp Delta i = Some t ->
    typeof_temp Delta' i = Some t.
Proof.
(* Goal: forall (i : ident) (t : type) (_ : @eq (option type) (typeof_temp Delta i) (@Some type t)), @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
intros.
(* Goal: @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
destruct extends as [? _].
(* Goal: @eq (option type) (typeof_temp Delta' i) (@Some type t) *)
specialize (H0 i).
unfold typeof_temp in *.
(* Goal: @eq (option type) match @PTree.get type i (temp_types Delta') with | Some t => @Some type t | None => @None type end (@Some type t) *)
destruct ((temp_types Delta) ! i); inv H.
(* Goal: @eq (option type) match @PTree.get type i (temp_types Delta') with | Some t => @Some type t | None => @None type end (@Some type t) *)
destruct ((temp_types Delta') ! i); try contradiction.
(* Goal: @eq (option type) (@Some type t0) (@Some type t0) *)
destruct H0; subst; auto.
Qed.

End STABILITY.
