From 95f5db6889237c4ecbac2bf05cfac16c3bd7af56 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Wed, 29 Mar 2017 13:45:04 +0200
Subject: [PATCH] Fix division by zero not being caught in inversion semantics

---
 coq/Expressions.v        | 5 +++--
 coq/IntervalValidation.v | 6 +++---
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/coq/Expressions.v b/coq/Expressions.v
index 3f31d77..aecb5c3 100644
--- a/coq/Expressions.v
+++ b/coq/Expressions.v
@@ -116,6 +116,7 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
 | Unop_inv f1 v1 delta:
     Rle (Rabs delta) eps ->
     eval_exp eps E f1 v1 ->
+    (~ v1 = 0)%R ->
     eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
 | Binop_dist op f1 f2 v1 v2 delta:
     Rle (Rabs delta) eps ->
@@ -164,7 +165,7 @@ Proof.
       subst; auto.
   - rewrite (IHf v0 v3); auto.
   - inversion H3.
-  - inversion H4.
+  - inversion H5.
   - rewrite (IHf v0 v3); auto.
   - rewrite (IHf1 v0 v4); auto.
     rewrite (IHf2 v3 v5); auto.
@@ -216,7 +217,7 @@ Proof.
     inversion H1; subst.
     unfold updEnv in *; simpl in *.
     constructor; auto.
-    inversion H2; subst; auto.
+    inversion H3; subst; auto.
 Qed.
 
 (**
diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v
index 2637dc8..22fa27a 100644
--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -232,7 +232,7 @@ Proof.
       * eapply Rle_trans.
         Focus 2. apply valid_hi.
         rewrite Q2R_opp; lra.
-    + specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H3).
+    + specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H2).
       rewrite absenv_f in IHf; simpl in IHf.
       apply andb_prop_elim in valid_unop.
       destruct valid_unop as [nodiv0 valid_unop].
@@ -273,7 +273,7 @@ Proof.
              hnf; intros is_0.
              assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
              rewrite <- Q2R0_is_0 in nodiv0_pos.
-             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
+             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
          }
          { eapply Rle_trans.
            Focus 2. apply valid_hi.
@@ -298,7 +298,7 @@ Proof.
              hnf; intros is_0.
              assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
              rewrite <- Q2R0_is_0 in nodiv0_pos.
-             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
+             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
          }
   - inversion eval_f; subst.
     rewrite delta_0_deterministic in eval_f; auto.
-- 
GitLab