Commit 5f848dec authored by Heiko Becker's avatar Heiko Becker
Browse files

Some cleanup for interval Validator soundness and show multiplication errorbound

parent 65a8b699
......@@ -9,11 +9,6 @@ needs "Expressions.hl";;
let updEnv = define
`updEnv (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;;
(**
TODO: Check wether we need Rabs (n * machineEpsilon) instead
**)
let const_abs_err_bounded =
prove (
`!(n:real) (nR:real) (nF:real) (cenv:num ->real).
......@@ -32,10 +27,6 @@ let const_abs_err_bounded =
THEN MATCH_MP_TAC REAL_LE_LMUL
THEN ASM_REWRITE_TAC [REAL_ABS_POS]);;
(**
TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
(nlo <= cenv n <= nhi)%R -> (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
**)
let param_abs_err_bounded =
prove (
`!(n:num) (nR:real) (nF:real) (cenv:num->real).
......@@ -236,3 +227,68 @@ let sub_abs_err_bounded =
THEN split
THENL [
REAL_ARITH_TAC; auto]]]]]]);;
let mul_abs_err_bounded = prove (
`!(e1:(real)exp) (e1R:real) (e1F:real) (e2:(real)exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (err1:real) (err2:real).
eval_exp (&0) cenv e1 e1R /\
eval_exp machineEpsilon cenv e1 e1F /\
eval_exp (&0) cenv e2 e2R /\
eval_exp machineEpsilon cenv e2 e2F /\
eval_exp (&0) cenv (Binop Mult e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + abs (e1F * e2F) * machineEpsilon`,
intros "!e1 e1R e1F e2 e2R e2F vR vF cenv err1 err2; e1_real e1_float e2_real e2_float mult_real mult_float bound_e1 bound_e2"
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
THEN pose_proof binop_inv "mult_inv"
[`(&0):real`;`cenv:env_ty`; `Mult:binop`; `e1:(real)exp`; `e2:(real)exp`; `vR:real`] ["mult_real"]
THEN destruct "mult_inv" "@delta. @v1. @v2. vR_eq eval_v1 eval_v2 abs_leq_0"
THEN ASM_SIMP_TAC[]
THEN (USE_THEN "abs_leq_0"
(fun th -> REWRITE_TAC [MP (SPECL [`vR:real`; `delta:real`] perturb_0_val) th]))
THEN pose_proof eval_0_det "eval_e1_0_det"
[`e1:(real)exp`; `v1:real`; `e1R:real`; `cenv:num->real`] ["eval_v1"; "e1_real"]
THEN pose_proof eval_0_det "eval_e2_0_det" [`e2:(real)exp`; `v2:real`; `e2R:real`; `cenv:num->real`] ["eval_v2"; "e2_real"]
THEN ASM_SIMP_TAC[eval_binop]
THEN clear["abs_leq_0"; "eval_v1"; "eval_v2"; "eval_e1_0_det"; "eval_e2_0_det"]
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
THEN pose_proof binop_inv "mult_float_inv"
[`machineEpsilon:real`;`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`; `Mult:binop`; `(Var 1):(real)exp`; `(Var 2):(real)exp`; `vF:real`] ["mult_float"]
THEN destruct "mult_float_inv" "@delta1. @v1F. @v2F. vF_eq eval_v1F eval_v2F abs_leq_delta"
THEN ASM_SIMP_TAC[]
THEN pose_proof var_inv "v1F_inv" [`machineEpsilon:real`;
`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`;
`1:num`; `v1F:real`] ["eval_v1F"]
THEN pose_proof var_inv "v2F_inv" [`machineEpsilon:real`;
`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`;
`2:num`; `v2F:real`] ["eval_v2F"]
THEN ASM_REWRITE_TAC[updEnv; eval_binop; perturb]
(* TODO: Find out how to evaluate the conditional here! *)
THEN SUBGOAL_TAC "1_neq_2" `1:num = 2:num <=> F` [ARITH_TAC]
THEN ASM_REWRITE_TAC[]
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; REAL_NEG_ADD; real_sub]
THEN clear ["1_neq_2"; "v1F_inv"; "v2F_inv"; "eval_v1F"; "eval_v2F"]
THEN SUBGOAL_TAC "simplify_bound" `((e1R:real) * (e2R:real) + --((e1F:real) * (e2F:real)) + --(((e1F:real) * (e2F:real)) * (delta1:real))) = (((e1R:real) * (e2R:real) + --((e1F:real) * (e2F:real))) + --(((e1F:real) * (e2F:real)) * (delta1:real)))` [REAL_ARITH_TAC]
THEN USE_THEN "simplify_bound" (fun th -> ONCE_REWRITE_TAC[th])
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `abs ((e1R:real) * (e2R:real) + --((e1F:real) * (e2F:real))) +
abs (--(((e1F:real) * (e2F:real)) * (delta1:real)))`
THEN split
THENL [
REWRITE_TAC[REAL_ABS_TRIANGLE];
REWRITE_TAC[REAL_LE_LADD; REAL_ABS_NEG; REAL_ABS_MUL]
THEN mp REAL_LE_LMUL
THEN split
THENL [
REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_ABS_POS];
auto
]
]);;
(*
Some tactic aliases that ease the use
First some tactics that can only work on goals
*)
let intros t = INTRO_TAC t;;
let specialize thn t =
REMOVE_THEN thn (fun th -> LABEL_TAC thn (SPEC t th));;
let (split:xtactic) =
fun g ->
try (CONJ_TAC g) with
|Failure _ -> EQ_TAC g;;
(* TODO: make this tactic explicitly state where it fails to specialize!*)
let rec specl thn tlst =
match tlst with
| [] -> ALL_TAC
| hd :: tl -> specialize thn hd THEN specl thn tl;;
let reflexivity =
(CONV_TAC TAUT);;
let eq_give_goal (eq:term) (impl:term) proj =
SUBGOAL_TAC "" impl [ASSUME_TAC (proj (EQ_IMP_RULE (ASSUME eq))) THEN ASM_REWRITE_TAC[]]
THEN MATCH_MP_TAC (ASSUME impl)
THEN ASM_MESON_TAC[];;
let eq_give_left eq impl = eq_give_goal eq impl fst;;
let eq_give_right eq impl = eq_give_goal eq impl snd;;
let left = DISJ1_TAC;;
let right = DISJ2_TAC;;
let contradiction (t:term) (ty:string) =
SUBGOAL_TAC "" `F` [MP_TAC (ASSUME t) THEN ASM_REWRITE_TAC [distinctness ty]]
......@@ -31,49 +19,79 @@ let lcontradiction (asm:string) (ty:string) =
REMOVE_THEN asm
(fun th -> SUBGOAL_TAC "" `F` [MP_TAC th THEN ASM_REWRITE_TAC [distinctness ty]]
THEN FIRST_ASSUM CONTR_TAC);;
let reflexivity =
(CONV_TAC TAUT);;
let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
(* Abbreviation! *)
let lcontra asm ty = lcontradiction asm ty;;
(* Only assumption manipulating tactics *)
let destruct (asm:string) (patt:string) =
REMOVE_THEN asm (DESTRUCT_TAC patt);;
(* FIXME: Ugly hack because split is not a proper function here... *)
let split =
try (CONJ_TAC) with
|Failure _ -> EQ_TAC;;
(*let split () =
if (is_conj (snd (top_goal())))
then CONJ_TAC
else
(if (is_eq (snd (top_goal())))
then EQ_TAC
else failwith "No destructable equivalence found");;*)
let coq_eq_hol = prove(
`!A B P. (A ==> B ==> P) <=> (A /\ B ==> P)`,
intros "!A B P" THEN split
THENL [
intros "impl; conj"
THEN destruct "conj" "A B"
THEN ASM_SIMP_TAC[];
intros "conj; A; B"
THEN ASM_SIMP_TAC[]
]);;
let left = DISJ1_TAC;;
let right = DISJ2_TAC;;
(* A theorem conversion to generate a "coq Theorem" and then specialize it as it would work in coq *)
let intuitionisticThm = REWRITE_RULE[GSYM coq_eq_hol];;
(* A theorem conversion to go back to the HOL style, to not mess around with the theorem structure *)
let classicalThm = REWRITE_RULE[coq_eq_hol];;
(* 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]));;
(* Now some tactics that allow pfor proof styles similar to Coq's proof style *)
let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
(* Specialize a single theorem for a specific VARIABLE *)
let specialize thn t =
REMOVE_THEN thn (fun th -> LABEL_TAC thn (SPEC t th));;
(* TODO: make this tactic explicitly state where it fails to specialize!*)
let rec lspecialize thn tlst =
match tlst with
| [] -> ALL_TAC
| hd :: tl -> specialize thn hd THEN lspecialize thn tl;;
let mp = MATCH_MP_TAC;;
(* Similar semantics to "apply" in Coq *)
let mp_asm th = USE_THEN th (fun th -> mp th);;
let rec clear strlst =
match strlst with
| [] -> ALL_TAC
| hd :: tl -> REMOVE_THEN hd (fun th -> clear tl);;
(* Specialize a theorem, providing asm as first assumption to the assumption named thn for modus ponens rule *)
let mp_spec thn asm =
(* Use only the assumption with which thn is specialized *)
USE_THEN asm
(fun theAsm ->
(* thn will be assumed in a more special shape, so remove it in its current form *)
REMOVE_THEN thn
(fun thmToSpec ->
LABEL_TAC thn
(MP thmToSpec theAsm)));;
let mp_spec thn str =
USE_THEN str
(fun th1 ->
(* Specialize a theorem using intuitionistic reasoning,
providing asm as first assumption to the assumption named thn for modus ponens rule *)
let mp_ispec thn asm =
(* Use only the assumption with which thn is specialized *)
USE_THEN asm
(fun theAsm ->
(* thn will be assumed in a more special shape, so remove it in its current form *)
REMOVE_THEN thn
(fun th2 ->
(fun thmToSpec ->
LABEL_TAC thn
(MP th2 th1)));;
(classicalThm
(MP (intuitionisticThm thmToSpec) theAsm))));;
let rec mp_ispecl thn asmList =
match asmList with
| [] -> ALL_TAC
| asm :: asmList -> mp_ispec thn asm THEN mp_ispecl thn asmList;;
let spec thn varl =
REMOVE_THEN thn
......@@ -104,3 +122,15 @@ let pose_spec th varl asm name =
(fun asm ->
LABEL_TAC name
(MP (SPECL varl th) asm));;
(* Exactly the behaviour as pose proof in coq *)
let pose_proof thm name varl hypList =
pose thm varl name
THEN mp_ispecl name hypList;;
(* Maintenance Tactics *)
let rec clear strlst =
match strlst with
| [] -> ALL_TAC
| hd :: tl -> REMOVE_THEN hd (fun th -> clear tl);;
This diff is collapsed.
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