Commit 354c9cfb authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove interval multiplication in HOL correct

parent f464b139
......@@ -37,3 +37,12 @@ let split = CONJ_TAC;;
let left = DISJ1_TAC;;
let right = DISJ2_TAC;;
(* From John Harrisons tutorial, with a sligh modification *)
let assume lab t =
DISCH_THEN(fun th -> if concl th = t then LABEL_TAC lab th
else failwith (String.concat("Cannot assume ") [string_of_term t]));;
let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
let mp = MATCH_MP_TAC;;
......@@ -214,6 +214,9 @@ 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 (I2:real#real))`; `&0:real`] REAL_LTE_TOTAL));;
e (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
e (MATCH_MP_TAC REAL_LE_TRANS);;
......@@ -222,24 +225,82 @@ e (split);;
e (ASM_SIMP_TAC[]);;
e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);;
e (MATCH_MP_TAC REAL_LE_TRANS);;
e (EXISTS_TAC `(a:real) * SND (I2:real#real)`);;
e (EXISTS_TAC `SND (I2:real#real) * (a:real)`);;
e (split);;
(** TODO!!! **)
e (MATCH_MP_TAC (SPECL [`a:real`; `b:real`; `SND (I2:real#real)`] REAL_MUL_LE_COMPAT_NEG_L));;
SPECL [`a:real`; `b:real`; `SND (I2:real#real)`] REAL_MUL_LE_COMPAT_NEG_L;;
REAL_MUL_LE_COMPAT_NEG_L;;
e
(*
TODO FIXME!
e (MATCH_MP_TAC REAL_MULT_LE);;
search [`(x:real)*y <= w* z`];;
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 I2 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `(FST (I1:real#real)) * SND (I2:real#real)`);;
e (split THEN TRY auto);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `(a:real) * SND (I2: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 (destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2");;
(* First case of case distinction for fst I2, fst I2 < 0 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `SND (I1:real#real) * FST (I2: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
[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 *)
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `FST (I1:real#real) * FST (I2: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]);;
(* 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
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 (destruct "cases_lo2" "lo2_lt_0 | 0_leq_lo2");;
(* First case of distinction for FST I2, FST I2 < 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
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 *)
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]);;
(* 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 (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
(* First case for case distinction for SND I2, SND I2 < 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
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 *)
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]);;
let interval_mult_valid = top_thm();;
search [`(<=):real->real->bool`];;
*)
e (CHEAT_TAC);;
e (CHEAT_TAC);;
e (CHEAT_TAC);;
e (CHEAT_TAC);;
let intv_div_err = define
`intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err)=
......
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