Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
AVA
FloVer
Commits
d5db0675
Commit
d5db0675
authored
Oct 31, 2016
by
Heiko Becker
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Start working on Division, simplify proofs adding Ltac for is_true automation
parent
aa2cc910
Changes
9
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
191 additions
and
235 deletions
+191
-235
coq/ErrorBounds.v
coq/ErrorBounds.v
+5
-5
coq/ErrorValidation.v
coq/ErrorValidation.v
+49
-126
coq/Expressions.v
coq/Expressions.v
+41
-40
coq/Infra/Ltacs.v
coq/Infra/Ltacs.v
+27
-0
coq/Infra/RationalSimps.v
coq/Infra/RationalSimps.v
+14
-39
coq/Infra/RealConstruction.v
coq/Infra/RealConstruction.v
+0
-8
coq/Infra/RealRationalProps.v
coq/Infra/RealRationalProps.v
+51
-12
coq/Infra/RealSimps.v
coq/Infra/RealSimps.v
+2
-3
coq/IntervalValidation.v
coq/IntervalValidation.v
+2
-2
No files found.
coq/ErrorBounds.v
View file @
d5db0675
...
...
@@ -52,8 +52,8 @@ Proof.
(
*
Prove
that
e1R
and
e2R
are
the
correct
values
and
that
vR
is
e1R
+
e2R
*
)
inversion
plus_real
;
subst
.
rewrite
delta_0_deterministic
in
plus_real
;
auto
.
rewrite
(
delta_0_deterministic
(
eval
_b
inop
Plus
v1
v2
)
delta
);
auto
.
unfold
eval
_b
inop
in
*
;
simpl
in
*
.
rewrite
(
delta_0_deterministic
(
eval
B
inop
Plus
v1
v2
)
delta
);
auto
.
unfold
eval
B
inop
in
*
;
simpl
in
*
.
clear
delta
H2
.
rewrite
(
meps_0_deterministic
H4
e1_real
);
rewrite
(
meps_0_deterministic
H5
e2_real
).
...
...
@@ -112,7 +112,7 @@ Proof.
inversion
sub_real
;
subst
.
rewrite
delta_0_deterministic
in
sub_real
;
auto
.
rewrite
delta_0_deterministic
;
auto
.
unfold
eval
_b
inop
in
*
;
simpl
in
*
.
unfold
eval
B
inop
in
*
;
simpl
in
*
.
clear
delta
H2
.
rewrite
(
meps_0_deterministic
H4
e1_real
);
rewrite
(
meps_0_deterministic
H5
e2_real
).
...
...
@@ -162,7 +162,7 @@ Proof.
inversion
mult_real
;
subst
.
rewrite
delta_0_deterministic
in
mult_real
;
auto
.
rewrite
delta_0_deterministic
;
auto
.
unfold
eval
_b
inop
in
*
;
simpl
in
*
.
unfold
eval
B
inop
in
*
;
simpl
in
*
.
clear
delta
H2
.
rewrite
(
meps_0_deterministic
H4
e1_real
);
rewrite
(
meps_0_deterministic
H5
e2_real
).
...
...
@@ -206,7 +206,7 @@ Proof.
inversion
div_real
;
subst
.
rewrite
delta_0_deterministic
in
div_real
;
auto
.
rewrite
delta_0_deterministic
;
auto
.
unfold
eval
_b
inop
in
*
;
simpl
in
*
.
unfold
eval
B
inop
in
*
;
simpl
in
*
.
clear
delta
H2
.
rewrite
(
meps_0_deterministic
H4
e1_real
);
rewrite
(
meps_0_deterministic
H5
e2_real
).
...
...
coq/ErrorValidation.v
View file @
d5db0675
...
...
@@ -9,8 +9,8 @@
Require
Import
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qminmax
Coq
.
QArith
.
Qabs
Coq
.
QArith
.
Qreals
Coq
.
Lists
.
List
.
Require
Import
Coq
.
micromega
.
Psatz
Coq
.
Reals
.
Reals
.
Require
Import
Daisy
.
Infra
.
Abbrevs
Daisy
.
Infra
.
RationalSimps
Daisy
.
Infra
.
RealRationalProps
Daisy
.
Infra
.
RealSimps
.
Require
Import
Daisy
.
Infra
.
ExpressionAbbrevs
Daisy
.
IntervalArith
Daisy
.
IntervalArithQ
.
Require
Import
Daisy
.
ErrorBounds
Daisy
.
IntervalValidation
.
Require
Import
Daisy
.
Infra
.
Ltacs
Daisy
.
Infra
.
ExpressionAbbrevs
.
Require
Import
Daisy
.
IntervalArith
Daisy
.
IntervalArithQ
Daisy
.
ErrorBounds
Daisy
.
IntervalValidation
.
(
**
Error
bound
validator
**
)
Fixpoint
validErrorbound
(
e
:
exp
Q
)
(
env
:
analysisResult
)
:=
...
...
@@ -38,10 +38,9 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
(
andb
(
Qleb
(
ivhi
errIve2
)
0
)
(
negb
(
Qeq_bool
(
ivhi
errIve2
)
0
)))
(
andb
(
Qleb
0
(
ivlo
errIve2
))
(
negb
(
Qeq_bool
(
ivlo
errIve2
)
0
)))
in
if
nodiv0_fl
then
Qleb
((
maxAbs
(
subtractIntv
(
divideIntv
ive1
ive2
)
(
divideIntv
errIve1
errIve2
)))
+
(
maxAbs
(
divideIntv
errIve1
errIve2
))
*
RationalSimps
.
machineEpsilon
)
err
then
let
minAbsIve2
:=
minAbs
(
errIve2
)
in
let
errInv
:=
(
1
/
(
minAbsIve2
*
minAbsIve2
))
*
err2
in
Qleb
((
upperBoundE1
*
errInv
+
upperBoundE2
*
err1
+
err1
*
errInv
)
+
(
maxAbs
(
divideIntv
errIve1
errIve2
))
*
RationalSimps
.
machineEpsilon
)
err
else
false
end
in
andb
(
andb
rec
errPos
)
theVal
...
...
@@ -61,25 +60,14 @@ Proof.
unfold
validErrorbound
in
validErrorbound_e
;
rewrite
<-
absenv_e
in
validErrorbound_e
;
simpl
in
*
.
-
inversion
validErrorbound_e
.
-
apply
Is_true_eq_left
in
validErrorbound_e
.
apply
andb_prop_elim
in
validErrorbound_e
.
destruct
validErrorbound_e
as
[
hyp
_
].
apply
Is_true_eq_true
in
hyp
.
apply
Qle_bool_iff
in
hyp
;
apply
Qle_Rle
in
hyp
;
rewrite
Q2R0_is_0
in
hyp
;
auto
.
-
apply
Is_true_eq_left
in
validErrorbound_e
.
apply
andb_prop_elim
in
validErrorbound_e
.
destruct
validErrorbound_e
as
[
hyp
_
].
apply
Is_true_eq_true
in
hyp
.
apply
Qle_bool_iff
in
hyp
;
apply
Qle_Rle
in
hyp
;
rewrite
Q2R0_is_0
in
hyp
;
auto
.
-
andb_to_prop
validErrorbound_e
.
apply
Qle_bool_iff
in
L
;
apply
Qle_Rle
in
L
;
rewrite
Q2R0_is_0
in
L
;
auto
.
-
andb_to_prop
validErrorbound_e
.
apply
Qle_bool_iff
in
L
;
apply
Qle_Rle
in
L
;
rewrite
Q2R0_is_0
in
L
;
auto
.
-
inversion
validErrorbound_e
.
-
destruct
(
absenv
e1
).
destruct
(
absenv
e2
).
apply
Is_true_eq_left
in
validErrorbound_e
.
apply
andb_prop_elim
in
validErrorbound_e
.
destruct
validErrorbound_e
as
[
hyp
_
].
apply
andb_prop_elim
in
hyp
.
destruct
hyp
as
[
_
hyp
].
apply
Is_true_eq_true
in
hyp
.
apply
Qle_bool_iff
in
hyp
;
apply
Qle_Rle
in
hyp
;
rewrite
Q2R0_is_0
in
hyp
;
auto
.
andb_to_prop
validErrorbound_e
.
apply
Qle_bool_iff
in
R0
;
apply
Qle_Rle
in
R0
;
rewrite
Q2R0_is_0
in
R0
;
auto
.
Qed
.
Lemma
validErrorboundCorrectConstant
:
...
...
@@ -102,10 +90,8 @@ Proof.
unfold
perturb
in
*
;
simpl
in
*
.
rewrite
Rabs_err_simpl
.
unfold
Qleb
in
error_valid
.
apply
Is_true_eq_left
in
error_valid
.
apply
andb_prop_elim
in
error_valid
.
destruct
error_valid
as
[
_
error_valid
].
apply
Is_true_eq_true
in
error_valid
.
andb_to_prop
error_valid
.
rename
R
into
error_valid
.
apply
Qle_bool_iff
in
error_valid
.
apply
Qle_Rle
in
error_valid
.
eapply
Rle_trans
.
...
...
@@ -123,10 +109,9 @@ Proof.
rewrite
<-
Qle_bool_iff
;
auto
.
rewrite
absenv_const
in
intv_valid
.
simpl
in
intv_valid
.
apply
Is_true_eq_left
in
intv_valid
.
apply
andb_prop_elim
in
intv_valid
.
destruct
intv_valid
as
[
valid_lo
valid_hi
];
unfold
Is_true
in
*
.
Focus
2.
apply
error_valid
.
andb_to_prop
intv_valid
.
Focus
2.
apply
error_valid
.
rewrite
<-
Rabs_eq_Qabs
.
rewrite
<-
maxAbs_impl_RmaxAbs
.
apply
RmaxAbs
;
simpl
;
apply
Qle_Rle
;
rewrite
<-
Qle_bool_iff
;
unfold
Qleb
in
*
;
simpl
in
*
;
...
...
@@ -182,10 +167,8 @@ Proof.
unfold
RmaxAbsFun
in
H5
.
simpl
in
H5
.
rewrite
H5
.
apply
Is_true_eq_left
in
error_valid
.
apply
andb_prop_elim
in
error_valid
.
destruct
error_valid
as
[
_
error_valid
].
apply
Is_true_eq_true
in
error_valid
.
andb_to_prop
error_valid
.
rename
R
into
error_valid
.
apply
Qle_bool_iff
in
error_valid
.
apply
Qle_Rle
in
error_valid
.
rewrite
Q2R_mult
in
error_valid
.
...
...
@@ -226,25 +209,13 @@ Proof.
rewrite
<-
mEps_eq_Rmeps
.
unfold
validErrorbound
in
valid_error
at
1.
rewrite
absenv_add
,
absenv_e1
,
absenv_e2
in
valid_error
.
apply
Is_true_eq_left
in
valid_error
.
apply
andb_prop_elim
in
valid_error
.
destruct
valid_error
as
[
valid_rec
valid_error
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_rec
err_pos
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_e1
valid_e2
].
apply
Is_true_eq_true
in
valid_error
.
apply
Qle_bool_iff
in
valid_error
.
apply
Qle_Rle
in
valid_error
.
andb_to_prop
valid_error
.
rename
R
into
valid_error
.
eapply
Rle_trans
.
apply
Rplus_le_compat_l
.
eapply
Rmult_le_compat_r
.
apply
mEps_geq_zero
.
Focus
2.
apply
Rle_Qle
in
valid_error
.
rewrite
<-
Qle_bool_iff
in
valid_error
.
apply
Is_true_eq_left
in
valid_error
.
apply
Is_true_eq_true
in
valid_error
.
rewrite
Qle_bool_iff
in
valid_error
.
apply
Qle_Rle
in
valid_error
.
repeat
rewrite
Q2R_plus
in
valid_error
.
...
...
@@ -254,15 +225,10 @@ Proof.
repeat
rewrite
Q2R_plus
in
valid_error
.
repeat
rewrite
<-
maxAbs_impl_RmaxAbs
in
valid_error
.
apply
valid_error
.
clear
valid_e1
valid_e2
.
clear
L
R1
.
simpl
in
valid_intv
.
rewrite
absenv_add
,
absenv_e1
,
absenv_e2
in
valid_intv
.
apply
Is_true_eq_left
in
valid_intv
.
apply
andb_prop_elim
in
valid_intv
.
destruct
valid_intv
as
[
valid_rec
valid_intv
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_iv_e1
valid_iv_e2
].
apply
Is_true_eq_true
in
valid_iv_e1
;
apply
Is_true_eq_true
in
valid_iv_e2
.
andb_to_prop
valid_intv
.
remember
(
addIntv
(
widenIntv
(
e1lo
,
e1hi
)
err1
)
(
widenIntv
(
e2lo
,
e2hi
)
err2
))
as
iv
.
iv_assert
iv
iv_unf
.
destruct
iv_unf
as
[
ivl
[
ivh
iv_unf
]].
...
...
@@ -271,11 +237,11 @@ Proof.
assert
(
ivlo
iv
=
ivl
)
by
(
rewrite
iv_unf
;
auto
).
assert
(
ivhi
iv
=
ivh
)
by
(
rewrite
iv_unf
;
auto
).
rewrite
<-
H
,
<-
H0
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e1
e1_real
)
as
valid_bounds_e1
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
L0
e1_real
)
as
valid_bounds_e1
.
rewrite
absenv_e1
in
valid_bounds_e1
.
simpl
in
valid_bounds_e1
.
pose
proof
(
distance_gives_iv
nR1
nF1
(
Q2R
err1
)
(
Q2R
e1lo
,
Q2R
e1hi
)
valid_bounds_e1
err1_bounded
).
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e2
e2_real
)
as
valid_bounds_e2
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
R1
e2_real
)
as
valid_bounds_e2
.
rewrite
absenv_e2
in
valid_bounds_e2
.
simpl
in
valid_bounds_e2
.
pose
proof
(
distance_gives_iv
nR2
nF2
(
Q2R
err2
)
(
Q2R
e2lo
,
Q2R
e2hi
)
valid_bounds_e2
err2_bounded
).
...
...
@@ -328,12 +294,8 @@ Proof.
rewrite
<-
mEps_eq_Rmeps
.
unfold
validErrorbound
in
valid_error
at
1.
rewrite
absenv_sub
,
absenv_e1
,
absenv_e2
in
valid_error
.
apply
Is_true_eq_left
in
valid_error
.
apply
andb_prop_elim
in
valid_error
.
destruct
valid_error
as
[
valid_rec
valid_error
].
apply
andb_prop_elim
in
valid_rec
.
clear
valid_rec
.
apply
Is_true_eq_true
in
valid_error
.
andb_to_prop
valid_error
.
rename
R
into
valid_error
.
apply
Qle_bool_iff
in
valid_error
.
apply
Qle_Rle
in
valid_error
.
repeat
rewrite
Q2R_plus
in
valid_error
.
...
...
@@ -348,12 +310,7 @@ Proof.
apply
mEps_geq_zero
.
simpl
in
valid_intv
.
rewrite
absenv_sub
,
absenv_e1
,
absenv_e2
in
valid_intv
.
apply
Is_true_eq_left
in
valid_intv
.
apply
andb_prop_elim
in
valid_intv
.
destruct
valid_intv
as
[
valid_rec
valid_intv
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_iv_e1
valid_iv_e2
].
apply
Is_true_eq_true
in
valid_iv_e1
;
apply
Is_true_eq_true
in
valid_iv_e2
.
andb_to_prop
valid_intv
.
Focus
2.
apply
valid_error
.
remember
(
subtractIntv
(
widenIntv
(
e1lo
,
e1hi
)
err1
)
(
widenIntv
(
e2lo
,
e2hi
)
err2
))
as
iv
.
...
...
@@ -364,11 +321,11 @@ Proof.
assert
(
ivlo
iv
=
ivl
)
by
(
rewrite
iv_unf
;
auto
).
assert
(
ivhi
iv
=
ivh
)
by
(
rewrite
iv_unf
;
auto
).
rewrite
<-
H
,
<-
H0
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e
1
e1_real
)
as
valid_bounds_e1
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
L
1
e1_real
)
as
valid_bounds_e1
.
rewrite
absenv_e1
in
valid_bounds_e1
.
simpl
in
valid_bounds_e1
.
pose
proof
(
distance_gives_iv
nR1
nF1
(
Q2R
err1
)
(
Q2R
e1lo
,
Q2R
e1hi
)
valid_bounds_e1
err1_bounded
).
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e
2
e2_real
)
as
valid_bounds_e2
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
R
2
e2_real
)
as
valid_bounds_e2
.
rewrite
absenv_e2
in
valid_bounds_e2
.
simpl
in
valid_bounds_e2
.
pose
proof
(
distance_gives_iv
nR2
nF2
(
Q2R
err2
)
(
Q2R
e2lo
,
Q2R
e2hi
)
valid_bounds_e2
err2_bounded
).
...
...
@@ -391,18 +348,6 @@ Proof.
repeat
rewrite
Q2R_minus
;
auto
.
Qed
.
(
**
Tactic
to
simplify
multiplication
bound
proof
.
Used
to
obtain
similarly
shaped
terms
in
every
subgoal
.
Thus
automation
can
then
be
applied
to
solve
it
**
)
Ltac
math_hnf
:=
repeat
rewrite
Rsub_eq_Ropp_Rplus
;
repeat
rewrite
Ropp_plus_distr
;
repeat
rewrite
Rmult_plus_distr_r
;
repeat
rewrite
Rmult_plus_distr_l
;
repeat
rewrite
Ropp_involutive
;
repeat
rewrite
<-
Rplus_assoc
.
Lemma
validErrorboundCorrectMult
cenv
absenv
(
e1
:
exp
Q
)
(
e2
:
exp
Q
)
(
nR
nR1
nR2
nF
nF1
nF2
:
R
)
(
e
err1
err2
:
error
)
(
alo
ahi
e1lo
e1hi
e2lo
e2hi
:
Q
)
P
:
precondValidForExec
P
cenv
->
eval_exp
0
%
R
cenv
(
toRExp
e1
)
nR1
->
...
...
@@ -435,19 +380,11 @@ Proof.
rewrite
<-
mEps_eq_Rmeps
.
unfold
validErrorbound
in
valid_error
at
1.
rewrite
absenv_mult
,
absenv_e1
,
absenv_e2
in
valid_error
.
apply
Is_true_eq_left
in
valid_error
.
apply
andb_prop_elim
in
valid_error
.
destruct
valid_error
as
[
valid_rec
valid_error
].
apply
andb_prop_elim
in
valid_rec
.
apply
Is_true_eq_true
in
valid_error
.
destruct
valid_rec
as
[
valid_rec
le_0_e
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_err1
valid_err2
].
apply
Is_true_eq_true
in
valid_err1
.
apply
Is_true_eq_true
in
valid_err2
.
andb_to_prop
valid_error
.
rename
R
into
valid_error
.
assert
(
0
<=
Q2R
err1
)
%
R
as
err1_pos
by
(
apply
(
err_always_positive
e1
absenv
(
e1lo
,
e1hi
)
err1
);
auto
).
assert
(
0
<=
Q2R
err2
)
%
R
as
err2_pos
by
(
apply
(
err_always_positive
e2
absenv
(
e2lo
,
e2hi
)
err2
);
auto
).
clear
valid_err1
valid_err2
.
clear
R1
L
.
apply
Qle_bool_iff
in
valid_error
.
apply
Qle_Rle
in
valid_error
.
repeat
rewrite
Q2R_plus
in
valid_error
.
...
...
@@ -462,14 +399,9 @@ Proof.
(
*
Simplify
Interval
correctness
assumption
*
)
simpl
in
valid_intv
.
rewrite
absenv_mult
,
absenv_e1
,
absenv_e2
in
valid_intv
.
apply
Is_true_eq_left
in
valid_intv
.
apply
andb_prop_elim
in
valid_intv
.
destruct
valid_intv
as
[
valid_rec
valid_intv
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_iv_e1
valid_iv_e2
].
apply
Is_true_eq_true
in
valid_iv_e1
;
apply
Is_true_eq_true
in
valid_iv_e2
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e1
e1_real
)
as
valid_e1
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e2
e2_real
)
as
valid_e2
.
andb_to_prop
valid_intv
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
L0
e1_real
)
as
valid_e1
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
R1
e2_real
)
as
valid_e2
.
apply
Rplus_le_compat
.
-
unfold
Rabs
in
err1_bounded
.
unfold
Rabs
in
err2_bounded
.
...
...
@@ -1016,11 +948,11 @@ Proof.
assert
(
ivlo
iv
=
ivl
)
by
(
rewrite
iv_unf
;
auto
).
assert
(
ivhi
iv
=
ivh
)
by
(
rewrite
iv_unf
;
auto
).
rewrite
<-
H
,
<-
H0
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e1
e1_real
)
as
valid_bounds_e1
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
L0
e1_real
)
as
valid_bounds_e1
.
rewrite
absenv_e1
in
valid_bounds_e1
.
simpl
in
valid_bounds_e1
.
pose
proof
(
distance_gives_iv
nR1
nF1
(
Q2R
err1
)
(
Q2R
e1lo
,
Q2R
e1hi
)
valid_bounds_e1
err1_bounded
).
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
valid_iv_e2
e2_real
)
as
valid_bounds_e2
.
pose
proof
(
validIntervalbounds_sound
_
_
_
_
_
p_valid
R1
e2_real
)
as
valid_bounds_e2
.
rewrite
absenv_e2
in
valid_bounds_e2
.
simpl
in
valid_bounds_e2
.
pose
proof
(
distance_gives_iv
nR2
nF2
(
Q2R
err2
)
(
Q2R
e2lo
,
Q2R
e2hi
)
valid_bounds_e2
err2_bounded
).
...
...
@@ -1062,7 +994,10 @@ Proof.
valid_error
valid_intv
absenv_e1
absenv_e2
absenv_div
err1_bounded
err2_bounded
.
pose
proof
(
ivbounds_approximatesPrecond_sound
(
Binop
Div
e1
e2
)
absenv
P
valid_intv
)
as
env_approx_p
.
eapply
Rle_trans
.
admit
.
Admitted
.
(
*
eapply
Rle_trans
.
eapply
(
div_abs_err_bounded
(
toRExp
e1
)
_
_
(
toRExp
e2
));
eauto
.
rewrite
<-
mEps_eq_Rmeps
.
apply
e1_float
.
...
...
@@ -1227,7 +1162,7 @@ Proof.
apply
Qle_Rle
in
H1
.
lra
.
}
+
rewrite
H
;
auto
.
}
Qed
.
Qed
.
*
)
(
**
Soundness
theorem
for
the
error
bound
validator
.
...
...
@@ -1267,26 +1202,10 @@ Proof.
destruct
iv_e2
as
[
ivlo2
[
ivhi2
iv_e2
]].
rewrite
iv_e2
in
absenv_e2
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
in
valid_error
.
apply
Is_true_eq_left
in
valid_error
.
apply
andb_prop_elim
in
valid_error
.
destruct
valid_error
as
[
valid_rec
valid_error
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_rec
le_0_e
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_err_e1
valid_err_e2
].
apply
Is_true_eq_true
in
valid_err_e1
;
apply
Is_true_eq_true
in
valid_err_e2
.
apply
Is_true_eq_true
in
valid_error
.
andb_to_prop
valid_error
.
simpl
in
valid_intv
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
in
valid_intv
.
apply
Is_true_eq_left
in
valid_intv
.
apply
andb_prop_elim
in
valid_intv
.
destruct
valid_intv
as
[
valid_rec
valid_intv
].
apply
andb_prop_elim
in
valid_rec
.
destruct
valid_rec
as
[
valid_intv_e1
valid_intv_e2
].
apply
Is_true_eq_true
in
valid_intv_e1
;
apply
Is_true_eq_true
in
valid_intv_e2
.
apply
Is_true_eq_true
in
valid_intv
.
andb_to_prop
valid_intv
.
inversion
eval_real
;
subst
.
apply
binary_unfolding
in
eval_float
.
destruct
eval_float
as
[
v1F
[
v2F
[
eval_e1_float
[
eval_e2_float
eval_float
]]]].
...
...
@@ -1299,7 +1218,8 @@ Proof.
*
apply
andb_prop_intro
.
split
;
try
auto
.
apply
andb_prop_intro
.
split
;
apply
Is_true_eq_left
;
auto
.
split
;
apply
Is_true_eq_left
;
try
auto
.
apply
Is_true_eq_left
;
auto
.
*
apply
Is_true_eq_left
;
auto
.
*
unfold
validIntervalbounds
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
;
simpl
.
...
...
@@ -1317,6 +1237,7 @@ Proof.
split
;
try
auto
.
apply
andb_prop_intro
.
split
;
apply
Is_true_eq_left
;
auto
.
apply
Is_true_eq_left
;
auto
.
*
apply
Is_true_eq_left
;
auto
.
*
unfold
validIntervalbounds
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
;
simpl
.
...
...
@@ -1334,6 +1255,7 @@ Proof.
split
;
try
auto
.
apply
andb_prop_intro
.
split
;
apply
Is_true_eq_left
;
auto
.
apply
Is_true_eq_left
;
auto
.
*
apply
Is_true_eq_left
;
auto
.
*
unfold
validIntervalbounds
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
;
simpl
.
...
...
@@ -1351,6 +1273,7 @@ Proof.
split
;
try
auto
.
apply
andb_prop_intro
.
split
;
apply
Is_true_eq_left
;
auto
.
apply
Is_true_eq_left
;
auto
.
*
apply
Is_true_eq_left
;
auto
.
*
unfold
validIntervalbounds
.
rewrite
absenv_eq
,
absenv_e1
,
absenv_e2
;
simpl
.
...
...
coq/Expressions.v
View file @
d5db0675
...
...
@@ -67,7 +67,10 @@ Inductive exp (V:Type): Type :=
|
Unop
:
unop
->
exp
V
->
exp
V
|
Binop
:
binop
->
exp
V
->
exp
V
->
exp
V
.
(
**
Boolean
equality
function
on
expressions
.
Used
in
certificates
to
define
the
analysis
result
as
function
**
)
Fixpoint
expEqBool
(
e1
:
exp
Q
)
(
e2
:
exp
Q
)
:=
match
e1
with
|
Var
_
v1
=>
...
...
@@ -96,6 +99,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
|
_
=>
false
end
end
.
(
**
Define
a
perturbation
function
to
ease
writing
of
basic
definitions
**
)
...
...
@@ -119,15 +123,16 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
|
Const_dist
n
delta
:
Rle
(
Rabs
delta
)
eps
->
eval_exp
eps
env
(
Const
n
)
(
perturb
n
delta
)
|
Unop_neg
e1
v1
:
eval_exp
eps
env
e1
v1
->
eval_exp
eps
env
(
Unop
Neg
e1
)
(
evalUnop
Neg
v1
)
|
Unop_inv
e1
v1
delta
:
Rle
(
Rabs
delta
)
eps
->
eval_exp
eps
env
e1
v1
->
eval_exp
eps
env
(
Unop
Inv
e1
)
(
perturb
(
evalUnop
Inv
v1
)
delta
)
|
Binop_dist
op
e1
e2
v1
v2
delta
:
|
Unop_neg
f1
v1
:
eval_exp
eps
env
f1
v1
->
eval_exp
eps
env
(
Unop
Neg
f1
)
(
evalUnop
Neg
v1
)
|
Unop_inv
f1
v1
delta
:
Rle
(
Rabs
delta
)
eps
->
eval_exp
eps
env
e1
v1
->
eval_exp
eps
env
e2
v2
->
eval_exp
eps
env
(
Binop
op
e1
e2
)
(
perturb
(
evalBinop
op
v1
v2
)
delta
).
eval_exp
eps
env
f1
v1
->
eval_exp
eps
env
(
Unop
Inv
f1
)
(
perturb
(
evalUnop
Inv
v1
)
delta
)
|
Binop_dist
op
f1
f2
v1
v2
delta
:
Rle
(
Rabs
delta
)
eps
->
eval_exp
eps
env
f1
v1
->
eval_exp
eps
env
f2
v2
->
eval_exp
eps
env
(
Binop
op
f1
f2
)
(
perturb
(
evalBinop
op
v1
v2
)
delta
).
(
**
If
|
delta
|
<=
0
then
perturb
v
delta
is
exactly
v
.
...
...
@@ -138,30 +143,27 @@ Lemma delta_0_deterministic (v:R) (delta:R):
Proof
.
intros
abs_0
;
apply
Rabs_0_impl_eq
in
abs_0
;
subst
.
unfold
perturb
.
rewrite
Rmult_plus_distr_l
.
rewrite
Rmult_0_r
.
rewrite
Rmult_1_r
.
rewrite
Rplus_0_r
;
auto
.
lra
.
Qed
.
(
**
Evaluation
with
0
as
machine
epsilon
is
deterministic
**
)
Lemma
meps_0_deterministic
(
e
:
exp
R
)
(
env
:
env_ty
)
:
Lemma
meps_0_deterministic
(
f
:
exp
R
)
(
env
:
env_ty
)
:
forall
v1
v2
,
eval_exp
R0
env
e
v1
->
eval_exp
R0
env
e
v2
->
eval_exp
R0
env
f
v1
->
eval_exp
R0
env
f
v2
->
v1
=
v2
.
Proof
.
induction
e
;
intros
v1
v2
eval_v1
eval_v2
;
inversion
eval_v1
;
inversion
eval_v2
;
[
auto
|
|
|
|
|
|
|
];
induction
f
;
intros
v1
v2
eval_v1
eval_v2
;
inversion
eval_v1
;
inversion
eval_v2
;
repeat
try
rewrite
delta_0_deterministic
;
subst
;
auto
.
-
rewrite
(
IH
e
v0
v3
);
auto
.
-
rewrite
(
IH
f
v0
v3
);
auto
.
-
inversion
H3
.
-
inversion
H4
.
-
rewrite
(
IH
e
v0
v3
);
auto
.
-
rewrite
(
IH
e
1
v0
v4
);
auto
.
rewrite
(
IH
e
2
v3
v5
);
auto
.
-
rewrite
(
IH
f
v0
v3
);
auto
.
-
rewrite
(
IH
f
1
v0
v4
);
auto
.
rewrite
(
IH
f
2
v3
v5
);
auto
.
Qed
.
(
**
...
...
@@ -171,11 +173,11 @@ evaluating the subexpressions and then binding the result values to different
variables
in
the
environment
.
This
relies
on
the
property
that
variables
are
not
perturbed
as
opposed
to
parameters
**
)
Lemma
binary_unfolding
(
b
:
binop
)
(
e
1
:
exp
R
)
(
e
2
:
exp
R
)
(
eps
:
R
)
(
cenv
:
env_ty
)
(
v
:
R
)
:
(
eval_exp
eps
cenv
(
Binop
b
e
1
e
2
)
v
<->
Lemma
binary_unfolding
(
b
:
binop
)
(
f
1
:
exp
R
)
(
f
2
:
exp
R
)
(
eps
:
R
)
(
cenv
:
env_ty
)
(
v
:
R
)
:
(
eval_exp
eps
cenv
(
Binop
b
f
1
f
2
)
v
<->
exists
v1
v2
,
eval_exp
eps
cenv
e
1
v1
/
\
eval_exp
eps
cenv
e
2
v2
/
\
eval_exp
eps
cenv
f
1
v1
/
\
eval_exp
eps
cenv
f
2
v2
/
\
eval_exp
eps
(
updEnv
2
v2
(
updEnv
1
v1
cenv
))
(
Binop
b
(
Var
R
1
)
(
Var
R
2
))
v
).
Proof
.
split
.
...
...
@@ -183,11 +185,10 @@ Proof.
inversion
eval_bin
;
subst
.
exists
v1
,
v2
.
repeat
split
;
try
auto
.
constructor
;
try
auto
.
constructor
;
auto
.
constructor
;
try
auto
;
constructor
;
auto
.
-
intros
exists_val
.
destruct
exists_val
as
[
v1
[
v2
[
eval_
e
1
[
eval_
e
2
eval_e_env
]]]].
destruct
exists_val
as
[
v1
[
v2
[
eval_
f
1
[
eval_
f
2
eval_e_env
]]]].
inversion
eval_e_env
;
subst
.
inversion
H4
;
inversion
H5
;
subst
.
unfold
updEnv
in
*
;
simpl
in
*
.
...
...
@@ -211,7 +212,7 @@ Proof.
constructor
;
try
auto
.
constructor
;
auto
.
-
intros
exists_val
.
destruct
exists_val
as
[
v1
[
eval_
e
1
eval_e_env
]].
destruct
exists_val
as
[
v1
[
eval_
f
1
eval_e_env
]].
inversion
eval_e_env
;
subst
.
inversion
H1
;
subst
.
unfold
updEnv
in
*
;
simpl
in
*
.
...
...
@@ -228,16 +229,16 @@ Inductive bexp (V:Type) : Type :=
Define
evaluation
of
booleans
for
reals
**
)
Inductive
bval
(
eps
:
R
)
(
env
:
env_ty
)
:
(
bexp
R
)
->
Prop
->
Prop
:=
leq_eval
(
e
1
:
exp
R
)
(
e
2
:
exp
R
)
(
v1
:
R
)
(
v2
:
R
)
:
eval_exp
eps
env
e
1
v1
->
eval_exp
eps
env
e
2
v2
->
bval
eps
env
(
leq
e
1
e
2
)
(
Rle
v1
v2
)
|
less_eval
(
e
1
:
exp
R
)
(
e
2
:
exp
R
)
(
v1
:
R
)
(
v2
:
R
)
:
eval_exp
eps
env
e
1
v1
->
eval_exp
eps
env
e
2
v2
->
bval
eps
env
(
less
e
1
e
2
)
(
Rlt
v1
v2
).
leq_eval
(
f
1
:
exp
R
)
(
f
2
:
exp
R
)
(
v1
:
R
)
(
v2
:
R
)
:
eval_exp
eps
env
f
1
v1
->
eval_exp
eps
env
f
2
v2
->
bval
eps
env
(
leq
f
1
f
2
)
(
Rle
v1
v2
)
|
less_eval
(
f
1
:
exp
R
)
(
f
2
:
exp
R
)
(
v1
:
R
)
(
v2
:
R
)
:
eval_exp
eps
env
f
1
v1
->
eval_exp
eps
env
f
2
v2
->
bval
eps
env
(
less
f
1
f
2
)
(
Rlt
v1
v2
).
(
**
Simplify
arithmetic
later
by
making
>
>=
only
abbreviations
**
)
Definition
gr
:=
fun
(
V
:
Type
)
(
e1
:
exp
V
)
(
e2
:
exp
V
)
=>
less
e2
e1
.
Definition
greq
:=
fun
(
V
:
Type
)
(
e1
:
exp
V
)
(
e2
:
exp
V
)
=>
leq
e2
e1
.
\ No newline at end of file
Definition
gr
:=
fun
(
V
:
Type
)
(
f1
:
exp
V
)
(
f2
:
exp
V
)
=>
less
f2
f1
.
Definition
greq
:=
fun
(
V
:
Type
)
(
f1
:
exp
V
)
(
f2
:
exp
V
)
=>
leq
f2
f1
.
\ No newline at end of file
coq/Infra/Ltacs.v
0 → 100644
View file @
d5db0675
(
**
Ltac
definitions
**
)
Require
Import
Coq
.
Bool
.
Bool
Coq
.
Reals
.
Reals
.
Require
Import
Daisy
.
Infra
.
RealSimps
.
(
**
Automatic
translation
and
destruction
of
conjuctinos
with
andb
into
Props
**
)
Ltac
andb_to_prop
H
:=
apply
Is_true_eq_left
in
H
;
apply
andb_prop_elim
in
H
;
let
Left
:=
fresh
"L"
in
let
Right
:=
fresh
"R"
in
destruct
H
as
[
Left
Right
];
apply
Is_true_eq_true
in
Left
;
apply
Is_true_eq_true
in
Right
;
try
andb_to_prop
Left
;
try
andb_to_prop
Right
.
(
**
Tactic
to
simplify
multiplication
bound
proof
.
Used
to
obtain
similarly
shaped
terms
in
every
subgoal
.
Thus
automation
can
then
be
applied
to
solve
it
**
)
Ltac
math_hnf
:=
repeat
rewrite
Rsub_eq_Ropp_Rplus
;
repeat
rewrite
Ropp_plus_distr
;
repeat
rewrite
Rmult_plus_distr_r
;
repeat
rewrite
Rmult_plus_distr_l
;
repeat
rewrite
Ropp_involutive
;
repeat
rewrite
<-
Rplus_assoc
.
\ No newline at end of file
coq/Infra/RationalSimps.v
View file @
d5db0675
...
...
@@ -13,6 +13,9 @@ Definition machineEpsilon := (1#(2^53)).
Definition
maxAbs
(
iv
:
intv
)
:=
Qmax
(
Qabs
(
fst
iv
))
(
Qabs
(
snd
iv
)).
Definition
minAbs
(
iv
:
intv
)
:=
Qmin
(
Qabs
(
fst
iv
))
(
Qabs
(
snd
iv
)).
Lemma
maxAbs_pointIntv
a
:
maxAbs
(
a
,
a
)
==
Qabs
a
.
Proof
.
...
...
@@ -63,43 +66,15 @@ Proof.
unfold
Qplus
,
Qeq
;
auto
.
Qed
.
Lemma
inv_err_prop
(
vR
vF
err
:
positive
)
:
(
vR
-
vF
<=
err
)
%
positive
->
(
vF
<=
vR
)
%
positive
->
(((
1
#
vF
)
-
(
1
#
vR
))
<=
(
1
#(
vF
*
vF
))
*
(
Zpos
err
#
1
))
%
Q
.
Lemma
foo
a
b
:
(
a
<
b
)
%
positive
->
(
Z
.
neg
a
<
'
b
)
%
Z
.
Proof
.
intros
err_diff
vF_less
.
apply
(
Qle_trans
_
((
1
#(
vF
*
vF
))
*
((
Zpos
vR
#
1
)
-
(
Zpos
vF
#
1
)))
_
).
-
rewrite
Qsub_eq_Qopp_Qplus
.
unfold
Qopp
.
rewrite
equal_naming
;
simpl
.
unfold
Qminus
,
Qplus
,
Qmult
;
simpl
.
repeat
rewrite
Pos
.
mul_1_r
.
rewrite
Pos
.
le_lteq
in
vF_less
.
destruct
vF_less
.
+
repeat
rewrite
Z
.
pos_sub_gt
;
auto
.
unfold
Qle
;
simpl
.
hnf
;
intros
cmp
.
inversion
cmp
.
rewrite
Pos
.
compare_gt_iff
in
H1
.
rewrite
<-
Pos
.
mul_lt_mono_l
in
H1
.
rewrite
<-
Pos
.
mul_lt_mono_l
in
H1
.
apply
Pos
.
lt_nle
in
H1
.
apply
H1
.
<