Commit 12b48b38 authored by Heiko Becker's avatar Heiko Becker

Remove last dependencies that were left

parent 5c07cdb7
......@@ -4,7 +4,7 @@ These are used in the soundness proofs since we want to have the final theorem o
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flocq.Core.Fcore_Raux.
(* Require Import Flocq.Core.Fcore_Raux.*)
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
......@@ -153,14 +153,25 @@ Proof.
unfold Q2R, machineEpsilon, RealSimps.machineEpsilon.
unfold RealConstruction.realFromNum, RealConstruction.negativePower.
unfold Qden.
assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
- assert (2^53 = ' (2^53))%Z by auto.
assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H0.
f_equal. unfold IZR. rewrite <- Fcore_Raux.P2R_INR.
unfold Fcore_Raux.P2R. simpl; lra.
- rewrite H.
f_equal. simpl; lra.
- unfold IZR. simpl. lra.
- assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H.
assert (2^53 = ' (2^53))%Z by auto.
rewrite <- H0.
unfold Z.pow.
rewrite (Zpower_pos_is_exp 52 1).
rewrite mult_IZR.
rewrite (Zpower_pos_is_exp 26 26).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 13 13).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 12 1).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 6 6).
repeat rewrite (Zpower_pos_is_exp 3 3).
repeat rewrite mult_IZR. simpl. lra.
Lemma mEps_geq_zero:
Formalization of real valued interval arithmetic
TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Coquelicot.Rcomplements.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
......@@ -338,14 +336,9 @@ Proof.
intros contained_a abs_le; unfold contained in *; simpl in *.
destruct contained_a as [lo_a a_hi].
rewrite Rabs_minus_sym in abs_le.
apply Rcomplements.Rabs_le_between' in abs_le.
destruct abs_le as [lo_le le_hi].
- eapply Rle_trans.
Focus 2. apply lo_le.
repeat rewrite Rsub_eq_Ropp_Rplus.
apply Rplus_le_compat_r; auto.
- eapply Rle_trans.
apply le_hi.
apply Rplus_le_compat_r; auto.
unfold Rabs in abs_le.
destruct Rcase_abs in abs_le.
- rewrite Ropp_minus_distr in abs_le.
split; lra.
- lra.
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