Commit 2dd19d8d authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into fixed_point_hol4

parents c7ff0b5e 67de6c46
......@@ -24,13 +24,22 @@ RUN git clone https://github.com/polyml/polyml.git polyml && \
git checkout v5.7 && \
./configure && make && make install
ENV HOLCOMMIT 0de2c07679bd3773231f63059bbdd86050eeb452
ADD ./hol4/.HOLCOMMIT /root/HOLCOMMIT
# RUN cat /root/HOLCOMMIT
# RUN export HOLCOMMIT="$(cat /root/HOLCOMMIT)"
# RUN echo $HOLCOMMIT
# Download HOL4 and compile
RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
cd HOL4 && \
git checkout $HOLCOMMIT &&\
git checkout `cat /root/HOLCOMMIT` &&\
git rev-parse HEAD &&\
poly < tools/smart-configure.sml && \
./bin/build
RUN echo "HOLDIR=/root/HOL4" >> /root/.profile
ENV HOLDIR /root/HOL4
......@@ -38,7 +38,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
CertificateChecker e absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_expr E2 defVars (toRExp e) vF m ->
......@@ -93,7 +93,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
CertificateCheckerCmd f absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
bstep (toRCmd f) E2 defVars vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
......
......@@ -29,7 +29,7 @@ Fixpoint toRCmd (f:cmd Q) :=
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
|Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
......
......@@ -8,7 +8,7 @@ Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.Real
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_expr E1 (toRMap defVars) (Const M0 n) nR M0 ->
eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
eval_expr E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= computeErrorR n m)%R.
Proof.
......@@ -31,11 +31,11 @@ Qed.
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Plus (Var R 1) (Var R 2)) vF m ->
......@@ -46,11 +46,11 @@ Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion plus_real; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join M0 M0) delta); auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join REAL REAL) delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
......@@ -104,11 +104,11 @@ Qed.
**)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Sub (Var R 1) (Var R 2)) vF m ->
......@@ -119,8 +119,8 @@ Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -182,11 +182,11 @@ Qed.
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Mult (Var R 1) (Var R 2)) vF m ->
......@@ -195,8 +195,8 @@ Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -231,11 +231,11 @@ Qed.
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Div (Var R 1) (Var R 2)) vF m ->
......@@ -244,8 +244,8 @@ Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -280,13 +280,13 @@ Qed.
Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(e3:expr Q) (e3R:R) (e3F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R REAL ->
eval_expr E2 defVars (toRExp e3) e3F m3->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
......@@ -294,9 +294,9 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
Proof.
intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
inversion fma_real; subst;
assert (m0 = 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).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in fma_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -345,7 +345,7 @@ Proof.
Qed.
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (mEps m:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval e) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval e) nR REAL ->
eval_expr E2 defVars e nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
......
......@@ -151,7 +151,7 @@ Qed.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars
dVars Gamma exprTypes:
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
validIntervalbounds (Var Q v) A P dVars = true ->
......@@ -181,7 +181,7 @@ Qed.
Lemma validErrorboundCorrectVariable:
forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma exprTypes,
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
......@@ -226,7 +226,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL ->
exists nF m',
eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
Proof.
......@@ -238,7 +238,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL ->
eval_expr E2 defVars (toRExp (Const m n)) nF m ->
typeCheck (Const m n) defVars Gamma = true ->
validErrorbound (Const m n) Gamma A dVars = true ->
......@@ -265,9 +265,9 @@ Lemma validErrorboundCorrectAddition E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -327,9 +327,9 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -859,9 +859,9 @@ Lemma validErrorboundCorrectMult E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -930,9 +930,9 @@ Lemma validErrorboundCorrectDiv E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -1845,10 +1845,10 @@ Lemma validErrorboundCorrectFma E1 E2 A
(e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars:
m = join3 m1 m2 m3 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr E2 defVars (toRExp e3) nF3 m3 ->
......@@ -1938,7 +1938,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
eval_expr E2 defVars (toRExp e) nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
......@@ -1981,7 +1981,7 @@ Theorem validErrorbound_sound (e:expr Q):
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
validErrorbound e Gamma A dVars = true ->
validIntervalbounds e A P dVars = true ->
dVars_range_valid dVars E1 A ->
......@@ -2029,7 +2029,7 @@ Proof.
- cbn in *. rewrite A_eq in *.
Flover_compute; try congruence; type_conv; subst; simpl in *.
inversion eval_real; subst.
assert (m0 = M0 /\ m3 = M0) as [? ?] by (split; eapply toRMap_eval_M0; eauto); subst.
assert (m0 = REAL /\ m3 = REAL) as [? ?] by (split; eapply toRMap_eval_REAL; eauto); subst.
destruct i as [ivlo1 ivhi1]; destruct i1 as [ivlo2 ivhi2];
rename e into err1; rename e3 into err2.
destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars)
......@@ -2120,7 +2120,7 @@ Proof.
- cbn in *. rewrite A_eq in *.
Flover_compute; try congruence; type_conv; subst; simpl in *.
inversion eval_real; subst.
assert (m0 = M0 /\ m4 = M0 /\ m5 = M0) as [? [? ?]] by (split; try split; eapply toRMap_eval_M0; eauto); subst.
assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]] by (split; try split; eapply toRMap_eval_REAL; eauto); subst.
destruct i as [ivlo1 ivhi1]; destruct i2 as [ivlo2 ivhi2]; destruct i1 as [ivlo3 ivhi3];
rename e into err1; rename e5 into err2; rename e4 into err3.
destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars)
......@@ -2175,7 +2175,7 @@ Proof.
auto. }
- cbn in *; Flover_compute; try congruence; type_conv; subst.
inversion eval_real; subst.
apply M0_least_precision in H1.
apply REAL_least_precision in H1.
subst.
destruct i0 as [ivlo_e ivhi_e]; rename e1 into err_e.
destruct (IHe E1 E2 fVars dVars A v1 err_e P ivlo_e ivhi_e Gamma defVars)
......@@ -2212,7 +2212,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
dVars_range_valid dVars E1 A ->
......@@ -2273,7 +2273,7 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto. }
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm. }
{ intros v1 v1_mem.
unfold updEnv.
......@@ -2324,7 +2324,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
bstep (toRCmd f) E2 defVars vF mF ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
......@@ -2385,7 +2385,7 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm.
+ intros v1 v1_mem.
unfold updEnv.
......
(**
Formalization of the base exprression language for the flover framework
**)
From Coq
Require Import Structures.Orders.
From Flover
Require Import Infra.RealRationalProps Infra.Ltacs.
......@@ -127,16 +124,16 @@ Fixpoint toRExp (e:expr Q) :=
Fixpoint toREval (e:expr R) :=
match e with
| Var _ v => Var R v
| Const _ n => Const M0 n
| Const _ n => Const REAL n
| Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
| Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3)
| Downcast _ e1 => Downcast M0 (toREval e1)
| Downcast _ e1 => Downcast REAL (toREval e1)
end.
Definition toRMap (d:nat -> option mType) (n:nat) :=
match d n with
| Some m => Some M0
| Some m => Some REAL
| None => None
end.
......@@ -151,7 +148,7 @@ Arguments toRMap _ _/.
Definition perturb (rVal:R) (m:mType) (delta:R) :R :=
match m with
(* The Real-type has no error *)
|M0 => rVal
|REAL => rVal
(* Fixed-point numbers have an absolute error *)
|F w f => rVal + delta
(* Floating-point numbers have a relative error *)
......@@ -299,8 +296,8 @@ Fixpoint usedVars (V:Type) (e:expr V) :NatSet.t :=
| _ => NatSet.empty
end.
Lemma toRMap_eval_M0 f v E Gamma m:
eval_expr E (toRMap Gamma) (toREval f) v m -> m = M0.
Lemma toRMap_eval_REAL f v E Gamma m:
eval_expr E (toRMap Gamma) (toREval f) v m -> m = REAL.
Proof.
revert v E Gamma m.
induction f; intros * eval_f; inversion eval_f; subst;
......@@ -313,16 +310,16 @@ Proof.
end; try auto.
- eapply IHf; eauto.
- eapply IHf; eauto.
- assert (m1 = M0)
- assert (m1 = REAL)
by (eapply IHf1; eauto).
assert (m2 = M0)
assert (m2 = REAL)
by (eapply IHf2; eauto);
subst; auto.
- assert (m1 = M0)
- assert (m1 = REAL)
by (eapply IHf1; eauto).
assert (m2 = M0)
assert (m2 = REAL)
by (eapply IHf2; eauto).
assert (m3 = M0)
assert (m3 = REAL)
by (eapply IHf3; eauto);
subst; auto.
Qed.
......@@ -343,8 +340,8 @@ Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:expr R) (E:env) Gamma:
forall v1 v2,
eval_expr E (toRMap Gamma) (toREval f) v1 M0 ->
eval_expr E (toRMap Gamma) (toREval f) v2 M0 ->
eval_expr E (toRMap Gamma) (toREval f) v1 REAL ->
eval_expr E (toRMap Gamma) (toREval f) v2 REAL ->
v1 = v2.
Proof.
induction f;
......@@ -358,27 +355,27 @@ Proof.
+ rewrite (IHf v0 v3); eauto.
+ cbn in H1, H8. subst. rewrite (IHf v0 v3); eauto.
- inversion ev1; inversion ev2; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = 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 (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); 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).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v5); try auto.
rewrite (IHf2 v3 v6); try auto.
rewrite (IHf3 v4 v7); try auto.
- inversion ev1; inversion ev2; subst.
apply M0_least_precision in H1;
apply M0_least_precision in H7; subst.
apply REAL_least_precision in H1;
apply REAL_least_precision in H7; subst.
rewrite (IHf v0 v3); try auto.
Qed.
......
......@@ -196,7 +196,7 @@ Proof.
- rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n M0 (toRMap Gamma))); eauto.
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm. }
{ set_tac; split.
- split; try auto.
......
This diff is collapsed.
(**
(*
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.MachineType.
Global Set Implicit Arguments.
(**
We define Intervals twice.
First we define intervals of reals and fractions.
......@@ -62,15 +61,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
Definition optionLift (V T:Type) (v:option V) default (f: V -> T) :=
match v with
| None => default
| Some val => f val
end.
Ltac optionD :=
match goal with
|H: context[optionLift ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
\ No newline at end of file
......@@ -2,6 +2,8 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Global Set Implicit Arguments.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -55,42 +57,57 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
|Some val => f val
| Some v => f v
| None => e
end.
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
match v with |Some val => f val | None => e end = optionLift X Y v f e.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
(only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
(only parsing, at level 0, t at level 200).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
match v with |Some val => f val | None => e end = optionBind v f e.
Proof.
reflexivity.
Qed.
Lemma optionLift_cond X (a:bool) (b c :X):
Lemma optionBind_cond X (a:bool) (b c: X):
(if a then b else c) = match a with |true => b |false => c end.
Proof.
reflexivity.
Qed.
Ltac remove_matches := rewrite optionLift_eq in *.
Ltac remove_matches := rewrite optionBind_eq in *.
Ltac remove_matches_asm := rewrite optionBind_eq in * |- .
Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
Ltac match_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
| [ H: ?t = ?u |- context [optionBind ?t _ _]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
| [ H1: ?t = ?u, H2: context [optionBind ?t _ _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [optionLift _ _ ?t _ _] |- _ ]
| [ H: context [optionBind ?t _ _] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac match_factorize :=
match_factorize_asm ||
match goal with
| [ |- context [optionLift _ _ ?t _ _] ]
| [ |- context [optionBind ?t _ _] ]
=> destruct t eqn:?; cbn; try congruence
end.
......@@ -120,8 +137,8 @@ Ltac bool_factorize :=
Ltac Flover_compute_asm :=
repeat (
(try remove_conds;
try remove_matches;
(try remove_conds_asm;
try remove_matches_asm;
repeat match_factorize_asm;
try pair_factorize) ||
bool_factorize).
......@@ -152,7 +169,7 @@ Ltac Flover_compute :=
(* Ltac match_destr t:= *)
(* match goal with *)
(* | H: context [optionLift (FloverMap.find ?k ?M) _ _] |- _ => *)
(* | H: context [optionBind (FloverMap.find ?k ?M) _ _] |- _ => *)
(* destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
(* end. *)
......@@ -179,4 +196,4 @@ Ltac destruct_ex H pat :=
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
\ No newline at end of file
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
......@@ -18,7 +18,7 @@ From Flover
like Flocq, where f:positive specifies the fraction size and w: the width of
the base field.
**)
Inductive mType: Type := M0 | M16 | M32 | M64
Inductive mType: Type := REAL | M16 | M32 | M64
| F (w:positive) (f:positive). (*| M128 | M256*)
(**
......@@ -26,7 +26,7 @@ Inductive mType: Type := M0 | M16 | M32 | M64
**)
Definition mTypeToR (m:mType) :R :=
match m with
| M0 => 0%R
| REAL => 0%R
| M16 => 1 / 2^11
| M32 => 1/ 2^24
| M64 => 1/ 2^53
......@@ -40,7 +40,7 @@ Definition mTypeToR (m:mType) :R :=