Commit 95f5db68 authored by Heiko Becker's avatar Heiko Becker

Fix division by zero not being caught in inversion semantics

parent 67e1af47
......@@ -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.
(**
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment