Commit 17650bfc authored by Heiko Becker's avatar Heiko Becker

Merge hol4 certificate checking into fork master

parents 88c19995 139e47af
......@@ -23,6 +23,10 @@ hol4/*Theory*
hol4/*.ui
hol4/*.uo
hol4/.*
hol4/*/*Theory*
hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/heap
daisy
rawdata/*
......
......@@ -92,12 +92,13 @@ Lemma validErrorboundCorrectConstant:
Proof.
intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
unfold validErrorbound in error_valid.
rewrite absenv_const in error_valid.
inversion eval_real; subst.
rewrite delta_0_deterministic in eval_real; auto.
rewrite delta_0_deterministic; auto.
clear delta H0.
inversion eval_float; subst.
pose proof (validIntervalbounds_sound (Const n) absenv P cenv (Q2R n) intv_valid eval_real) as iv_valid.
rewrite absenv_const in *; simpl in *.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl.
unfold Qleb in error_valid.
......@@ -106,27 +107,17 @@ Proof.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans.
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | ].
apply H0.
rewrite Rabs_eq_Qabs.
rewrite Q2R_mult in error_valid.
eapply Rle_trans.
eapply Rmult_le_compat_r.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
assert (Qle_bool 0 (1 # (2^53)) = true) by (unfold Qle_bool; auto).
rewrite <- Qle_bool_iff; auto.
rewrite absenv_const in intv_valid.
simpl in intv_valid.
andb_to_prop intv_valid.
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 *; simpl in *;
[destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
- rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | eauto ].
- rewrite Q2R_mult in error_valid.
eapply Rle_trans.
+ eapply Rmult_le_compat_r.
apply mEps_geq_zero.
destruct iv_valid.
apply RmaxAbs; eauto.
+ rewrite <- maxAbs_impl_RmaxAbs in error_valid.
unfold RmaxAbsFun in error_valid.
auto.
Qed.
Lemma validErrorboundCorrectParam:
......@@ -179,6 +170,7 @@ Proof.
rewrite <- H8;unfold RmaxAbsFun;simpl;auto.
Qed.
(* TODO: Maybe extract subproof for ivbounds of operands into main lemma *)
Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
......@@ -196,17 +188,10 @@ Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 n
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Plus e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply add_abs_err_bounded.
apply e1_real.
apply e1_float.
apply e2_real.
apply e2_float.
apply eval_real.
apply eval_float.
apply err1_bounded.
apply err2_bounded.
apply
(add_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P (Q2R err1) (Q2R err2));
try auto.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
......@@ -277,7 +262,6 @@ Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_sub
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Sub e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply subtract_abs_err_bounded.
apply e1_real.
......@@ -363,7 +347,6 @@ Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_mult
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Mult e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply (mult_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto.
unfold validErrorbound in valid_error at 1.
......@@ -419,6 +402,8 @@ Proof.
assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as zero_up_nR1 by lra.
assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as nR1_to_sum by lra.
assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R as sum_to_errsum by lra.
clear e1_real e1_float e2_real e2_float eval_real eval_float valid_error
absenv_e1 absenv_e2.
(* Large case distinction for
a) different cases of the value of Rabs (...) and
b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
......@@ -739,6 +724,7 @@ Proof.
apply H.
lra.
}
(* All positive *)
+ assert (nF1 <= Q2R err1 + nR1)%R by lra.
assert (nF2 <= Q2R err2 + nR2)%R by lra.
unfold Rabs.
......@@ -872,51 +858,6 @@ Proof.
repeat rewrite Q2R_plus; auto.
Qed.
Lemma err_prop_inversion_pos_down nF2 nR2 err2 (e2lo e2hi :Q)
(float_iv_pos : (Q2R 0 < Q2R (e2lo - err2))%R)
(real_iv_pos : (Q2R 0 < Q2R e2lo)%R)
(r0 : (nR2 - nF2 < 0)%R)
(err2_bounded : (- nR2 + nF2 <= Q2R err2)%R)
(valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R)
(valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R)
(err2_pos : (0 <= Q2R err2)%R):
( - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) <= / nF2 - / nR2)%R.
Proof.
assert (nF2 <= Q2R err2 + nR2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (0 < nR2 - Q2R err2)%R.
- rewrite <- Q2R0_is_0.
eapply Rlt_le_trans.
apply float_iv_pos.
rewrite Q2R_minus; lra.
- assert (0 < nF2)%R by (rewrite <- Q2R0_is_0; lra).
apply Rinv_le_contravar in H; try auto.
apply Rinv_le_contravar in H0; try auto.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
Focus 2.
eapply Rplus_le_compat_r.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (Q2R err2 + nR2 + - nR2 = Q2R err2)%R by lra.
rewrite H3.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
+ rewrite <- Ropp_mult_distr_r. apply Ropp_le_contravar.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
* rewrite <- Rsub_eq_Ropp_Rplus.
apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra.
* eapply Rmult_le_compat; try lra;
rewrite <- Rsub_eq_Ropp_Rplus;
rewrite <- Q2R_minus, <- Q2R0_is_0; lra.
+ assert (0 < (Q2R err2 + nR2) * nR2)%R.
* apply Rmult_0_lt_preserving; lra.
* lra.
Qed.
Lemma validErrorboundCorrectDiv cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
......@@ -936,7 +877,6 @@ Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_div
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Div e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
apply (div_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P); auto.
unfold validErrorbound in valid_error at 1;
......@@ -983,7 +923,7 @@ Proof.
apply Rplus_le_compat.
(* Error Propagation proof *)
+ clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
e1_real e2_float e2_real env_approx_p absenv_div
e1_real e2_float e2_real absenv_div
valid_err_e1 valid_err_e2 cenv absenv alo ahi nR nF e1 e2 e P.
unfold IntervalArith.contained, widenInterval in *.
simpl in *.
......@@ -1012,7 +952,8 @@ Proof.
as bound_neg_nR1
by (apply Rmult_le_compat_r; auto).
unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2.
(* Case distinction for the divisor range *)
(* Case distinction for the divisor range
positive or negative in float and real valued execution *)
destruct no_div_zero_real as [ real_iv_neg | real_iv_pos];
destruct no_div_zero_float as [float_iv_neg | float_iv_pos].
(* The range of the divisor lies in the range from -infinity until 0 *)
......@@ -1040,6 +981,7 @@ Proof.
assert (nF1 <= Q2R err1 + nR1)%R as ub_nF1 by lra.
assert (nR1 - Q2R err1 <= nF1)%R as lb_nF1 by lra.
destruct err2_bounded as [[nR2_sub_pos err2_bounded] | [nR2_sub_neg err2_bounded]].
(* Positive case for abs (nR2 - nF2) <= err2 *)
{ rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive.
apply Rgt_lt in nR2_sub_pos.
assert (nF2 < nR2)%R as nF2_le_nR2 by lra.
......@@ -1056,10 +998,12 @@ Proof.
(* Next do a case distinction for the absolute value*)
unfold Rabs.
destruct Rcase_abs.
(* Case 1: Absolute value negative *)
- rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr.
rewrite Ropp_involutive.
(* To upper bound terms, do a case distinction for nF1 *)
destruct (Rle_lt_dec 0 nF1).
(* 0 <= nF1 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_l; try lra.
......@@ -1085,7 +1029,8 @@ Proof.
apply lb_nF1.
rewrite (Rmult_comm (Q2R err2) _).
remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv.
assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) = nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R
assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) =
nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R
as simpl_properr by lra.
rewrite simpl_properr.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -1102,6 +1047,7 @@ Proof.
- assert (0 <= (Q2R err1 * err_inv))%R
by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra).
apply (Rle_trans _ 0); lra. }
(* nF1 < 0 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_neg_l; try lra.
......@@ -1146,9 +1092,10 @@ Proof.
{ apply Rmult_le_compat_r; try lra. }
{ apply Rmult_le_compat_r; try lra.
repeat (rewrite Q2R_inv; try auto). }
- rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_mult_distr_l.
(* Case 2: Absolute value positive *)
- rewrite Rsub_eq_Ropp_Rplus, Ropp_mult_distr_l.
destruct (Rle_lt_dec 0 (- nF1)).
(* 0 <= - nF1 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_l; try lra.
......@@ -1192,6 +1139,7 @@ Proof.
- assert (0 <= (Q2R err1 * err_inv))%R
by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra).
apply (Rle_trans _ 0); lra. }
(* - nF1 <= 0 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_neg_l; try lra.
......
(**
This file contains the HOL4 implementation of the certificate checker as well as its soundness proof.
The checker is a composition of the range analysis validator and the error bound validator.
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory ErrorValidationTheory
val _ = new_theory "CertificateChecker";
(** Certificate checking function **)
val CertificateChecker_def = Define
`CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) =
((validIntervalbounds e absenv P) /\ (validErrorbound e absenv))`;
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
``!(e:real exp) (absenv:analysisResult) P (cenv:env) (vR:real) (vF:real).
eval_exp 0 cenv P e vR /\
eval_exp machineEpsilon cenv P e vF /\
CertificateChecker e absenv P ==>
abs (vR - vF) <= (SND (absenv e))``,
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
simp [CertificateChecker_def] \\
rpt strip_tac \\
Cases_on `absenv e` \\
rename1 `absenv e = (iv, err)` \\
Cases_on `iv` \\
rename1 `absenv e = ((elo, ehi), err)` \\
match_mp_tac validErrorbound_sound \\
qexistsl_tac [`e`, `cenv`, `absenv`, `P`, `elo`, `ehi`] \\
fs[]);
val _ = export_theory();
This diff is collapsed.
This diff is collapsed.
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple common
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \
combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \
listTheory llistTheory markerLib realTheory realLib RealArith\
optionTheory pairLib pairTheory pred_setTheory \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith common/preamble
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
(**
Formalization of real valued interval arithmetic
Used in soundness proofs for error bound validator.
**)
open preamble
open realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory;
val _ = new_theory "IntervalArith";
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
**)
val valid_def = Define `
valid (iv:interval) = (IVlo iv <= IVhi iv)`;
val contained_def = Define `
contained (a:real) (iv:interval) = (IVlo iv <= a /\ a <= IVhi iv)`;
(**
Subset definition; when an interval is a subinterval of another
**)
val isSupersetInterval_def = Define `
isSupersetInterval (iv1:interval) (iv2:interval) =
((IVlo iv2 <= IVlo iv1) /\ (IVhi iv1 <= IVhi iv2))`;
val pointInterval_def = Define `pointInterval (x:real) = (x,x)`;
(**
Definitions of validity conditions for interval operations: Addition,
Subtraction, Multiplication and Division
**)
val validIntervalAdd_def = Define `
validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a + b) iv3)`;
val validIntervalSub_def = Define `
validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a - b) iv3)`;
val validIntervalMult_def = Define`
validIntervalMult (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a * b) iv3)`;
val validIntervalDiv_def = Define `
validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a / b) iv3)`;
val min4_def = Define `
min4 a b c d = min a (min b (min c d))`;
val max4_def = Define `
max4 a b c d = max a (max b (max c d))`;
val absIntvUpd_def = Define `
absIntvUpd (op:real->real->real) (iv1:interval) (iv2:interval) =
(
min4 (op (IVlo iv1) (IVlo iv2))
(op (IVlo iv1) (IVhi iv2))
(op (IVhi iv1) (IVlo iv2))
(op (IVhi iv1) (IVhi iv2)),
max4 (op (IVlo iv1) (IVlo iv2))
(op (IVlo iv1) (IVhi iv2))
(op (IVhi iv1) (IVlo iv2))
(op (IVhi iv1) (IVhi iv2))
)`;
val widenInterval_def = Define `
widenInterval (iv:interval) (v:real) = ((IVlo iv - v), (IVhi iv + v))`;
val negateInterval_def = Define `
negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))`;
val invertInterval_def = Define `
invertInterval (iv:interval) = (inv (IVhi iv), inv (IVlo iv))`;
val addInterval_def = Define `
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`;
val subtractInterval_def = Define `
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)`;
val multInterval_def = Define `
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
val maxAbsFun_def = Define `
maxAbsFun iv = max (abs (FST iv)) (abs (SND iv))`;
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_def,
pointInterval_def, validIntervalAdd_def,
validIntervalSub_def, validIntervalMult_def,
validIntervalDiv_def,
min4_def, max4_def,
absIntvUpd_def, widenInterval_def,
negateInterval_def,
invertInterval_def,
addInterval_def, subtractInterval_def,
multInterval_def, divideInterval_def,
maxAbsFun_def, minAbsFun_def
];
val contained_implies_valid = store_thm ("contained_implies_valid",
``!(a:real) (iv:interval).
contained a iv ==> valid iv``,
metis_tac (iv_ss @ [REAL_LE_TRANS]));
val contained_implies_subset = store_thm ("contained_implies_subset",
``!(a:real) (iv:interval).
contained a iv ==> isSupersetInterval (pointInterval a) iv``,
fs iv_ss);
val validPointInterval = store_thm("validPointInterval",
``!(a:real).
contained a (pointInterval a)``,
fs iv_ss);
val min4_correct = store_thm ("min4_correct",
``!a b c d.
let m = min4 a b c d in
m <= a /\ m <= b /\ m <= c /\ m <= d``,
rpt strip_tac \\fs [min4_def] \\ conj_tac \\
try (fs [REAL_MIN_LE1]) \\ conj_tac
>- (`min b (min c d) <= b` by fs[REAL_MIN_LE1] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_MIN_LE2])
>- (conj_tac
>- (`min c d <= c` by fs [REAL_MIN_LE1] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_MIN_LE2] \\
match_mp_tac REAL_LE_TRANS \\
`min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\
HINT_EXISTS_TAC \\
fs [REAL_MIN_LE2] )
>- (`min c d <= d` by fs [REAL_MIN_LE2] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_MIN_LE2] \\
match_mp_tac REAL_LE_TRANS \\
`min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\
HINT_EXISTS_TAC \\
fs [REAL_MIN_LE2])));
val max4_correct = store_thm ("max4_correct",
``!a b c d.
let m = max4 a b c d in
a <= m /\ b <= m /\ c <= m /\ d <= m``,
rpt strip_tac \\fs [max4_def] \\ conj_tac \\
try (fs [REAL_LE_MAX1]) \\ conj_tac
>-(`b <= max b (max c d)` by fs[REAL_LE_MAX1] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2])
>- (conj_tac
>- (`c <= max c d` by fs [REAL_LE_MAX1] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2] \\
match_mp_tac REAL_LE_TRANS \\
`max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2] )
>- (`d <= max c d` by fs [REAL_LE_MAX2] \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2] \\
match_mp_tac REAL_LE_TRANS \\
`max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\
HINT_EXISTS_TAC \\
fs [REAL_LE_MAX2] )));
val interval_negation_valid = store_thm ("interval_negation_valid",
``!iv a.
contained a iv ==> contained (- a) (negateInterval iv)``,
fs iv_ss);
val interval_inversion_valid = store_thm ("interval_inversion_valid",
``!iv a.
(IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==>
contained (inv a) (invertInterval iv)``,
fs iv_ss \\ rpt strip_tac
(* First subgoal *)
>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\
`0 < - a` by REAL_ASM_ARITH_TAC \\
`a <> 0` by REAL_ASM_ARITH_TAC \\
`0 < - SND iv` by REAL_ASM_ARITH_TAC \\
`SND iv <> 0` by REAL_ASM_ARITH_TAC \\
`-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp[]) \\
`-(SND iv)⁻¹ = (-(SND iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\
asm_rewrite_tac [] \\
`inv(-a) inv (-SND iv) <=> (- SND iv) <= - a` by match_mp_tac REAL_INV_LE_ANTIMONO \\ fs [])
(* Second subgoal *)
>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\
`a < 0` by REAL_ASM_ARITH_TAC \\
`0 < -a` by REAL_ASM_ARITH_TAC \\
`- a <> 0` by REAL_ASM_ARITH_TAC \\
`a <> 0` by REAL_ASM_ARITH_TAC \\
`-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\
`-(FST iv)⁻¹ = (-(FST iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp [] \\
try REAL_ASM_ARITH_TAC \\ asm_rewrite_tac []) \\
`inv (- (FST iv)) <= inv (- a) <=> - a <= - (FST iv)`
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
REAL_ASM_ARITH_TAC)
(* Third subgoal *)
>- (rewrite_tac [GSYM REAL_INV_1OVER] \\
`inv (SND iv) <= inv a <=> a <= SND iv`
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
REAL_ASM_ARITH_TAC)
(* Fourth subgoal *)
>- (rewrite_tac [GSYM REAL_INV_1OVER] \\
`inv a <= inv (FST iv) <=> FST iv <= a`
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
REAL_ASM_ARITH_TAC));
val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
fs iv_ss \\ rpt strip_tac
(* First subgoal, lower bound *)
>- (`FST iv1 + FST iv2 <= a + b`
by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\ strip_tac \\ fs[REAL_MIN_LE1])
(* Second subgoal, upper bound *)
>- (`a + b <= SND iv1 + SND iv2`
by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX]));
val interval_subtraction_valid = store_thm ("interval_subtraction_valid",
``!iv1 iv2.
validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``,
rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_sub]) \\
rpt gen_tac \\ strip_tac \\
(** TODO: FIXME, use qspecl_then or sth else **)
match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\
fs []);
val interval_multiplication_valid = store_thm ("interval_multiplication_valid",
``!iv1 iv2 a b.
contained a iv1 /\ contained b iv2 ==> contained (a * b) (multInterval iv1 iv2)``,
fs iv_ss \\ rpt strip_tac
(* Lower Bound *)
(* Case distinction for a *)
>- (qspecl_then [`a`,`0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* First case: a < 0 *)
>- (`a <= 0 /\ a <> 0` by fs[REAL_LT_LE] \\
(* Case distinction for SND iv2 *)
qspecl_then [`SND iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* First case: SND iv2 < 0 *)