Fix proofs broken by new syntax for option bindings

coq/IEEE_connection.v

@@ -506,17 +506,19 @@ Proof.
                      fVars_defined vars_typed dVars_sound dVars_valid
                      usedVars_64bit;
     (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
+     revert eval_IEEE_valid_e;
      Flover_compute_asm; try congruence; type_conv; subst;
-     unfold optionBind.
-  - unfold toREnv in *.
+     unfold optionBind;
+     intros eval_IEEE_valid_e.
+     - unfold toREnv in *.
     destruct (E2 n) eqn:HE2; try congruence.
     exists f; split; try eauto.
     eapply Var_load; try auto. rewrite HE2; auto.
-  - eexists; split; try eauto.
+     - eexists; split; try eauto.
     eapply (Const_dist') with (delta:=0%R); eauto.
     + rewrite Rabs_R0; apply mTypeToR_pos_R.
     + unfold perturb. lra.
-  - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
+     - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
     assert (is_finite 53 1024 v_e = true).
     { apply validValue_is_finite.
       eapply FPRangeValidator_sound; eauto.
@@ -527,17 +529,17 @@ Proof.
     rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
     eapply Unop_neg'; eauto.
     unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
-  - repeat (match goal with
+     - repeat (match goal with
             |H: _ /\ _ |- _ => destruct H
             end).
-    assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
+       assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
             FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
             FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
            as [tMap_e1 [tMap_e2 tMap_b]].
     { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
-      - rewrite Heqo1, Heqo6, Heqo8.
+      - rewrite Heqo, Heqo4, Heqo6.
         apply Is_true_eq_true; apply andb_prop_intro; split.
         + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
           apply mTypeEq_refl.
@@ -556,10 +558,11 @@ Proof.
       as [v_e2 [eval_float_e2 eval_rel_e2]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    (* rewrite eval_float_e1, eval_float_e2. *)
     edestruct (validIntervalbounds_sound (B2Qexpr e2))
       as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
       eauto; set_tac.
+    rewrite eval_float_e1, eval_float_e2.
+    inversion Heqo1; subst.
     destr_factorize.
     destruct iv_2 as [ivlo_2 ivhi_2].
     assert (forall vF2 m2,
@@ -599,13 +602,13 @@ Proof.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
         apply andb_prop_intro; split; auto using Is_true_eq_left.
-      - inversion Heqo3; subst. Flover_compute.
+      - Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
-        apply Is_true_eq_left. inversion Heqo4; subst. auto.
-      - rewrite Heqo1, Heqo2.
+        apply Is_true_eq_left. inversion Heqo2; subst. auto.
+      - rewrite Heqo, Heqo0.
         apply Is_true_eq_true.
-        inversion Heqo3; inversion Heqo4; subst.
+        inversion Heqo1; inversion Heqo2; subst.
         repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
     assert (validFloatValue (Q2R (B2Q v_e1)) M64).
     { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
@@ -636,11 +639,11 @@ Proof.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
       - cbn. Flover_compute.
-        inversion Heqo3; inversion Heqo4; subst.
+        inversion Heqo1; inversion Heqo2; subst.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
       - cbn. Flover_compute.
-        inversion Heqo3; inversion Heqo4; subst.
+        inversion Heqo1; inversion Heqo2; subst.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
     assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
@@ -667,30 +670,33 @@ Proof.
     pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                     (-1022)%Z 53%Z expr_valid)
       as rel_error_exists.
-    (* rewrite eval_float_e1, eval_float_e2 in H1. *)
+    rewrite eval_float_e1, eval_float_e2 in H1.
     unfold optionBind, normal_or_zero in *; simpl in *.
     assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
             (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
-    { revert H1; intros case_val. destruct case_val; try auto.
+    { revert H1; intros case_val.
+      destruct case_val as [eval_is_zero | eval_normal]; try auto.
       left; unfold Normal, Denormal in H15; unfold Normal;
         destruct H15 as [normal_b | [denormal_b |zero_b]].
       - repeat rewrite <- B2Q_B2R_eq; try auto.
       - destruct denormal_b.
         assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
-        { eapply Rlt_le_trans with (r2 := 0); eauto.
+        { eapply Rlt_le_trans; eauto.
           repeat rewrite B2Q_B2R_eq; auto. }
         lra.
       - rewrite B2Q_B2R_eq in zero_b; auto.
         rewrite B2Q_B2R_eq in zero_b; auto.
         rewrite zero_b in *.
-        rewrite Rabs_R0 in H1.
-        unfold minValue_pos, minExponentPos in H1.
-        rewrite Q2R_inv in H1; [|vm_compute; congruence].
-        unfold Q2R, Qnum, Qden in H1.
+        rewrite Rabs_R0 in eval_normal.
+        unfold minValue_pos, minExponentPos in eval_normal.
+        rewrite Q2R_inv in eval_normal; [|vm_compute; congruence].
+        unfold Q2R, Qnum, Qden in eval_normal.
         assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
           by (vm_compute; auto).
-        rewrite H2 in H1. rewrite <- Z2R_IZR in H1.  unfold IZR in H1.
-        simpl in H1. rewrite <- INR_IPR in H1. simpl in H1. lra. }
+        rewrite H1 in eval_normal. rewrite <- Z2R_IZR in eval_normal.
+        unfold IZR in eval_normal.
+        simpl in eval_normal. rewrite <- INR_IPR in eval_normal.
+        simpl in eval_normal. lra. }
     pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
     destruct b; revert H1; intros case_eval.
     (* Addition *)
@@ -929,7 +935,10 @@ Proof.
                      freeVars_sound is64_eval nodowncast_f bstep_sound
                      dVars_sound fVars_defined vars_typed dVars_valid
                      freeVars_typed;
-    cbn in *; Flover_compute_asm; try congruence; type_conv; subst;
+    cbn in *;
+    revert bstep_sound;
+    Flover_compute_asm; try congruence; type_conv; subst;
+      intros bstep_sound;
       unfold Ltacs.optionBind;
       inversion bstep_float; inversion bstep_real;
       inversion ssa_f; subst; simpl in *;

coq/Infra/Ltacs.v

@@ -88,8 +88,12 @@ Qed.
 
 Ltac remove_matches := rewrite optionBind_eq in *.
 
+Ltac remove_matches_asm := rewrite optionBind_eq in * |- .
+
 Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
 
+Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
+
 Ltac match_factorize_asm :=
   match goal with
   | [ H: ?t = ?u |- context [optionBind ?t _ _]]
@@ -133,8 +137,8 @@ Ltac bool_factorize :=
 
 Ltac Flover_compute_asm :=
   repeat (
-      (try remove_conds;
-       try remove_matches;
+      (try remove_conds_asm;
+       try remove_matches_asm;
        repeat match_factorize_asm;
        try pair_factorize) ||
       bool_factorize).