Commit f7b47a46 authored by Heiko Becker's avatar Heiko Becker

Make proper use of isSupersetInterval function for clarification

parent 8563f301
......@@ -119,7 +119,8 @@ Section ComputableErrors.
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 *; [ destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
apply RmaxAbs; simpl; apply Qle_Rle; rewrite <- Qle_bool_iff; unfold Qleb in *; simpl in *;
[destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
Qed.
Lemma validErrorboundCorrectParam:
......
......@@ -9,10 +9,9 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
(* let bounds_v := P v in
andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv))) *)
| Param v =>
let bounds_v := P v in
andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
isSupersetIntv (P v) intv
| Const n =>
andb (Qleb (fst intv) n) (Qleb n (snd intv))
isSupersetIntv (n,n) intv
| Binop b e1 e2 =>
let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
let (iv1,_) := absenv e1 in
......
......@@ -82,14 +82,14 @@ let validErrorboundCorrectConstant = prove (
absenv (Const n) = ((nlo,nhi),e) ==>
(abs (nR - nF)) <= e`,
intros "!cenv absenv n nR nF e nlo nhi P; eval_real eval_float error_valid intv_valid absenv_const"
THEN rewrite validErrorbound "error_valid"
THEN pose_spec const_inv [`&0:real`; `cenv:env_ty`; `n:real`; `nR:real`] "eval_real" "eval_inv"
THEN destruct "eval_inv" "@d. perturb_nR abs_0"
THEN ASM_SIMP_TAC[perturb_0_val]
THEN pose_spec const_inv [`machineEpsilon:real`; `cenv:env_ty`; `n:real`; `nF:real`] "eval_float" "eval_inv"
THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN rewrite validErrorbound "error_valid"
THEN pose_spec const_inv [`&0:real`; `cenv:env_ty`; `n:real`; `nR:real`] "eval_real" "eval_inv"
THEN destruct "eval_inv" "@d. perturb_nR abs_0"
THEN ASM_SIMP_TAC[perturb_0_val]
THEN pose_spec const_inv [`machineEpsilon:real`; `cenv:env_ty`; `n:real`; `nF:real`] "eval_float" "eval_inv"
THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (n:real) * (machineEpsilon:real)` THEN split
THENL [
......@@ -97,7 +97,9 @@ let validErrorboundCorrectConstant = prove (
THEN split THENL [ SIMP_TAC[REAL_ABS_POS]; auto];
rewrite validIntervalbounds "intv_valid"
THEN rewrite_asm "absenv_const" "intv_valid"
THEN rewrite FST "intv_valid"
THEN rewrite isSupersetInterval "intv_valid"
THEN rewrite IVlo "intv_valid"
THEN rewrite IVhi "intv_valid"
THEN rewrite SND "intv_valid"
THEN destruct "intv_valid" "lo_le_n n_le_hi"
THEN rewrite_asm "absenv_const" "error_valid" THEN simplify "error_valid"
......
......@@ -9,9 +9,9 @@ let validIntervalbounds = define
`(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))))) /\
isSupersetInterval (n,n) (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)))))) /\
isSupersetInterval (P v) (FST (absenv (Param v)))) /\
(validIntervalbounds (Binop Plus e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
(validIntervalbounds e1 absenv P /\
validIntervalbounds e2 absenv P /\
......@@ -27,15 +27,15 @@ let validIntervalbounds = define
(validIntervalbounds (Binop Div e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) = F)`;;
let validIntervalbounds_sound = prove (
`!(e:(real)exp) (absenv:analysisResult) (P:precond) (cenv:env_ty) (vR:real).
`!(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)))) /\
precondValidForExec P cenv /\
validIntervalbounds e absenv P = T /\
eval_exp (&0) cenv e vR ==>
(FST (FST(absenv e)) <= vR /\ vR <= SND (FST (absenv e)))`,
mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN split
mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN split THEN SIMP_TAC[isSupersetInterval]
THENL [
(* Parameter case, needs some unfolding, rest straight forward *)
SIMP_TAC [validIntervalbounds; precondValidForExec; precondValidForExecFun]
......@@ -65,6 +65,9 @@ mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN USE_THEN "abs_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`(cenv a:real)`; `delta:real`] perturb_0_val) th])
THEN rewrite IVhi "bounds_valid"
THEN rewrite IVlo "bounds_valid"
THEN rewrite FST "bounds_valid"
THEN destruct "bounds_valid" "ivlo_eq_abslo ivhi_eq_abshi"
THEN SUBGOAL_TAC "a_elem_fV_a" `MEM (a:num) (freeVars ((Param a):(real)exp))` [MESON_TAC[freeVars; MEM]]
THEN mp_spec "env_approx_p" "a_elem_fV_a"
......@@ -94,6 +97,9 @@ mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN intros "env_approx_p p_valid bounds_valid eval_const"
THEN USE_THEN "eval_const" (fun th -> LABEL_TAC "eval_const_inv" (MATCH_MP const_inv th))
THEN destruct "eval_const_inv" "@delta. vR_eq abs_0"
THEN rewrite IVhi "bounds_valid"
THEN rewrite IVlo "bounds_valid"
THEN rewrite FST "bounds_valid"
THEN USE_THEN "abs_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`a:real`; `delta:real`] perturb_0_val) th]);
......@@ -118,15 +124,15 @@ mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN ASM_SIMP_TAC[eval_binop]
THENL [
(* Plus case *)
USE_THEN "a0_Plus" (fun th -> RULE_ASSUM_TAC (REWRITE_RULE [th]))
USE_THEN "a0_Plus" (fun th -> RULE_ASSUM_TAC (REWRITE_RULE [th]))
THEN REMOVE_THEN "valid_bounds" (fun th -> LABEL_TAC "valid_bounds" (ONCE_REWRITE_RULE[validIntervalbounds] th))
THEN destruct "valid_bounds" "valid_rec1 valid_rec2 valid_bin"
THEN lspecialize "IH1" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v1:real`]
THEN lspecialize "IH2" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v2:real`]
THEN SUBGOAL_TAC "fv_a1_superset" `!v. MEM (v:num) (freeVars (a1:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN SUBGOAL_TAC "fv_a2_superset" `!v. MEM (v:num) (freeVars (a2:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN 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]
THEN 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]
THEN LABEL_TAC "addition_valid"
......@@ -172,9 +178,9 @@ mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN lspecialize "IH1" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v1:real`]
THEN lspecialize "IH2" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v2:real`]
THEN SUBGOAL_TAC "fv_a1_superset" `!v. MEM (v:num) (freeVars (a1:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN SUBGOAL_TAC "fv_a2_superset" `!v. MEM (v:num) (freeVars (a2:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN 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]
THEN 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]
THEN LABEL_TAC "subtraction_valid"
......@@ -220,9 +226,9 @@ mp exp_IND THEN SIMP_TAC[validIntervalbounds]
THEN lspecialize "IH1" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v1:real`]
THEN lspecialize "IH2" [`absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `v2:real`]
THEN SUBGOAL_TAC "fv_a1_superset" `!v. MEM (v:num) (freeVars (a1:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN SUBGOAL_TAC "fv_a2_superset" `!v. MEM (v:num) (freeVars (a2:(real)exp)) ==> isSupersetInterval (P v) (FST ((absenv:analysisResult) (Param v)))`
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[]]
[intros "!v; MEM_v" THEN specialize "env_approx_p" `v:num` THEN ASM_SIMP_TAC[isSupersetInterval]]
THEN 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]
THEN 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]
THEN LABEL_TAC "mult_valid"
......
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