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

Require Export rt_gen.
Require Export rt_opt_util.
Require Export well_typed_util.

Scheme expression_ind := Induction for exp Sort Prop
                         with name_ind := Induction for name Sort Prop.

Scheme expression_x_ind := Induction for expRT Sort Prop
                         with name_x_ind := Induction for nameRT Sort Prop.

Lemma eval_expr_value_in_bound: forall e st st' s e' v e'' eBound,
  toExpRT st e e' ->
    toSymTabRT st st' ->
      well_typed_stack st' s ->
        well_typed_exp_x st' e' ->
          evalExpRT st' s e' (OK (Int v)) ->
            optExp st' e' (e'', eBound) ->
              in_bound v eBound true.
Proof.
  apply (expression_ind
    (fun e: exp =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (e' : expRT) (v : Z) (e'' : expRT) eBound,
         toExpRT st e e' ->
         toSymTabRT st st' ->
         well_typed_stack st' s ->
         well_typed_exp_x st' e' ->
         evalExpRT st' s e' (OK (Int v)) ->
         optExp st' e' (e'', eBound) ->
         in_bound v eBound true)
    (fun n: name =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (n' : nameRT) (v : Z) (n'' : nameRT) eBound,
         toNameRT st n n' ->
         toSymTabRT st st' ->
         well_typed_stack st' s ->
         well_typed_name_x st' n' ->
         evalNameRT st' s n' (OK (Int v)) ->
         optName st' n' (n'', eBound) ->
         in_bound v eBound true)
    ); intros.
- inversion H; subst;
  inversion H3; subst;
  inversion H4; subst.
  + inversion H12; subst.
  + inversion H13; subst.
    inversion H8; subst.
    inversion H7; subst.
    inversion H11; subst.
    apply In_Bound_Refl; auto.
    apply In_Bound_Two; auto.
    apply In_Bound_Refl; auto.
  + inversion H13; subst.
    inversion H8; subst.
    inversion H5; subst.
    apply_in_bound_conflict; smack.
- inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H5; subst.
  specialize (H _ _ _ _ _ _ _ H10 H1 H2 H11 H14 H8); assumption.
- inversion H1; subst;
  inversion H4; subst;
  inversion H5; subst;
  inversion H6; subst.

  +

    apply_binop_arithm_operand_format; subst.
    specialize (H _ _ _ _ _ _ _ H14 H2 H3 H17 H25 H11).
    specialize (H0 _ _ _ _ _ _ _ H15 H2 H3 H18 H26 H29).
    apply_plus_result_in_bound; auto.
  +

    apply_binop_arithm_operand_format; subst.
    specialize (H _ _ _ _ _ _ _ H14 H2 H3 H16 H24 H11).
    specialize (H0 _ _ _ _ _ _ _ H15 H2 H3 H17 H25 H28).
    match goal with
    | [H1: evalBinOpRTS (DivCheck :: _) _ _ _ _ |- _] => inversion H1; subst
    end;
    repeat progress match goal with
    | [H1: evalBinOpRT DivCheck _ _ _ _ |- _] => inversion H1; subst; clear H1
    | [H1: divCheck ?op ?v0 ?v3 (OK ?v4) |- _ ] => inversion H1; subst; clear H1
    end.
    apply_divide_result_in_bound; auto.
  +

    apply_binop_arithm_operand_format; subst.
    specialize (H _ _ _ _ _ _ _ H14 H2 H3 H16 H24 H11).
    specialize (H0 _ _ _ _ _ _ _ H15 H2 H3 H17 H25 H28).
    match goal with
    | [H1: evalBinOpRTS (DivCheck :: _) _ _ _ _ |- _] => inversion H1; subst
    end;
    repeat progress match goal with
    | [H1: evalBinOpRT DivCheck _ _ _ _ |- _] => inversion H1; subst; clear H1
    | [H1: divCheck ?op ?v0 ?v3 (OK ?v4) |- _ ] => inversion H1; subst; clear H1
    end.
    apply_modulus_result_in_bound; auto.
  + inversion H31; subst.
    clear - H11 H12 H13 H15 H17 H8.
    destruct b; smack;
    destruct v1, v2; inversion H8.
- inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H5; subst.
  + apply_unop_arithm_operand_format; subst.
    specialize (H _ _ _ _ _ _ _ H12 H1 H2 H11 H19 H9).
    apply_unop_arithm_in_bound; auto.
  + inversion H21; subst.
    destruct u; destruct v0; inversion H7; smack.
- inversion H; subst;
  inversion H1; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; subst.
  specialize (H5 _ _ H10).
  destruct H5 as [md' [t' [HZ1 HZ2]]].
  rewrite HZ1 in H11; inversion H11; subst.
  rewrite H12 in H9; inversion H9; subst.
  inversion HZ2; subst;
  inversion H16; smack;
  [inversion H5; subst; inversion H13 | | | ];
  apply_extract_subtype_range_unique; smack.
- apply_eval_name_well_typed_value.
  inversion H1; subst;
  inversion H4; subst;
  inversion H6; subst.
  smack.
  rewrite H23 in H17; inversion H17; subst.
  rewrite H16 in HZ0; inversion HZ0; subst.
  inversion H26; subst.
  rewrite H7 in H18; inversion H18; subst.

  inversion HZ1; subst;
  inversion H8; smack;
  [inversion H9; subst; inversion H20 | | | ];
  apply_extract_subtype_range_unique; smack.
- apply_eval_name_well_typed_value.
  inversion H0; subst;
  inversion H3; subst;
  inversion H5; smack.
  rewrite H20 in H14; inversion H14; subst.
  rewrite H13 in HZ0; inversion HZ0; subst.
  inversion H21; subst.
  rewrite H6 in H15; inversion H15; subst.
  rewrite H7 in H16; inversion H16; subst.

  inversion HZ1; subst;
  inversion H8; smack;
  [ inversion H9; subst; inversion H22 | | | ];
  apply_extract_subtype_range_unique; smack.
Qed.

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

Lemma eval_name_value_in_bound: forall n st st' s n' v n'' nBound,
  toNameRT st n n' ->
    toSymTabRT st st' ->
      well_typed_stack st' s ->
        well_typed_name_x st' n' ->
          evalNameRT st' s n' (OK (Int v)) ->
            optName st' n' (n'', nBound) ->
              in_bound v nBound true.
Proof.
  induction n; intros.
- inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; subst.

  apply_eval_name_well_typed_value. simpl in HZ0.
  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
  | _ => idtac
  end.
  apply_typed_value_in_bound; auto.
- apply_eval_name_well_typed_value.
  inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; subst.

  simpl in HZ0.
  clear H H2 H3 H4 IHn.
  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
  | _ => idtac
  end.
  clear - H30 H16 HZ1.   inversion H30; subst.
  match goal with
  | [H1: fetch_type_rt ?x ?st = _,
     H2: fetch_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
  end.
  apply_typed_value_in_bound; auto.
- apply_eval_name_well_typed_value.
  inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; smack.

  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
  | _ => idtac
  end.
  clear - H22 H14 H15 HZ1.
  inversion H22; subst.
  repeat progress match goal with
  | [H1: fetch_type_rt ?x ?st = _,
     H2: fetch_type_rt ?x ?st = _ |- _] => rewrite H1 in H2; inversion H2; subst
  | [H1: record_field_type _ _ = _,
     H2: record_field_type _ _ = _ |- _] => rewrite H1 in H2; inversion H2; subst
  end.
  apply_typed_value_in_bound; auto.
Qed.

Ltac apply_eval_name_value_in_bound :=
  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 (Int ?v)),
     H6: optName ?st' ?n' (?n'', ?nBound) |- _] =>
      specialize (eval_name_value_in_bound _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma binop_int_operant_exists: forall op cks v1 v2 v,
  (op = Plus \/ op = Minus \/ op = Multiply) \/ (op = Divide \/ op = Modulus) ->
    evalBinOpRTS cks op v1 v2 v ->
      exists v1' v2', v1 = (Int v1') /\ v2 = (Int v2').
Proof.
  intros.
  destruct H as [[HZ1 | [HZ2 | HZ3]] | [HZ4 | HZ5]]; subst;
  destruct v1, v2;
  inversion H0;
  match goal with
  | [|- exists v1' v2', Int ?n = Int v1' /\ Int ?n0 = Int v2'] => exists n, n0; auto
  | [H: Math.binary_operation _ _ _ = _ |- _] => inversion H; subst
  | _ => idtac
  end;
  match goal with
  | [H: evalBinOpRT _ _ _ _ _ |- _] => inversion H; subst
  | _ => idtac
  end;
  match goal with
  | [|- exists v1' v2', Int ?n = Int v1' /\ Int ?n0 = Int v2'] => exists n, n0; auto
  | [H: Math.binary_operation _ _ _ = _ |- _] => inversion H; subst
  | _ => idtac
  end.
Qed.

Ltac apply_binop_int_operant_exists :=
  match goal with
  | [H1: (?op = Plus \/ ?op = Minus \/ ?op = Multiply) |- _] =>
      let HA := fresh "HA" in
      assert (HA: (op = Plus \/ op = Minus \/ op = Multiply) \/ (op = Divide \/ op = Modulus))
  | [H1: evalBinOpRTS _ Divide _ _ _ |- _] =>
      let HA := fresh "HA" in
      assert (HA: (Divide = Plus \/ Divide = Minus \/ Divide = Multiply) \/ (Divide = Divide \/ Divide = Modulus))
  | [H1: evalBinOpRTS _ Modulus _ _ _ |- _] =>
      let HA := fresh "HA" in
      assert (HA: (Modulus = Plus \/ Modulus = Minus \/ Modulus = Multiply) \/ (Modulus = Divide \/ Modulus = Modulus))
  end; auto;
  match goal with
  | [H1: (?op = Plus \/ ?op = Minus \/ ?op = Multiply) \/ (?op = Divide \/ ?op = Modulus),
     H2: evalBinOpRTS ?cks ?op ?v1 ?v2 ?v |- _] =>
      specialize (binop_int_operant_exists _ _ _ _ _ H1 H2);
      let HZ := fresh "HZ" in intros HZ
  end.

Lemma optimize_range_check_reserve_storeUpdate: forall st s n v s' u l u' l' n' ast_num ast_num',
  storeUpdateRT st s n v s' ->
    optimize_range_check (NameRT ast_num n) (Interval l u) (Interval l' u') (NameRT ast_num' n') ->
      storeUpdateRT st s n' v s'.
Proof.
  intros.
  inversion H0; smack.
  apply_store_update_ex_cks_added; auto.
Qed.

Ltac apply_optimize_range_check_reserve_storeUpdate :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n ?v ?s',
     H2: optimize_range_check (NameRT ?ast_num ?n) (Interval ?l ?u) (Interval ?l' ?u') (NameRT ?ast_num' ?n') |- _] =>
    specialize (optimize_range_check_reserve_storeUpdate _ _ _ _ _ _ _ _ _ _ _ _ H1 H2);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_range_check_reserve_storeUpdate_backward: forall st s n v s' u l u' l' n' ast_num ast_num',
  storeUpdateRT st s n' v s' ->
    optimize_range_check (NameRT ast_num n) (Interval l u) (Interval l' u') (NameRT ast_num' n') ->
      storeUpdateRT st s n v s'.
Proof.
  intros.
  inversion H0; smack.
  apply_store_update_ex_cks_stripped; auto.
Qed.

Ltac apply_optimize_range_check_reserve_storeUpdate_backward :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n' ?v ?s',
     H2: optimize_range_check (NameRT ?ast_num ?n) (Interval ?l ?u) (Interval ?l' ?u') (NameRT ?ast_num' ?n') |- _] =>
    specialize (optimize_range_check_reserve_storeUpdate_backward _ _ _ _ _ _ _ _ _ _ _ _ H1 H2);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_range_check_on_copy_out_reserve_storeUpdate: forall st s n v s' u l u' l' n' ast_num ast_num',
  storeUpdateRT st s n v s' ->
    optimize_range_check_on_copy_out (NameRT ast_num n) (Interval u l) (Interval u' l') (NameRT ast_num' n') ->
      storeUpdateRT st s n' v s'.
Proof.
  intros.
  inversion H0; smack.
  apply_store_update_ex_cks_added; auto.
Qed.

Ltac apply_optimize_range_check_on_copy_out_reserve_storeUpdate :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n ?v ?s',
     H2: optimize_range_check_on_copy_out (NameRT ?ast_num ?n) (Interval ?l ?u) (Interval ?l' ?u') (NameRT ?ast_num' ?n') |- _] =>
    specialize (optimize_range_check_on_copy_out_reserve_storeUpdate _ _ _ _ _ _ _ _ _ _ _ _ H1 H2);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_range_check_on_copy_out_reserve_storeUpdate_backward: forall st s n v s' u l u' l' n' ast_num ast_num',
  storeUpdateRT st s n' v s' ->
    optimize_range_check_on_copy_out (NameRT ast_num n) (Interval u l) (Interval u' l') (NameRT ast_num' n') ->
      storeUpdateRT st s n v s'.
Proof.
  intros.
  inversion H0; smack.
  apply_store_update_ex_cks_stripped; auto.
Qed.

Ltac apply_optimize_range_check_on_copy_out_reserve_storeUpdate_backward :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n' ?v ?s',
     H2: optimize_range_check_on_copy_out (NameRT ?ast_num ?n) (Interval ?l ?u) (Interval ?l' ?u') (NameRT ?ast_num' ?n') |- _] =>
    specialize (optimize_range_check_on_copy_out_reserve_storeUpdate_backward _ _ _ _ _ _ _ _ _ _ _ _ H1 H2);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_range_check_both_reserve_storeUpdate: forall st s n v s' u l u' l' n' n'' u1 l1 u1' l1' ast_num ast_num' ast_num'',
  storeUpdateRT st s n v s' ->
    optimize_range_check (NameRT ast_num n) (Interval u l) (Interval u' l') (NameRT ast_num' n') ->
      optimize_range_check_on_copy_out (NameRT ast_num' n') (Interval u1 l1) (Interval u1' l1') (NameRT ast_num'' n'') ->
        storeUpdateRT st s n'' v s'.
Proof.
  intros.
  specialize (optimize_range_check_reserve_storeUpdate _ _ _ _ _ _ _ _ _ _ _ _ H H0); intro.
  specialize (optimize_range_check_on_copy_out_reserve_storeUpdate _ _ _ _ _ _ _ _ _ _ _ _ H2 H1); auto.
Qed.

Ltac apply_optimize_range_check_both_reserve_storeUpdate :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n ?v ?s',
     H2: optimize_range_check (NameRT _ ?n) (Interval ?u ?l) (Interval ?u' ?l') (NameRT _ ?n'),
     H3: optimize_range_check_on_copy_out (NameRT _ ?n') (Interval ?u1 ?l1) (Interval ?u1' ?l1') (NameRT _ ?n'') |- _] =>
    specialize (optimize_range_check_both_reserve_storeUpdate _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H1 H2 H3);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_range_check_both_reserve_storeUpdate_backward: forall st s n v s' u l u' l' n' n'' u1 l1 u1' l1' ast_num ast_num' ast_num'',
  storeUpdateRT st s n'' v s' ->
    optimize_range_check (NameRT ast_num n) (Interval u l) (Interval u' l') (NameRT ast_num' n') ->
      optimize_range_check_on_copy_out (NameRT ast_num' n') (Interval u1 l1) (Interval u1' l1') (NameRT ast_num'' n'') ->
        storeUpdateRT st s n v s'.
Proof.
  intros.
  specialize (optimize_range_check_on_copy_out_reserve_storeUpdate_backward _ _ _ _ _ _ _ _ _ _ _ _ H H1); intro.
  specialize (optimize_range_check_reserve_storeUpdate_backward _ _ _ _ _ _ _ _ _ _ _ _ H2 H0); auto.
Qed.

Ltac apply_optimize_range_check_both_reserve_storeUpdate_backward :=
  match goal with
  | [H1: storeUpdateRT ?st ?s ?n'' ?v ?s',
     H2: optimize_range_check (NameRT _ ?n) (Interval ?u ?l) (Interval ?u' ?l') (NameRT _ ?n'),
     H3: optimize_range_check_on_copy_out (NameRT _ ?n') (Interval ?u1 ?l1) (Interval ?u1' ?l1') (NameRT _ ?n'') |- _] =>
    specialize (optimize_range_check_both_reserve_storeUpdate_backward _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H1 H2 H3);
    let HZ := fresh "HZ" in intro HZ
  end.

Lemma optimize_expression_exist_int_value: forall e e0 e' st0 st s v l u,
  toExpRT st0 e0 e ->
    toSymTabRT st0 st ->
      well_typed_stack_and_symboltable st s ->
        well_typed_exp_x st e ->
          evalExpRT st s e (OK v) ->
            v <> Undefined ->
              optExp st e (e', Interval l u) ->
                exists n, v = Int n.
Proof.
  induction e; intros;
  apply_eval_expr_well_typed_value;
  destruct HZ as [t' [HZ1 HZ2]];
  inversion H3; subst; clear H3;
  inversion H5; smack; clear H5.
  - inversion H13; smack.
    inversion H7; smack.
    inversion H13; smack.
    inversion H8; smack.
    inversion H8; smack. inversion H6; smack.
  - match goal with
    | [H: well_typed_stack_and_symboltable ?st ?s |- _] => destruct H as [st s HStack HSymb]
    end;
    apply_well_typed_stack_infer.
    inversion H; subst;
    inversion HZ; subst;
    inversion H2; smack;
    apply_eval_name_well_typed_value.
    inversion H7; smack.
    rewrite H13 in HZ3; inversion HZ3; subst.
    apply_well_typed_int_value_exists; smack.
    match goal with
    | [H: well_typed_name_x _ _ |- _] => inversion H; subst
    end.
    match goal with
    | [H: bound_of_array_component_type _ ?t _ |- _] => inversion H; subst
    end.
    repeat progress match goal with
    | [H1: fetch_exp_type_rt ?a ?st = Some ?t1, H2: fetch_exp_type_rt ?a ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    | [H1: fetch_type_rt ?t ?st = Some ?t1, H2: fetch_type_rt ?t ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    end.
    clear - H5 HZ4 H4.
    apply_well_typed_int_value_exists; smack.
    match goal with
    | [H: well_typed_name_x _ _ |- _] => inversion H; subst
    end.
    match goal with
    | [H: bound_of_record_field_type _ ?t ?f _ |- _] => inversion H; smack
    end.
    repeat progress match goal with
    | [H1: fetch_exp_type_rt ?a ?st = Some ?t1, H2: fetch_exp_type_rt ?a ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    | [H1: fetch_type_rt ?t ?st = Some ?t1, H2: fetch_type_rt ?t ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    | [H1: record_field_type ?fields ?f = Some ?t1, H2: record_field_type ?fields ?f = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    end.
    apply_well_typed_int_value_exists; smack.
  - inversion H2; subst;
    inversion H; subst.
    clear - H4 H10 H17 H19.
    repeat progress match goal with
    | [H: evalBinOpRTS _ ?op ?v1 ?v2 (OK ?v) |- _] => inversion H; clear H; smack
    end;
    destruct v1, v2;
    match goal with
    | [H: _ ?v1 ?v2 = Some ?v |- _] => inversion H; smack
    end.
    clear - H4 H17 H19.
    repeat progress match goal with
    | [H: evalBinOpRTS _ ?op ?v1 ?v2 (OK ?v) |- _] => inversion H; clear H; smack
    end;
    destruct v1, v2;
    match goal with
    | [H: _ ?v1 ?v2 = Some ?v |- _] => inversion H; smack
    end.
    clear - H4 H17 H19.
    repeat progress match goal with
    | [H: evalBinOpRTS _ ?op ?v1 ?v2 (OK ?v) |- _] => inversion H; clear H; smack
    end;
    destruct v1, v2;
    match goal with
    | [H: _ ?v1 ?v2 = Some ?v |- _] => inversion H; smack
    end.
    match goal with
    | [H: optimize_rtc_binop ?op ?bound1 ?bound2 _ _ |- _] => inversion H; smack
    end.
  - inversion H2; subst;
    inversion H; subst.
    clear - H15.
    repeat progress match goal with
    | [H: evalUnOpRTS _ ?op ?v (OK ?v') |- _] => inversion H; clear H; smack
    end.
    destruct v0;
    match goal with
    | [H: Math.unary_minus ?v = Some ?v' |- _] => inversion H; smack
    end.
    match goal with
    | [H: evalUnOpRTS _ ?op ?v (OK ?v') |- _] => inversion H; smack
    end.
    destruct u, v0;
    match goal with
    | [H: Math.unary_operation ?op ?v = Some ?v' |- _] => inversion H; smack
    end.
    clear - H9 H15 H16.
    inversion H16; smack.
Qed.

Ltac apply_optimize_expression_exist_int_value :=
  match goal with
  | [H1: toExpRT ?st0 ?e0 ?e,
     H2: toSymTabRT ?st0 ?st,
     H3: well_typed_stack_and_symboltable ?st ?s,
     H4: well_typed_exp_x ?st ?e,
     H5: evalExpRT ?st ?s ?e (OK ?v),
     H6: ?v <> Undefined,
     H7: optExp ?st ?e (?e', Interval ?l ?u) |- _] =>
    specialize (optimize_expression_exist_int_value _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7);
    let HZ := fresh "HZ" in
    let v := fresh "v0" in
    intro HZ; destruct HZ as [v HZ]; subst
  | [H1: toExpRT ?st0 ?e0 ?e,
     H2: toSymTabRT ?st0 ?st,
     H3: well_typed_stack_and_symboltable ?st ?s,
     H4: well_typed_exp_x ?st ?e,
     H5: evalExpRT ?st ?s ?e (OK ?v),
     H6: ?v = Undefined -> False,
     H7: optExp ?st ?e (?e', Interval ?l ?u) |- _] =>
    specialize (optimize_expression_exist_int_value _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7);
    let HZ := fresh "HZ" in
    let v := fresh "v0" in
    intro HZ; destruct HZ as [v HZ]; subst
  end.

Lemma optimize_name_exist_int_value: forall n n0 n' st0 st s v l u,
  toNameRT st0 n0 n ->
    toSymTabRT st0 st ->
      well_typed_stack st s ->
        well_typed_name_x st n ->
          evalNameRT st s n (OK v) ->
            v <> Undefined ->
              optName st n (n', Interval l u) ->
                exists n, v = Int n.
Proof.
  induction n; intros;
  apply_eval_name_well_typed_value;
  inversion H3; subst; clear H3;
  inversion H5; smack; clear H5;
  inversion H; subst;
  inversion H1; subst;
  inversion H2; smack.
  rewrite H8 in HZ0; inversion HZ0; subst.
  apply_well_typed_int_value_exists; smack.
  match goal with
  | [H: bound_of_array_component_type _ ?t _ |- _] => inversion H; subst
  end.
  repeat progress match goal with
  | [H1: fetch_exp_type_rt ?a ?st = Some ?t1, H2: fetch_exp_type_rt ?a ?st = Some ?t2 |- _]
      => rewrite H1 in H2; inversion H2; subst
  | [H1: fetch_type_rt t' st = Some ?t1, H2: fetch_type_rt t' st = Some ?t2 |- _]
      => rewrite H1 in H2; inversion H2; subst
  end.
  clear - H4 HZ1 H6.
  apply_well_typed_int_value_exists; smack.
  match goal with
  | [H: bound_of_record_field_type _ ?t ?f _ |- _] => inversion H; smack
  end.
  repeat progress match goal with
  | [H1: fetch_exp_type_rt ?a ?st = Some ?t1, H2: fetch_exp_type_rt ?a ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
  | [H1: fetch_type_rt ?t ?st = Some ?t1, H2: fetch_type_rt ?t ?st = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
  | [H1: record_field_type ?fields ?f = Some ?t1, H2: record_field_type ?fields ?f = Some ?t2 |- _]
        => rewrite H1 in H2; inversion H2; subst
    end.
  apply_well_typed_int_value_exists; smack.
Qed.

Ltac apply_optimize_name_exist_int_value :=
  match goal with
  | [H1: toNameRT ?st0 ?n0 ?n,
     H2: toSymTabRT ?st0 ?st,
     H3: well_typed_stack ?st ?s,
     H4: well_typed_name_x ?st ?n,
     H5: evalNameRT ?st ?s ?n (OK ?v),
     H6: ?v <> Undefined,
     H7: optName ?st ?n (?n', Interval ?l ?u) |- _] =>
    specialize (optimize_name_exist_int_value _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7);
    let HZ := fresh "HZ" in
    let v := fresh "v0" in
    intro HZ; destruct HZ as [v HZ]; subst
  | [H1: toNameRT ?st0 ?n0 ?n,
     H2: toSymTabRT ?st0 ?st,
     H3: well_typed_stack ?st ?s,
     H4: well_typed_name_x ?st ?n,
     H5: evalNameRT ?st ?s ?n (OK ?v),
     H6: ?v = Undefined -> False,
     H7: optName ?st ?n (?n', Interval ?l ?u) |- _] =>
    specialize (optimize_name_exist_int_value _ _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6 H7);
    let HZ := fresh "HZ" in
    let v := fresh "v0" in
    intro HZ; destruct HZ as [v HZ]; subst
  end.

Lemma optExp_soundness: forall e st st' s e' e'' eBound v,
  toExpRT st e e' ->
    toSymTabRT st st' ->
      well_typed_stack st' s ->
        well_typed_exp_x st' e' ->
          optExp st' e' (e'', eBound) ->
            evalExpRT st' s e'' v ->
              evalExpRT st' s e' v.
Proof.
  apply (expression_ind
    (fun e: exp =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (e': expRT) (e'': expRT) (eBound: bound) (v : Ret value),
      toExpRT st e e' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_exp_x st' e' ->
      optExp st' e' (e'', eBound) ->
      evalExpRT st' s e'' v ->
      evalExpRT st' s e' v)
    (fun n: name =>
       forall (st : symTab) (st' : symTabRT) (s : STACK.state)
              (n': nameRT) (n'': nameRT) (nBound: bound) (v : Ret value),
      toNameRT st n n' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_name_x st' n' ->
      optName st' n' (n'', nBound) ->
      evalNameRT st' s n'' v ->
      evalNameRT st' s n' v)
    ); intros.
-

  inversion H; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H7; subst; auto;
  constructor; smack;
  inversion H10; smack.
  inversion H12; subst.
  apply_in_bound_conflict; smack.
-

  inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H5; subst.
  specialize (H _ _ _ _ _ _ _ H10 H1 H2 H11 H8 H15).
  constructor; auto.
-

  inversion H1; subst;
  inversion H4; subst;
  inversion H5; subst;
  inversion H6; subst;
  repeat progress match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (e' e'' : expRT) (eBound : bound)
        (v : Ret value),
      toExpRT st ?e e' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_exp_x st' e' ->
      optExp st' e' (e'', eBound) ->
      evalExpRT st' s e'' v -> evalExpRT st' s e' v,
     H1: toExpRT ?st ?e ?e',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack ?st' ?s,
     H4: well_typed_exp_x ?st' ?e',
     H5: optExp ?st' ?e' (?e'', ?eBound),
     H6: evalExpRT ?st' ?s ?e'' ?v |- _] => specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end;
  [apply EvalBinOpRTE1_RTE; auto | | | apply EvalBinOpRTE1_RTE; auto | | | apply EvalBinOpRTE1_RTE; auto | | |
   apply EvalBinOpRTE1_RTE; auto | | ];
  [apply EvalBinOpRTE2_RTE with (v1:=v1); auto | |
   apply EvalBinOpRTE2_RTE with (v1:=v1); auto | |
   apply EvalBinOpRTE2_RTE with (v1:=v1); auto | |
   apply EvalBinOpRTE2_RTE with (v1:=v1); auto | ];
  apply EvalBinOpRT with (v1:=v1) (v2:=v2); auto.
  +
    apply_binop_int_operant_exists.
    destruct HZ; subst. destruct H7; subst. destruct H7; subst.
    apply_eval_expr_value_in_bound.
    specialize (eval_expr_value_in_bound _ _ _ _ _ _ _ _ H14 H2 H3 H17 H H11); intros.
    apply_plus_result_in_bound_backward; auto.
  +
    apply_binop_int_operant_exists.
    destruct HZ; subst. destruct H7; subst. destruct H7; subst.
    apply_eval_expr_value_in_bound.
    specialize (eval_expr_value_in_bound _ _ _ _ _ _ _ _ H14 H2 H3 H16 H H11); intros.
    apply_divide_result_in_bound_backward; auto.
  +
    apply_binop_int_operant_exists.
    destruct HZ; subst. destruct H7; subst. destruct H7; subst.
    apply_eval_expr_value_in_bound.
    specialize (eval_expr_value_in_bound _ _ _ _ _ _ _ _ H14 H2 H3 H16 H H11); intros.
    apply_modulus_result_in_bound_backward; auto.
  +
  inversion H31; smack.
-

  inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H5; subst;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (e' e'' : expRT) (eBound : bound)
        (v : Ret value),
      toExpRT st ?e e' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_exp_x st' e' ->
      optExp st' e' (e'', eBound) ->
      evalExpRT st' s e'' v -> evalExpRT st' s e' v,
     H1: toExpRT ?st ?e ?e',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack ?st' ?s,
     H4: well_typed_exp_x ?st' ?e',
     H5: optExp ?st' _ (?e'', _),
     H6: evalExpRT ?st' ?s ?e'' ?v |- _] => specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end;
  [ apply EvalUnOpRT_RTE; auto | |
    apply EvalUnOpRT_RTE; auto | ];
  apply EvalUnOpRT with (v:=v0); auto.
  +
    inversion H20; smack.
    inversion H18; smack.
    destruct v0; inversion H22; smack.
    apply_eval_expr_value_in_bound.
    specialize (In_Bound_Unary_Minus_Compat _ _ _ HZ); intro.
    apply_In_Bound_SubBound_Trans; auto.
    apply Do_Checks_Unop with (v':=(Int (- n))); auto.
    eapply OverflowCheckUnop; smack.
    constructor; auto.
  + inversion H21; smack.
-

  inversion H; subst;
  inversion H3; subst;
  inversion H4; subst. assumption.
-

  inversion H1; subst;
  inversion H4; subst;
  inversion H5; subst;
  inversion H6; subst;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (n' n'' : nameRT) (nBound : bound)
        (v : Ret value),
      toNameRT st ?n n' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_name_x st' n' ->
      optName st' n' (n'', nBound) ->
      evalNameRT st' s n'' v -> evalNameRT st' s n' v,
    H1: toNameRT ?st ?n ?n',
    H2: toSymTabRT ?st ?st',
    H3: well_typed_stack ?st' ?s,
    H4: well_typed_name_x ?st' ?n',
    H5: optName ?st' ?n' (?n'', _),
    H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
      specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (e' e'' : expRT) (eBound : bound)
        (v : Ret value),
      toExpRT st ?e e' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_exp_x st' e' ->
      optExp st' e' (e'', eBound) ->
      evalExpRT st' s e'' v -> evalExpRT st' s e' v,
     H1: toExpRT ?st ?e ?e',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack ?st' ?s,
     H4: well_typed_exp_x ?st' ?e',
     H5: optExp ?st' ?e' (?e'', _),
     H6: evalExpRT ?st' ?s ?e'' ?v |- _] => specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  | _ => idtac
  end.
  + apply EvalIndexedComponentRTX_RTE; auto.
  + apply EvalIndexedComponentRTE_RTE with (a:=a0); auto.
    apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H22); intro HZ1.
    apply eval_exp_ex_cks_added.
    apply H0 with (st:=st)
                  (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT))
                  (eBound:=Interval u v0); smack.
    apply eval_exp_ex_cks_added; auto.
  + apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H22); intro HZ1.
    apply EvalIndexedComponentRT_Range_RTE with (a:=a0) (i:=i) (t:=t0) (l:=l) (u:=u0); auto.
    apply eval_exp_ex_cks_added; smack.
    apply H0 with (st:=st)
                  (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT))
                  (eBound:=Interval u v0); smack.
    apply eval_exp_ex_cks_added; auto.
    specialize (optimize_name_ast_num_eq _ _ _ _ H21); smack.
    rewrite exp_updated_exterior_checks.
    clear - H31.
    inversion H31; subst.
    constructor; auto.
  + apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H22); intro HZ1.
    apply EvalIndexedComponentRT with (a:=a0) (i:=i) (t:=t0) (l:=l) (u:=u0); auto.
    apply eval_exp_ex_cks_added; smack.
    apply H0 with (st:=st)
                  (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT))
                  (eBound:=Interval u v0); smack.
    apply eval_exp_ex_cks_added; auto.
    specialize (optimize_name_ast_num_eq _ _ _ _ H21); smack.
    rewrite exp_updated_exterior_checks.
    specialize (optimize_exp_ex_cks_eq _ _ _ _ H22); intro HZZ1.
    rewrite exp_updated_exterior_checks in HZZ1.
    inversion H25; smack.
    specialize (optimize_name_ast_num_eq _ _ _ _ H21); smack.
    match goal with
    | [H1: fetch_exp_type_rt ?x1 _ = fetch_exp_type_rt ?x2 _,
       H2: fetch_exp_type_rt ?x1 _ = Some _,
       H3: fetch_exp_type_rt ?x2 _ = Some _ |- _ ] => rewrite H2 in H1; rewrite H3 in H1; inversion H1; subst
    end.
    apply_extract_array_index_range_rt_unique; subst.
    assert(HZZ2: evalExpRT st' s (update_exterior_checks_exp e' (exp_exterior_checks eRT)) (OK (Int i))).
    apply eval_exp_ex_cks_added; auto.
    specialize (H0 _ _ _ _ _ _ _ H12 H2 H3 HZ HZ1 HZZ2).
    apply_eval_expr_value_in_bound.
    apply_optimize_range_check_backward; auto.
-

  inversion H0; subst;
  inversion H3; subst;
  inversion H4; subst;
  inversion H5; subst;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (n' n'' : nameRT) (nBound : bound)
        (v : Ret value),
      toNameRT st ?n n' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_name_x st' n' ->
      optName st' n' (n'', nBound) ->
      evalNameRT st' s n'' v -> evalNameRT st' s n' v,
    H1: toNameRT ?st ?n ?n',
    H2: toSymTabRT ?st ?st',
    H3: well_typed_stack ?st' ?s,
    H4: well_typed_name_x ?st' ?n',
    H5: optName ?st' ?n' (?n'', _),
    H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
      specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end.
  + apply EvalSelectedComponentRTX_RTE; auto.
  + apply EvalSelectedComponentRT with (r:=r); auto.
Qed.

Ltac apply_optExp_soundness :=
  match goal with
  | [H1: toExpRT ?st ?e ?e',
     H2: toSymTabRT ?st ?st',
     H3: well_typed_stack ?st' ?s,
     H4: well_typed_exp_x ?st' ?e',
     H5: optExp ?st' ?e' (?e'', _),
     H6: evalExpRT ?st' ?s ?e'' ?v |- _] =>
      specialize (optExp_soundness _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
      let HZ := fresh "HZ" in
      intro HZ
  | [H1: well_typed_stack_and_symboltable ?st' ?s |- _] =>
      inversion H1; subst; apply_well_typed_stack_infer;
      match goal with
      | [H1: toExpRT ?st ?e ?e',
         H2: toSymTabRT ?st ?st',
         H3: well_typed_stack ?st' ?s,
         H4: well_typed_exp_x ?st' ?e',
         H5: optExp ?st' ?e' (?e'', _),
         H6: evalExpRT ?st' ?s ?e'' ?v |- _] =>
          specialize (optExp_soundness _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
      let HZ := fresh "HZ" in
      intro HZ
      end
  end.

Lemma optName_soundness: forall n st st' s n' n'' nBound v,
  toNameRT st n n' ->
    toSymTabRT st st' ->
      well_typed_stack st' s ->
        well_typed_name_x st' n' ->
          optName st' n' (n'', nBound) ->
            evalNameRT st' s n'' v ->
              evalNameRT st' s n' v.
Proof.
  induction n; intros.
-

  inversion H; subst;
  inversion H3; subst;
  inversion H4; subst. assumption.
-

  inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; subst;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (n' n'' : nameRT) (nBound : bound)
        (v : Ret value),
      toNameRT st ?n n' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_name_x st' n' ->
      optName st' n' (n'', nBound) ->
      evalNameRT st' s n'' v -> evalNameRT st' s n' v,
    H1: toNameRT ?st ?n ?n',
    H2: toSymTabRT ?st ?st',
    H3: well_typed_stack ?st' ?s,
    H4: well_typed_name_x ?st' ?n',
    H5: optName ?st' ?n' (?n'', _),
    H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
      specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end.
  + apply EvalIndexedComponentRTX_RTE; auto.
  + apply EvalIndexedComponentRTE_RTE with (a:=a0); auto.
    apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H20); intro HZ1.
    apply eval_exp_ex_cks_added.
    apply optExp_soundness with (e:=e) (st:=st)
        (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT)) (eBound:=Interval u v0); auto.
    apply eval_exp_ex_cks_added; auto.
  + apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H20); intro HZ1.
    apply EvalIndexedComponentRT_Range_RTE with (a:=a0) (i:=i) (t:=t0) (l:=l) (u:=u0); auto.
    apply eval_exp_ex_cks_added; smack.
    apply optExp_soundness with (e:=e) (st:=st)
        (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT)) (eBound:=Interval u v0); auto.
    apply eval_exp_ex_cks_added; auto.
    specialize (optimize_name_ast_num_eq _ _ _ _ H19); smack.
    rewrite exp_updated_exterior_checks.
    clear - H29.
    inversion H29; subst.
    constructor; auto.
  + apply_well_typed_exp_preserve.
    apply_eval_expr_value_reserve_backward.
    specialize (optimize_exp_ex_cks_stripped _ _ _ _ _ H20); intro HZ1.
    apply EvalIndexedComponentRT with (a:=a0) (i:=i) (t:=t0) (l:=l) (u:=u0); auto.
    apply eval_exp_ex_cks_added; smack.
    apply optExp_soundness with (e:=e) (st:=st)
        (e'':=update_exterior_checks_exp e' (exp_exterior_checks eRT)) (eBound:=Interval u v0); auto.
    apply eval_exp_ex_cks_added; auto.
    specialize (optimize_name_ast_num_eq _ _ _ _ H19); smack.
    rewrite exp_updated_exterior_checks.
    specialize (optimize_exp_ex_cks_eq _ _ _ _ H20); intro HZZ1.
    rewrite exp_updated_exterior_checks in HZZ1.
    inversion H23; smack.
    specialize (optimize_name_ast_num_eq _ _ _ _ H19); smack.
    match goal with
    | [H1: fetch_exp_type_rt ?x1 _ = fetch_exp_type_rt ?x2 _,
       H2: fetch_exp_type_rt ?x1 _ = Some _,
       H3: fetch_exp_type_rt ?x2 _ = Some _ |- _ ] => rewrite H2 in H1; rewrite H3 in H1; inversion H1; subst
    end.
    apply_extract_array_index_range_rt_unique; subst.
    assert(HZZ2: evalExpRT st' s (update_exterior_checks_exp e' (exp_exterior_checks eRT)) (OK (Int i))).
    apply eval_exp_ex_cks_added; auto.
    apply_optExp_soundness.
    apply_eval_expr_value_in_bound.
    apply_optimize_range_check_backward; auto.
-

  inversion H; subst;
  inversion H2; subst;
  inversion H3; subst;
  inversion H4; subst;
  match goal with
  | [H: forall (st : symTab) (st' : symTabRT)
        (s : STACK.state) (n' n'' : nameRT) (nBound : bound)
        (v : Ret value),
      toNameRT st ?n n' ->
      toSymTabRT st st' ->
      well_typed_stack st' s ->
      well_typed_name_x st' n' ->
      optName st' n' (n'', nBound) ->
      evalNameRT st' s n'' v -> evalNameRT st' s n' v,
    H1: toNameRT ?st ?n ?n',
    H2: toSymTabRT ?st ?st',
    H3: well_typed_stack ?st' ?s,
    H4: well_typed_name_x ?st' ?n',
    H5: optName ?st' ?n' (?n'', _),
    H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
      specialize (H _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6)
  end.
  + apply EvalSelectedComponentRTX_RTE; auto.
  + apply EvalSelectedComponentRT with (r:=r); auto.
Qed.

Ltac apply_optName_soundness :=
  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: optName ?st' ?n' (?n'', _),
     H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
      specialize (optName_soundness _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
      let HZ := fresh "HZ" in
      intro HZ
  | [H1: well_typed_stack_and_symboltable ?st' ?s |- _] =>
      inversion H1; subst; apply_well_typed_stack_infer;
      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: optName ?st' ?n' (?n'', _),
         H6: evalNameRT ?st' ?s ?n'' ?v |- _] =>
           specialize (optName_soundness _ _ _ _ _ _ _ _ H1 H2 H3 H4 H5 H6);
           let HZ := fresh "HZ" in
           intro HZ
      end
  end.