Fix bug in join definition in Coq

coq/ErrorBounds.v

@@ -25,6 +25,7 @@ Proof.
   rewrite Q2R0_is_0; lra.
 Qed.
 
+
 Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
       (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
   eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
@@ -42,8 +43,9 @@ Proof.
   intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion plus_real; subst.
-  destruct m0; destruct m3; inversion H2;
-      simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in plus_real; auto.
   rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
   unfold evalBinop in *; simpl in *.
@@ -109,8 +111,9 @@ Proof.
   intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion sub_real; subst;
-  destruct m0; destruct m3; inversion H2;
-      simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in sub_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -168,8 +171,9 @@ Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion mult_real; subst;
-    destruct m0; destruct m3; inversion H2;
-      simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in mult_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -219,8 +223,9 @@ Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion div_real; subst;
-  destruct m0; destruct m3; inversion H2;
-    simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in div_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.

coq/ErrorValidation.v

@@ -2075,8 +2075,7 @@ Proof.
            end.
     type_conv.
     inversion eval_real; subst.
-    apply M0_join_is_M0 in H2.
-    destruct H2; subst.
+    assert (m2 = M0 /\ m3 = M0) as [? ?] by (split; eapply toRMap_eval_M0; eauto); subst.
     destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars)
       as [[vF1 [mF1 eval_float_e1]] bounded_e1];
       try auto; set_tac.
@@ -2122,7 +2121,7 @@ Proof.
     + intros * eval_float.
       clear eval_float_e1 eval_float_e2.
       inversion eval_float; subst.
-      eapply (binary_unfolding _ H2 H4 H8) in eval_float; try auto.
+      eapply (binary_unfolding _ H4 H5 H9) in eval_float; try auto.
       destruct b.
       * eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
         { simpl.

coq/Expressions.v

@@ -336,6 +336,27 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
   | _ => NatSet.empty
   end.
 
+Lemma toRMap_eval_M0 f v E Gamma m:
+  eval_exp E (toRMap Gamma) (toREval f) v m -> m = M0.
+Proof.
+  revert v E Gamma m.
+  induction f; intros * eval_f; inversion eval_f; subst;
+  repeat
+    match goal with
+    | H: context[toRMap _ _] |- _ => unfold toRMap in H
+    | H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
+    | H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
+    | H: None = Some ?m |- _ => inversion H
+    end; try auto.
+  - eapply IHf; eauto.
+  - eapply IHf; eauto.
+  - assert (m1 = M0)
+      by (eapply IHf1; eauto).
+    assert (m2 = M0)
+      by (eapply IHf2; eauto);
+      subst; auto.
+Qed.
+
 (**
   If |delta| <= 0 then perturb v delta is exactly v.
 **)
@@ -352,8 +373,8 @@ Evaluation with 0 as machine epsilon is deterministic
 **)
 Lemma meps_0_deterministic (f:exp R) (E:env) Gamma:
   forall v1 v2,
-  eval_exp E Gamma (toREval f) v1 M0 ->
-  eval_exp E Gamma (toREval f) v2 M0 ->
+  eval_exp E (toRMap Gamma) (toREval f) v1 M0 ->
+  eval_exp E (toRMap Gamma) (toREval f) v2 M0 ->
   v1 = v2.
 Proof.
   induction f;
@@ -372,8 +393,11 @@ Proof.
       rewrite Q2R0_is_0 in *;
         repeat (rewrite delta_0_deterministic; try auto).
   - inversion ev1; inversion ev2; subst.
-    apply M0_join_is_M0 in H11; apply M0_join_is_M0 in H2.
-    destruct H2, H11; subst.
+    assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+    assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+    assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
+    assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
+    subst.
     rewrite (IHf1 v0 v4); try auto.
     rewrite (IHf2 v3 v5); try auto.
     simpl in *.

coq/Infra/MachineType.v

@@ -133,12 +133,12 @@ Qed.
   has to happen in 64 bits
 **)
 Definition join (m1:mType) (m2:mType) :=
-  if (isMorePrecise m1 m2) then m2 else m1.
-
-Lemma M0_join_is_M0 m1 m2:
-  join m1 m2 = M0 -> m1 = M0 /\ m2 = M0.
-Proof.
-  unfold join.
-  intros.
-  destruct m1, m2; simpl in *; cbv in *; try congruence; try auto.
-Qed.
\ No newline at end of file
+  if (isMorePrecise m1 m2) then m1 else m2.
+
+(* Lemma M0_join_is_M0 m1 m2: *)
+(*   join m1 m2 = M0 -> m1 = M0 /\ m2 = M0. *)
+(* Proof. *)
+(*   unfold join. *)
+(*   intros. *)
+(*   destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
+(* Qed. *)
\ No newline at end of file