diff options
Diffstat (limited to 'backend/Cmconstrproof.v')
| -rw-r--r-- | backend/Cmconstrproof.v | 727 |
1 files changed, 385 insertions, 342 deletions
diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v index f27fa73c..b9976eec 100644 --- a/backend/Cmconstrproof.v +++ b/backend/Cmconstrproof.v @@ -16,6 +16,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Mem. +Require Import Events. Require Import Op. Require Import Globalenvs. Require Import Cminor. @@ -67,34 +68,67 @@ Scheme eval_expr_ind_3 := Minimality for eval_expr Sort Prop with eval_exprlist_ind_3 := Minimality for eval_exprlist Sort Prop. Hint Resolve eval_Evar eval_Eassign eval_Eop eval_Eload eval_Estore - eval_Ecall eval_Econdition + eval_Ecall eval_Econdition eval_Ealloc eval_Elet eval_Eletvar eval_CEtrue eval_CEfalse eval_CEcond eval_CEcondition eval_Enil eval_Econs: evalexpr. +Lemma eval_list_one: + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_exprlist ge sp le e1 m1 (a ::: Enil) t e2 m2 (v :: nil). +Proof. + intros. econstructor. eauto. constructor. traceEq. +Qed. + +Lemma eval_list_two: + forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 t, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 -> + t = t1 ** t2 -> + eval_exprlist ge sp le e1 m1 (a1 ::: a2 ::: Enil) t e3 m3 (v1 :: v2 :: nil). +Proof. + intros. econstructor. eauto. econstructor. eauto. constructor. + reflexivity. traceEq. +Qed. + +Lemma eval_list_three: + forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 a3 t3 e4 m4 v3 t, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 -> + eval_expr ge sp le e3 m3 a3 t3 e4 m4 v3 -> + t = t1 ** t2 ** t3 -> + eval_exprlist ge sp le e1 m1 (a1 ::: a2 ::: a3 ::: Enil) t e4 m4 (v1 :: v2 :: v3 :: nil). +Proof. + intros. econstructor. eauto. econstructor. eauto. econstructor. eauto. constructor. + reflexivity. reflexivity. traceEq. +Qed. + +Hint Resolve eval_list_one eval_list_two eval_list_three: evalexpr. + Lemma eval_lift_expr: - forall w sp le e1 m1 a e2 m2 v, - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall w sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e1 m1 (lift_expr p a) e2 m2 v. + eval_expr ge sp le' e1 m1 (lift_expr p a) t e2 m2 v. Proof. intros w. apply (eval_expr_ind_3 ge - (fun sp le e1 m1 a e2 m2 v => + (fun sp le e1 m1 a t e2 m2 v => forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e1 m1 (lift_expr p a) e2 m2 v) - (fun sp le e1 m1 a e2 m2 vb => + eval_expr ge sp le' e1 m1 (lift_expr p a) t e2 m2 v) + (fun sp le e1 m1 a t e2 m2 vb => forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp le' e1 m1 (lift_condexpr p a) e2 m2 vb) - (fun sp le e1 m1 al e2 m2 vl => + eval_condexpr ge sp le' e1 m1 (lift_condexpr p a) t e2 m2 vb) + (fun sp le e1 m1 al t e2 m2 vl => forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp le' e1 m1 (lift_exprlist p al) e2 m2 vl)); + eval_exprlist ge sp le' e1 m1 (lift_exprlist p al) t e2 m2 vl)); simpl; intros; eauto with evalexpr. destruct v1; eapply eval_Econdition; eauto with evalexpr; simpl; eauto with evalexpr. - eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. + eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. auto. case (le_gt_dec p n); intro. apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. @@ -105,9 +139,9 @@ Proof. Qed. Lemma eval_lift: - forall sp le e1 m1 a e2 m2 v w, - eval_expr ge sp le e1 m1 a e2 m2 v -> - eval_expr ge sp (w::le) e1 m1 (lift a) e2 m2 v. + forall sp le e1 m1 a t e2 m2 v w, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp (w::le) e1 m1 (lift a) t e2 m2 v. Proof. intros. unfold lift. eapply eval_lift_expr. eexact H. apply insert_lenv_0. @@ -126,67 +160,69 @@ Ltac TrivialOp cstr := of operator applications. *) Lemma inv_eval_Eop_0: - forall sp le e1 m1 op e2 m2 v, - eval_expr ge sp le e1 m1 (Eop op Enil) e2 m2 v -> - e2 = e1 /\ m2 = m1 /\ eval_operation ge sp op nil = Some v. + forall sp le e1 m1 op t e2 m2 v, + eval_expr ge sp le e1 m1 (Eop op Enil) t e2 m2 v -> + t = E0 /\ e2 = e1 /\ m2 = m1 /\ eval_operation ge sp op nil = Some v. Proof. intros. inversion H. inversion H6. intuition. congruence. Qed. Lemma inv_eval_Eop_1: - forall sp le e1 m1 op a1 e2 m2 v, - eval_expr ge sp le e1 m1 (Eop op (a1 ::: Enil)) e2 m2 v -> + forall sp le e1 m1 op t a1 e2 m2 v, + eval_expr ge sp le e1 m1 (Eop op (a1 ::: Enil)) t e2 m2 v -> exists v1, - eval_expr ge sp le e1 m1 a1 e2 m2 v1 /\ + eval_expr ge sp le e1 m1 a1 t e2 m2 v1 /\ eval_operation ge sp op (v1 :: nil) = Some v. Proof. intros. - inversion H. inversion H6. inversion H21. - subst e4; subst m4. subst e6; subst m6. - exists v1; intuition. congruence. + inversion H. inversion H6. inversion H19. + subst. exists v1; intuition. rewrite E0_right. auto. Qed. Lemma inv_eval_Eop_2: - forall sp le e1 m1 op a1 a2 e3 m3 v, - eval_expr ge sp le e1 m1 (Eop op (a1 ::: a2 ::: Enil)) e3 m3 v -> - exists e2, exists m2, exists v1, exists v2, - eval_expr ge sp le e1 m1 a1 e2 m2 v1 /\ - eval_expr ge sp le e2 m2 a2 e3 m3 v2 /\ + forall sp le e1 m1 op a1 a2 t3 e3 m3 v, + eval_expr ge sp le e1 m1 (Eop op (a1 ::: a2 ::: Enil)) t3 e3 m3 v -> + exists t1, exists t2, exists e2, exists m2, exists v1, exists v2, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 /\ + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 /\ + t3 = t1 ** t2 /\ eval_operation ge sp op (v1 :: v2 :: nil) = Some v. Proof. intros. - inversion H. inversion H6. inversion H21. inversion H32. - subst e7; subst m7. subst e9; subst m9. - exists e4; exists m4; exists v1; exists v2. intuition. congruence. + inversion H. subst. inversion H6. subst. inversion H8. subst. + inversion H10. subst. + exists t1; exists t0; exists e0; exists m0; exists v0; exists v1. + intuition. traceEq. Qed. Ltac SimplEval := match goal with - | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op Enil) ?e2 ?m2 ?v) -> _] => + | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op Enil) ?t ?e2 ?m2 ?v) -> _] => intro XX1; - generalize (inv_eval_Eop_0 sp le e1 m1 op e2 m2 v XX1); + generalize (inv_eval_Eop_0 sp le e1 m1 op t e2 m2 v XX1); clear XX1; - intros [XX1 [XX2 XX3]]; - subst e2; subst m2; simpl in XX3; - try (simplify_eq XX3; clear XX3; + intros [XX1 [XX2 [XX3 XX4]]]; + subst t e2 m2; simpl in XX4; + try (simplify_eq XX4; clear XX4; let EQ := fresh "EQ" in (intro EQ; rewrite EQ)) - | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: Enil)) ?e2 ?m2 ?v) -> _] => + | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?e2 ?m2 ?v) -> _] => intro XX1; - generalize (inv_eval_Eop_1 sp le e1 m1 op a1 e2 m2 v XX1); + generalize (inv_eval_Eop_1 sp le e1 m1 op t a1 e2 m2 v XX1); clear XX1; let v1 := fresh "v" in let EV := fresh "EV" in let EQ := fresh "EQ" in (intros [v1 [EV EQ]]; simpl in EQ) - | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?e2 ?m2 ?v) -> _] => + | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?e2 ?m2 ?v) -> _] => intro XX1; - generalize (inv_eval_Eop_2 sp le e1 m1 op a1 a2 e2 m2 v XX1); + generalize (inv_eval_Eop_2 sp le e1 m1 op a1 a2 t e2 m2 v XX1); clear XX1; + let t1 := fresh "t" in let t2 := fresh "t" in let e := fresh "e" in let m := fresh "m" in let v1 := fresh "v" in let v2 := fresh "v" in let EV1 := fresh "EV" in let EV2 := fresh "EV" in - let EQ := fresh "EQ" in - (intros [e [m [v1 [v2 [EV1 [EV2 EQ]]]]]]; simpl in EQ) + let EQ := fresh "EQ" in let TR := fresh "TR" in + (intros [t1 [t2 [e [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]]; simpl in EQ) | _ => idtac end. @@ -209,57 +245,57 @@ Ltac InvEval H := *) Theorem eval_negint: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (negint a) e2 m2 (Vint (Int.neg x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (negint a) t e2 m2 (Vint (Int.neg x)). Proof. TrivialOp negint. Qed. Theorem eval_negfloat: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e1 m1 (negfloat a) e2 m2 (Vfloat (Float.neg x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) -> + eval_expr ge sp le e1 m1 (negfloat a) t e2 m2 (Vfloat (Float.neg x)). Proof. TrivialOp negfloat. Qed. Theorem eval_absfloat: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e1 m1 (absfloat a) e2 m2 (Vfloat (Float.abs x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) -> + eval_expr ge sp le e1 m1 (absfloat a) t e2 m2 (Vfloat (Float.abs x)). Proof. TrivialOp absfloat. Qed. Theorem eval_intoffloat: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e1 m1 (intoffloat a) e2 m2 (Vint (Float.intoffloat x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) -> + eval_expr ge sp le e1 m1 (intoffloat a) t e2 m2 (Vint (Float.intoffloat x)). Proof. TrivialOp intoffloat. Qed. Theorem eval_floatofint: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (floatofint a) e2 m2 (Vfloat (Float.floatofint x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (floatofint a) t e2 m2 (Vfloat (Float.floatofint x)). Proof. TrivialOp floatofint. Qed. Theorem eval_floatofintu: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (floatofintu a) e2 m2 (Vfloat (Float.floatofintu x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (floatofintu a) t e2 m2 (Vfloat (Float.floatofintu x)). Proof. TrivialOp floatofintu. Qed. Theorem eval_notint: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (notint a) e2 m2 (Vint (Int.not x)). + forall sp le e1 m1 a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (notint a) t e2 m2 (Vint (Int.not x)). Proof. unfold notint; intros until x; case (notint_match a); intros. InvEval H. FuncInv. EvalOp. simpl. congruence. @@ -269,15 +305,15 @@ Proof. eapply eval_Eop. eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - apply eval_Enil. - simpl. rewrite Int.or_idem. auto. + apply eval_Enil. reflexivity. reflexivity. + simpl. rewrite Int.or_idem. auto. traceEq. Qed. Lemma eval_notbool_base: - forall sp le e1 m1 a e2 m2 v b, - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall sp le e1 m1 a t e2 m2 v b, + eval_expr ge sp le e1 m1 a t e2 m2 v -> Val.bool_of_val v b -> - eval_expr ge sp le e1 m1 (notbool_base a) e2 m2 (Val.of_bool (negb b)). + eval_expr ge sp le e1 m1 (notbool_base a) t e2 m2 (Val.of_bool (negb b)). Proof. TrivialOp notbool_base. simpl. inversion H0. @@ -290,10 +326,10 @@ Hint Resolve Val.bool_of_true_val Val.bool_of_false_val Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. Theorem eval_notbool: - forall a sp le e1 m1 e2 m2 v b, - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall a sp le e1 m1 t e2 m2 v b, + eval_expr ge sp le e1 m1 a t e2 m2 v -> Val.bool_of_val v b -> - eval_expr ge sp le e1 m1 (notbool a) e2 m2 (Val.of_bool (negb b)). + eval_expr ge sp le e1 m1 (notbool a) t e2 m2 (Val.of_bool (negb b)). Proof. assert (N1: forall v b, Val.is_false v -> Val.bool_of_val v b -> Val.is_true (Val.of_bool (negb b))). intros. inversion H0; simpl; auto; subst v; simpl in H. @@ -305,34 +341,33 @@ Proof. induction a; simpl; intros; try (eapply eval_notbool_base; eauto). destruct o; try (eapply eval_notbool_base; eauto). - destruct e. inversion H. inversion H7. subst vl. - simpl in H11. inversion H11. subst v0; subst v. + destruct e. InvEval H. injection XX4; clear XX4; intro; subst v. inversion H0. rewrite Int.eq_false; auto. simpl; eauto with evalexpr. rewrite Int.eq_true; simpl; eauto with evalexpr. eapply eval_notbool_base; eauto. - inversion H. subst sp0 le0 e0 m op al e3 m0 v0. - simpl in H11. eapply eval_Eop; eauto. + inversion H. subst. + simpl in H12. eapply eval_Eop; eauto. simpl. caseEq (eval_condition c vl); intros. - rewrite H1 in H11. + rewrite H1 in H12. assert (b0 = b). - destruct b0; inversion H11; subst v; inversion H0; auto. + destruct b0; inversion H12; subst v; inversion H0; auto. subst b0. rewrite (Op.eval_negate_condition _ _ H1). destruct b; reflexivity. - rewrite H1 in H11; discriminate. + rewrite H1 in H12; discriminate. inversion H; eauto 10 with evalexpr valboolof. inversion H; eauto 10 with evalexpr valboolof. - inversion H. eapply eval_Econdition. eexact H11. - destruct v1; eauto. + inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H36. + destruct v4; eauto. auto. Qed. Theorem eval_addimm: - forall sp le e1 m1 n a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (addimm n a) e2 m2 (Vint (Int.add x n)). + forall sp le e1 m1 n a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (addimm n a) t e2 m2 (Vint (Int.add x n)). Proof. unfold addimm; intros until x. generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. @@ -341,16 +376,16 @@ Proof. InvEval H0. EvalOp. simpl. rewrite Int.add_commut. auto. InvEval H0. destruct (Genv.find_symbol ge s); discriminate. InvEval H0. - destruct sp; simpl in XX3; discriminate. + destruct sp; simpl in XX4; discriminate. InvEval H0. FuncInv. EvalOp. simpl. subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. EvalOp. Qed. Theorem eval_addimm_ptr: - forall sp le e1 m1 n a e2 m2 b ofs, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr b ofs) -> - eval_expr ge sp le e1 m1 (addimm n a) e2 m2 (Vptr b (Int.add ofs n)). + forall sp le e1 m1 n t a e2 m2 b ofs, + eval_expr ge sp le e1 m1 a t e2 m2 (Vptr b ofs) -> + eval_expr ge sp le e1 m1 (addimm n a) t e2 m2 (Vptr b (Int.add ofs n)). Proof. unfold addimm; intros until ofs. generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. @@ -361,8 +396,8 @@ Proof. destruct (Genv.find_symbol ge s). rewrite Int.add_commut. congruence. discriminate. - InvEval H0. destruct sp; simpl in XX3; try discriminate. - inversion XX3. EvalOp. simpl. decEq. decEq. + InvEval H0. destruct sp; simpl in XX4; try discriminate. + inversion XX4. EvalOp. simpl. decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. InvEval H0. FuncInv. subst b0; subst ofs. EvalOp. simpl. rewrite (Int.add_commut n m). rewrite Int.add_assoc. auto. @@ -370,13 +405,14 @@ Proof. Qed. Theorem eval_add: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (add a b) e3 m3 (Vint (Int.add x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vint (Int.add x y)). Proof. intros until y. unfold add; case (add_match a b); intros. - InvEval H. rewrite Int.add_commut. apply eval_addimm. assumption. + InvEval H. rewrite Int.add_commut. apply eval_addimm. + rewrite E0_left; assumption. InvEval H. FuncInv. InvEval H0. FuncInv. replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)). apply eval_addimm. EvalOp. @@ -387,7 +423,7 @@ Proof. apply eval_addimm. EvalOp. subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. InvEval H0. FuncInv. - apply eval_addimm. auto. + apply eval_addimm. rewrite E0_right. auto. InvEval H0. FuncInv. replace (Int.add x y) with (Int.add (Int.add x i) n2). apply eval_addimm. EvalOp. @@ -396,10 +432,10 @@ Proof. Qed. Theorem eval_add_ptr: - forall sp le e1 m1 a e2 m2 p x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr p x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (add a b) e3 m3 (Vptr p (Int.add x y)). + forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vptr p (Int.add x y)). Proof. intros until y. unfold add; case (add_match a b); intros. InvEval H. @@ -412,7 +448,7 @@ Proof. replace (Int.add x y) with (Int.add (Int.add i y) n1). apply eval_addimm_ptr. subst b0. EvalOp. subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. apply eval_addimm_ptr. auto. + InvEval H0. apply eval_addimm_ptr. rewrite E0_right. auto. InvEval H0. FuncInv. replace (Int.add x y) with (Int.add (Int.add x i) n2). apply eval_addimm_ptr. EvalOp. @@ -421,14 +457,14 @@ Proof. Qed. Theorem eval_add_ptr_2: - forall sp le e1 m1 a e2 m2 p x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vptr p y) -> - eval_expr ge sp le e1 m1 (add a b) e3 m3 (Vptr p (Int.add y x)). + forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) -> + eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vptr p (Int.add y x)). Proof. intros until y. unfold add; case (add_match a b); intros. InvEval H. - apply eval_addimm_ptr. auto. + apply eval_addimm_ptr. rewrite E0_left. auto. InvEval H. FuncInv. InvEval H0. FuncInv. replace (Int.add y x) with (Int.add (Int.add i0 i) (Int.add n1 n2)). apply eval_addimm_ptr. subst b0. EvalOp. @@ -448,15 +484,15 @@ Proof. Qed. Theorem eval_sub: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (sub a b) e3 m3 (Vint (Int.sub x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vint (Int.sub x y)). Proof. intros until y. unfold sub; case (sub_match a b); intros. InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm. assumption. + apply eval_addimm. rewrite E0_right. assumption. InvEval H. FuncInv. InvEval H0. FuncInv. replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)). apply eval_addimm. EvalOp. @@ -476,15 +512,15 @@ Proof. Qed. Theorem eval_sub_ptr_int: - forall sp le e1 m1 a e2 m2 p x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr p x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (sub a b) e3 m3 (Vptr p (Int.sub x y)). + forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vptr p (Int.sub x y)). Proof. intros until y. unfold sub; case (sub_match a b); intros. InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm_ptr. assumption. + apply eval_addimm_ptr. rewrite E0_right. assumption. InvEval H. FuncInv. InvEval H0. FuncInv. subst b0. replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)). @@ -505,10 +541,10 @@ Proof. Qed. Theorem eval_sub_ptr_ptr: - forall sp le e1 m1 a e2 m2 p x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr p x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vptr p y) -> - eval_expr ge sp le e1 m1 (sub a b) e3 m3 (Vint (Int.sub x y)). + forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) -> + eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vint (Int.sub x y)). Proof. intros until y. unfold sub; case (sub_match a b); intros. @@ -535,9 +571,9 @@ Proof. Qed. Lemma eval_rolm: - forall sp le e1 m1 a amount mask e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (rolm a amount mask) e2 m2 (Vint (Int.rolm x amount mask)). + forall sp le e1 m1 a amount mask t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (rolm a amount mask) t e2 m2 (Vint (Int.rolm x amount mask)). Proof. intros until x. unfold rolm; case (rolm_match a); intros. InvEval H. eauto with evalexpr. @@ -554,10 +590,10 @@ Proof. Qed. Theorem eval_shlimm: - forall sp le e1 m1 a n e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + forall sp le e1 m1 a n t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e1 m1 (shlimm a n) e2 m2 (Vint (Int.shl x n)). + eval_expr ge sp le e1 m1 (shlimm a n) t e2 m2 (Vint (Int.shl x n)). Proof. intros. unfold shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. @@ -568,10 +604,10 @@ Proof. Qed. Theorem eval_shruimm: - forall sp le e1 m1 a n e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + forall sp le e1 m1 a n t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e1 m1 (shruimm a n) e2 m2 (Vint (Int.shru x n)). + eval_expr ge sp le e1 m1 (shruimm a n) t e2 m2 (Vint (Int.shru x n)). Proof. intros. unfold shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. @@ -582,9 +618,9 @@ Proof. Qed. Lemma eval_mulimm_base: - forall sp le e1 m1 a n e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (mulimm_base n a) e2 m2 (Vint (Int.mul x n)). + forall sp le e1 m1 a t n e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (mulimm_base n a) t e2 m2 (Vint (Int.mul x n)). Proof. intros; unfold mulimm_base. generalize (Int.one_bits_decomp n). @@ -597,7 +633,7 @@ Proof. rewrite Int.add_zero. rewrite <- Int.shl_mul. apply eval_shlimm. auto. auto with coqlib. destruct l. - intros. apply eval_Elet with e2 m2 (Vint x). auto. + intros. apply eval_Elet with t e2 m2 (Vint x) E0. auto. rewrite H1. simpl. rewrite Int.add_zero. rewrite Int.mul_add_distr_r. rewrite <- Int.shl_mul. @@ -609,18 +645,19 @@ Proof. apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. auto with coqlib. auto with evalexpr. - reflexivity. + reflexivity. traceEq. reflexivity. traceEq. intros. EvalOp. Qed. Theorem eval_mulimm: - forall sp le e1 m1 a n e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (mulimm n a) e2 m2 (Vint (Int.mul x n)). + forall sp le e1 m1 a n t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (mulimm n a) t e2 m2 (Vint (Int.mul x n)). Proof. intros until x; unfold mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - subst n. rewrite Int.mul_zero. eauto with evalexpr. + subst n. rewrite Int.mul_zero. + intro. eapply eval_Elet; eauto with evalexpr. traceEq. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. subst n. rewrite Int.mul_one. auto. case (mulimm_match a); intros. @@ -633,24 +670,25 @@ Proof. Qed. Theorem eval_mul: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (mul a b) e3 m3 (Vint (Int.mul x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (mul a b) (t1**t2) e3 m3 (Vint (Int.mul x y)). Proof. intros until y. unfold mul; case (mul_match a b); intros. - InvEval H. rewrite Int.mul_commut. apply eval_mulimm. auto. - InvEval H0. apply eval_mulimm. auto. + InvEval H. rewrite Int.mul_commut. apply eval_mulimm. + rewrite E0_left; auto. + InvEval H0. rewrite E0_right. apply eval_mulimm. auto. EvalOp. Qed. Theorem eval_divs: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (divs a b) e3 m3 (Vint (Int.divs x y)). + eval_expr ge sp le e1 m1 (divs a b) (t1**t2) e3 m3 (Vint (Int.divs x y)). Proof. TrivialOp divs. simpl. predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. @@ -662,11 +700,11 @@ Lemma eval_mod_aux: y <> Int.zero -> eval_operation ge sp divop (Vint x :: Vint y :: nil) = Some (Vint (semdivop x y))) -> - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (mod_aux divop a b) e3 m3 + eval_expr ge sp le e1 m1 (mod_aux divop a b) (t1**t2) e3 m3 (Vint (Int.sub x (Int.mul (semdivop x y) y))). Proof. intros; unfold mod_aux. @@ -678,18 +716,21 @@ Proof. eapply eval_Econs. eapply eval_Eop. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. apply H. assumption. + apply eval_Enil. reflexivity. reflexivity. + apply H. assumption. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. simpl; reflexivity. apply eval_Enil. - reflexivity. + apply eval_Enil. reflexivity. reflexivity. + simpl; reflexivity. apply eval_Enil. + reflexivity. reflexivity. reflexivity. + reflexivity. traceEq. Qed. Theorem eval_mods: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (mods a b) e3 m3 (Vint (Int.mods x y)). + eval_expr ge sp le e1 m1 (mods a b) (t1**t2) e3 m3 (Vint (Int.mods x y)). Proof. intros; unfold mods. rewrite Int.mods_divs. @@ -699,44 +740,44 @@ Proof. Qed. Lemma eval_divu_base: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (Eop Odivu (a ::: b ::: Enil)) e3 m3 (Vint (Int.divu x y)). + eval_expr ge sp le e1 m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) e3 m3 (Vint (Int.divu x y)). Proof. intros. EvalOp. simpl. predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. Qed. Theorem eval_divu: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (divu a b) e3 m3 (Vint (Int.divu x y)). + eval_expr ge sp le e1 m1 (divu a b) (t1**t2) e3 m3 (Vint (Int.divu x y)). Proof. intros until y. unfold divu; case (divu_match b); intros. InvEval H0. caseEq (Int.is_power2 y). intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. auto. + apply eval_shruimm. rewrite E0_right. auto. apply Int.is_power2_range with y. auto. intros. subst n2. eapply eval_divu_base. eexact H. EvalOp. auto. eapply eval_divu_base; eauto. Qed. Theorem eval_modu: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e1 m1 (modu a b) e3 m3 (Vint (Int.modu x y)). + eval_expr ge sp le e1 m1 (modu a b) (t1**t2) e3 m3 (Vint (Int.modu x y)). Proof. intros until y; unfold modu; case (divu_match b); intros. InvEval H0. caseEq (Int.is_power2 y). intros. rewrite (Int.modu_and x y i H0). - rewrite <- Int.rolm_zero. apply eval_rolm. auto. + rewrite <- Int.rolm_zero. apply eval_rolm. rewrite E0_right; auto. intro. rewrite Int.modu_divu. eapply eval_mod_aux. intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. contradiction. auto. @@ -748,9 +789,9 @@ Proof. Qed. Theorem eval_andimm: - forall sp le e1 m1 n a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (andimm n a) e2 m2 (Vint (Int.and x n)). + forall sp le e1 m1 n a t e2 m2 x, + eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (andimm n a) t e2 m2 (Vint (Int.and x n)). Proof. intros. unfold andimm. case (Int.is_rlw_mask n). rewrite <- Int.rolm_zero. apply eval_rolm; auto. @@ -758,25 +799,26 @@ Proof. Qed. Theorem eval_and: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (and a b) e3 m3 (Vint (Int.and x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (and a b) (t1**t2) e3 m3 (Vint (Int.and x y)). Proof. intros until y; unfold and; case (mul_match a b); intros. - InvEval H. rewrite Int.and_commut. apply eval_andimm; auto. - InvEval H0. apply eval_andimm; auto. + InvEval H. rewrite Int.and_commut. + rewrite E0_left; apply eval_andimm; auto. + InvEval H0. rewrite E0_right; apply eval_andimm; auto. EvalOp. Qed. Remark eval_same_expr_pure: - forall a1 a2 sp le e1 m1 e2 m2 v1 e3 m3 v2, + forall a1 a2 sp le e1 m1 t1 e2 m2 v1 t2 e3 m3 v2, same_expr_pure a1 a2 = true -> - eval_expr ge sp le e1 m1 a1 e2 m2 v1 -> - eval_expr ge sp le e2 m2 a2 e3 m3 v2 -> - a2 = a1 /\ v2 = v1 /\ e2 = e1 /\ m2 = m1. + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 -> + t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ e2 = e1 /\ m2 = m1. Proof. - intros until v1. + intros until v2. destruct a1; simpl; try (intros; discriminate). destruct a2; simpl; try (intros; discriminate). case (ident_eq i i0); intros. @@ -786,22 +828,20 @@ Proof. Qed. Lemma eval_or: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (or a b) e3 m3 (Vint (Int.or x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (or a b) (t1**t2) e3 m3 (Vint (Int.or x y)). Proof. intros until y; unfold or; case (or_match a b); intros. generalize (Int.eq_spec amount1 amount2); case (Int.eq amount1 amount2); intro. case (Int.is_rlw_mask (Int.or mask1 mask2)). - caseEq (same_expr_pure t1 t2); intro. + caseEq (same_expr_pure t0 t3); intro. simpl. InvEval H. FuncInv. InvEval H0. FuncInv. - generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0). - intros [EQ1 [EQ2 [EQ3 EQ4]]]. - injection EQ2; intro EQ5. - subst t2; subst e2; subst m2; subst i0. - EvalOp. simpl. subst x; subst y; subst amount2. - rewrite Int.or_rolm. auto. + generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0). + intros [EQ1 [EQ2 [EQ3 [EQ4 [EQ5 EQ6]]]]]. + injection EQ4; intro EQ7. subst. + EvalOp. simpl. rewrite Int.or_rolm. auto. simpl. EvalOp. simpl. EvalOp. simpl. EvalOp. @@ -809,173 +849,184 @@ Proof. Qed. Theorem eval_xor: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (xor a b) e3 m3 (Vint (Int.xor x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (xor a b) (t1**t2) e3 m3 (Vint (Int.xor x y)). Proof. TrivialOp xor. Qed. Theorem eval_shl: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e1 m1 (shl a b) e3 m3 (Vint (Int.shl x y)). + eval_expr ge sp le e1 m1 (shl a b) (t1**t2) e3 m3 (Vint (Int.shl x y)). Proof. intros until y; unfold shl; case (shift_match b); intros. - InvEval H0. apply eval_shlimm; auto. + InvEval H0. rewrite E0_right. apply eval_shlimm; auto. EvalOp. simpl. rewrite H1. auto. Qed. Theorem eval_shr: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e1 m1 (shr a b) e3 m3 (Vint (Int.shr x y)). + eval_expr ge sp le e1 m1 (shr a b) (t1**t2) e3 m3 (Vint (Int.shr x y)). Proof. TrivialOp shr. simpl. rewrite H1. auto. Qed. Theorem eval_shru: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e1 m1 (shru a b) e3 m3 (Vint (Int.shru x y)). + eval_expr ge sp le e1 m1 (shru a b) (t1**t2) e3 m3 (Vint (Int.shru x y)). Proof. intros until y; unfold shru; case (shift_match b); intros. - InvEval H0. apply eval_shruimm; auto. + InvEval H0. rewrite E0_right; apply eval_shruimm; auto. EvalOp. simpl. rewrite H1. auto. Qed. Theorem eval_addf: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vfloat y) -> - eval_expr ge sp le e1 m1 (addf a b) e3 m3 (Vfloat (Float.add x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) -> + eval_expr ge sp le e1 m1 (addf a b) (t1**t2) e3 m3 (Vfloat (Float.add x y)). Proof. intros until y; unfold addf; case (addf_match a b); intros. - InvEval H. FuncInv. EvalOp. simpl. subst x. reflexivity. + InvEval H. FuncInv. EvalOp. + econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. + traceEq. simpl. subst x. reflexivity. InvEval H0. FuncInv. eapply eval_Elet. eexact H. EvalOp. - eapply eval_Econs. apply eval_lift. eexact EV. - eapply eval_Econs. apply eval_lift. eexact EV0. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. - subst y. rewrite Float.addf_commut. reflexivity. + econstructor; eauto with evalexpr. + econstructor; eauto with evalexpr. + econstructor. apply eval_Eletvar. simpl; reflexivity. + constructor. reflexivity. traceEq. + subst y. rewrite Float.addf_commut. reflexivity. auto. EvalOp. Qed. Theorem eval_subf: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vfloat y) -> - eval_expr ge sp le e1 m1 (subf a b) e3 m3 (Vfloat (Float.sub x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) -> + eval_expr ge sp le e1 m1 (subf a b) (t1**t2) e3 m3 (Vfloat (Float.sub x y)). Proof. intros until y; unfold subf; case (subf_match a b); intros. - InvEval H. FuncInv. EvalOp. subst x. reflexivity. + InvEval H. FuncInv. EvalOp. + econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. + traceEq. subst x. reflexivity. EvalOp. Qed. Theorem eval_mulf: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vfloat y) -> - eval_expr ge sp le e1 m1 (mulf a b) e3 m3 (Vfloat (Float.mul x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) -> + eval_expr ge sp le e1 m1 (mulf a b) (t1**t2) e3 m3 (Vfloat (Float.mul x y)). Proof. TrivialOp mulf. Qed. Theorem eval_divf: - forall sp le e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vfloat y) -> - eval_expr ge sp le e1 m1 (divf a b) e3 m3 (Vfloat (Float.div x y)). + forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) -> + eval_expr ge sp le e1 m1 (divf a b) (t1**t2) e3 m3 (Vfloat (Float.div x y)). Proof. TrivialOp divf. Qed. Theorem eval_cast8signed: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast8signed a) e2 m2 (Vint (Int.cast8signed x)). + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp le e1 m1 (cast8signed a) t e2 m2 (Val.cast8signed v). Proof. - intros until x; unfold cast8signed; case (cast8signed_match a); intros. - InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast8_signed_idem. reflexivity. + intros until v; unfold cast8signed; case (cast8signed_match a); intros. + replace (Val.cast8signed v) with v. auto. + InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity. EvalOp. Qed. Theorem eval_cast8unsigned: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast8unsigned a) e2 m2 (Vint (Int.cast8unsigned x)). + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp le e1 m1 (cast8unsigned a) t e2 m2 (Val.cast8unsigned v). Proof. - intros. unfold cast8unsigned. rewrite Int.cast8unsigned_and. - rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. + intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros. + replace (Val.cast8unsigned v) with v. auto. + InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity. + EvalOp. Qed. - + Theorem eval_cast16signed: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast16signed a) e2 m2 (Vint (Int.cast16signed x)). + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp le e1 m1 (cast16signed a) t e2 m2 (Val.cast16signed v). Proof. - intros until x; unfold cast16signed; case (cast16signed_match a); intros. - InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast16_signed_idem. reflexivity. + intros until v; unfold cast16signed; case (cast16signed_match a); intros. + replace (Val.cast16signed v) with v. auto. + InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity. EvalOp. Qed. Theorem eval_cast16unsigned: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast16unsigned a) e2 m2 (Vint (Int.cast16unsigned x)). + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp le e1 m1 (cast16unsigned a) t e2 m2 (Val.cast16unsigned v). Proof. - intros. unfold cast16unsigned. rewrite Int.cast16unsigned_and. - rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. + intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros. + replace (Val.cast16unsigned v) with v. auto. + InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity. + EvalOp. Qed. Theorem eval_singleoffloat: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e1 m1 (singleoffloat a) e2 m2 (Vfloat (Float.singleoffloat x)). + forall sp le e1 m1 a t e2 m2 v, + eval_expr ge sp le e1 m1 a t e2 m2 v -> + eval_expr ge sp le e1 m1 (singleoffloat a) t e2 m2 (Val.singleoffloat v). Proof. - intros until x; unfold singleoffloat; case (singleoffloat_match a); intros. - InvEval H. FuncInv. EvalOp. subst x. rewrite Float.singleoffloat_idem. reflexivity. + intros until v; unfold singleoffloat; case (singleoffloat_match a); intros. + replace (Val.singleoffloat v) with v. auto. + InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. EvalOp. Qed. Theorem eval_cmp: - forall sp le c e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (cmp c a b) e3 m3 (Val.of_bool (Int.cmp c x y)). + forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmp c x y)). Proof. TrivialOp cmp. simpl. case (Int.cmp c x y); auto. Qed. Theorem eval_cmp_null_r: - forall sp le c e1 m1 a e2 m2 p x b e3 m3 v, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr p x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint Int.zero) -> + forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 v, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint Int.zero) -> (c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) -> - eval_expr ge sp le e1 m1 (cmp c a b) e3 m3 v. + eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 v. Proof. TrivialOp cmp. simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity. Qed. Theorem eval_cmp_null_l: - forall sp le c e1 m1 a e2 m2 p x b e3 m3 v, - eval_expr ge sp le e1 m1 a e2 m2 (Vint Int.zero) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vptr p x) -> + forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 v, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint Int.zero) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p x) -> (c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) -> - eval_expr ge sp le e1 m1 (cmp c a b) e3 m3 v. + eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 v. Proof. TrivialOp cmp. simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity. Qed. Theorem eval_cmp_ptr: - forall sp le c e1 m1 a e2 m2 p x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vptr p x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vptr p y) -> - eval_expr ge sp le e1 m1 (cmp c a b) e3 m3 (Val.of_bool (Int.cmp c x y)). + forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) -> + eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmp c x y)). Proof. TrivialOp cmp. simpl. unfold eq_block. rewrite zeq_true. @@ -983,32 +1034,32 @@ Proof. Qed. Theorem eval_cmpu: - forall sp le c e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vint y) -> - eval_expr ge sp le e1 m1 (cmpu c a b) e3 m3 (Val.of_bool (Int.cmpu c x y)). + forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) -> + eval_expr ge sp le e1 m1 (cmpu c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmpu c x y)). Proof. TrivialOp cmpu. simpl. case (Int.cmpu c x y); auto. Qed. Theorem eval_cmpf: - forall sp le c e1 m1 a e2 m2 x b e3 m3 y, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e2 m2 b e3 m3 (Vfloat y) -> - eval_expr ge sp le e1 m1 (cmpf c a b) e3 m3 (Val.of_bool (Float.cmp c x y)). + forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y, + eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) -> + eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) -> + eval_expr ge sp le e1 m1 (cmpf c a b) (t1**t2) e3 m3 (Val.of_bool (Float.cmp c x y)). Proof. TrivialOp cmpf. simpl. case (Float.cmp c x y); auto. Qed. Lemma eval_base_condition_of_expr: - forall sp le a e1 m1 e2 m2 v (b: bool), - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall sp le a e1 m1 t e2 m2 v (b: bool), + eval_expr ge sp le e1 m1 a t e2 m2 v -> Val.bool_of_val v b -> eval_condexpr ge sp le e1 m1 (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil)) - e2 m2 b. + t e2 m2 b. Proof. intros. eapply eval_CEcond. eauto with evalexpr. @@ -1016,62 +1067,60 @@ Proof. Qed. Lemma eval_condition_of_expr: - forall a sp le e1 m1 e2 m2 v (b: bool), - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall a sp le e1 m1 t e2 m2 v (b: bool), + eval_expr ge sp le e1 m1 a t e2 m2 v -> Val.bool_of_val v b -> - eval_condexpr ge sp le e1 m1 (condexpr_of_expr a) e2 m2 b. + eval_condexpr ge sp le e1 m1 (condexpr_of_expr a) t e2 m2 b. Proof. induction a; simpl; intros; try (eapply eval_base_condition_of_expr; eauto; fail). destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). - destruct e. inversion H. subst sp0 le0 e m op al e0 m0 v0. - inversion H7. subst sp0 le0 e m e1 m1 vl. - simpl in H11. inversion H11; subst v. + destruct e. InvEval H. inversion XX4; subst v. inversion H0. rewrite Int.eq_false; auto. constructor. subst i; rewrite Int.eq_true. constructor. eapply eval_base_condition_of_expr; eauto. - inversion H. eapply eval_CEcond; eauto. simpl in H11. + inversion H. subst. eapply eval_CEcond; eauto. simpl in H12. destruct (eval_condition c vl); try discriminate. - destruct b0; inversion H11; subst v0; subst v; inversion H0; congruence. + destruct b0; inversion H12; subst; inversion H0; congruence. - inversion H. + inversion H. subst. destruct v1; eauto with evalexpr. Qed. Theorem eval_conditionalexpr_true: - forall sp le e1 m1 a1 e2 m2 v1 a2 e3 m3 v2 a3, - eval_expr ge sp le e1 m1 a1 e2 m2 v1 -> + forall sp le e1 m1 a1 t1 e2 m2 v1 t2 a2 e3 m3 v2 a3, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> Val.is_true v1 -> - eval_expr ge sp le e2 m2 a2 e3 m3 v2 -> - eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) e3 m3 v2. + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 -> + eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) (t1**t2) e3 m3 v2. Proof. intros; unfold conditionalexpr. - apply eval_Econdition with e2 m2 true; auto. + apply eval_Econdition with t1 e2 m2 true t2; auto. eapply eval_condition_of_expr; eauto with valboolof. Qed. Theorem eval_conditionalexpr_false: - forall sp le e1 m1 a1 e2 m2 v1 a2 e3 m3 v2 a3, - eval_expr ge sp le e1 m1 a1 e2 m2 v1 -> + forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 a3, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> Val.is_false v1 -> - eval_expr ge sp le e2 m2 a3 e3 m3 v2 -> - eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) e3 m3 v2. + eval_expr ge sp le e2 m2 a3 t2 e3 m3 v2 -> + eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) (t1**t2) e3 m3 v2. Proof. intros; unfold conditionalexpr. - apply eval_Econdition with e2 m2 false; auto. + apply eval_Econdition with t1 e2 m2 false t2; auto. eapply eval_condition_of_expr; eauto with valboolof. Qed. Lemma eval_addressing: - forall sp le e1 m1 a e2 m2 v b ofs, - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall sp le e1 m1 a t e2 m2 v b ofs, + eval_expr ge sp le e1 m1 a t e2 m2 v -> v = Vptr b ofs -> match addressing a with (mode, args) => exists vl, - eval_exprlist ge sp le e1 m1 args e2 m2 vl /\ + eval_exprlist ge sp le e1 m1 args t e2 m2 vl /\ eval_addressing ge sp mode vl = Some v end. Proof. @@ -1080,19 +1129,13 @@ Proof. simpl. auto. InvEval H. exists (@nil val). split. eauto with evalexpr. simpl. auto. - InvEval H. FuncInv. + InvEval H. InvEval EV. rewrite E0_left in TR. subst t1. FuncInv. congruence. - InvEval EV. + destruct (Genv.find_symbol ge s); congruence. exists (Vint i0 :: nil). split. eauto with evalexpr. simpl. subst v. destruct (Genv.find_symbol ge s). congruence. discriminate. InvEval H. FuncInv. - destruct (Genv.find_symbol ge s); congruence. - InvEval EV. - exists (Vint i0 :: nil). split. eauto with evalexpr. - simpl. destruct (Genv.find_symbol ge s). congruence. - discriminate. - InvEval H. FuncInv. congruence. exists (Vptr b0 i :: nil). split. eauto with evalexpr. simpl. congruence. @@ -1108,56 +1151,56 @@ Proof. Qed. Theorem eval_load: - forall sp le e1 m1 a e2 m2 v chunk v', - eval_expr ge sp le e1 m1 a e2 m2 v -> + forall sp le e1 m1 a t e2 m2 v chunk v', + eval_expr ge sp le e1 m1 a t e2 m2 v -> Mem.loadv chunk m2 v = Some v' -> - eval_expr ge sp le e1 m1 (load chunk a) e2 m2 v'. + eval_expr ge sp le e1 m1 (load chunk a) t e2 m2 v'. Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. unfold load. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). destruct (addressing a). intros [vl [EV EQ]]. eapply eval_Eload; eauto. Qed. Theorem eval_store: - forall sp le e1 m1 a1 e2 m2 v1 a2 e3 m3 v2 chunk m4, - eval_expr ge sp le e1 m1 a1 e2 m2 v1 -> - eval_expr ge sp le e2 m2 a2 e3 m3 v2 -> + forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 chunk m4, + eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 -> + eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 -> Mem.storev chunk m3 v1 v2 = Some m4 -> - eval_expr ge sp le e1 m1 (store chunk a1 a2) e3 m4 v2. + eval_expr ge sp le e1 m1 (store chunk a1 a2) (t1**t2) e3 m4 v2. Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). destruct (addressing a1). intros [vl [EV EQ]]. eapply eval_Estore; eauto. Qed. Theorem exec_ifthenelse_true: - forall sp e1 m1 a e2 m2 v ifso ifnot e3 m3 out, - eval_expr ge sp nil e1 m1 a e2 m2 v -> + forall sp e1 m1 a t1 e2 m2 v ifso ifnot t2 e3 m3 out, + eval_expr ge sp nil e1 m1 a t1 e2 m2 v -> Val.is_true v -> - exec_stmt ge sp e2 m2 ifso e3 m3 out -> - exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) e3 m3 out. + exec_stmt ge sp e2 m2 ifso t2 e3 m3 out -> + exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out. Proof. intros. unfold ifthenelse. - apply exec_Sifthenelse with e2 m2 true. + apply exec_Sifthenelse with t1 e2 m2 true t2. eapply eval_condition_of_expr; eauto with valboolof. - auto. + auto. auto. Qed. Theorem exec_ifthenelse_false: - forall sp e1 m1 a e2 m2 v ifso ifnot e3 m3 out, - eval_expr ge sp nil e1 m1 a e2 m2 v -> + forall sp e1 m1 a t1 e2 m2 v ifso ifnot t2 e3 m3 out, + eval_expr ge sp nil e1 m1 a t1 e2 m2 v -> Val.is_false v -> - exec_stmt ge sp e2 m2 ifnot e3 m3 out -> - exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) e3 m3 out. + exec_stmt ge sp e2 m2 ifnot t2 e3 m3 out -> + exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out. Proof. intros. unfold ifthenelse. - apply exec_Sifthenelse with e2 m2 false. + apply exec_Sifthenelse with t1 e2 m2 false t2. eapply eval_condition_of_expr; eauto with valboolof. - auto. + auto. auto. Qed. End CMCONSTR. |