Zhi Zhang
Department of Computer and Information Sciences
Kansas State University
zhangzhi@ksu.edu

Require Export rt_gen.
Require Export rt_gen_util.
Require Export rt_opt_util.
Require Export well_typed.

Import STACK.

Lemma fetchG_split: forall s1 s2 x v,
  fetchG x (s1 ++ s2) = Some v ->
    fetchG x s1 = Some v \/ fetchG x s2 = Some v.
Proof.
  induction s1; smack.
  destruct (fetch x a); smack.
Qed.

Ltac apply_fetchG_split :=
  match goal with
  | [H: fetchG ?x (?s1 ++ ?s2) = Some _ |- _] =>
      specialize (fetchG_split _ _ _ _ H);
      let HZ1 := fresh "HZ" in
      let HZ2 := fresh "HZ" in intros HZ1; destruct HZ1 as [HZ1 | HZ2]
  end.


Lemma range_constrainted_type_true: forall st x u v,
  extract_subtype_range_rt st x (RangeRT u v) ->
    is_range_constrainted_type x = true.
Proof.
  intros;
  inversion H; subst;
  destruct x; smack.
Qed.

Lemma well_typed_exp_preserve: forall e st cks,
  well_typed_exp_x st (update_exterior_checks_exp e cks) ->
    well_typed_exp_x st e.
Proof.
  apply (expression_x_ind
    (fun e: expRT =>
       forall (st : symTabRT) (cks : exterior_checks),
       well_typed_exp_x st (update_exterior_checks_exp e cks) ->
       well_typed_exp_x st e)
    (fun n: nameRT =>
       forall (st : symTabRT) (cks : exterior_checks),
       well_typed_name_x st (update_exterior_checks_name n cks) ->
       well_typed_name_x st n)
    ); intros.
- inversion H; subst; simpl in H;
  constructor; smack.
- inversion H0; subst.
  specialize (H _ _ H5); constructor; auto.
  inversion H; subst; simpl in *; smack.
- simpl in H1.
  inversion H1; subst.
  rewrite <- (exp_exterior_checks_refl e) in H9.
  rewrite <- (exp_exterior_checks_refl e0) in H10.
  specialize (H _ _ H9).
  specialize (H0 _ _ H10).
  apply WT_Binary_Exp_X with (t := t) (t1 := t1) (t2 := t2); auto.
- simpl in H0.
  inversion H0; subst.
  rewrite <- (exp_exterior_checks_refl e) in H6.
  specialize (H _ _ H6).
  apply WT_Unary_Exp_X with (t := t) (t' := t'); auto.
- simpl in H.
  inversion H; subst.
  apply WT_Identifier_X with (md := md) (t := t); auto.
- inversion H1; subst.
  rewrite <- (name_exterior_checks_refl n) in H6.
  rewrite <- (exp_exterior_checks_refl e) in H8.
  specialize (H _ _ H6).
  specialize (H0 _ _ H8).
  apply WT_Indexed_Component_X with (t := t) (t' := t') (a_ast_num := a_ast_num) (tn := tn) (tm := tm); auto.
- simpl in H0.
  inversion H0; subst.
  rewrite <- (name_exterior_checks_refl n) in H5.
  specialize (H _ _ H5).
  apply WT_Selected_Component_X with (t := t) (t' := t') (r_ast_num := r_ast_num)
                                     (tn := tn) (fields := fields); auto.
Qed.

Ltac apply_well_typed_exp_preserve :=
  match goal with
  | [H: well_typed_exp_x ?st (update_exterior_checks_exp ?e ?cks) |- _] =>
      specialize (well_typed_exp_preserve _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma well_typed_name_preserve: forall n st cks,
  well_typed_name_x st (update_exterior_checks_name n cks) ->
    well_typed_name_x st n.
Proof.
  induction n; intros;
  inversion H; subst.
- apply WT_Identifier_X with (md := md) (t := t); auto.
- apply WT_Indexed_Component_X with (t := t) (t' := t') (a_ast_num := a_ast_num) (tn := tn) (tm := tm); auto.
- apply WT_Selected_Component_X with (t := t) (t' := t') (r_ast_num := r_ast_num)
                                     (tn := tn) (fields := fields); auto.
Qed.

Ltac apply_well_typed_name_preserve :=
  match goal with
  | [H: well_typed_name_x _ (update_exterior_checks_name _ _) |- _] =>
      specialize (well_typed_name_preserve _ _ _ H);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma well_typed_store_updated_by_undefined_value: forall st f x m t,
  well_typed_store st (snd f) ->
    fetch_var_rt x st = Some (m, t) ->
      well_typed_store st (snd (push f x Undefined)).
Proof.
  intros.
  inversion H; subst.
  constructor; smack.
  remember (beq_nat x0 x) as b.
  destruct b; smack.
  rewrite (beq_nat_eq _ _ Heqb).
  exists m, t; smack.
  constructor.
Qed.

Ltac apply_well_typed_store_updated_by_undefined_value :=
  match goal with
  | [H1: well_typed_store ?st _,
     H2: fetch_var_rt ?x ?st = Some (?m, ?t) |- _] =>
      specialize (well_typed_store_updated_by_undefined_value _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_store_stack_merge: forall st f s,
  well_typed_store st (snd f) ->
    well_typed_stack st s ->
      well_typed_stack st (f :: s).
Proof.
  intros.
  constructor; smack.
- remember (fetch x f) as b.
  destruct b; smack.
  inversion H; smack.
  inversion H0; smack.
Qed.

Ltac apply_well_typed_store_stack_merge :=
  match goal with
  | [H1: well_typed_store ?st _,
     H2: well_typed_stack ?st _ |- _] =>
      specialize (well_typed_store_stack_merge _ _ _ H1 H2); let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_stacks_merge: forall st s1 s2,
  well_typed_stack st s1 ->
    well_typed_stack st s2 ->
      well_typed_stack st (s1 ++ s2).
Proof.
  intros.
  constructor; smack.
- apply_fetchG_split.
  inversion H; smack.
  inversion H0; smack.
Qed.

Ltac apply_well_typed_stacks_merge :=
  match goal with
  | [H1: well_typed_stack ?st ?s1,
     H2: well_typed_stack ?st ?s2 |- _] =>
      specialize (well_typed_stacks_merge _ _ _ H1 H2); let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_store_updated_by_undefined_value': forall st f x m t,
  well_typed_value_in_store st (snd f) ->
    fetch_var_rt x st = Some (m, t) ->
      well_typed_value_in_store st (snd (push f x Undefined)).
Proof.
  intros.
  constructor; smack.
  exists m, t; smack; constructor.
Qed.

Ltac apply_well_typed_store_updated_by_undefined_value' :=
  match goal with
  | [H1: well_typed_value_in_store ?st _,
     H2: fetch_var_rt ?x ?st = Some (?m, ?t) |- _] =>
      specialize (well_typed_store_updated_by_undefined_value' _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_store_stack_merge': forall st f s,
  well_typed_value_in_store st (snd f) ->
    well_typed_value_in_stack st s ->
      well_typed_value_in_stack st (f :: s).
Proof.
  intros;
  constructor; smack.
Qed.

Ltac apply_well_typed_store_stack_merge' :=
  match goal with
  | [H1: well_typed_value_in_store ?st _,
     H2: well_typed_value_in_stack ?st _ |- _] =>
      specialize (well_typed_store_stack_merge' _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_store_merge': forall st s1 s2,
  well_typed_value_in_store st s1 ->
    well_typed_value_in_store st s2 ->
      well_typed_value_in_store st (s1 ++ s2).
Proof.
  intros st s1;
  induction s1; smack.
  inversion H; subst.
  specialize (IHs1 _ H6 H0).
  constructor; smack.
Qed.

Ltac apply_well_typed_store_merge' :=
  match goal with
  | [H1: well_typed_value_in_store ?st ?s1,
     H2: well_typed_value_in_store ?st ?s2 |- _] =>
      specialize (well_typed_store_merge' _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_stacks_merge': forall st s1 s2,
  well_typed_value_in_stack st s1 ->
    well_typed_value_in_stack st s2 ->
      well_typed_value_in_stack st (s1 ++ s2).
Proof.
  intros st s1; revert st;
  induction s1; smack;
  inversion H; subst;
  specialize (IHs1 _ _ H5 H0);
  constructor; auto.
Qed.

Ltac apply_well_typed_stacks_merge' :=
  match goal with
  | [H1: well_typed_value_in_stack ?st ?s1,
     H2: well_typed_value_in_stack ?st ?s2 |- _] =>
      specialize (well_typed_stacks_merge' _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_store_stack_split': forall st f s,
  well_typed_value_in_stack st (f :: s) ->
    well_typed_value_in_stack st s /\ well_typed_value_in_store st (snd f).
Proof.
  intros;
  inversion H; auto.
Qed.

Ltac apply_well_typed_store_stack_split' :=
  match goal with
  | [H: well_typed_value_in_stack ?st (?f :: ?s) |- _] =>
      specialize (well_typed_store_stack_split' _ _ _ H);
      let HZ := fresh "HZ" in
      let HZ1 := fresh "HZ" in
      let HZ2 := fresh "HZ" in
      intros HZ; destruct HZ as [HZ1 HZ2]
  end.

Lemma well_typed_store_split': forall st s1 s2,
  well_typed_value_in_store st (s1 ++ s2) ->
    well_typed_value_in_store st s1 /\ well_typed_value_in_store st s2.
Proof.
  intros st s1;
  induction s1; smack;
  match goal with
  | [ |- well_typed_value_in_store _ nil] => constructor
  | [H: well_typed_value_in_store _ _ |- _] => inversion H; subst; specialize (IHs1 _ H5); smack
  end;
  constructor; smack.
Qed.

Ltac apply_well_typed_store_split' :=
  match goal with
  | [H: well_typed_value_in_store ?st (?s1 ++ ?s2) |- _] =>
      specialize (well_typed_store_split' _ _ _ H);
      let HZ := fresh "HZ" in
      let HZ1 := fresh "HZ" in
      let HZ2 := fresh "HZ" in
      intros HZ; destruct HZ as [HZ1 HZ2]
  end.

Lemma well_typed_stack_split': forall st s1 s2,
  well_typed_value_in_stack st (s1 ++ s2) ->
    well_typed_value_in_stack st s1 /\ well_typed_value_in_stack st s2.
Proof.
  intros st s1; revert st.
  induction s1; smack;
  match goal with
  | [|- well_typed_value_in_stack _ nil] => constructor
  | [H: well_typed_value_in_stack _ _ |- _] =>
      inversion H; subst; specialize (IHs1 _ _ H4); smack
  end;
  constructor; auto.
Qed.

Ltac apply_well_typed_stack_split' :=
  match goal with
  | [H: well_typed_value_in_stack _ (?s1 ++ ?s2) |- _] =>
      specialize (well_typed_stack_split' _ _ _ H);
      let HZ := fresh "HZ" in
      let HZ1 := fresh "HZ" in
      let HZ2 := fresh "HZ" in
      intros HZ; destruct HZ as [HZ1 HZ2]
  end.

Lemma value_in_range_is_well_typed: forall st t v l u,
  extract_subtype_range_rt st t (RangeRT l u) ->
    rangeCheck v l u (OK (Int v)) ->
      well_typed_value st t (Int v).
Proof.
  intros.
  destruct t; inversion H; subst;
  inversion H3; subst;
  [ apply TV_Subtype with (l:=l) (u:=u); auto |
    apply TV_Derived_Type with (l:=l) (u:=u); auto |
    apply TV_Integer_Type with (l:=l) (u:=u); auto
  ];
  match goal with
  | [H: rangeCheck _ _ _ _ |- _] => inversion H; subst; auto
  end.
Qed.

Ltac apply_value_in_range_is_well_typed :=
  match goal with
  | [H1: extract_subtype_range_rt ?st ?t (RangeRT ?l ?u),
     H2: rangeCheck ?v ?l ?u (OK (Int ?v)) |- _] =>
      specialize (value_in_range_is_well_typed _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.


Lemma binop_int_type: forall op t1 t2 t,
  (op = Plus \/ op = Minus \/ op = Multiply) \/ (op = Divide \/ op = Modulus) ->
    binop_type op t1 t2 = Some t ->
      t = Integer.
Proof.
  intros;
  destruct H as [[H1 | [H1 | H1]] | [H1 | H1]]; subst;
  destruct t1, t2; smack.
Qed.

Ltac apply_binop_int_type :=
  match goal with
  | [H1: ?op' = Plus \/ ?op' = Minus \/ ?op' = Multiply,
     H2: binop_type ?op' ?t1' ?t2' = Some ?t' |- _] =>
      apply binop_int_type with (op := op') (t1 := t1') (t2 := t2'); auto;
      left; auto
  | [H1: ?op' = Divide,
     H2: binop_type ?op' ?t1' ?t2' = Some ?t' |- _] =>
      apply binop_int_type with (op := op') (t1 := t1') (t2 := t2'); auto;
      right; smack
  | [H1: ?op' = Modulus,
     H2: binop_type ?op' ?t1' ?t2' = Some ?t' |- _] =>
      apply binop_int_type with (op := op') (t1 := t1') (t2 := t2'); auto;
      right; smack
  end.

Lemma binop_bool_type: forall op t1 t2 t,
  op <> Plus ->
  op <> Minus ->
  op <> Multiply ->
  op <> Divide ->
  op <> Modulus ->
  binop_type op t1 t2 = Some t ->
  t = Boolean.
Proof.
  intros;
  destruct op; smack; clear H H0 H1 H2 H3;
  destruct t1, t2; inversion H4; auto.
Qed.

Ltac apply_binop_bool_type :=
  match goal with
  | [H1: ?op <> Plus,
     H2: ?op <> Minus,
     H3: ?op <> Multiply,
     H4: ?op <> Divide,
     H5: ?op <> Modulus,
     H6: binop_type ?op ?t1 ?t2 = Some ?t |- _] => specialize (binop_bool_type _ _ _ _ H1 H2 H3 H4 H5 H6)
  end.

Lemma binop_arithm_typed: forall op v1 v2 v,
  evalBinOpRTS (OverflowCheck :: nil) op v1 v2 (OK v) ->
    forall st, well_typed_value st Integer v.
Proof.
  intros;
  inversion H; subst;
  inversion H2; subst;
  inversion H7; subst;
  rewrite H5 in H1; inversion H1; subst;
  inversion H3; subst;
  constructor; auto.
Qed.

Ltac apply_binop_arithm_typed :=
  match goal with
  | [H: evalBinOpRTS (OverflowCheck :: nil) _ _ _ _ |- _] =>
      specialize (binop_arithm_typed _ _ _ _ H)
  end.

Lemma binop_logic_typed: forall op v1 v2 v,
  op <> Plus ->
  op <> Minus ->
  op <> Multiply ->
  op <> Divide ->
  op <> Modulus ->
  evalBinOpRTS nil op v1 v2 (OK v) ->
  forall st, well_typed_value st Boolean v.
Proof.
  intros;
  inversion H4; subst; clear H4;
  destruct op; smack;
  clear H H0 H1 H2 H3;
  destruct v1, v2; inversion H6;
  constructor;
  match goal with
  | [|- ?b = _ \/ ?b = _] => destruct b; auto
  end.
Qed.

Ltac apply_binop_logic_typed :=
  match goal with
  | [H1: ?op <> Plus,
     H2: ?op <> Minus,
     H3: ?op <> Multiply,
     H4: ?op <> Divide,
     H5: ?op <> Modulus,
     H6: evalBinOpRTS nil ?op _ _ _ |- _] =>
      specialize (binop_logic_typed _ _ _ _ H1 H2 H3 H4 H5 H6)
  end.

Lemma unop_minus_typed: forall v v',
  evalUnOpRTS (OverflowCheck :: nil) Unary_Minus v (OK v') ->
    forall st, well_typed_value st Integer v'.
Proof.
  intros;
  inversion H; subst; clear H;
  inversion H2; subst; clear H2;
  inversion H6; subst; clear H6;
  inversion H2; subst; clear H2;
  rewrite H3 in H; inversion H; subst;
  inversion H0; subst;
  constructor; auto.
Qed.

Ltac apply_unop_minus_typed :=
  match goal with
  | [H: evalUnOpRTS (OverflowCheck :: nil) Unary_Minus _ (OK _) |- _] =>
      specialize (unop_minus_typed _ _ H)
  end.

Lemma exp_type_same: forall st e t t',
  well_typed_exp_x st e ->
    type_of_exp_x st e = Some t ->
      fetch_exp_type_rt (expression_astnum_rt e) st = Some t' ->
        t = t'.
Proof.
  intros;
  inversion H; smack;
  inversion H2; smack.
Qed.

Ltac apply_exp_type_same :=
  match goal with
  | [H1: well_typed_exp_x ?st ?e,
     H2: type_of_exp_x ?st ?e = Some _,
     H3: fetch_exp_type_rt (expression_astnum_rt ?e) ?st = Some _ |- _] =>
      specialize (exp_type_same _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intros HZ; subst
  end.

Lemma eval_expr_well_typed_value: forall e st st' s e' v,
  toExpRT st e e' ->
    toSymTabRT st st' ->
      well_typed_stack_and_symboltable st' s ->
        well_typed_exp_x st' e' ->
          evalExpRT st' s e' (OK v) ->
            exists t, fetch_exp_type_rt (expression_astnum_rt e') st' = Some t /\
                      well_typed_value st' t v.
Proof.
  apply (expression_ind
    (fun e: exp =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (e' : expRT) (v : value),
       toExpRT st e e' ->
       toSymTabRT st st' ->
       well_typed_stack_and_symboltable st' s ->
       well_typed_exp_x st' e' ->
       evalExpRT st' s e' (OK v) ->
       exists t,
         fetch_exp_type_rt (expression_astnum_rt e') st' = Some t /\
         well_typed_value st' t v)
    (fun n: name =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (n' : nameRT) (v : value),
       toNameRT st n n' ->
       toSymTabRT st st' ->
       well_typed_stack_and_symboltable st' s ->
       well_typed_name_x st' n' ->
       evalNameRT st' s n' (OK v) ->
       exists t,
         fetch_exp_type_rt (name_astnum_rt n') st' = Some t /\
         well_typed_value st' t v)
    ); intros.
- inversion H; subst;
  inversion H2; subst;
  inversion H3; subst.

  exists Boolean; smack.
  inversion H12; smack. constructor; destruct b; smack.

  exists Integer; smack.
  inversion H13; smack. inversion H7; subst. constructor; smack.

  exists Integer; smack.
  inversion H13; smack. inversion H7; subst. inversion H4; subst.
  apply_in_bound_conflict; smack.
- inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst.
  specialize(H _ _ _ _ _ H9 H1 H2 H10 H13); smack.
- inversion H1; subst;
  inversion H4; subst;
  inversion H5; subst;
  simpl;
  match goal with
  | [H: fetch_exp_type_rt _ _ = Some ?t |- _] => rewrite H; exists t
  end; split; auto.
  + assert (HZ1: t = Integer).
    apply_binop_int_type. subst.
    apply_binop_arithm_typed; auto.
  + assert (HZ1: t = Integer).
    apply binop_int_type with (op := Divide) (t1 := t1) (t2 := t2); auto.
    inversion H25; subst.
    apply_binop_arithm_typed; auto.
  + assert (HZ1: t = Integer).

    apply binop_int_type with (op := Modulus) (t1 := t1) (t2 := t2); auto. subst.
    specialize (H0 _ _ _ _ _ H14 H2 H3 H16 H24). destruct H0 as [t' [H0a H0b]].
    apply_exp_type_same.
    match goal with
    | [H: well_typed_stack_and_symboltable ?st ?s |- _] => destruct H as [st s HStack HSymb]
    end;
    match goal with
    | [H: binop_type Modulus ?t1 ?t' = Some Integer |- _] =>
        destruct t1, t'; inversion H; subst
    end;
    repeat progress match goal with
    | [H1: evalBinOpRTS (_ :: nil) _ _ _ _ |- _] => inversion H1; subst; clear H1
    | [H1: evalBinOpRTS nil _ _ _ _ |- _] => inversion H1; subst; clear H1
    | [H1: Math.binary_operation _ _ _ = _ |- _] => inversion H1; subst; clear H1
    | [H1: evalBinOpRT _ _ _ _ _ |- _] => inversion H1; subst; clear H1
    | [H1: Math.mod' _ _ = Some _ |- _] => inversion H1; subst; clear H1
    | [H1: divCheck ?op ?v0 ?v3 (OK ?v4) |- _ ] => inversion H1; subst; clear H1
    end;
    match goal with
    | [H0: well_typed_symbol_table ?st',
       H1: fetch_exp_type_rt ?x ?st' = Some ?t,
       H2: well_typed_value ?st' ?t (Int ?v3),
       H3: Zeq_bool ?v3 0 = false |- _ ] =>
        clear - H0 H1 H2 H3
    end; constructor;
    match goal with
    | [H1: well_typed_value _ _ _ |- _] => inversion H1; subst; clear H1
    end;
    repeat progress match goal with
    | [H1: well_typed_symbol_table _ |- _] => inversion H1; subst; clear H1
    | [H1: well_typed_subtype_declaration _ |- _] => inversion H1; subst; clear H1
    | [H1:forall (t0 : type) (l0 u0 : Z),
       extract_subtype_range_rt ?st' t0 (RangeRT l0 u0) ->
       sub_bound (Interval l0 u0) int32_bound true,
       H2: extract_subtype_range_rt ?st' ?t0 _ |- _] => specialize (H1 _ _ _ H2)
    end;
    match goal with
    | [H1: in_bound ?v ?vBound true,
       H2: sub_bound ?vBound int32_bound true |- _] =>
      apply modulus_in_bound_trans with (bound := vBound); auto
    | _ => apply modulus_in_int32_bound; auto
    end.
  + assert (HZ1: t = Boolean).
    apply_binop_bool_type; auto.
    apply_binop_logic_typed; subst; auto.
- inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  simpl;
  match goal with
  | [H: fetch_exp_type_rt _ _ = Some ?t |- _] => rewrite H; exists t
  end; split; auto.
  + assert(HZ1: t = Integer).
    destruct t'; inversion H15; auto.
    apply_unop_minus_typed. subst; auto.
  + destruct u;
    specialize (H _ _ _ _ _ H11 H1 H2 H12 H19);
    inversion H; destruct H5;
    apply_exp_type_same; intros.
    inversion H20; subst. inversion H8; subst.
    destruct v0; inversion H9; subst.
    inversion H16; subst; auto.
    smack.
    inversion H20; subst. inversion H8; subst.
    destruct v0; inversion H9; subst.
    destruct x; inversion H16; subst.
    destruct (negb n); constructor; auto.
- inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  simpl;
  match goal with
  | [H: fetch_exp_type_rt _ _ = Some ?t |- _] => rewrite H; exists t
  end; split; auto.
  match goal with
  | [H: well_typed_stack_and_symboltable ?st ?s |- _] => destruct H as [st s HStack HSymb]
  end;
  specialize (well_typed_stack_infer _ _ HStack); intro HB1.
  inversion HB1; subst.
  specialize (H1 _ _ H8); smack.
- inversion H1; subst;
  inversion H4; subst;
  inversion H5; subst;
  simpl;
  match goal with
  | [H: fetch_exp_type_rt _ _ = Some ?t |- _] => rewrite H; exists t
  end; split; auto.
  specialize (H _ _ _ _ _ H12 H2 H3 H10 H18).
  inversion H. destruct H6.
  inversion H7; subst.
  specialize (H26 _ _ H25).
  rewrite H16 in H6; inversion H6; subst.
  rewrite H17 in H9; inversion H9; subst.
  destruct H26 as [H26a [H26b H26c]]; assumption.
- inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  simpl;
  match goal with
  | [H: fetch_exp_type_rt _ _ = Some ?t |- _] => rewrite H; exists t
  end; split; auto.
  specialize (H _ _ _ _ _ H10 H1 H2 H9 H11).
  inversion H; subst.
  destruct H5.
  inversion H6; subst.
  rewrite H13 in H5; inversion H5; subst.
  rewrite H14 in H8; inversion H8; subst.
  specialize (H18 _ _ H19).
  destruct H18 as [t' [HZ1 [HZ2 HZ3]]].
  rewrite H15 in HZ1; inversion HZ1; subst; assumption.
Qed.

Ltac apply_eval_expr_well_typed_value :=
  match goal with
  | [H1: toExpRT ?st ?e ?e',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack_and_symboltable ?st' ?s,
     H4: well_typed_exp_x ?st' ?e',
     H5: evalExpRT ?st' ?s ?e' (OK ?v) |- _] =>
      specialize (eval_expr_well_typed_value _ _ _ _ _ _ H1 H2 H3 H4 H5);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma eval_name_well_typed_value: forall n st st' s n' v,
  toNameRT st n n' ->
    toSymTabRT st st' ->
      well_typed_stack st' s ->
        well_typed_name_x st' n' ->
          evalNameRT st' s n' (OK v) ->
            exists t, fetch_exp_type_rt (name_astnum_rt n') st' = Some t /\
                      well_typed_value st' t v.
Proof.
  induction n; intros.
- inversion H; subst;
  inversion H1; subst;
  inversion H2; subst;
  inversion H3; subst.
  specialize (H4 _ _ H9).
  destruct H4 as [md' [t' [HZ1 HZ2]]].
  exists t; smack.
- inversion H; subst;
  inversion H2; subst;
  inversion H3; subst.
  specialize (IHn _ _ _ _ _ H10 H0 H1 H8 H16).
  destruct IHn as [t'' [HZ1 HZ2]].
  simpl.
  inversion HZ2; subst.
  specialize (H17 _ _ H23).
  exists typ; smack.
- inversion H; subst;
  inversion H2; subst;
  inversion H3; subst.
  specialize (IHn _ _ _ _ _ H9 H0 H1 H8 H10).
  destruct IHn as [t'' [HZ1 HZ2]].
  simpl.
  inversion HZ2; subst.
  rewrite H12 in HZ1; inversion HZ1; subst.
  rewrite H13 in H5; inversion H5; subst.
  specialize (H15 _ _ H18).
  destruct H15 as [t' [HZ3 HZ4]].
  rewrite H14 in HZ3; inversion HZ3; subst;
  exists t'; smack.
Qed.

Ltac apply_eval_name_well_typed_value :=
  match goal with
  | [H1: toNameRT ?st ?n ?n',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack ?st' ?s,
     H4: well_typed_name_x ?st' ?n',
     H5: evalNameRT ?st' ?s ?n' (OK ?v) |- _] =>
      specialize (eval_name_well_typed_value _ _ _ _ _ _ H1 H2 H3 H4 H5);
      let t := fresh "t" in
      let HZ := fresh "HZ" in
      let HZ1 := fresh "HZ" in
      let HZ2 := fresh "HZ" in
      intros HZ; destruct HZ as [t [HZ1 HZ2]]
end.

Lemma typed_value_in_bound1: forall st t v vBound,
  well_typed_value st t (Int v) ->
    bound_of_type st t vBound ->
      in_bound v vBound true.
Proof.
  intros;
  inversion H; subst; inversion H0; subst; smack;
  match goal with
  | [H1: extract_subtype_range_rt _ _ _,
     H2: extract_subtype_range_rt _ _ _ |- _] => apply_extract_subtype_range_unique; auto
  | _ => idtac
  end;
  match goal with
  | [H: extract_subtype_range_rt _ _ _ |- _] => inversion H; subst; smack
  end.
Qed.

Lemma typed_value_in_bound2: forall st t v l u,
  well_typed_value st t (Int v) ->
    extract_subtype_range_rt st t (RangeRT l u) ->
      in_bound v (Interval l u) true.
Proof.
  intros;
  inversion H; subst; inversion H0; subst; smack;
  match goal with
  | [H1: extract_subtype_range_rt _ _ _,
     H2: extract_subtype_range_rt _ _ _ |- _] => apply_extract_subtype_range_unique; auto
  | _ => idtac
  end;
  match goal with
  | [H: extract_subtype_range_rt _ _ _ |- _] => inversion H; subst; smack
  end.
Qed.

Ltac apply_typed_value_in_bound :=
  match goal with
  | [H1: well_typed_value ?st ?t (Int ?v),
     H2: bound_of_type ?st ?t ?vBound |- _] =>
      specialize (typed_value_in_bound1 _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  | [H1: well_typed_value ?st ?t (Int ?v),
     H2: extract_subtype_range_rt ?st ?t (RangeRT ?l ?u) |- _] =>
      specialize (typed_value_in_bound2 _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma well_typed_bounded_var_exists_int_value: forall st f x m t l u v,
  well_typed_store st (snd f) ->
    fetch_var_rt x st = Some (m, t) ->
      bound_of_type st t (Interval l u) ->
        STACK.fetch x f = Some v ->
          v <> Undefined ->
            exists n, v = Int n.
Proof.
  intros.
  inversion H; smack.
  unfold STACK.fetch in H2.
  specialize (H4 _ _ H2).
  destruct H4 as [m' [t' [H4a H4b]]].
  match goal with
  | [H1: fetch_var_rt ?x ?st = ?t1,
     H2: fetch_var_rt ?x ?st = ?t2 |- _] => rewrite H1 in H2; inversion H2; subst
  end.
  inversion H1; subst;
  inversion H4b; smack;
  match goal with
  | [H: extract_subtype_range_rt _ _ _ |- _] => inversion H; smack
  end.
Qed.

Ltac apply_well_typed_bounded_var_exists_int_value :=
  match goal with
  | [H1: well_typed_store ?st (snd ?f),
     H2: fetch_var_rt ?x ?st = Some (?m, ?t),
     H3: bound_of_type ?st ?t (Interval ?l ?u),
     H4: STACK.fetch ?x ?f = Some ?v,
     H5: ?v <> Undefined |- _] =>
      specialize (well_typed_bounded_var_exists_int_value _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5);
      let HZ := fresh "HZ" in intro HZ; destruct HZ; subst
  end.

Lemma well_typed_var_in_bound: forall st f t x v l u m,
  well_typed_store st (snd f) ->
    STACK.fetch x f = Some (Int v) ->
      fetch_var_rt x st = Some (m, t) ->
        bound_of_type st t (Interval l u) ->
          in_bound v (Interval l u) true.
Proof.
  intros.
  inversion H; smack.
  unfold STACK.fetch in H0.
  specialize (H3 _ _ H0); smack.
  rewrite H4 in H1; inversion H1; subst.
  apply_typed_value_in_bound; auto.
Qed.

Ltac apply_well_typed_var_in_bound :=
  match goal with
  [H1: well_typed_store ?st (snd ?f),
   H2: STACK.fetch ?x ?f = Some (Int ?v),
   H3: fetch_var_rt ?x ?st = Some (?m, ?t),
   H4: bound_of_type ?st ?t (Interval ?l ?u) |- _] =>
    specialize (well_typed_var_in_bound _ _ _ _ _ _ _ _ H1 H2 H3 H4);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma well_typed_value_of_var: forall st f x m t v,
  well_typed_store st (snd f) ->
    fetch_var_rt x st = Some (m, t) ->
        STACK.fetch x f = Some v ->
            well_typed_value st t v.
Proof.
  intros.
  inversion H; smack.
  unfold STACK.fetch in H1.
  specialize (H2 _ _ H1).
  destruct H2 as [m' [t' [H2a H2b]]].
  match goal with
  | [H1: fetch_var_rt ?x ?st = ?t1,
     H2: fetch_var_rt ?x ?st = ?t2 |- _] => rewrite H1 in H2; inversion H2; subst
  end.
  auto.
Qed.

Ltac apply_well_typed_value_of_var :=
  match goal with
  | [H1: well_typed_store ?st (snd ?f),
     H2: fetch_var_rt ?x ?st = Some (?m, ?t),
     H3: STACK.fetch ?x ?f = Some ?v |- _] =>
      specialize (well_typed_value_of_var _ _ _ _ _ _ H1 H2 H3);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma well_typed_value_subtype_trans: forall st t x l u t' l' u',
  well_typed_value st t (Int x) ->
    bound_of_type st t (Interval l u) ->
      extract_subtype_range_rt st t' (RangeRT l' u') ->
        sub_bound (Interval l u) (Interval l' u') true ->
          well_typed_value st t' (Int x).
Proof.
  intros.
  assert (HA2: in_bound x (Interval l' u') true).
    apply_typed_value_in_bound;
    apply_In_Bound_SubBound_Trans; auto.
  destruct t';
  inversion H1; subst;
  inversion H5; subst;
  [ apply TV_Subtype with (l:=l') (u:=u'); auto |
    apply TV_Derived_Type with (l:=l') (u:=u'); auto |
    apply TV_Integer_Type with (l:=l') (u:=u'); auto
  ].
Qed.

Ltac apply_well_typed_value_subtype_trans :=
  match goal with
  | [H1: well_typed_value ?st ?t (Int ?x),
     H2: bound_of_type ?st ?t (Interval ?l ?u),
     H3: extract_subtype_range_rt ?st ?t' (RangeRT ?l' ?u'),
     H4: sub_bound (Interval ?l ?u) (Interval ?l' ?u') true |- _] =>
      specialize (well_typed_value_subtype_trans _ _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intro HZ
  end.

Lemma well_typed_int_value_exists: forall v st t l u,
  v <> Undefined ->
    bound_of_type st t (Interval l u) ->
      well_typed_value st t v ->
        exists n, v = Int n.
Proof.
  intros.
  match goal with
  | [H: bound_of_type ?st ?x1 (Interval ?l ?u) |- _] => inversion H; smack
  end.
  match goal with
  | [H: well_typed_value ?st ?x1 ?v |- _] => inversion H; smack
  end.
  match goal with
  | [H: extract_subtype_range_rt ?st ?x1 (RangeRT ?l ?u) |- _] => inversion H; smack
  end.
  match goal with
  | [H: well_typed_value ?st ?x1 ?v |- _] => inversion H; smack
  end.
Qed.

Ltac apply_well_typed_int_value_exists :=
  match goal with
  | [H1: ?v <> Undefined,
     H2: bound_of_type ?st ?t (Interval ?l ?u),
     H3: well_typed_value ?st ?t ?v |- _] =>
    specialize (well_typed_int_value_exists _ _ _ _ _ H1 H2 H3);
    let HZ := fresh "HZ" in intro HZ;
    destruct HZ as [v' HZ']
  | [H1: ?v = Undefined -> False,
     H2: bound_of_type ?st ?t (Interval ?l ?u),
     H3: well_typed_value ?st ?t ?v |- _] =>
    specialize (well_typed_int_value_exists _ _ _ _ _ H1 H2 H3);
    let HZ := fresh "HZ" in intro HZ;
    destruct HZ as [v' HZ']
  end.


Lemma value_well_typed_with_matched_type: forall st t t' v,
  well_typed_symbol_table st ->
    is_range_constrainted_type t = false ->
      well_typed_value st t' v ->
        type_match t t' = true ->
          well_typed_value st t v.
Proof.
  intros.
  inversion H; subst; inversion H3; subst.
  destruct t; inversion H0; smack;
  destruct t'; inversion H2; smack;
  match goal with
  | [H: beq_nat _ _ = true |- _] => symmetry in H; rewrite (beq_nat_eq _ _ H); auto
  | [H: well_typed_value st _ _ |- _] => inversion H; subst
  | _ => idtac
  end;
  match goal with
  | [|- well_typed_value _ _ Undefined] => constructor
  | [H1: forall (t : type) (l u : Z),
       extract_subtype_range_rt ?st t (RangeRT l u) ->
       sub_bound (Interval l u) int32_bound true,
     H2: extract_subtype_range_rt ?st ?t (RangeRT ?l ?u) |- _] =>
      specialize (H1 _ _ _ H2)
  end;
  apply_In_Bound_SubBound_Trans;
  constructor; auto.
Qed.

Ltac apply_value_well_typed_with_matched_type :=
  match goal with
  | [H1: well_typed_symbol_table ?st,
     H2: is_range_constrainted_type ?t = false,
     H3: well_typed_value ?st ?t' ?v,
     H4: type_match ?t ?t' = true |- _] =>
      specialize (value_well_typed_with_matched_type _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma storeUpdate_with_typed_value_preserve_typed_store: forall st f f' x m t v,
  update f x v = Some f' ->
    well_typed_value_in_store st (snd f) ->
      fetch_var_rt x st = Some (m, t) ->
        well_typed_value st t v ->
          well_typed_value_in_store st (snd f').
Proof.
  intros st f f' x m t v H.
  unfold update in H. remember (updates (store_of f) x v) as b.
  destruct b; inversion H; subst; simpl. clear H.
  revert m t s Heqb. destruct f; simpl in *.
  functional induction (updates s0 x v); intros;
  match goal with
  | [H: Some ?s = _ |- _] => inversion H; subst
  end;
  match goal with
  | [H: well_typed_value_in_store ?st _ |- _] => inversion H; subst
  end;
  constructor; smack.

  symmetry in e0; rewrite (beq_nat_eq _ _ e0) in *.
  rewrite H0 in H3; inversion H3; subst.
  exists x0, x1; smack.
Qed.

Ltac apply_storeUpdate_with_typed_value_preserve_typed_store :=
  match goal with
  | [H1: update ?f ?x ?v = Some ?f',
     H2: well_typed_value_in_store ?st _,
     H3: fetch_var_rt ?x ?st = Some (?m, ?t),
     H4: well_typed_value ?st ?t ?v |- _] =>
      specialize (storeUpdate_with_typed_value_preserve_typed_store _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma updateG_with_typed_value_preserve_typed_stack: forall st s s' x m t v,
  updateG s x v = Some s' ->
    well_typed_value_in_stack st s ->
      fetch_var_rt x st = Some (m, t) ->
        well_typed_value st t v ->
          well_typed_value_in_stack st s'.
Proof.
  intros st s s' x m t v; revert s' m t.
  functional induction (updateG s x v); smack;
  match goal with
  | [H: well_typed_value_in_stack ?st _ |- _] => inversion H; subst
  end;
  constructor; smack.
  apply_storeUpdate_with_typed_value_preserve_typed_store; auto.
Qed.

Ltac apply_updateG_with_typed_value_preserve_typed_stack :=
  match goal with
  | [H1: updateG ?s ?x ?v = Some ?s',
     H2: well_typed_value_in_stack ?st ?s,
     H3: fetch_var_rt ?x ?st = Some (?m, ?t),
     H4: well_typed_value ?st ?t ?v |- _] =>
      specialize (updateG_with_typed_value_preserve_typed_stack _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma updated_array_select_eq: forall a i v,
  array_select (updateIndexedComp a i v) i = Some v.
Proof.
  induction a; smack.
  assert (HA: Zeq_bool i i = true).
  apply Zeq_is_eq_bool; auto.
  rewrite HA; auto.
  remember (Zeq_bool a1 i) as bx.
  destruct bx; smack; rewrite <- Heqbx; auto.
Qed.

Lemma updated_record_select_eq: forall r f v,
  record_select (updateSelectedComp r f v) f = Some v.
Proof.
  induction r; smack.
  rewrite <- beq_nat_refl; auto.
  remember (beq_nat a0 f) as bx.
  destruct bx; smack; rewrite <- Heqbx; auto.
Qed.

Lemma updated_array_select: forall a i v i1 v1,
  array_select (updateIndexedComp a i v) i1 = Some v1 ->
    i = i1 \/ (Zeq_bool i i1 = false /\ array_select a i1 = Some v1).
Proof.
  induction a; smack.
  remember (Zeq_bool i i1) as b.
  destruct b; inversion H.
  symmetry in Heqb; rewrite (Zeq_bool_eq _ _ Heqb); auto.

  remember (Zeq_bool a1 i1) as b1;
  remember (Zeq_bool a1 i) as b2;
  destruct b1, b2; subst;
  repeat progress match goal with
  | [H: true = Zeq_bool _ _ |- _] =>
      symmetry in H; specialize (Zeq_bool_eq _ _ H); clear H; smack
  end.
  right.
  assert(HA: Zeq_bool i i1 = Zeq_bool i1 i).
    clear. remember (Zeq_bool i i1) as b1. remember (Zeq_bool i1 i) as b2.
    destruct b1, b2; auto;
    match goal with
    | [H: true = Zeq_bool _ _ |- _] =>
        symmetry in H; specialize (Zeq_bool_eq _ _ H); clear H; smack
    end.
    assert (HA1: Zeq_bool i1 i1 = true). apply Zeq_is_eq_bool; auto. auto.
    apply Zeq_is_eq_bool; auto.
  assert(HA1: Zeq_bool i1 i1 = true). apply Zeq_is_eq_bool; auto.
  rewrite HA1 in H; inversion H; subst. auto.
  right. rewrite <- Heqb1 in H; smack.
  unfold array_select in H.
  rewrite <- Heqb1 in H. fold array_select in H.
  specialize (IHa _ _ _ _ H); auto.
Qed.

Ltac apply_updated_array_select :=
  match goal with
  | [H: array_select (updateIndexedComp ?a ?i ?v) ?i1 = Some ?v1 |- _] =>
      specialize (updated_array_select _ _ _ _ _ H);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma updated_record_select: forall r f v f1 v1,
  record_select (updateSelectedComp r f v) f1 = Some v1 ->
    f = f1 \/ (beq_nat f f1 = false /\ record_select r f1 = Some v1).
Proof.
  induction r; smack.
  remember (beq_nat f f1) as b.
  destruct b; inversion H.
  symmetry in Heqb; rewrite (beq_nat_true _ _ Heqb); auto.

  remember (beq_nat a0 f1) as b1;
  remember (beq_nat a0 f) as b2;
  destruct b1, b2; subst;
  repeat progress match goal with
  | [H: true = beq_nat _ _ |- _] =>
      symmetry in H; specialize (beq_nat_true _ _ H); clear H; smack
  end.
  right.
  assert(HA: beq_nat f f1 = beq_nat f1 f).
    clear. remember (beq_nat f f1) as b1. remember (beq_nat f1 f) as b2.
    destruct b1, b2; auto;
    match goal with
    | [H: true = beq_nat _ _ |- _] =>
        symmetry in H; specialize (beq_nat_true _ _ H); clear H; smack
    end.
    apply beq_nat_refl; auto.

    assert (HA1: true = beq_nat f f). apply beq_nat_refl; auto. auto.
  rewrite <- beq_nat_refl in H; inversion H; subst; auto.
  right. rewrite <- Heqb1 in H; auto.
  unfold record_select in H.
  rewrite <- Heqb1 in H. fold record_select in H.
  specialize (IHr _ _ _ _ H); auto.
Qed.

Ltac apply_updated_record_select :=
  match goal with
  | [H: record_select (updateSelectedComp ?r ?f ?v) ?f1 = Some ?v1 |- _] =>
      specialize (updated_record_select _ _ _ _ _ H);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma arrayUpdate_with_typed_value_preserve_typed_array: forall st t t0 arrObj a a1 i v a_ast_num tn tm l u,
  well_typed_value st (Array_Type t) arrObj ->
  arrObj = ArrayV a \/ arrObj = Undefined ->
  arrayUpdate arrObj i v = Some (ArrayV a1) ->
  fetch_type_rt t st = Some (ArrayTypeDeclRT a_ast_num tn tm t0) ->
  well_typed_value st t0 v ->
  v <> Undefined ->
  extract_array_index_range_rt st t (RangeRT l u) ->
  rangeChecks (RangeCheck :: nil) i l u (OK (Int i)) ->
  well_typed_value st (Array_Type t) (ArrayV a1).
Proof.
  intros.
  unfold arrayUpdate in H1; smack.
- inversion H6; subst.
  apply TV_Array_Type with (ast_num:=a_ast_num) (tid:=tn) (tm:=tm) (typ:=t0) (l:=l) (u:=u); smack;
  inversion H; subst;
  apply_updated_array_select; smack;
  [apply_extract_array_index_range_rt_unique; subst | | | | ];
  solve [
      rewrite updated_array_select_eq in H1; inversion H1; subst; auto |
      specialize (H12 _ _ H10); destruct H12 as [H12a [H12b H12c]]; smack
    ].
- apply TV_Array_Type with (ast_num:=a_ast_num) (tid:=tn) (tm:=tm) (typ:=t0) (l:=l) (u:=u); smack;
  inversion H6; subst;
  remember (Zeq_bool i i0) as b;
  destruct b; inversion H0; subst; auto;
  symmetry in Heqb;
  rewrite <- (Zeq_bool_eq _ _ Heqb); auto.
Qed.

Ltac apply_arrayUpdate_with_typed_value_preserve_typed_array :=
  match goal with
  | [H1: well_typed_value ?st (Array_Type ?t) ?arrObj,
     H2: ?arrObj = ArrayV ?a \/ ?arrObj = Undefined,
     H3: arrayUpdate ?arrObj ?i ?v = Some (ArrayV ?a1),
     H4: fetch_type_rt ?t ?st = Some (ArrayTypeDeclRT ?a_ast_num ?tn ?tm ?t0),
     H5: well_typed_value ?st ?t0 ?v,
     H6: ?v <> Undefined,
     H7: extract_array_index_range_rt ?st ?t (RangeRT ?l ?u),
     H8: rangeChecks (RangeCheck :: nil) ?i ?l ?u (OK (Int ?i)) |- _] =>
        specialize (arrayUpdate_with_typed_value_preserve_typed_array _ _ _ _ _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8);
        let HZ := fresh "HZ" in intros HZ
  end.

Lemma recordUpdate_with_typed_value_preserve_typed_array: forall st t t0 recObj r r1 f v r_ast_num tn fields,
  well_typed_value st (Record_Type t) recObj ->
  recObj = RecordV r \/ recObj = Undefined ->
  recordUpdate recObj f v = Some (RecordV r1) ->
  fetch_type_rt t st = Some (RecordTypeDeclRT r_ast_num tn fields) ->
  record_field_type fields f = Some t0 ->
  well_typed_value st t0 v ->
  v <> Undefined ->
  well_typed_value st (Record_Type t) (RecordV r1).
Proof.
  intros.
  unfold recordUpdate in H1; smack.
- apply TV_Record_Type with (ast_num:=r_ast_num) (tid:=tn) (fields:=fields); auto; intros.
  apply_updated_record_select; smack.

  rewrite updated_record_select_eq in H0; inversion H0; subst.
  exists t0; auto.

  inversion H; subst. rewrite H2 in H10; inversion H10; subst.
  specialize (H11 _ _ H7); auto.
- apply TV_Record_Type with (ast_num:=r_ast_num) (tid:=tn) (fields:=fields); smack.
  remember (beq_nat f f0) as b.
  destruct b; inversion H0; subst.
  symmetry in Heqb; rewrite <- (beq_nat_true _ _ Heqb).
  exists t0; auto.
Qed.

Ltac apply_recordUpdate_with_typed_value_preserve_typed_array :=
  match goal with
  | [H1: well_typed_value ?st (Record_Type ?t) ?recObj,
     H2: ?recObj = RecordV ?r \/ ?recObj = Undefined,
     H3: recordUpdate ?recObj ?f ?v = Some (RecordV ?r1),
     H4: fetch_type_rt ?t ?st = Some (RecordTypeDeclRT ?r_ast_num ?tn ?fields),
     H5: record_field_type ?fields ?f = Some ?t0,
     H6: well_typed_value ?st ?t0 ?v,
     H7: ?v <> Undefined |- _] =>
      specialize (recordUpdate_with_typed_value_preserve_typed_array _ _ _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma storeUpdate_with_typed_value_preserve_typed_stack: forall st0 st x0 x s s' t v,
  storeUpdateRT st s x v (OK s') ->
    toSymTabRT st0 st ->
      toNameRT st0 x0 x ->
        well_typed_symbol_table st ->
          well_typed_value_in_stack st s ->
            well_typed_name_x st x ->
              fetch_exp_type_rt (name_astnum_rt x) st = Some t ->
                well_typed_value st t v ->
                  v <> Undefined ->
                    well_typed_value_in_stack st s'.
Proof.
  intros st0 st x0 x s s' t v H.
  remember (OK s') as sx.
  revert st0 x0 t s' Heqsx.
  induction H; intros;
  match goal with
  | [H: _ = OK ?s' |- _] => inversion H; subst
  end.
-
  inversion H4; subst.
  simpl in H5.
  rewrite H5 in H11; inversion H11; subst.
  apply_updateG_with_typed_value_preserve_typed_stack; auto.
-
  
  inversion H11; subst.
  inversion H8; subst. simpl in *.

  assert(HA: well_typed_value st (Array_Type t') (ArrayV a1)).
    apply_well_typed_stack_infer.
    apply_eval_name_well_typed_value.
    repeat progress match goal with
    | [H1: fetch_exp_type_rt ?x ?st = _, H2: fetch_exp_type_rt ?x ?st = _ |- _] =>
        rewrite H1 in H2; inversion H2; subst
    end.
    rewrite exp_updated_exterior_checks in H4.
    apply_arrayUpdate_with_typed_value_preserve_typed_array; auto.
  specialize (IHstoreUpdateRT _ _ _ _ H15 H7 H28 H9 H10 H20 H24 HA);
  apply IHstoreUpdateRT; smack.
-
  
  inversion H7; subst.
  inversion H4; subst. simpl in *.

  assert(HA: well_typed_value st (Record_Type t') (RecordV r1)).
    apply_well_typed_stack_infer.
    apply_eval_name_well_typed_value.
    repeat progress match goal with
    | [H1: fetch_exp_type_rt ?x ?st = _, H2: fetch_exp_type_rt ?x ?st = _ |- _] =>
        rewrite H1 in H2; inversion H2; subst
    end.
    apply_recordUpdate_with_typed_value_preserve_typed_array; auto.
  specialize (IHstoreUpdateRT _ _ _ _ H11 H3 H15 H5 H6 H16 H19 HA); auto;
  apply IHstoreUpdateRT; smack.
Qed.

Ltac apply_storeUpdate_with_typed_value_preserve_typed_stack :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?x ?v (OK ?s'),
     H2: toSymTabRT ?st0 ?st,
     H3: toNameRT ?st0 ?x0 ?x,
     H4: well_typed_symbol_table ?st,
     H5: well_typed_value_in_stack ?st ?s,
     H6: well_typed_name_x ?st ?x,
     H7: fetch_exp_type_rt (name_astnum_rt ?x) ?st = Some ?t,
     H8: well_typed_value ?st ?t ?v,
     H9: ?v <> Undefined |- _] =>
      specialize (storeUpdate_with_typed_value_preserve_typed_stack _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8 H9);
      let HZ := fresh "HZ" in intros HZ
  | [H1: storeUpdateRT ?st ?s ?x ?v (OK ?s'),
     H2: toSymTabRT ?st0 ?st,
     H3: toNameRT ?st0 ?x0 ?x,
     H4: well_typed_symbol_table ?st,
     H5: well_typed_value_in_stack ?st ?s,
     H6: well_typed_name_x ?st ?x,
     H7: fetch_exp_type_rt (name_astnum_rt ?x) ?st = Some ?t,
     H8: well_typed_value ?st ?t ?v,
     H9: ?v = Undefined -> False |- _] =>
      specialize (storeUpdate_with_typed_value_preserve_typed_stack _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7 H8 H9);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma push_value_in_range_preserve_typed_store: forall st f x m t l u v,
  well_typed_value_in_store st (snd f) ->
    fetch_var_rt x st = Some (m, t) ->
      extract_subtype_range_rt st t (RangeRT l u) ->
        rangeCheck v l u (OK (Int v)) ->
          well_typed_value_in_store st (snd (push f x (Int v))).
Proof.
  intros.
  constructor; auto.
  exists m, t; smack.
  inversion H2; subst.
  destruct t;
  inversion H1; smack.
  apply TV_Subtype with (l:=l) (u:=u); auto.
  apply TV_Derived_Type with (l:=l) (u:=u); auto.
  apply TV_Integer_Type with (l:=l) (u:=u); auto.
Qed.

Ltac apply_push_value_in_range_preserve_typed_store :=
  match goal with
  | [H1: well_typed_value_in_store ?st _,
     H2: fetch_var_rt ?x ?st = Some (?m, ?t),
     H3: extract_subtype_range_rt ?st ?t (RangeRT ?l ?u),
     H4: rangeCheck ?v ?l ?u (OK (Int ?v)) |- _] =>
      specialize (push_value_in_range_preserve_typed_store _ _ _ _ _ _ _ _ H1 H2 H3 H4);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma push_typed_value_preserve_typed_store: forall st f x m t t' v,
  well_typed_symbol_table st ->
    well_typed_value_in_store st (snd f) ->
      fetch_var_rt x st = Some (m, t) ->
        is_range_constrainted_type t = false ->
          well_typed_value st t' v ->
            type_match t' t = true ->
              well_typed_value_in_store st (snd (push f x v)).
Proof.
  intros.
  constructor; auto.
  exists m, t; smack.
  inversion H; subst.
  inversion H5; subst.
  destruct t; inversion H2; smack;
  destruct t'; inversion H4; smack;
  inversion H3; smack;
  match goal with
  | [ |- well_typed_value _ _ Undefined ] => constructor
  | [H: beq_nat _ _ = _ |- _] => symmetry in H; rewrite <- (beq_nat_eq _ _ H); auto
  | [H1: forall (t : type) (l u : Z),
       extract_subtype_range_rt ?st t (RangeRT l u) ->
       sub_bound (Interval l u) int32_bound true,
     H2: extract_subtype_range_rt ?st ?t (RangeRT ?l ?u) |- _] =>
      specialize (H1 _ _ _ H2)
  | _ => idtac
  end;
  apply_In_Bound_SubBound_Trans; constructor; auto.
Qed.

Ltac apply_push_typed_value_preserve_typed_store :=
  match goal with
  | [H1: well_typed_symbol_table ?st,
     H2: well_typed_value_in_store ?st _,
     H3: fetch_var_rt ?x ?st = Some (?m, ?t),
     H4: is_range_constrainted_type ?t = false,
     H5: well_typed_value ?st ?t' ?v,
     H6: type_match ?t' ?t = true |- _] =>
      specialize (push_typed_value_preserve_typed_store _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
      let HZ := fresh "HZ" in intros HZ
  end.