Skip to content

GitLab

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

Cleanup files and prove same theorems as in Coq for IVArith

parent db5ae1e7
Hide whitespace changes
Inline Side-by-side
hol/ErrorValidation.hl
View file @ f36f9610
......@@ -2,15 +2,6 @@ needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalValidation.hl";;
needs "ErrorBounds.hl";;
let mEps_geq_zero =
prove (
`(&0) <= machineEpsilon`,
SIMP_TAC [machineEpsilon]
THEN REAL_ARITH_TAC);;
let maxAbsFun = define
`maxAbsFun (iv:real#real) = max (abs (FST iv)) (abs (SND iv))`;;
let validErrorbound = define
`(validErrorbound (Const n) (absenv:(real)exp->(real#real)#real) =
let (intv, err) = absenv (Const n) in
......
hol/Infra/RealSimps.hl
View file @ f36f9610
......@@ -81,3 +81,9 @@ let iv_le_maxAbs = prove (
Current value: 2^(-53)
*)
let machineEpsilon = define `machineEpsilon:real = &1 /((&2) pow 53)`;;
let mEps_geq_zero =
prove (
`(&0) <= machineEpsilon`,
SIMP_TAC [machineEpsilon]
THEN REAL_ARITH_TAC);;
hol/IntervalArith.hl
View file @ f36f9610
......@@ -197,110 +197,217 @@ let multInterval = define
`multInterval (I1:interval) (I2:interval) =
absIntvUpd ( * ) I1 I2`;;
g `!(iv1:interval) (iv2:interval) (a:real) (b:real).
contained a iv1 /\
contained b iv2 ==>
contained (a * b) (multInterval iv1 iv2)`;;
e (SIMP_TAC[contained; multInterval; absIntvUpd; IVlo; IVhi]);;
e (intros "!iv1 iv2 a b; contained_a lo_leq_b b_leq_hi");;
e (destruct "contained_a" "lo_leq_a a_leq_hi");;
e (LABEL_TAC "min4_correct"
(SPECL
[`FST (iv1:real#real) * FST (iv2:real#real)`; `FST (iv1:real#real) * SND (iv2:real#real)`; `SND (iv1:real#real) * FST (iv2:real#real)`; `SND (iv1:real#real) * SND (iv2:real#real)`] min4_correct));;
e (LABEL_TAC "max4_correct" (SPECL [`FST (iv1:real#real) * FST (iv2:real#real)`; `FST (iv1:real#real) * SND (iv2:real#real)`; `SND (iv1:real#real) * FST (iv2:real#real)`; `SND (iv1:real#real) * SND (iv2:real#real)`] max4_correct));;
e (destruct "min4_correct" "leq_lolo leq_lohi leq_hilo leq_hihi");;
e (destruct "max4_correct" "lolo_leq lohi_leq hilo_leq hihi_leq");;
e (split);;
(* Lower Bound *) (* REAL_LE_NEGTOTAL or REAL_LE_NEG??? *)
e (LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_a" "a_lt_0 | 0_leq_a");;
(* First case of outer case distinction, a < 0 *)
e (REMOVE_THEN "a_lt_0" (fun th -> LABEL_TAC "a_le_0" (REWRITE_RULE [REAL_LT_LE] th))
THEN destruct "a_le_0" "a_le_0 a_neq_0");;
e (LABEL_TAC "cases_hi2" (SPECL [`(SND (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `SND (iv1:real#real) * SND (iv2:real#real)`);;
e (split);;
e (ASM_SIMP_TAC[]);;
e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `SND (iv2:real#real) * (a:real)`);;
e (split);;
e (MATCH_MP_TAC REAL_MUL_LE_COMPAT_NEG_L);;
e (split THEN ASM_SIMP_TAC[]);;
(* TODO: Make this a tactic : *)
e (REMOVE_THEN "hi2_lt_0" (fun th -> LABEL_TAC "hi2_le_0" (REWRITE_RULE [REAL_LT_LE] th)));;
e (destruct "hi2_le_0" "hi2_le_0 hi2_neq_0");;
e (ASM_SIMP_TAC[]);;
e (ONCE_REWRITE_TAC[REAL_MUL_SYM]);;
e (mp REAL_MUL_LE_COMPAT_NEG_L);;
e (split THEN auto);;
(* Second case of case distinction for SND iv2 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `(FST (iv1:real#real)) * SND (iv2:real#real)`);;
e (split THEN TRY auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `(a:real) * SND (iv2:real#real)`);;
e (split THENL [mp REAL_LE_RMUL THEN auto; mp REAL_MUL_LE_COMPAT_NEG_L THEN split THEN auto]);;
(* Second case of case distinction for a, 0 <= a *)
e (LABEL_TAC "cases_lo2" (SPECL [`(FST (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2");;
(* First case of case distinction for fst iv2, fst iv2 < 0 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (iv1:real#real) * FST (iv2:real#real)`);;
e (split THEN TRY auto);;
e (mp REAL_LE_TRANS);;
e (REMOVE_THEN "lo2_lt_0" (fun th -> LABEL_TAC "lo2_le_0" (REWRITE_RULE [REAL_LT_LE] th)));;
e (destruct "lo2_le_0" "lo2_le_0 lo2_neq_0");;
e (EXISTS_TAC `(a:real) * (FST (iv2:real#real))` THEN split THENL
[ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN mp REAL_MUL_LE_COMPAT_NEG_L THEN auto;
mp REAL_LE_LMUL THEN auto]);;
(* Second case, 0 <= fst iv2 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (iv1:real#real) * FST (iv2:real#real)` THEN split THEN TRY auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `a:real * FST (iv2:real#real)` THEN split THENL [ mp REAL_LE_RMUL THEN auto ; mp REAL_LE_LMUL THEN auto]);;
(* Upper Bound *)
e (LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_a" "a_lt_0 | 0_leq_a");;
e (REMOVE_THEN "a_lt_0" (fun th -> LABEL_TAC "a_le_0" (REWRITE_RULE [REAL_LT_LE] th))
THEN destruct "a_le_0" "a_le_0 a_neq_0");;
(* First case for case distinction for a, a < 0 *)
e (mp REAL_LE_TRANS THEN EXISTS_TAC `a:real * FST (iv2:real#real)` THEN split
THENL [mp REAL_MUL_LE_COMPAT_NEG_L THEN split THEN auto; ALL_TAC]);;
e (LABEL_TAC "cases_lo2" (SPECL [`FST (iv2:real#real)`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2");;
(* First case of distinction for FST iv2, FST iv2 < 0 *)
e (REMOVE_THEN "lo2_lt_0" (fun th -> LABEL_TAC "lo2_le_0" (REWRITE_RULE [REAL_LT_LE] th)));;
e (destruct "lo2_le_0" "lo2_le_0 lo2_neq_0");;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (iv1:real#real) * FST (iv2:real#real)` THEN split
THENL [ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN mp REAL_MUL_LE_COMPAT_NEG_L
THEN split THEN auto;
auto]);;
(* Second case for case distinction for FST iv2, 0 <= FST iv2 *)
e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (iv2:real#real) * SND (iv1:real#real)` THEN split THENL [mp REAL_LE_LMUL THEN auto; ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto]);;
(* Second case for case distinction for a. 0 <= a *)
e (LABEL_TAC "cases_hi2" (SPECL [`(SND (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
(* First case for case distinction for SND iv2, SND iv2 < 0 *)
e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);;
e (mp REAL_LE_TRANS);;
e (REMOVE_THEN "hi2_lt_0" (fun th -> LABEL_TAC "hi2_le_0" (REWRITE_RULE [REAL_LT_LE] th)));;
e (destruct "hi2_le_0" "hi2_le_0 hi2_neq_0");;
e (EXISTS_TAC `SND (iv2:real#real) * FST (iv1:real#real)` THEN split THENL [ mp REAL_LE_TRANS ; ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto]);;
e (EXISTS_TAC `SND (iv2:real#real) * a:real` THEN split
THENL [ mp REAL_LE_RMUL THEN auto; mp REAL_MUL_LE_COMPAT_NEG_L THEN auto]);;
(* Second case for case distinction for SND iv2, 0 <= SND iv2 *)
e (ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (iv2:real#real) * SND (iv1:real#real)` THEN split THENL [mp REAL_LE_TRANS; ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN auto]);;
e (EXISTS_TAC `SND (iv2:real#real) * a:real` THEN split THENL [ mp REAL_LE_RMUL THEN auto; mp REAL_LE_LMUL THEN auto]);;
let interval_mult_valid = top_thm();;
let interval_mult_valid = prove (
`!(iv1:interval) (iv2:interval) (a:real) (b:real).
contained a iv1 /\
contained b iv2 ==>
contained (a * b) (multInterval iv1 iv2)`,
SIMP_TAC[contained; multInterval; absIntvUpd; IVlo; IVhi]
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 LABEL_TAC "min4_correct"
(SPECL
[`FST (iv1:real#real) * FST (iv2:real#real)`; `FST (iv1:real#real) * SND (iv2:real#real)`; `SND (iv1:real#real) * FST (iv2:real#real)`; `SND (iv1:real#real) * SND (iv2:real#real)`] min4_correct)
THEN LABEL_TAC "max4_correct" (SPECL [`FST (iv1:real#real) * FST (iv2:real#real)`; `FST (iv1:real#real) * SND (iv2:real#real)`; `SND (iv1:real#real) * FST (iv2:real#real)`; `SND (iv1:real#real) * SND (iv2:real#real)`] max4_correct)
THEN destruct "min4_correct" "leq_lolo leq_lohi leq_hilo leq_hihi"
THEN destruct "max4_correct" "lolo_leq lohi_leq hilo_leq hihi_leq"
THEN split
THENL [
(* Lower Bound *)
LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_a" "a_lt_0 | 0_leq_a"
THENL [
(* First case of outer case distinction, a < 0 *)
rewrite REAL_LT_LE "a_lt_0"
THEN destruct "a_lt_0" "a_le_0 a_neq_0"
THEN LABEL_TAC "cases_hi2" (SPECL [`(SND (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2"
THENL [
MATCH_MP_TAC REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv1:real#real) * SND (iv2:real#real)`
THEN split
THENL [
ASM_SIMP_TAC[];
ONCE_REWRITE_TAC [REAL_MUL_SYM]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv2:real#real) * (a:real)`
THEN split
THENL[
mp REAL_MUL_LE_COMPAT_NEG_L
THEN split THEN auto
THEN rewrite REAL_LT_LE "hi2_lt_0"
THEN destruct "hi2_lt_0" "hi2_le_0 hi2_neq_0"
THEN auto;
ONCE_REWRITE_TAC[REAL_MUL_SYM]
THEN mp REAL_MUL_LE_COMPAT_NEG_L
THEN split THEN auto
]
];
(* Second case of case distinction for SND iv2 *)
mp REAL_LE_TRANS
THEN EXISTS_TAC `(FST (iv1:real#real)) * SND (iv2:real#real)`
THEN split THEN TRY auto
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(a:real) * SND (iv2:real#real)`
THEN split
THENL [
mp REAL_LE_RMUL THEN auto;
mp REAL_MUL_LE_COMPAT_NEG_L THEN split THEN auto
]
];
(* Second case of case distinction for a, 0 <= a *)
LABEL_TAC "cases_lo2" (SPECL [`(FST (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2"
THENL [
(* First case of case distinction for fst iv2, fst iv2 < 0 *)
mp REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv1:real#real) * FST (iv2:real#real)`
THEN split THEN TRY auto
THEN mp REAL_LE_TRANS
THEN rewrite REAL_LT_LE "lo2_lt_0"
THEN destruct "lo2_lt_0" "lo2_le_0 lo2_neq_0"
THEN EXISTS_TAC `(a:real) * (FST (iv2:real#real))` THEN split
THENL [
ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN mp REAL_MUL_LE_COMPAT_NEG_L THEN auto;
mp REAL_LE_LMUL THEN auto];
(* Second case, 0 <= fst iv2 *)
mp REAL_LE_TRANS
THEN EXISTS_TAC `FST (iv1:real#real) * FST (iv2:real#real)`
THEN split THEN TRY auto
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `a:real * FST (iv2:real#real)`
THEN split
THENL [
mp REAL_LE_RMUL THEN auto ;
mp REAL_LE_LMUL THEN auto]
]
];
(* Upper Bound *)
LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_a" "a_lt_0 | 0_leq_a"
THENL [
(* First case for case distinction for a, a < 0 *)
rewrite REAL_LT_LE "a_lt_0"
THEN destruct "a_lt_0" "a_le_0 a_neq_0"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `a:real * FST (iv2:real#real)`
THEN split
THENL [
mp REAL_MUL_LE_COMPAT_NEG_L THEN split THEN auto;
LABEL_TAC "cases_lo2" (SPECL [`FST (iv2:real#real)`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2"
THENL [
(* First case of distinction for FST iv2, FST iv2 < 0 *)
rewrite REAL_LT_LE "lo2_lt_0"
THEN destruct "lo2_lt_0" "lo2_le_0 lo2_neq_0"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `FST (iv1:real#real) * FST (iv2:real#real)`
THEN split
THENL [
ONCE_REWRITE_TAC [REAL_MUL_SYM]
THEN mp REAL_MUL_LE_COMPAT_NEG_L
THEN split THEN auto;
auto];
(* Second case for case distinction for FST iv2, 0 <= FST iv2 *)
ONCE_REWRITE_TAC [REAL_MUL_SYM]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `FST (iv2:real#real) * SND (iv1:real#real)`
THEN split
THENL [
mp REAL_LE_LMUL THEN auto;
ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto
]
]
];
(* Second case for case distinction for a. 0 <= a *)
LABEL_TAC "cases_hi2" (SPECL [`(SND (iv2:real#real))`; `&0:real`] REAL_LTE_TOTAL)
THEN destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2"
THENL [
(* First case for case distinction for SND iv2, SND iv2 < 0 *)
ONCE_REWRITE_TAC [REAL_MUL_SYM]
THEN mp REAL_LE_TRANS
THEN rewrite REAL_LT_LE "hi2_lt_0"
THEN destruct "hi2_lt_0" "hi2_le_0 hi2_neq_0"
THEN EXISTS_TAC `SND (iv2:real#real) * FST (iv1:real#real)`
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv2:real#real) * a:real` THEN split
THENL [
mp REAL_LE_RMUL THEN auto;
mp REAL_MUL_LE_COMPAT_NEG_L THEN auto
];
ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto
];
(* Second case for case distinction for SND iv2, 0 <= SND iv2 *)
ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv2:real#real) * SND (iv1:real#real)`
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `SND (iv2:real#real) * a:real`
THEN split
THENL [
mp REAL_LE_RMUL THEN auto;
mp REAL_LE_LMUL THEN auto
];
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN auto]
]
]
]);;
let intv_div_err = define
`intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err)=
intv_mult_err I1 e1 ((&1) / IVlo (I2), (&1) / IVhi (I2)) e2`;;
let maxAbsFun = define
`maxAbsFun (iv:real#real) = max (abs (FST iv)) (abs (SND iv))`;;
let contained_leq_maxAbs = prove (
`! (a:real) ivlo ivhi.
contained a (ivlo, ivhi) ==>
(abs a <= maxAbsFun (ivlo, ivhi))`,
intros "!a ivlo ivhi; contained_a"
THEN rewrite contained "contained_a"
THEN rewrite IVlo "contained_a"
THEN rewrite IVhi "contained_a"
THEN rewrite SND "contained_a"
THEN SIMP_TAC[maxAbsFun]
THEN mp iv_le_maxAbs
THEN auto);;
let Rabs_error_bounded_maxAbs = prove (
`!(a:real) b eps ivlo ivhi.
(abs (a - b) <= eps) /\
contained a (ivlo, ivhi) ==>
(abs b <= abs (maxAbsFun (ivlo, ivhi) + eps))`,
intros "!a b eps ivlo ivhi; abs_le contained_a"
THEN SUBGOAL_TAC "a_bounded" `abs (a:real) <= maxAbsFun (ivlo, ivhi)` [mp contained_leq_maxAbs THEN auto]
THEN rewrite contained "contained_a"
THEN rewrite IVlo "contained_a"
THEN rewrite IVhi "contained_a"
THEN rewrite SND "contained_a"
THEN SIMP_TAC[maxAbsFun]
THEN rewrite REAL_ABS_SUB "abs_le"
THEN SUBGOAL_TAC "eps_simpl" `abs (b:real) - abs (a:real) <= eps`
[
mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (b - a)`
THEN split THEN auto
THEN SIMP_TAC[REAL_SUB_ABS]
]
THEN SUBGOAL_TAC "abs_flip" `abs (b:real) <= abs (a:real) + eps` [ASM_REAL_ARITH_TAC]
THEN SUBGOAL_TAC "abs_eps_le" `abs (a:real) + eps <= maxAbsFun (ivlo,ivhi) + eps`
[ ONCE_REWRITE_TAC [REAL_LE_RADD] THEN auto ]
THEN rewrite maxAbsFun "abs_eps_le"
THEN rewrite FST "abs_eps_le"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (a:real) + eps`
THEN split
THEN TRY auto
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `max (abs (ivlo:real)) (abs (ivhi:real)) + (eps:real)`
THEN split
THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]
);;
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