
Require Import VST.floyd.base.

Local Open Scope logic.

Lemma denote_tc_assert_andp:
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {CS: compspecs} (a b : tc_assert),
  denote_tc_assert (tc_andp a b) = andp (denote_tc_assert a) (denote_tc_assert b).
Proof.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
  intros.
(* Goal: @eq (forall _ : environ, mpred) (@denote_tc_assert CS (tc_orp a b)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert CS a) (@denote_tc_assert CS b)) *)
  extensionality rho.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
  simpl.
(* Goal: @eq mpred (@denote_tc_assert CS (tc_andp a b) rho) (@andp mpred Nveric (@denote_tc_assert CS a rho) (@denote_tc_assert CS b rho)) *)
  apply expr2.denote_tc_assert_andp.
Qed.

Lemma denote_tc_assert_orp:
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {CS: compspecs} (a b : tc_assert),
  denote_tc_assert (tc_orp a b) = orp (denote_tc_assert a) (denote_tc_assert b).
Proof.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
  intros.
(* Goal: @eq (forall _ : environ, mpred) (@denote_tc_assert CS (tc_orp a b)) (@orp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert CS a) (@denote_tc_assert CS b)) *)
  extensionality rho.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
  simpl.
(* Goal: @eq mpred (@denote_tc_assert CS (tc_orp a b) rho) (@orp mpred Nveric (@denote_tc_assert CS a rho) (@denote_tc_assert CS b rho)) *)
  apply binop_lemmas2.denote_tc_assert_orp.
Qed.

Lemma denote_tc_assert_bool:
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {CS: compspecs} b c, denote_tc_assert (tc_bool b c) =
               prop (b=true).
Proof.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
  intros.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
  extensionality rho; simpl.
(* Goal: @eq mpred (@denote_tc_assert CS (tc_bool b c) rho) (@prop mpred Nveric (@eq bool b true)) *)
  unfold tc_bool.
(* Goal: @eq mpred (@denote_tc_assert CS (if b then tc_TT else tc_FF c) rho) (@prop mpred Nveric (@eq bool b true)) *)
  destruct b.
(* Goal: @eq mpred (@denote_tc_assert CS tc_TT rho) (@prop mpred Nveric (@eq bool true true)) *)
(* Goal: @eq mpred (@denote_tc_assert CS (tc_FF c) rho) (@prop mpred Nveric (@eq bool false true)) *)
  apply pred_ext; normalize; apply derives_refl.
(* Goal: @eq mpred (@denote_tc_assert CS (tc_FF c) rho) (@prop mpred Nveric (@eq bool false true)) *)
  apply pred_ext.  apply @FF_left.
(* Goal: @derives mpred Nveric (@prop mpred Nveric (@eq bool false true)) (@denote_tc_assert CS (tc_FF c) rho) *)
  normalize. inv H.
Qed.

Lemma neutral_isCastResultType_64:
 Archi.ptr64 = true ->
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {cs: compspecs}  P t t' v rho,
   is_neutral_cast t' t = true ->
   P |-- denote_tc_assert (isCastResultType t' t v) rho.
Proof.
(* Goal: forall (_ : @eq bool Archi.ptr64 false) (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
intro Hp.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
intros.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
unfold isCastResultType, classify_cast; rewrite Hp.
  destruct t'  as [ | [ | | | ] [ | ] | | [ | ] | | | | |], t  as [ | [ | | | ] [ | ] | | [ | ] | | | | |];
try solve [
     inv H; simpl; try apply @TT_right;
           simpl; (destruct (eqb_tac _ _)); apply @TT_right].
*
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tlong s a) (Tlong s0 a0) then tc_TT else if orb (andb (is_pointer_type (Tlong s0 a0)) (is_pointer_type (Tlong s a))) (andb (is_long_type (Tlong s0 a0)) (is_long_type (Tlong s a))) then tc_TT else if andb (eqb_type (Tlong s0 a0) int_or_ptr_type) (is_long_type (Tlong s a)) then tc_TT else if andb (eqb_type (Tlong s0 a0) int_or_ptr_type) (is_pointer_type (Tlong s a)) then tc_TT else if andb (eqb_type (Tlong s a) int_or_ptr_type) (is_pointer_type (Tlong s0 a0)) then tc_isptr v else if andb (eqb_type (Tlong s a) int_or_ptr_type) (is_long_type (Tlong s0 a0)) then tc_islong v else @tc_iszero cs v) rho) *)
try destruct (eqb_type _ _); apply @TT_right.
*
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
unfold is_neutral_cast in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_long_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
destruct (eqb_type (Tpointer t a0) int_or_ptr_type) eqn:H0.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
{
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb true (is_long_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite (eqb_type_true _ _ H0).
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
destruct (eqb_type (Tpointer t' a) int_or_ptr_type) eqn:H1.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
{
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
apply @TT_right.
}
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
{
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (is_pointer_type int_or_ptr_type) (is_pointer_type (Tpointer t' a))) (andb (is_long_type int_or_ptr_type) (is_long_type (Tpointer t' a))) then tc_TT else if andb true (is_long_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type int_or_ptr_type) then tc_isptr v else if andb false (is_long_type int_or_ptr_type) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite (eqb_type_true _ _ H0) in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb true (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite H1 in H. inv H.
}
}
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
{
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
destruct (eqb_type (Tpointer t' a) int_or_ptr_type) eqn:H1.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb true (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite (eqb_type_true _ _ H1) in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb true (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite expr_lemmas4.eqb_type_sym in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb true (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb true (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite H0 in H. inv H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite orb_true_iff in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
unfold is_pointer_type.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) (negb (eqb_type (Tpointer t' a) int_or_ptr_type))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (negb (eqb_type (Tpointer t' a) int_or_ptr_type)) then tc_TT else if andb false (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) then tc_isptr v else if andb false (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
rewrite H0,H1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
simpl.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
simple_if_tac; apply @TT_right.
}
Qed.

Lemma neutral_isCastResultType_32:
 Archi.ptr64 = false ->
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {cs: compspecs}  P t t' v rho,
   is_neutral_cast t' t = true ->
   P |-- denote_tc_assert (isCastResultType t' t v) rho.
Proof.
(* Goal: forall (_ : @eq bool Archi.ptr64 false) (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
intro Hp.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
intros.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
unfold isCastResultType, classify_cast; rewrite Hp.
  unfold isCastResultType;
  destruct t'  as [ | [ | | | ] [ | ] | | [ | ] | | | | |], t  as [ | [ | | | ] [ | ] | | [ | ] | | | | |];
try solve [
     inv H; simpl; try apply @TT_right;
           simpl; (destruct (eqb_tac _ _)); apply @TT_right].
*
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
simpl; simple_if_tac; apply @TT_right.
*
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
simpl; simple_if_tac; apply @TT_right.
*
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
unfold is_neutral_cast in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite orb_true_iff in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
destruct H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite (eqb_type_true _ _ H).
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite eqb_type_refl. apply @TT_right.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite andb_true_iff in H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
destruct H.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_int_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t a0) int_or_ptr_type) (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite negb_true_iff in H, H0. rewrite H,H0.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
destruct (eqb_type (Tpointer t' a) (Tpointer t a0)); try apply @TT_right.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
unfold is_pointer_type.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) (negb (eqb_type (Tpointer t' a) int_or_ptr_type))) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb (eqb_type (Tpointer t' a) int_or_ptr_type)) then tc_TT else if andb false (negb (eqb_type (Tpointer t a0) int_or_ptr_type)) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
rewrite H,H0.
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if orb (andb (negb false) (negb false)) (andb (is_int_type (Tpointer t a0)) (is_int_type (Tpointer t' a))) then tc_TT else if andb false (is_int_type (Tpointer t' a)) then tc_TT else if andb false (negb false) then tc_TT else if andb false (negb false) then tc_isptr v else if andb false (is_int_type (Tpointer t a0)) then tc_isint v else @tc_iszero cs v) rho) *)
apply @TT_right.
Qed.

Lemma neutral_isCastResultType:
(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
  forall {cs: compspecs}  P t t' v rho,
   is_neutral_cast t' t = true ->
   P |-- denote_tc_assert (isCastResultType t' t v) rho.
Proof.
(* Goal: forall (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
destruct Archi.ptr64 eqn:Hp.
(* Goal: forall (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
(* Goal: forall (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
exact (@neutral_isCastResultType_64 Hp).
(* Goal: forall (cs : compspecs) (P : mpred) (t t' : type) (v : expr) (rho : environ) (_ : @eq bool (is_neutral_cast t' t) true), @derives mpred Nveric P (@denote_tc_assert cs (@isCastResultType cs t' t v) rho) *)
exact (@neutral_isCastResultType_32 Hp).
Qed.

Lemma tc_andp_TT2:  forall e, tc_andp e tc_TT = e.
Proof. intros; unfold tc_andp.  destruct e; reflexivity. Qed.

Lemma tc_andp_TT1:  forall e, tc_andp tc_TT e = e.
Proof. intros; unfold tc_andp; reflexivity. Qed.
Hint Rewrite tc_andp_TT1 tc_andp_TT2 : norm.

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Definition typecheck_LR_strong {cs: compspecs} Delta e lr :=
  match lr with
  | LLLL => typecheck_lvalue Delta e
  | RRRR => typecheck_expr Delta e
  end.

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Definition typecheck_LR {cs: compspecs} Delta e lr :=
  match e with
  | Ederef e0 t =>
     match lr with
     | LLLL => tc_andp
                 (typecheck_expr Delta e0)
                 (tc_bool (is_pointer_type (typeof e0))(op_result_type e))
     | RRRR => match access_mode t with
               | By_reference =>
                  tc_andp
                     (typecheck_expr Delta e0)
                     (tc_bool (is_pointer_type (typeof e0))(op_result_type e))
               | _ => tc_FF (deref_byvalue t)
               end
    end
  | _ => typecheck_LR_strong Delta e lr
  end.

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Definition tc_LR_strong {cs: compspecs} Delta e lr := denote_tc_assert (typecheck_LR_strong Delta e lr).

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Definition tc_LR {cs: compspecs} Delta e lr := denote_tc_assert (typecheck_LR Delta e lr).

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Definition eval_LR {cs: compspecs} e lr :=
  match lr with
  | LLLL => eval_lvalue e
  | RRRR => eval_expr e
  end.

(* Goal: @derives mpred Nveric P (@denote_tc_assert cs (if eqb_type (Tpointer t' a) (Tpointer t a0) then tc_TT else if orb (andb (is_pointer_type (Tpointer t a0)) (is_pointer_type (Tpointer t' a))) (andb (is_long_type (Tpointer t a0)) (is_long_type (Tpointer t' a))) then tc_TT else if andb false (is_long_type (Tpointer t' a)) then tc_TT else if andb false (is_pointer_type (Tpointer t' a)) then tc_TT else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_pointer_type (Tpointer t a0)) then tc_isptr v else if andb (eqb_type (Tpointer t' a) int_or_ptr_type) (is_long_type (Tpointer t a0)) then tc_islong v else @tc_iszero cs v) rho) *)
Lemma tc_LR_tc_LR_strong: forall {cs: compspecs} Delta e lr rho,
  tc_LR Delta e lr rho && !! isptr (eval_LR e lr rho) |-- tc_LR_strong Delta e lr rho.
Proof.
(* Goal: forall (cs : compspecs) (Delta : tycontext) (e : expr) (lr : LLRR) (rho : environ), @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
  intros.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@tc_LR cs Delta e lr rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@tc_LR_strong cs Delta e lr rho) *)
  unfold tc_LR, tc_LR_strong, typecheck_LR, typecheck_LR_strong.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@denote_tc_assert cs match e with | Econst_int i t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Econst_float f t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Econst_single f t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Econst_long i t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Evar i t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Etempvar i t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Ederef e0 t => match lr with | LLLL => tc_andp (@typecheck_expr cs Delta e0) (tc_bool (is_pointer_type (typeof e0)) (op_result_type e)) | RRRR => match access_mode t with | By_value m => tc_FF (deref_byvalue t) | By_reference => tc_andp (@typecheck_expr cs Delta e0) (tc_bool (is_pointer_type (typeof e0)) (op_result_type e)) | By_copy => tc_FF (deref_byvalue t) | By_nothing => tc_FF (deref_byvalue t) end end | Eaddrof e0 t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Eunop u e0 t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Ebinop b e0 e1 t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Ecast e0 t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Efield e0 i t => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Esizeof t t0 => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end | Ealignof t t0 => match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end end rho) (@prop mpred Nveric (isptr (@eval_LR cs e lr rho)))) (@denote_tc_assert cs match lr with | LLLL => @typecheck_lvalue cs Delta e | RRRR => @typecheck_expr cs Delta e end rho) *)
  destruct e; try solve [apply andp_left1; auto].
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@denote_tc_assert cs match lr with | LLLL => tc_andp (@typecheck_expr cs Delta e) (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) | RRRR => match access_mode t with | By_value m => tc_FF (deref_byvalue t) | By_reference => tc_andp (@typecheck_expr cs Delta e) (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))) | By_copy => tc_FF (deref_byvalue t) | By_nothing => tc_FF (deref_byvalue t) end end rho) (@prop mpred Nveric (isptr (@eval_LR cs (Ederef e t) lr rho)))) (@denote_tc_assert cs match lr with | LLLL => @typecheck_lvalue cs Delta (Ederef e t) | RRRR => @typecheck_expr cs Delta (Ederef e t) end rho) *)
  unfold tc_lvalue, tc_expr.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
  destruct lr; simpl.
  + rewrite !denote_tc_assert_andp.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
    simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@liftx (Tarrow val (LiftEnviron mpred)) denote_tc_isptr (@eval_expr cs e) rho)) *)
    unfold denote_tc_isptr.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@liftx (Tarrow val (LiftEnviron mpred)) (fun v : val => @prop mpred Nveric (isptr v)) (@eval_expr cs e) rho)) *)
    unfold_lift.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) *)
    auto.
  + destruct (access_mode t); try solve [apply andp_left1; auto].
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@denote_tc_assert cs (tc_andp (@typecheck_expr cs Delta e) (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@denote_tc_assert cs (tc_andp (tc_andp (@typecheck_expr cs Delta e) (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) (tc_isptr e)) rho) *)
    rewrite !denote_tc_assert_andp.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t)))) rho) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@denote_tc_assert cs (@typecheck_expr cs Delta e)) (@denote_tc_assert cs (tc_bool (is_pointer_type (typeof e)) (op_result_type (Ederef e t))))) (@denote_tc_assert cs (tc_isptr e)) rho) *)
    simpl.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@liftx (Tarrow val (LiftEnviron mpred)) denote_tc_isptr (@eval_expr cs e) rho)) *)
    unfold denote_tc_isptr.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@liftx (Tarrow val (LiftEnviron mpred)) (fun v : val => @prop mpred Nveric (isptr v)) (@eval_expr cs e) rho)) *)
    unfold_lift.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) (@andp mpred Nveric (@andp mpred Nveric (@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)) (@prop mpred Nveric (isptr (@eval_expr cs e rho)))) *)
    auto.
Qed.

