Commit 5a981682 authored by Heiko Becker's avatar Heiko Becker
Browse files

Progress on validation of IVs in HOL Light

parent 10c11261
......@@ -40,7 +40,6 @@ let perturb = define
Abbreviations for the environment types
**)
new_type_abbrev("env_ty",`:num->real`);;
new_type_abbrev("analysisResult",`:(real)exp->intv#err`);;
(**
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
......
......@@ -7,6 +7,7 @@ new_type_abbrev ("err", `:real`);;
new_type_abbrev ("intv", `:real#real`);;
new_type_abbrev ("error", `:real`);;
new_type_abbrev ("ann", `:intverval#err`);;
new_type_abbrev ("precond",`:num->real#real`);;
let mkInterval = define `mkInterval (a:real) (b:real) = (a,b)`;;
let IVhi = define `IVhi (iv:interval) = SND (iv)`;;
......
needs "Infra/Abbrevs.hl";;
needs "Expressions.hl";;
(**
Abbreviations for the environment types
**)
new_type_abbrev("analysisResult",`:(real)exp->intv#err`);;
let envApproximatesPrecondFun = define
`envApproximatesPrecondFun (P:num->intv) (absenv:analysisResult) (u:num) =
let (ivlo,ivhi) = P u in
let (absIv,err) = absenv (Param u) in
let (abslo,abshi) = absIv in
abslo <= ivlo /\ ivhi <= abshi`;;
let envApproximatesPrecond = define
`envApproximatesPrecond (P:num->intv) (absenv:analysisResult) = !(u:num). envApproximatesPrecondFun P absenv u`;;
let precondValidForExecFun = define `
precondValidForExecFun (P:num->intv) (cenv:env_ty) (v:num) =
let (ivlo,ivhi) = P v in
(ivlo <= cenv v /\ cenv v <= ivhi)`;;
let precondValidForExec = define
`precondValidForExec (P:num->intv) (cenv:env_ty) = !(v:num). precondValidForExecFun P cenv v`;;
......@@ -5,8 +5,14 @@
let intros = REPEAT STRIP_TAC;;
let intros t = INTRO_TAC t;;
let specialize v t =
ASSUME_TAC (SPECL [v] (ASSUME t));;
let specialize thn t =
REMOVE_THEN thn (fun th -> LABEL_TAC thn (SPEC t th));;
(* TODO: make this tactic explicitly state where it fails to specialize!*)
let rec specl thn tlst =
match tlst with
| [] -> ALL_TAC
| hd :: tl -> specialize thn hd THEN specl thn tl;;
let reflexivity =
(CONV_TAC TAUT);;
......@@ -59,3 +65,12 @@ let mp_spec thn str =
(fun th2 ->
LABEL_TAC thn
(MP th2 th1)));;
let simplify thn =
REMOVE_THEN thn (fun th -> LABEL_TAC thn (CONV_RULE let_CONV th));;
let unfold thn th =
REMOVE_THEN thn
(fun th_old ->
LABEL_TAC thn
(REWRITE_RULE [th] th_old));;
......@@ -172,7 +172,7 @@ let interval_subtraction_valid =
SIMP_TAC[validIntervalSub; subtractInterval; contained; absIntvUpd]
THEN intros "!iv1 iv2 a b; contained_a lo_leq_b b_leq_hi"
THEN destruct "contained_a" "lo_leq_a a_leq_hi"
THEN ASM_REWRITE_TAC [Rsub_eq_Ropp_Rplus]
THEN ASM_REWRITE_TAC [real_sub]
THEN MATCH_MP_TAC (REWRITE_RULE [validIntervalAdd; contained] interval_add_valid)
THEN REPEAT split THEN ASM_REWRITE_TAC[negateInterval; mkInterval]
THENL [
......
needs "Infra/Abbrevs.hl";;
needs "Expressions.hl";;
needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalArith.hl";;
let validIntervalBounds = define
`(validIntervalBounds (Const n) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
`(validIntervalBounds (Var v) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
F) /\
(validIntervalBounds (Const n) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
(FST (FST (absenv (Const n))) <= n /\ n <= SND (FST (absenv (Const n))))) /\
(validIntervalBounds (Param v) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
(FST (P v) = FST (FST (absenv (Param v))) /\ (SND (P v) = SND (FST (absenv (Param v)))))) /\
......@@ -20,3 +23,188 @@ let validIntervalBounds = define
validIntervalBounds e2 absenv P /\
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)`;;
g `
!(e:(real)exp) (absenv:analysisResult) (P:precond) (cenv:env_ty) (vR:real).
envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
validIntervalBounds e absenv P = T /\
eval_exp (&0) cenv e vR ==>
(FST (FST(absenv e)) <= vR /\ vR <= SND (FST (absenv e)))`;;
e (mp exp_IND);;
e (split);;
(* Variable case, closed by contradiction *)
e (SIMP_TAC [validIntervalBounds]);;
e (split);;
(* Parameter case, needs some unfolding, rest straight forward *)
e (SIMP_TAC [validIntervalBounds; envApproximatesPrecond; envApproximatesPrecondFun; precondValidForExec; precondValidForExecFun]);;
e (intros "!a absenv P cenv vR");;
e (SUBGOAL_TAC "P_a_def" `?(ivlo:real) (ivhi:real). (P:num->real#real) a = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]);;
e (destruct "P_a_def" "@ivlo. @ivhi. P_a_def");;
e (SUBGOAL_TAC "absenv_param_def" `?absIv err. (absenv:analysisResult) (Param a) = (absIv, err)` [MESON_TAC [cases "prod"]]);;
e (destruct "absenv_param_def" "@absIv. @err. absenv_param_def");;
e (SUBGOAL_TAC "absIv_def" `?abslo abshi. (absIv:intv) = (abslo, abshi)` [MESON_TAC[cases "prod"]]);;
e (destruct "absIv_def" "@abslo. @abshi. absIv_def");;
e (ASM_SIMP_TAC[]);;
e (intros "env_approx_p p_valid bounds_valid eval_param");;
e (specialize "env_approx_p" `a:num`);;
e (specialize "p_valid" `a:num`);;
e (USE_THEN "P_a_def" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE[th])));;
e (simplify "env_approx_p");;
e (simplify "p_valid");;
e (USE_THEN "absenv_param_def" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE[th])));;
e (simplify "env_approx_p");;
e (USE_THEN "absIv_def" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE[th])));;
e (simplify "env_approx_p");;
e (USE_THEN "eval_param" (fun th -> LABEL_TAC "eval_param_inv" (MATCH_MP param_inv th)));;
e (destruct "eval_param_inv" "@delta. vR_eq abs_0");;
e (USE_THEN "abs_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`(cenv a:real)`; `delta:real`] perturb_0_val) th]));;
e (destruct "bounds_valid" "ivlo_eq_abslo ivhi_eq_abshi");;
e (destruct "env_approx_p" "abslo_le_ivlo ivhi_le_abshi");;
e (destruct "p_valid" "ivlo_le_env env_le_ivhi");;
e (split);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `ivlo:real` THEN split THEN auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `ivhi:real` THEN split THEN auto);;
e (split);;
(* Constant case, analogous to Parameter case *)
e (SIMP_TAC [validIntervalBounds; envApproximatesPrecond; envApproximatesPrecondFun; precondValidForExec; precondValidForExecFun]);;
e (intros "!a absenv P cenv vR");;
e (SUBGOAL_TAC "absenv_const_def" `?absIv err. (absenv:analysisResult) (Const a) = (absIv, err)` [MESON_TAC [cases "prod"]]);;
e (destruct "absenv_const_def" "@absIv. @err. absenv_const_def");;
e (SUBGOAL_TAC "absIv_def" `?abslo abshi. (absIv:intv) = (abslo, abshi)` [MESON_TAC[cases "prod"]]);;
e (destruct "absIv_def" "@abslo. @abshi. absIv_def");;
e (ASM_SIMP_TAC[]);;
e (intros "env_approx_p p_valid bounds_valid eval_const");;
e (USE_THEN "eval_const" (fun th -> LABEL_TAC "eval_const_inv" (MATCH_MP const_inv th)));;
e (destruct "eval_const_inv" "@delta. vR_eq abs_0");;
e (USE_THEN "abs_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`a:real`; `delta:real`] perturb_0_val) th]));;
(* Last, binary operator case *)
e (intros "!a0 a1 a2; IH1 IH2");;
e (SIMP_TAC [validIntervalBounds]);;
e (intros "!absenv P cenv vR");;
e (SUBGOAL_TAC "absenv_bin_def" `?absIv err. (absenv:analysisResult) (Binop a0 a1 a2) = (absIv, err)` [MESON_TAC [cases "prod"]]);;
e (destruct "absenv_bin_def" "@absIv. @err. absenv_bin_def");;
e (SUBGOAL_TAC "absIv_def" `?abslo abshi. (absIv:intv) = (abslo, abshi)` [MESON_TAC[cases "prod"]]);;
e (destruct "absIv_def" "@abslo. @abshi. absIv_def");;
e (ASM_SIMP_TAC[]);;
e (intros "env_approx_p p_valid valid_bounds eval_real");;
e (USE_THEN "eval_real" (fun th -> LABEL_TAC "eval_inv" (MATCH_MP binop_inv th)));;
e (destruct "eval_inv" "@delta. @v1. @v2. vR_eq eval_a1 eval_a2 abs_0");;
e (USE_THEN "abs_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`eval_binop (a0:binop) (v1:real) (v2:real)`; `delta:real`] perturb_0_val) th]));;
e (LABEL_TAC "cases_a0" (SPEC `a0:binop` (cases "binop")));;
e (destruct "cases_a0" "a0_Plus | a0_Sub | a0_Mult | a0_Div" THEN ASM_SIMP_TAC[eval_binop]);;
(* Plus case *)
e (USE_THEN "a0_Plus" (fun th -> RULE_ASSUM_TAC (REWRITE_RULE [th])));;
e (REMOVE_THEN "valid_bounds" (fun th -> LABEL_TAC "valid_bounds" (ONCE_REWRITE_RULE[validIntervalBounds] th)));;
e (destruct "valid_bounds" "valid_rec1 valid_rec2 valid_bin");;
e (specl "IH1" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v1:real`]);;
e (specl "IH2" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v2:real`]);;
e (SUBGOAL_TAC "valid_v1iv" `FST (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) <= (v1:real) /\ (v1:real) <= SND (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp)))` [REMOVE_THEN "IH1" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
e (SUBGOAL_TAC "valid_v2iv" `FST (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))) <= (v2:real) /\ (v2:real) <= SND (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp)))` [REMOVE_THEN "IH2" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
e (LABEL_TAC "addition_valid"
(REWRITE_RULE [validIntervalAdd; contained]
(SPECL
[`FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))`;
`FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))`] interval_add_valid)));;
e (specl "addition_valid" [`v1:real`; `v2:real`]);;
e (clear [ "valid_rec1"; "valid_rec2"; "IH1"; "IH2"]);;
e (unfold "valid_bin" isSupersetInterval);;
e (unfold "addition_valid" IVlo);;
e (unfold "addition_valid" IVhi);;
e (SUBGOAL_TAC "addition_valid2" `FST
(addInterval
(FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp)))
(FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp)))) <=
(v1:real) + (v2:real) /\
(v1:real) + (v2:real) <=
SND
(addInterval
(FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp)))
(FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))` [USE_THEN "addition_valid" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
+ pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
unfold validIntervalAdd in valid_add.
specialize (valid_add v1 v2 IHe1 IHe2).
unfold contained in valid_add.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_add as [valid_add_lo valid_add_hi].
split.
* eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold addIntv.
simpl in valid_add_lo.
repeat rewrite <- Q2R_plus in valid_add_lo.
rewrite <- Q2R_min4 in valid_add_lo.
unfold absIvUpd; auto.
* eapply Rle_trans.
Focus 2.
apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_add_hi.
repeat rewrite <- Q2R_plus in valid_add_hi.
rewrite <- Q2R_max4 in valid_add_hi.
unfold absIvUpd; auto.
+ pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
specialize (valid_sub v1 v2 IHe1 IHe2).
unfold contained in valid_sub.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_sub as [valid_sub_lo valid_sub_hi].
split.
* eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold subtractIntv.
simpl in valid_sub_lo.
repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo.
repeat rewrite <- Q2R_minus in valid_sub_lo.
rewrite <- Q2R_min4 in valid_sub_lo.
unfold absIvUpd; auto.
* eapply Rle_trans.
Focus 2.
apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_sub_hi.
repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi.
repeat rewrite <- Q2R_minus in valid_sub_hi.
rewrite <- Q2R_max4 in valid_sub_hi.
unfold absIvUpd; auto.
+ pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
specialize (valid_mul v1 v2 IHe1 IHe2).
unfold contained in valid_mul.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_mul as [valid_mul_lo valid_mul_hi].
split.
* eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_mul_lo.
repeat rewrite <- Q2R_mult in valid_mul_lo.
rewrite <- Q2R_min4 in valid_mul_lo.
unfold absIvUpd; auto.
* eapply Rle_trans.
Focus 2.
apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_mul_hi.
repeat rewrite <- Q2R_mult in valid_mul_hi.
rewrite <- Q2R_max4 in valid_mul_hi.
unfold absIvUpd; auto.
+ contradiction.
Qed.
let validIntervalbounds_correct = top_thm();;
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