Commit 9ef2537b authored by Heiko Becker's avatar Heiko Becker
Browse files

Update to latest HOL4 version, remove cakeml submodule, add dependency to CAKEMLDIR variable

parent 91790db5
[submodule "hol4/cakeml"]
branch = master
path = hol4/cakeml
url = https://github.com/CakeML/cakeml.git
[submodule "daisy"]
branch = certified
path = daisy
......
4f67f38e1314dcb1488b3925ddbbc4bbd80795bf
9eb85f2893da888359e9bff54ed3bca6467523d1
This diff is collapsed.
This diff is collapsed.
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic cakeml/misc
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra \
$(CAKEMLDIR)/translator $(CAKEMLDIR)/basis \
$(CAKEMLDIR)/characteristic $(CAKEMLDIR)/misc
OPTIONS = QUIT_ON_FAILURE
#ifdef POLY
......
......@@ -10,6 +10,7 @@ open preamble;
val _ = new_theory "IEEE_connection";
val _ = temp_overload_on("abs",``real$abs``);
val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
(** FloVer assumes rounding with ties to even, thus we exprlicitly define
a rounding mode here **)
......@@ -214,8 +215,8 @@ val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finitenes
\\ qexists_tac `minValue_pos M64` \\ fs[]
\\ irule REAL_LET_TRANS \\ qexists_tac `maxValue M64`
\\ `minValue_pos M64 <= 1`
by (once_rewrite_tac [GSYM REAL_INV1]
\\ fs[minValue_pos_def, minExponentPos_def]
by (fs[minValue_pos_def, minExponentPos_def]
\\ once_rewrite_tac [GSYM REAL_INV1]
\\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[threshold_64_bit_lt_maxValue]
\\ irule REAL_LE_TRANS \\ qexists_tac `1`
......@@ -335,7 +336,8 @@ val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
\\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ fs[]
by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM]
\\ rewrite_tac[REAL_INV1] \\ asm_exists_tac \\ fs[]
\\ qmatch_goalsub_abbrev_tac `cst1 < cst2`
\\ `0 <= (1:real) + &n / 4503599627370496`
by (irule REAL_LE_ADD \\ fs[real_div]
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../cakeml/basis ../cakeml/characteristic ../cakeml/misc
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple \
$(CAKEMLDIR)/basis $(CAKEMLDIR)/characteristic $(CAKEMLDIR)/misc
OPTIONS = QUIT_ON_FAILURE
......@@ -53,9 +53,7 @@ Theorem computeError_up:
computeError v m <= computeError (maxAbs (a,b)) m
Proof
rpt strip_tac \\ Cases_on `m`
\\ fs[mTypeToR_def, computeError_def]
\\ irule REAL_LE_RMUL_IMP \\ fs[]
\\ fs[maxAbs_def]
\\ fs[mTypeToR_def, computeError_def, maxAbs_def]
\\ irule REAL_LE_TRANS \\ asm_exists_tac
\\ fs[ABS_LE]
QED
......@@ -108,122 +106,136 @@ Proof
\\ fs[morePrecise_def]
QED
val isMorePrecise_morePrecise = store_thm (
"isMorePrecise_morePrecise",
``!m1 m2.
isMorePrecise m1 m2 = morePrecise m1 m2``,
Theorem isMorePrecise_morePrecise:
!m1 m2.
isMorePrecise m1 m2 = morePrecise m1 m2
Proof
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2`
\\ once_rewrite_tac [morePrecise_def, isMorePrecise_def]
\\ fs[morePrecise_def, isMorePrecise_def, mTypeToR_def]);
\\ fs[morePrecise_def, isMorePrecise_def, mTypeToR_def]
QED
val isMorePrecise_refl = store_thm (
"isMorePrecise_refl",
``!m. isMorePrecise m m``,
Cases_on `m` \\ EVAL_TAC \\ fs[]);
Theorem isMorePrecise_refl:
!m. isMorePrecise m m
Proof
Cases_on `m` \\ EVAL_TAC \\ fs[]
QED
val REAL_least_precision = store_thm ("REAL_least_precision",
``!(m:mType).
isMorePrecise m REAL ==> m = REAL``,
Theorem REAL_least_precision:
!(m:mType).
isMorePrecise m REAL ==> m = REAL
Proof
fs [isMorePrecise_def, mTypeToR_def]
\\ rpt strip_tac
\\ Cases_on `m`
\\ fs []);
\\ fs []
QED
val REAL_lower_bound = store_thm ("REAL_lower_bound",
``!(m:mType).
isMorePrecise REAL m``,
Cases_on `m` \\ EVAL_TAC);
Theorem REAL_lower_bound:
!(m:mType).
isMorePrecise REAL m
Proof
Cases_on `m` \\ EVAL_TAC
QED
(**
Function computing the join of two precisions, this is the most precise type,
in which evaluation has to be performed, e.g. addition of 32 and 64 bit floats
has to happen in 64 bits
**)
val join_fl_def = Define `
Definition join_fl_def:
join_fl (F w1 f1) (F w2 f2) = NONE /\
join_fl m1 m2 = if (morePrecise m1 m2) then SOME m1 else SOME m2`;
join_fl m1 m2 = if (morePrecise m1 m2) then SOME m1 else SOME m2
End
val join_fl3_def = Define `
join_fl3 m1 m2 m3 =
do mj <- join_fl m1 m2; join_fl mj m3; od`;
Definition join_fl3_def:
join_fl3 m1 m2 m3 = do mj <- join_fl m1 m2; join_fl mj m3; od
End
(** Since we cannot compute a join for Fixed-Points, we give a
isJoin predicate which returns true for fixed-points, but needs to inspect
it for floating-points **)
val isCompat_def = Define `
Definition isCompat_def:
isCompat (REAL) (REAL) = T /\
isCompat (F w1 f1) (F w2 f2) = morePrecise (F w1 f1) (F w2 f2) /\
isCompat (F _ _) _ = F /\
isCompat _ (F _ _) = F /\
isCompat m1 m2 = (m1 = m2)`;
isCompat m1 m2 = (m1 = m2)
End
val isJoin_def = Define `
Definition isJoin_def:
isJoin m1 m2 mj =
if (isFixedPoint m1 /\ isFixedPoint m2)
then morePrecise m1 mj /\ morePrecise m2 mj
else
(case join_fl m1 m2 of
|NONE => F
|SOME mNew => mNew = mj) `;
|SOME mNew => mNew = mj)
End
val isJoin3_def = Define `
Definition isJoin3_def:
isJoin3 m1 m2 m3 mj =
if (isFixedPoint m1 /\ isFixedPoint m2 /\ isFixedPoint m3)
then morePrecise m1 mj /\ morePrecise m2 mj /\ morePrecise m3 mj
else
(case join_fl3 m1 m2 m3 of
|NONE => F
|SOME mNew => mNew = mj) `;
|SOME mNew => mNew = mj)
End
val maxExponent_def = Define `
Definition maxExponent_def:
(maxExponent (REAL) = 0n) /\
(maxExponent (M16) = 15) /\
(maxExponent (M32) = 127) /\
(maxExponent (M64) = 1023) /\
(maxExponent (F w f) = f)`;
(maxExponent (F w f) = f)
End
val minExponentPos_def = Define `
Definition minExponentPos_def:
(minExponentPos (REAL) = 0n) /\
(minExponentPos (M16) = 14) /\
(minExponentPos (M32) = 126) /\
(minExponentPos (M64) = 1022) /\
(minExponentPos (F w f) = f)`;
(minExponentPos (F w f) = f)
End
(**
Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)
which simplifies to 2^(e_max) for base 2
**)
val maxValue_def = Define `
Definition maxValue_def:
maxValue (m:mType) =
case m of
| F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
| _ => (&(2n ** (maxExponent m))):real`;
| _ => (&(2n ** (maxExponent m))):real
End
(** Using the sign bit, the very same number is representable as a negative number,
thus just apply negation here **)
val minValue_pos_def = Define `
Definition minValue_pos_def:
minValue_pos (m:mType) =
case m of
| F w f => 0
| _ => inv (&(2n ** (minExponentPos m)))`;
| _ => inv (&(2n ** (minExponentPos m)))
End
(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
**)
val normal_def = Define `
Definition normal_def:
normal (v:real) (m:mType) =
(minValue_pos m <= abs v /\ abs v <= maxValue m)`;
(minValue_pos m <= abs v /\ abs v <= maxValue m)
End
val denormal_def = Define `
Definition denormal_def:
denormal (v:real) (m:mType) =
case m of
| REAL => F
| _ => ((abs v) < (minValue_pos m) /\ v <> 0)`;
| _ => ((abs v) < (minValue_pos m) /\ v <> 0)
End
(**
Predicate that is true if and only if the given value v is a valid
......@@ -231,21 +243,24 @@ val denormal_def = Define `
Since we use the 1 + 𝝳 abstraction, the value must either be
in normal range or 0.
**)
val validFloatValue_def = Define `
Definition validFloatValue_def:
validFloatValue (v:real) (m:mType) =
case m of
| REAL => T
| _ => normal v m \/ denormal v m \/ v = 0`
| _ => normal v m \/ denormal v m \/ v = 0
End
val validValue_def = Define `
Definition validValue_def:
validValue (v:real) (m:mType) =
case m of
| REAL => T
| _ => abs v <= maxValue m`;
| _ => abs v <= maxValue m
End
val no_underflow_fixed_point = store_thm (
"no_underflow_fixed_point",
``!v f w. ~ denormal v (F w f)``,
fs[denormal_def, minValue_pos_def, REAL_NOT_LT, REAL_ABS_POS]);
Theorem no_underflow_fixed_point:
!v f w. ~ denormal v (F w f)
Proof
fs[denormal_def, minValue_pos_def, REAL_NOT_LT, REAL_ABS_POS]
QED
val _ = export_theory();
......@@ -15,28 +15,34 @@ val _ = temp_overload_on("min",``real$min``);
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)`;
Definition valid_def:
valid (iv:interval) = (IVlo iv <= IVhi iv)
End
val contained_def = Define `
contained (a:real) (iv:interval) = (IVlo iv <= a /\ a <= IVhi iv)`;
Definition contained_def:
contained (a:real) (iv:interval) = (IVlo iv <= a /\ a <= IVhi iv)
End
(**
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))`;
Definition isSupersetInterval_def:
isSupersetInterval (iv1:interval) (iv2:interval) =
((IVlo iv2 <= IVlo iv1) /\ (IVhi iv1 <= IVhi iv2))
End
val pointInterval_def = Define `pointInterval (x:real) = (x,x)`;
Definition pointInterval_def:
pointInterval (x:real) = (x,x)
End
(**
Definitions of validity conditions for interval operations: Addition,
Subtraction, Multiplication and Division
**)
val validIntervalAdd_def = Define `
Definition validIntervalAdd_def:
validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) =
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a + b) iv3)`;
(! a b. contained a iv1 /\ contained b iv2 ==> contained (a + b) iv3)
End
val validIntervalSub_def = Define `
validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) =
......@@ -50,15 +56,17 @@ 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))`;
Definition min4_def:
min4 a b c d = min a (min b (min c d))
End
val max4_def = Define `
max4 a b c d = max a (max b (max c d))`;
Definition max4_def:
max4 a b c d = max a (max b (max c d))
End
val absIntvUpd_def = Define `
absIntvUpd (op:real->real->real) (iv1:interval) (iv2:interval) =
(
Definition absIntvUpd_def:
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))
......@@ -67,39 +75,48 @@ absIntvUpd (op:real->real->real) (iv1:interval) (iv2:interval) =
(op (IVlo iv1) (IVhi iv2))
(op (IVhi iv1) (IVlo iv2))
(op (IVhi iv1) (IVhi iv2))
)`;
)
End
val widenInterval_def = Define `
widenInterval (iv:interval) (v:real) = ((IVlo iv - v), (IVhi iv + v))`;
Definition widenInterval_def:
widenInterval (iv:interval) (v:real) = ((IVlo iv - v), (IVhi iv + v))
End
val negateInterval_def = Define `
negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))`;
Definition negateInterval_def:
negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))
End
val invertInterval_def = Define `
invertInterval (iv:interval) = (1 /(IVhi iv), 1 /(IVlo iv))`;
Definition invertInterval_def:
invertInterval (iv:interval) = (1 /(IVhi iv), 1 /(IVlo iv))
End
val addInterval_def = Define `
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`;
Definition addInterval_def:
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2
End
add_unevaluated_function ``addInterval``;
val subtractInterval_def = Define `
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)`;
Definition subtractInterval_def:
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)
End
add_unevaluated_function ``subtractInterval``;
val multInterval_def = Define `
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
Definition multInterval_def:
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2
End
add_unevaluated_function ``multInterval``;
val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
Definition divideInterval_def:
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)
End
add_unevaluated_function ``divideInterval``;
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
Definition minAbsFun_def:
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))
End
val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_def,
pointInterval_def, validIntervalAdd_def,
......@@ -114,10 +131,12 @@ val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_de
maxAbs_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]));
Theorem contained_implies_valid:
!(a:real) (iv:interval).
contained a iv ==> valid iv
Proof
metis_tac (iv_ss @ [REAL_LE_TRANS])
QED
val contained_implies_subset = store_thm ("contained_implies_subset",
``!(a:real) (iv:interval).
......@@ -185,7 +204,6 @@ 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)``,
......@@ -302,150 +320,106 @@ val iv_sub_preserves_valid = store_thm ("iv_sub_preserves_valid",
\\ conj_tac \\ fs []
\\ match_mp_tac iv_neg_preserves_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 *)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``SND (iv1:interval) * SND (iv2:interval)`` \\
conj_tac
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
min4_correct)
>- (once_rewrite_tac[REAL_MUL_SYM] \\
match_mp_tac REAL_LE_TRANS \\
exists_tac ``SND (iv2:interval) * (a:real)`` \\
conj_tac
>- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
fs [REAL_LT_LE])
>- (once_rewrite_tac [REAL_MUL_SYM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
fs [])))
(* Second case: 0 <= SND iv2 *)
>- (match_mp_tac REAL_LE_TRANS\\
exists_tac ``FST (iv1:interval) * SND (iv2:interval)`` \\
conj_tac
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
min4_correct)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``(a:real) * SND (iv2:interval)`` \\
conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L])))
(* Second case: 0 <= a*)
(* Case distinction for FST iv2 *)
>- (qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* First case: FST iv2 < 0 *)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\
conj_tac
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
min4_correct)
>- (once_rewrite_tac [REAL_MUL_SYM] \\
match_mp_tac REAL_LE_TRANS \\
exists_tac ``FST (iv2:interval) * (a:real)`` \\
conj_tac
>- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE])
>- (fs [REAL_LE_RMUL_IMP])))
(* Second case: 0 <= FST iv2 *)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\
conj_tac
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)])
min4_correct)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``a:real * FST (iv2:interval)`` \\
conj_tac \\ fs [REAL_LE_RMUL_IMP, REAL_LE_LMUL_IMP]))))
(* Upper 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] \\
Theorem interval_multiplication_valid:
!iv1 iv2 a b.
contained a iv1 /\ contained b iv2 ==>
contained (a * b) (multInterval iv1 iv2)
Proof
fs iv_ss \\ rpt strip_tac
(* Lower Bound *)
(* Case distinction for a *)
>- (
qspecl_then [`a`,`0`] assume_tac REAL_LTE_TOTAL \\ fs[]
(* First case: a < 0 *)
>- (
`a <= 0 /\ a <> 0` by fs[REAL_LT_LE]
(* Case distinction for SND iv2 *)
qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* First case: FST iv2 < 0 *)
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\
conj_tac
>- (once_rewrite_tac[REAL_MUL_SYM] \\
match_mp_tac REAL_LE_TRANS \\
exists_tac ``FST (iv2:interval) * (a:real)`` \\
conj_tac
>- (once_rewrite_tac [REAL_MUL_SYM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
fs [])
>- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
fs [REAL_LT_LE]))
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
max4_correct))
(* Second case: 0 <= FST iv2 *)
>- (match_mp_tac REAL_LE_TRANS\\
exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\
conj_tac
>- (match_mp_tac REAL_LE_TRANS \\
exists_tac ``(a:real) * FST (iv2:interval)`` \\
conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L])
>- (qspecl_then
[`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`]
(fn thm =>
rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
max4_correct)))
\\ qspecl_then [`SND iv2`, `0`] assume_tac REAL_LTE_TOTAL \\ fs[]
(* First case: SND iv2 < 0 *)
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `SND iv1 * SND iv2`
\\ conj_tac
>- metis_tac [CONV_RULE (DEPTH_CONV let_CONV) min4_correct, min4_def]
\\ irule REAL_LE_TRANS
\\ qexists_tac `a * SND iv2` \\ conj_tac
>- (
once_rewrite_tac[REAL_MUL_SYM]
\\ irule REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE])
\\ irule REAL_MUL_LE_COMPAT_NEG_L
\\ fs [REAL_LT_LE])
(* Second case: 0 <= SND iv2 *)
\\ irule REAL_LE_TRANS
\\ qexists_tac `FST iv1 * SND iv2` \\ conj_tac
>- metis_tac [CONV_RULE (DEPTH_CONV let_CONV) min4_correct, min4_def]
\\ irule REAL_LE_TRANS
\\ qexists_tac `a * SND iv2` \\ conj_tac
\\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L])
(* Second case: 0 <= a*)
(* Case distinction for FST iv2 *)
\\ qspecl_then [`FST iv2`, `0`] assume_tac REAL_LTE_TOTAL \\ fs[]
>- (
irule REAL_LE_TRANS
\\ qexists_tac `FST iv2 * SND iv1`
\\ conj_tac