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

Fix bug in IV Arith and prove nearly full IV checker

parent 5a981682
......@@ -74,3 +74,7 @@ let unfold thn th =
(fun th_old ->
LABEL_TAC thn
(REWRITE_RULE [th] th_old));;
let rewrite th asm =
REMOVE_THEN asm
(fun th_old -> LABEL_TAC asm (ONCE_REWRITE_RULE [th] th_old));;
......@@ -198,16 +198,16 @@ let multInterval = define
absIntvUpd ( * ) I1 I2`;;
g `!(iv1:interval) (iv2:interval) (a:real) (b:real).
contained a I1 /\
contained b I2 ==>
contained (a * b) (multInterval I1 I2)`;;
contained a iv1 /\
contained b iv2 ==>
contained (a * b) (multInterval iv1 iv2)`;;
e (SIMP_TAC[contained; multInterval; absIntvUpd; IVlo; IVhi]);;
e (intros "!a b; contained_a lo_leq_b b_leq_hi");;
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 (I1:real#real) * FST (I2:real#real)`; `FST (I1:real#real) * SND (I2:real#real)`; `SND (I1:real#real) * FST (I2:real#real)`; `SND (I1:real#real) * SND (I2:real#real)`] min4_correct));;
e (LABEL_TAC "max4_correct" (SPECL [`FST (I1:real#real) * FST (I2:real#real)`; `FST (I1:real#real) * SND (I2:real#real)`; `SND (I1:real#real) * FST (I2:real#real)`; `SND (I1:real#real) * SND (I2:real#real)`] max4_correct));;
[`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);;
......@@ -217,15 +217,15 @@ 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 (I2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
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 (I1:real#real) * SND (I2:real#real)`);;
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 (I2:real#real) * (a:real)`);;
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[]);;
......@@ -236,68 +236,68 @@ 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 I2 *)
(* Second case of case distinction for SND iv2 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `(FST (I1:real#real)) * SND (I2:real#real)`);;
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 (I2:real#real)`);;
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 (I2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
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 I2, fst I2 < 0 *)
(* First case of case distinction for fst iv2, fst iv2 < 0 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (I1:real#real) * FST (I2:real#real)`);;
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 (I2:real#real))` THEN split THENL
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 I2 *)
(* Second case, 0 <= fst iv2 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (I1:real#real) * FST (I2:real#real)` THEN split THEN TRY auto);;
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 (I2:real#real)` THEN split THENL [ mp REAL_LE_RMUL THEN auto ; mp REAL_LE_LMUL THEN auto]);;
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 (I2:real#real)` THEN split
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 (I2:real#real)`; `&0:real`] REAL_LTE_TOTAL));;
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 I2, FST I2 < 0 *)
(* 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 (I1:real#real) * FST (I2:real#real)` THEN split
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 I2, 0 <= FST I2 *)
(* 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 (I2:real#real) * SND (I1:real#real)` THEN split THENL [mp REAL_LE_LMUL THEN auto; ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto]);;
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 (I2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
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 I2, SND I2 < 0 *)
(* 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 (I2:real#real) * FST (I1:real#real)` THEN split THENL [ mp REAL_LE_TRANS ; ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN auto]);;
e (EXISTS_TAC `SND (I2:real#real) * a:real` THEN split
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 I2, 0 <= SND I2 *)
(* 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 (I2:real#real) * SND (I1:real#real)` THEN split THENL [mp REAL_LE_TRANS; ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN auto]);;
e (EXISTS_TAC `SND (I2:real#real) * a:real` THEN split THENL [ mp REAL_LE_RMUL THEN auto; mp REAL_LE_LMUL THEN auto]);;
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();;
......
......@@ -128,83 +128,106 @@ e (SUBGOAL_TAC "addition_valid2" `FST
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.
(FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))` [USE_THEN "addition_valid" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
e (clear ["addition_valid"]);;
e (rewrite IVlo "valid_bin");;
e (rewrite IVhi "valid_bin");;
e (USE_THEN "absenv_bin_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (rewrite FST "valid_bin");;
e (destruct "addition_valid2" "add_le_v1v2 v1v2_le_add");;
e (destruct "valid_bin" "lo_le_add add_le_hi");;
e (split);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (addInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (addInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
(* Subtraction *)
e (USE_THEN "a0_Sub" (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 "subtraction_valid"
(REWRITE_RULE [validIntervalSub; contained]
(SPECL
[`FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))`;
`FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))`] interval_subtraction_valid)));;
e (specl "subtraction_valid" [`v1:real`; `v2:real`]);;
e (clear [ "valid_rec1"; "valid_rec2"; "IH1"; "IH2"]);;
e (unfold "valid_bin" isSupersetInterval);;
e (unfold "subtraction_valid" IVlo);;
e (unfold "subtraction_valid" IVhi);;
e (SUBGOAL_TAC "subtraction_valid2" `FST (subtractInterval (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 (subtractInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp)))
(FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))` [USE_THEN "subtraction_valid" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
e (clear ["subtraction_valid"]);;
e (rewrite IVlo "valid_bin");;
e (rewrite IVhi "valid_bin");;
e (USE_THEN "absenv_bin_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (rewrite FST "valid_bin");;
e (destruct "subtraction_valid2" "sub_le_v1v2 v1v2_le_sub");;
e (destruct "valid_bin" "lo_le_sub sub_le_hi");;
e (split);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (subtractInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (subtractInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
(* Multiplication case *)
e (USE_THEN "a0_Mult" (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]);;
interval_mult_valid;;
e (LABEL_TAC "mult_valid"
(REWRITE_RULE [contained]
(SPECL
[`FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))`;
`FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))`; `v1:real`; `v2:real` ] interval_mult_valid)));;
e (clear [ "valid_rec1"; "valid_rec2"; "IH1"; "IH2"]);;
e (unfold "valid_bin" isSupersetInterval);;
e (unfold "mult_valid" IVlo);;
e (unfold "mult_valid" IVhi);;
show_types();;
e (SUBGOAL_TAC "mult_valid2" `FST
(multInterval
(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
(multInterval
(FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp)))
(FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))` [USE_THEN "mult_valid" (fun th -> MATCH_MP_TAC th) THEN split THEN auto]);;
e (clear ["mult_valid"]);;
e (rewrite IVlo "valid_bin");;
e (rewrite IVhi "valid_bin");;
e (USE_THEN "absenv_bin_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (USE_THEN "absIv_def" (fun th -> rewrite th "valid_bin"));;
e (rewrite FST "valid_bin");;
e (destruct "mult_valid2" "mult_le_v1v2 v1v2_le_mult");;
e (destruct "valid_bin" "lo_le_mult mult_le_hi");;
e (split);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (multInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (multInterval (FST ((absenv:(real)exp->(real#real)#real) (a1:(real)exp))) (FST ((absenv:(real)exp->(real#real)#real) (a2:(real)exp))))`);;
e (split THEN auto);;
(* Division Case *)
(*** TODO ***)
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