Update proofs for FMA

coq/Expressions.v

@@ -102,22 +102,16 @@ Definition teropEq (o1: terop) (o2: terop) :=
   | Fma, Fma => true
   end.
 
-Lemma teropEq_refl b:
-  teropEq b b = true.
+Lemma teropEq_refl t:
+  teropEq t t = true.
 Proof.
-  now destruct b.
+  now destruct t.
 Qed.
 
-Lemma teropEq_compat_eq b1 b2:
-  teropEq b1 b2 = true <-> b1 = b2.
+Lemma teropEq_compat_eq t1 t2:
+  teropEq t1 t2 = true <-> t1 = t2.
 Proof.
-  now destruct b1, b2.
-Qed.
-
-Lemma teropEq_compat_eq_false b1 b2:
-  teropEq b1 b2 = false <-> ~ (b1 = b2).
-Proof.
-  now destruct b1, b2.
+  now destruct t1, t2.
 Qed.
 
 Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) :=
@@ -306,7 +300,15 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -
     eval_exp E Gamma f1 v1 m1 ->
     eval_exp E Gamma f2 v2 m2 ->
     ((op = Div) -> (~ v2 = 0)%R) ->
-    eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta)  (join m1 m2).
+    eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta)  (join m1 m2)
+| Terop_dist m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta:
+    Rle (Rabs delta) (Q2R (mTypeToQ (join3 m1 m2 m3))) ->
+    eval_exp E Gamma f1 v1 m1 ->
+    eval_exp E Gamma f2 v2 m2 ->
+    eval_exp E Gamma f3 v3 m3 ->
+    eval_exp E Gamma (Terop op f1 f2 f3)
+             (perturb (evalTerop op v1 v2 v3) delta)
+             (join3 m1 m2 m3).
 
 Hint Constructors eval_exp.
 
@@ -375,6 +377,20 @@ Qed.
 
 Hint Resolve Binop_dist'.
 
+Lemma Terop_dist' m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta v m' E Gamma:
+  Rle (Rabs delta) (Q2R (mTypeToQ m')) ->
+  eval_exp E Gamma f1 v1 m1 ->
+  eval_exp E Gamma f2 v2 m2 ->
+  eval_exp E Gamma f3 v3 m3 ->
+  v = perturb (evalTerop op v1 v2 v3) delta ->
+  m' = join3 m1 m2 m3 ->
+  eval_exp E Gamma (Terop op f1 f2 f3) v m'.
+Proof.
+  intros; subst; auto.
+Qed.
+
+Hint Resolve Terop_dist'.
+
 (**
   Define the set of "used" variables of an expression to be the set of variables
   occuring in it
@@ -384,6 +400,7 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
   | Var _ x => NatSet.singleton x
   | Unop u e1 => usedVars e1
   | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
+  | Terop t e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3))
   | Downcast _ e1 => usedVars e1
   | _ => NatSet.empty
   end.
@@ -407,6 +424,13 @@ Proof.
     assert (m2 = M0)
       by (eapply IHf2; eauto);
       subst; auto.
+  - assert (m1 = M0)
+      by (eapply IHf1; eauto).
+    assert (m2 = M0)
+      by (eapply IHf2; eauto).
+    assert (m3 = M0)
+      by (eapply IHf3; eauto);
+      subst; auto.
 Qed.
 
 (**
@@ -455,6 +479,20 @@ Proof.
     simpl in *.
     rewrite Q2R0_is_0 in *.
     repeat (rewrite delta_0_deterministic; try auto).
+  - inversion ev1; inversion ev2; subst.
+    assert (m0 = 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).
+    assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
+    assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
+    assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
+    subst.
+    rewrite (IHf1 v0 v5); try auto.
+    rewrite (IHf2 v3 v6); try auto.
+    rewrite (IHf3 v4 v7); try auto.
+    simpl in *.
+    rewrite Q2R0_is_0 in *.
+    repeat (rewrite delta_0_deterministic; try auto).
   - inversion ev1; inversion ev2; subst.
     apply M0_least_precision in H1;
       apply M0_least_precision in H7; subst.

coq/Infra/MachineType.v

@@ -138,6 +138,9 @@ Qed.
 Definition join (m1:mType) (m2:mType) :=
   if (isMorePrecise m1 m2) then m1 else m2.
 
+Definition join3 (m1:mType) (m2:mType) (m3:mType) :=
+  join m1 (join m2 m3).
+
 (* Lemma M0_join_is_M0 m1 m2: *)
 (*   join m1 m2 = M0 -> m1 = M0 /\ m2 = M0. *)
 (* Proof. *)