Commit de0c5b3a authored by Heiko Becker's avatar Heiko Becker
Browse files

Start working on proving multiplication bound in HOL-Light

parent 80e84183
......@@ -382,57 +382,77 @@ e (SIMP_TAC[freeVars; MEM; MEM_APPEND]
mp_asm "mult_bounded" THEN auto;
clear ["mult_bounded"]
THEN rewrite validErrorbound "valid_error"
THEN rewrite_asm "absenv_mult" "valid_error"]);;
THEN rewrite_asm "absenv_mult" "valid_error"
THEN simplify "valid_error"
THEN rewrite_asm "absenv_e1" "valid_error"
THEN rewrite_asm "absenv_e2" "valid_error"
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN simplify "valid_error"
THEN pose_proof err_always_positive "err1_pos" [`e1:(real)exp`; `absenv:analysisResult`; `(e1lo,e1hi):interval`; `err1:error`] []
THEN destruct "valid_error" "valid_err_e1 valid_err_e2 err_geq_0 valid_error"
THEN pose_proof err_always_positive "err1_pos" [`e1:(real)exp`; `absenv:analysisResult`; `(e1lo,e1hi):interval`; `err1:error`] ["valid_err_e1"; "absenv_e1"]
THEN pose_proof err_always_positive "err2_pos" [`e2:(real)exp`; `absenv:analysisResult`; `(e2lo,e2hi):interval`; `err2:error`] ["valid_err_e2"; "absenv_e2"]
THEN clear["valid_err_e1"; "valid_err_e2"]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(maxAbsFun ((e1lo:real),(e1hi:real)) * (err2:real) +
maxAbsFun ((e2lo:real),(e2hi:real)) * (err1:real) +
(err1:real) * (err2:real)) +
abs
((maxAbsFun ((e1lo:real),(e1hi:real)) + (err1:real)) *
(maxAbsFun ((e2lo:real),(e2hi:real)) + (err2:real))) *
machineEpsilon`
THEN split
THENL [
clear ["valid_error"]
THEN SUBGOAL_TAC "env_approx_e1" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e1:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "env_approx_e2" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e2:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN pose_proof validIntervalbounds_sound "validbounds_e1" [`e1:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR1:real`] ["env_approx_e1"; "p_valid"; "valid_e1"; "e1_real"]
THEN pose_proof validIntervalbounds_sound "validbounds_e2" [`e2:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR2:real`] ["env_approx_e2"; "p_valid"; "valid_e2"; "e2_real"]
THEN mp REAL_LE_ADD2
THEN split
THENL[
rewrite real_abs "err1_bounded"
THEN rewrite real_abs "err2_bounded"
(** TODO: CONTINUE HERE **)
;
mp REAL_LE_RMUL THEN split
THENL [
REWRITE_TAC [REAL_ABS_MUL]
THEN mp REAL_LE_MUL2
THEN (REPEAT split)
THENL[
SIMP_TAC[REAL_ABS_POS];
rewrite_asm "absenv_e1" "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN split
THEN ASM_SIMP_TAC[contained; IVlo; IVhi; FST; SND];
SIMP_TAC[REAL_ABS_POS];
rewrite_asm "absenv_e2" "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN split
THEN ASM_SIMP_TAC[contained; IVlo; IVhi; FST; SND];
]
;
SIMP_TAC[mEps_geq_zero]
]
];
SUBGOAL_TAC "mult_neq_plus" `Mult = Plus \/ Mult = Sub <=> F` [MESON_TAC[distinctness "binop"]]
THEN rewrite_asm "mult_neq_plus" "valid_error"
THEN REMOVE_THEN "valid_error" (fun th -> LABEL_TAC "valid_error" (CONV_RULE COND_ELIM_CONV th))
THEN destruct "valid_error" "asm1 asm2"
THEN mp_asm "asm2"
THEN auto
]
]);;
search [ `(a:real) <= a`];;
search [ ` (a:real) <= b`];;
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.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
Focus 2.
apply valid_error.
(* 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.
assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1
by (intros v in_fV_e1;
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto);
apply (env_approx_p v H)).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_e1.
assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
by ( intros v in_fV_e2;
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto);
apply (env_approx_p v H)).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_e2.
apply Rplus_le_compat.
-
unfold Rabs in err1_bounded.
unfold Rabs in err2_bounded.
(* Before doing case distinction, prove bounds that will be used many times: *)
assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R
as upperBound_nR1
......@@ -968,13 +988,4 @@ e (SIMP_TAC[freeVars; MEM; MEM_APPEND]
rewrite H1.
lra.
}
- apply Rmult_le_compat; [ apply Rabs_pos | apply mEps_geq_zero | | apply Req_le; auto ].
rewrite Q2R_mult; repeat rewrite Q2R_plus.
repeat rewrite <- maxAbs_impl_RmaxAbs.
repeat rewrite Rabs_mult.
apply Rmult_le_compat; [apply Rabs_pos | apply Rabs_pos | | ].
+ apply (Rabs_error_bounded_maxAbs nR1); try auto.
rewrite absenv_e1 in valid_e1; simpl in *; unfold contained; auto.
+ apply (Rabs_error_bounded_maxAbs nR2); try auto.
rewrite absenv_e2 in valid_e2; simpl in *; unfold contained; auto.
Qed.
......@@ -26,7 +26,7 @@ let validIntervalbounds = define
isSupersetInterval (multInterval (FST (absenv e1)) (FST (absenv e2))) (FST (absenv (Binop Mult e1 e2))))) /\
(validIntervalbounds (Binop Div e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) = F)`;;
let validIntervalbounds_correct = prove (
let validIntervalbounds_sound = prove (
`!(e:(real)exp) (absenv:analysisResult) (P:precond) (cenv:env_ty) (vR:real).
(!(v:num).
MEM v (freeVars e) ==> isSupersetInterval (P v) (FST (absenv (Param v)))) /\
......
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