Fix merge errors in IEEE_connection

coq/IEEE_connection.v

@@ -317,23 +317,14 @@ Proof.
   - repeat (match goal with
             |H: _ /\ _ |- _=> destruct H
             end).
-    destruct (tMap (Fma e1 e2 e3)) eqn:?; try congruence;
-      erewrite IHe1 in *; eauto.
-    + erewrite IHe2 in *; eauto.
-      * unfold join3, join in typecheck_e.
-        erewrite IHe3 in *; eauto.
-        ++ rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
-          type_conv; subst; auto.
-        ++ destruct (tMap e3); try congruence.
-           andb_to_prop typecheck_e; eauto.
-        ++ intros; apply types_valid. set_tac.
-      * destruct (tMap e2); destruct (tMap e3); try congruence.
-        andb_to_prop typecheck_e; eauto.
-      * intros.
-        apply types_valid. set_tac.
-    + destruct (tMap e1); destruct (tMap e2); destruct (tMap e3); try congruence;
-        andb_to_prop typecheck_e; eauto.
-    + intros; apply types_valid; set_tac.
+    erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail).
+    erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail).
+    unfold join3, join in *.
+    erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail).
+    repeat destr_factorize.
+    repeat rewrite <- isMorePrecise_morePrecise.
+    repeat rewrite isMorePrecise_refl;
+      type_conv; subst; auto.
 Qed.
 
 Lemma typing_cmd_64_bit f:
@@ -374,22 +365,12 @@ Proof.
       Daisy_compute; try congruence; type_conv; subst; try auto.
   - eapply IHe; eauto.
   - eapply IHe; eauto.
-  - assert (m0 = m).
-    { eapply IHe1; eauto. }
-    assert (m3 = m1).
-    { eapply IHe2; eauto. }
+  - assert (m0 = m) by eauto using IHe1.
+    assert (m3 = m1) by eauto using IHe2.
     subst; auto.
-  - destruct (tMap e1) eqn:?; try congruence;
-      destruct (tMap e2) eqn:?; try congruence;
-      destruct (tMap e3) eqn:?; try congruence.
-    andb_to_prop typeCheck_e.
-    type_conv; subst.
-    assert (m0 = m).
-    { eapply IHe1; eauto. }
-    assert (m3 = m1).
-    { eapply IHe2; eauto. }
-    assert (m4 = m5).
-    { eapply IHe3; eauto. }
+  - assert (m0 = m) by eauto using IHe1.
+    assert (m3 = m1) by eauto using IHe2.
+    assert (m4 = m5) by eauto using IHe3.
     subst; auto.
 Qed.
 
@@ -917,21 +898,16 @@ Proof.
   - repeat (match goal with
             |H: _ /\ _ |- _ => destruct H
             end).
-    destruct (tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?; try congruence;
-      destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
-      destruct (tMap (B2Qexp e2)) eqn:?; try congruence;
-      destruct (tMap (B2Qexp e3)) eqn:?; try congruence.
-    andb_to_prop typecheck_e; type_conv; subst.
-    assert (tMap (B2Qexp e1) = Some M64 /\
-            tMap (B2Qexp e2) = Some M64 /\
-            tMap (B2Qexp e3) = Some M64 /\
-            tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) = Some M64)
+    assert (DaisyMap.find (B2Qexp e1) tMap = Some M64 /\
+            DaisyMap.find (B2Qexp e2) tMap = Some M64 /\
+            DaisyMap.find (B2Qexp e3) tMap = Some M64 /\
+            DaisyMap.find (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) tMap = Some M64)
            as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
     { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
-      - rewrite Heqo, Heqo0, Heqo1, Heqo2.
+      - rewrite Heqo, Heqo4, Heqo6, Heqo8.
         apply Is_true_eq_true; apply andb_prop_intro; split.
         + apply andb_prop_intro; split.
           * apply andb_prop_intro; split.
@@ -940,7 +916,7 @@ Proof.
             ++ apply Is_true_eq_left; auto.
           * apply Is_true_eq_left; auto.
         + apply Is_true_eq_left; auto. }
-    rewrite tMap_e1, tMap_e2, tMap_e3, tMap_fma in *.
+    repeat destr_factorize.
     inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
     assert (m1 = M64).
     { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
@@ -949,14 +925,6 @@ Proof.
     assert (m3 = M64).
     { eapply (typing_agrees_exp (B2Qexp e3)); eauto. }
     subst.
-    destruct (A (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?;
-             destruct (A (B2Qexp e1)) eqn:?;
-             destruct (A (B2Qexp e2)) eqn:?;
-             destruct (A (B2Qexp e3)) eqn:?;
-             simpl in *.
-    repeat (match goal with
-            |H: _ = true |- _ => andb_to_prop H
-            end).
     destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
       as [v_e1 [eval_float_e1 eval_rel_e1]];
       try auto; try set_tac;