Commit b28441ba authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove IEEE connection in Coq

parent afdfc31e
......@@ -86,3 +86,19 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
| Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
| Ret e => usedVars e
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
\ No newline at end of file
......@@ -432,6 +432,19 @@ Proof.
econstructor; try auto.
Qed.
Lemma eval_eq_env e:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
eval_exp E1 Gamma e v m ->
eval_exp E2 Gamma e v m.
Proof.
induction e; intros;
(match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
try eauto.
eapply Var_load; auto.
rewrite <- (H n); auto.
Qed.
(*
(**
Analogous lemma for unary expressions.
......
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz
Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps
Daisy.Infra.RealRationalProps.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Typing
Daisy.IntervalValidation Daisy.ErrorValidation Daisy.CertificateChecker
Daisy.FPRangeValidator Daisy.Environments Daisy.Infra.RealRationalProps
Daisy.Commands Daisy.Infra.Ltacs.
Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):=
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.
Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
match e with
| Some v => some_cont v
| None => none_cont
end.
Definition normal_or_zero v :=
(v = 0 \/ (Q2R (minValue M64)) <= (Rabs v))%R.
Definition updFlEnv x v E :=
fun y => if y =? x
then Some (A:=(binary_float 53 1024)) v
else E y.
Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):=
match e with
| Var _ x => E x
| Const m v => Some v
......@@ -19,388 +38,1291 @@ Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_
match eval_exp_float e1 E, eval_exp_float e2 E with
| Some f1, Some f2 =>
match b with
| Plus => Some (b64_plus mode_NE f1 f2)
| Sub => Some (b64_minus mode_NE f1 f2)
| Mult => Some (b64_mult mode_NE f1 f2)
| Div => Some (b64_div mode_NE f1 f2)
| Plus => Some (b64_plus dmode f1 f2)
| Sub => Some (b64_minus dmode f1 f2)
| Mult => Some (b64_mult dmode f1 f2)
| Div => Some (b64_div dmode f1 f2)
end
|_ , _ => None
end
| _ => None
end.
Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
Fixpoint bstep_float f E :option fl64 :=
match f with
| Let m x e g => optionLift (eval_exp_float e E)
(fun v => bstep_float g (updFlEnv x v E))
None
| Ret e => eval_exp_float e E
end.
Definition isValid e :=
let trans_e := optionLift e (fun v => Some (B2R 53 1024 v)) None in
optionLift trans_e normal_or_zero False.
Fixpoint eval_exp_valid (e:exp fl64) E :=
match e with
| Some v => some_cont v
| None => none_cont
| Var _ x => True (*isValid (eval_exp_float (Var n) E)*)
| Const m v => True (*isValid (eval_exp_float (Const m v) E)*)
| Unop u e => eval_exp_valid e E
| Binop b e1 e2 =>
(eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\
(let e1_res := eval_exp_float e1 E in
let e2_res := eval_exp_float e2 E in
optionLift e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
normal_or_zero (evalBinop b v1_real v2_real))
True)
True)
| Downcast m e => eval_exp_valid e E
end.
Definition normal_or_zero v :=
Qeq_bool v 0 || Qle_bool (minValue M64) (Qabs v).
(* Lemma eval_exp_float_finite e E: *)
(* forall v, eval_exp_float e E = Some v -> *)
(* (forall n, exists v, E n = Some v -> Is_true (is_finite 53 1024 v)) -> *)
(* Is_true (is_finite 53 1024 v). *)
(* Proof. *)
(* induction e. *)
(* - intros v eval_v; simpl in *)
(* Fixpoint toRExp e := *)
(* match e with *)
(* |Const c => Const (B2R 53 1024 c) *)
(* |Var _ x => Var R x *)
(* |Unop u e => Unop u (toRExp e) *)
(* |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2) *)
(* end. *)
(* Definition toREnv E :env:= fun x:nat => match E x with *)
(* |None => None *)
(* |Some c => Some (B2R 53 1024 c) *)
(* end. *)
(* Definition Binop_to_Rop (b:binop) := *)
(* match b with *)
(* |Plus => Rplus *)
(* |Sub => Rminus *)
(* |Mult => Rmult *)
(* |Div => Rdiv *)
(* end. *)
(* Definition no_overflow b fl1 fl2 := *)
(* let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in *)
(* (Rlt_bool *)
(* (Rabs *)
(* (Fcore_generic_fmt.round radix2 *)
(* (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53) *)
(* (round_mode mode_NE) *)
(* the_val)) *)
(* (bpow radix2 1024) = true). *)
(* Definition no_overflow_in_eval := *)
(* forall b e1 e2 E fl1 fl2, *)
(* eval_exp_float e1 E = Some fl1 -> *)
(* eval_exp_float e2 E = Some fl2 -> *)
(* no_overflow b fl1 fl2. *)
(* (* TODO: Maybe move to Prop *) *)
(* Definition no_underflow b fl1 fl2 := *)
(* let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in *)
(* ((bpow radix2 (-1022)) <= (Rabs the_val))%R. *)
(* Definition no_underflow_in_eval := *)
(* forall b e1 e2 E fl1 fl2, *)
(* eval_exp_float e1 E = Some fl1 -> *)
(* eval_exp_float e2 E = Some fl2 -> *)
(* no_underflow b fl1 fl2. *)
(* Lemma b64_plus_preserves_finite f1 f2: *)
(* is_finite 53 1024 (b64_plus mode_NE f1 f2) = true -> *)
(* is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true. *)
(* Proof. *)
(* intros finite_add. *)
(* case_eq (b64_plus mode_NE f1 f2); *)
(* intros res add_res; *)
(* unfold b64_plus, Bplus in *; *)
(* case_eq f1; intros * f1_eq; *)
(* try rewrite f1_eq in *; simpl in *; *)
(* case_eq f2; intros * f2_eq; *)
(* try rewrite f2_eq in *; simpl in *; *)
(* try destruct (eqb b b0); *)
(* try congruence; try auto. *)
(* Qed. *)
(* Lemma b64_minus_preserves_finite f1 f2: *)
(* is_finite 53 1024 (b64_minus mode_NE f1 f2) = true -> *)
(* is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true. *)
(* Proof. *)
(* intros finite_minus. *)
(* case_eq (b64_minus mode_NE f1 f2); *)
(* intros res add_res; *)
(* unfold b64_minus, Bminus in *; *)
(* case_eq f1; intros * f1_eq; *)
(* try rewrite f1_eq in *; simpl in *; *)
(* case_eq f2; intros * f2_eq; *)
(* try rewrite f2_eq in *; simpl in *; *)
(* try destruct (eqb b (negb b0)); *)
(* try congruence; try auto. *)
(* Qed. *)
(* Lemma b64_mult_preserves_finite f1 f2: *)
(* is_finite 53 1024 (b64_mult mode_NE f1 f2) = true -> *)
(* is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true. *)
(* Proof. *)
(* intros finite_mult. *)
(* case_eq (b64_mult mode_NE f1 f2); *)
(* intros res mult_res; *)
(* unfold b64_mult, Bmult in *; *)
(* case_eq f1; intros * f1_eq; *)
(* try rewrite f1_eq in *; simpl in *; *)
(* case_eq f2; intros * f2_eq; *)
(* try rewrite f2_eq in *; simpl in *; *)
(* try destruct (eqb b b0); *)
(* try congruence; try auto. *)
(* Qed. *)
(* Lemma b64_div_preserves_finite f1 f2: *)
(* is_finite 53 1024 (b64_div mode_NE f1 f2) = true -> *)
(* (forall sgn, f2 = B754_infinity 53 1024 sgn -> False) -> *)
(* is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true. *)
(* Proof. *)
(* intros finite_div no_infty. *)
(* case_eq (b64_div mode_NE f1 f2); *)
(* intros res div_res; *)
(* unfold b64_div, Bdiv in *; *)
(* case_eq f1; intros * f1_eq; *)
(* try rewrite f1_eq in *; simpl in *; *)
(* case_eq f2; intros * f2_eq; *)
(* try rewrite f2_eq in *; simpl in *; *)
(* try congruence; try auto. *)
(* Qed. *)
(* (* Hypothesis Environment not finite --> remove finiteness assumption *)
(* no_overflow and no_underflow need to check only for expression in question. *)
(* As is they are ~ false, move the checks into eval function! *)
(* *) *)
(* Theorem eval_gives_sem e E v: *)
(* (forall v, *)
(* exists q, E v = Some q -> is_finite 53 1024 q = true) -> *)
(* eval_exp_float e E = Some v -> *)
(* no_overflow_in_eval -> *)
(* no_underflow_in_eval -> *)
(* is_finite 53 1024 v = true -> *)
(* eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e) (B2R 53 1024 v). *)
(* Proof. *)
(* revert v; induction e; *)
(* intros v1 eval_succeeds eval_not_overf eval_not_underf finite_res; *)
(* simpl in eval_succeeds. *)
(* - econstructor. *)
(* unfold toREnv. *)
(* rewrite eval_succeeds; auto. *)
(* - inversion eval_succeeds; subst. *)
(* assert (perturb (B2R 53 1024 v1) 0 = B2R 53 1024 v1) as const_def. *)
(* + unfold perturb. *)
(* rewrite Rmult_plus_distr_l. *)
(* rewrite Rmult_1_r. *)
(* rewrite Rmult_0_r. *)
(* rewrite Rplus_0_r. *)
(* reflexivity. *)
(* + simpl. *)
(* setoid_rewrite <- const_def at 2. *)
(* eapply Const_dist. *)
(* rewrite Rabs_R0. *)
(* eapply mEps_geq_zero. *)
(* - inversion eval_succeeds. *)
(* - case_eq (eval_exp_float e1 E); intros * eval_float_e1; *)
(* case_eq (eval_exp_float e2 E); intros * eval_float_e2; *)
(* rewrite eval_float_e1, eval_float_e2 in *; *)
(* try congruence. *)
(* specialize (IHe1 b0 (refl_equal (Some b0)) eval_not_overf eval_not_underf); *)
(* specialize (IHe2 b1 (refl_equal (Some b1)) eval_not_overf eval_not_underf). *)
(* specialize (eval_not_overf b e1 e2 E b0 b1 eval_float_e1 eval_float_e2). *)
(* specialize (eval_not_underf b e1 e2 E b0 b1 eval_float_e1 eval_float_e2). *)
(* unfold no_overflow, no_underflow in *. *)
(* simpl. *)
(* pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr. *)
(* pose proof (relative_error_N_ex radix2 *)
(* (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
Fixpoint bstep_valid f E :=
match f with
| Let m x e g => eval_exp_valid e E /\
(optionLift (eval_exp_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_exp_valid e E
end.
Definition bpowQ (r:radix) (e: Z) :=
match e with
|0%Z => 1%Q
| (' p)%Z => (Z.pow_pos r p) #1
| Z.neg p => Qinv ((Z.pow_pos r p)#1)
end.
Definition B2Q :=
fun prec emax : Z =>
let emin := (3 - emax - prec)%Z in
let fexp := Fcore_FLT.FLT_exp emin prec in
fun f : binary_float prec emax =>
match f with
| B754_zero _ _ _ => 0%Q
| B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_finite _ _ s m e _ =>
let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexp := e |} in
(Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
end.
Lemma B2Q_B2R_eq :
forall v,
is_finite 53 1024 v = true ->
Q2R (B2Q v) = B2R 53 1024 v.
Proof.
intros; unfold B2Q, B2R, is_finite in *.
destruct v eqn:?; try congruence;
try rewrite Q2R0_is_0; try lra.
unfold Fcore_defs.F2R.
rewrite Q2R_mult.
f_equal.
- unfold Z2R, Q2R.
simpl. rewrite RMicromega.Rinv_1.
destruct (cond_Zopp b (' m)); unfold IZR;
try rewrite P2R_INR; try lra.
- unfold Q2R; simpl.
unfold bpow, bpowQ.
destruct e; simpl; try lra.
+ rewrite RMicromega.Rinv_1.
unfold Z2R, IZR.
destruct (Z.pow_pos 2 p); try rewrite P2R_INR; auto.
+ unfold Z2R, IZR. unfold Qinv; simpl.
destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR; simpl; try lra.
* unfold bounded in e0. simpl in e0. unfold canonic_mantissa in e0.
simpl in e0.
pose proof (Is_true_eq_left _ e0).
apply Is_true_eq_true in H0; andb_to_prop H0.
assert (0 < Z.pow_pos 2 p)%Z.
{ apply Zpower_pos_gt_0. cbv; auto. }
rewrite Heqz in H0. inversion H0.
* rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute; try lra.
hnf; intros. pose proof (pos_INR_nat_of_P p0).
rewrite H0 in H1; lra.
Qed.
Fixpoint B2Qexp (e: exp fl64) :=
match e with
| Var _ x => Var Q x
| Const m v => Const m (B2Q v)
| Unop u e => Unop u (B2Qexp e)
| Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2)
| Downcast m e => Downcast m (B2Qexp e)
end.
Fixpoint B2Qcmd (f:cmd fl64) :=
match f with
| Let m x e g => Let m x (B2Qexp e) (B2Qcmd g)
| Ret e => Ret (B2Qexp e)
end.
Definition toREnv (E: nat -> option fl64) (x:nat):option R :=
match E x with
|Some v => Some (Q2R (B2Q v))
|_ => None
end.
Fixpoint is64BitEval (V:Type) (e:exp V) :=
match e with
| Var _ x => True
| Const m e => m = M64
| Unop u e => is64BitEval e
| Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2
| Downcast m e => m = M64 /\ is64BitEval e
end.
Fixpoint is64BitBstep (V:Type) (f:cmd V) :=
match f with
| Let m x e g => is64BitEval e /\ m = M64 /\ is64BitBstep g
| Ret e => is64BitEval e
end.
Fixpoint noDowncast (V:Type) (e:exp V) :=
match e with
| Var _ x => True
| Const m e => True
| Unop u e => noDowncast e
| Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
| Downcast m e => False
end.
Fixpoint noDowncastFun (V:Type) (f:cmd V) :=
match f with
| Let m x e g => noDowncast e /\ noDowncastFun g
| Ret e => noDowncast e
end.
Opaque mTypeToQ.
Lemma validValue_is_finite v:
validFloatValue (Q2R (B2Q v)) M64 -> is_finite 53 1024 v = true.
Proof.
intros validVal.
unfold is_finite.
unfold validFloatValue, B2Q in *.
destruct v; try auto;
destruct validVal; unfold Normal in *; unfold Denormal in *;
unfold maxValue, minValue, maxExponent, minExponentPos in*;
rewrite Q2R_inv in *; unfold bpowQ in *.
- assert (Z.pow_pos radix2 1024 = 179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216%Z)
by (vm_compute;auto).
rewrite H0 in H; destruct H; try lra.
assert (Z.pow_pos 2 1023 = 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608%Z)
by (vm_compute; auto).
rewrite H2 in *.
clear H0 H2.
rewrite Rabs_right in H1.
apply Rle_Qle in H1.
+ rewrite <- Qle_bool_iff in H1.
cbv in H1; try congruence.
+ rewrite <- Q2R0_is_0.
apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
- vm_compute; intros; congruence.
- destruct H.
+ destruct H. rewrite Rabs_right in H.
* rewrite <- Q2R_inv in H.
apply Rlt_Qlt in H.
vm_compute in H.
congruence.
vm_compute; congruence.
* rewrite <- Q2R0_is_0.
apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
+ rewrite <- Q2R0_is_0 in H.
apply eqR_Qeq in H.
vm_compute in H; congruence.
- vm_compute; congruence.
- destruct H.
rewrite Rabs_right in H0.
+ apply Rle_Qle in H0.
rewrite <- Qle_bool_iff in H0.
vm_compute in H0; auto.
+ rewrite <- Q2R0_is_0.
apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
- vm_compute; congruence.
- destruct H.
+ rewrite Rabs_right in H.
* destruct H. rewrite <- Q2R_inv in H.
{ apply Rlt_Qlt in H. rewrite Qlt_alt in H.
vm_compute in H. congruence. }
{ vm_compute; congruence. }
* rewrite <- Q2R0_is_0.
apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
+ rewrite <- Q2R0_is_0 in H.
apply eqR_Qeq in H. vm_compute in H; congruence.
- vm_compute; congruence.
Qed.
Lemma typing_exp_64_bit e:
forall Gamma tMap,
noDowncast e ->
is64BitEval e ->
typeCheck e Gamma tMap = true ->
(forall v,
NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
tMap e = Some M64.
Proof.
induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
simpl in *; try inversion noDowncast_e;
subst.
- destruct (tMap (Var Q n)); try congruence.
rewrite types_valid in *; try set_tac.
type_conv; subst; auto.
- destruct (tMap (Const M64 v)) eqn:?; try congruence; type_conv; subst; auto.
- destruct (tMap (Unop u e)) eqn:?; try congruence.
erewrite IHe in *; eauto.
+ andb_to_prop typecheck_e; type_conv; subst; auto.
+ destruct (tMap e); try congruence; andb_to_prop typecheck_e; auto.
- repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
destruct (tMap (Binop b e1 e2)) eqn:?; try congruence;
erewrite IHe1 in *; eauto.
+ erewrite IHe2 in *; eauto.
* unfold join in typecheck_e.
rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
type_conv; subst; auto.
* destruct (tMap e2); try congruence.
andb_to_prop typecheck_e; eauto.
* intros.
apply types_valid. set_tac.
+ destruct (tMap e1); destruct (tMap e2); try congruence;
andb_to_prop typecheck_e; eauto.
+ intros; apply types_valid; set_tac.
Qed.
Lemma typing_cmd_64_bit f:
forall Gamma tMap,
noDowncastFun f ->
is64BitBstep f ->
typeCheckCmd f Gamma tMap = true ->
(forall v,
NatSet.In v (freeVars f) -> Gamma v = Some M64) ->
tMap (getRetExp f) = Some M64.
Proof.
induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
simpl in *;
subst; try eauto using typing_exp_64_bit.
andb_to_prop typecheck_f.
destruct (tMap e) eqn:?; destruct (tMap (Var Q n)); try congruence.
andb_to_prop R.
destruct noDowncast_f; destruct is64BitEval_f as [Ha [Hb Hc]].
eapply IHf; eauto.
intros. unfold updDefVars.
destruct (v =? n) eqn:?.
- type_conv; auto.
- apply types_valid.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst. rewrite Nat.eqb_neq in Heqb.
congruence.
Qed.
Lemma typing_agrees_exp e:
forall E Gamma tMap v m1 m2,
typeCheck e Gamma tMap = true ->
eval_exp E Gamma (toRExp e) v m1 ->
tMap e = Some m2 ->
m1 = m2.
Proof.
induction e; intros * typeCheck_e eval_e tMap_e; simpl in *;
rewrite tMap_e in *;
inversion eval_e; subst; simpl in *.
- rewrite H0 in *; type_conv; subst; auto.
- type_conv; subst; auto.
- destruct (tMap e) eqn:?; try congruence; type_conv; subst.
andb_to_prop typeCheck_e.
eapply IHe; eauto.
type_conv; subst; auto.
- destruct (tMap e) eqn:?; try congruence; type_conv; subst.
andb_to_prop typeCheck_e.
eapply IHe; eauto.
type_conv; subst; auto.
- destruct (tMap e1) eqn:?; try congruence;
destruct (tMap e2) eqn:?; try congruence.
andb_to_prop typeCheck_e.
type_conv; subst.
assert (m0 = m).
{ eapply IHe1; eauto. }
assert (m3 = m1).
{ eapply IHe2; eauto. }
subst; auto.
- destruct (tMap e) eqn:?; try congruence; type_conv; subst.
andb_to_prop typeCheck_e.
type_conv; subst; auto.
Qed.
Lemma typing_agrees_cmd f:
forall E Gamma tMap v m1 m2,
typeCheckCmd f Gamma tMap = true ->
bstep (toRCmd f) E Gamma v m1 ->
tMap (getRetExp f) = Some m2 ->
m1 = m2.
Proof.
induction f; intros * typeCheck_f eval_f tMap_f; simpl in *.
- andb_to_prop typeCheck_f.
inversion eval_f; subst; simpl in *.
destruct (tMap e); destruct (tMap (Var Q n)); try congruence.
andb_to_prop R; type_conv.
specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).