Commit 369a1703 authored by Heiko Becker's avatar Heiko Becker

Merge with Nikitas FMA proofs

parents 235270e4 97b9a584
open preamble
open MachineTypeTheory ExpressionAbbrevsTheory
val _ = new_theory "DaisyMap";
val _ = Datatype `
cmp = Lt | Eq | Gt`;
val expCompare_def = Define `
expCompare (e1:real exp) e2 =
case e1, e2 of
|(Var (n1:num)), (Var n2) =>
if (n1 < n2)
then Lt
else
if (n1 = n2) then Eq else Gt
| (Var n), _ => Lt
| (Const _ _), Var _ => Gt
| Const m1 v1, Const m2 v2 =>
if m1 = m2
then
(if (v1 < v2)
then Lt
else if (v1 = v2)
then Eq
else Gt)
else (if morePrecise m1 m2 then Lt else Gt)
| Const _ _, _ => Lt
| Unop u1 e1, Unop u2 e2 =>
if u1 = u2
then expCompare e1 e2
else (if u1 = Neg then Lt else Gt)
| Unop _ _, Binop _ _ _ => Lt
| Unop _ _, Downcast _ _ => Lt
| Unop _ _, _ => Gt
| Downcast m1 e1, Downcast m2 e2 =>
if m1 = m2
then expCompare e1 e2
else (if morePrecise m1 m2 then Lt else Gt)
| Downcast _ _, Binop _ _ _ => Lt
| Downcast _ _, _ => Gt
| Binop b1 e11 e12, Binop b2 e21 e22 =>
let res = case b1, b2 of
| Plus, Plus => Eq
| Plus, _ => Lt
| Sub, Sub => Eq
| Sub, Plus => Gt
| Sub, _ => Lt
| Mult, Mult => Eq
| Mult, Div => Lt
| Mult, _ => Gt
| Div, Div => Eq
| Div, _ => Gt
in
(case res of
| Eq =>
(case expCompare e11 e21 of
| Eq => expCompare e12 e22
| Lt => Lt
| Gt => Gt)
| _ => res)
|_ , _ => Gt`;
val DaisyMapList_insert_def = Define `
(DaisyMapList_insert e k NIL = [(e,k)]) /\
(DaisyMapList_insert e k ((e1,l1) :: el) =
case expCompare e e1 of
| Lt => (e,k)::(e1,l1)::el
| Eq => (e1,l1) :: el
| Gt => (e1,l1):: DaisyMapList_insert e k el)`;
val DaisyMapList_find_def = Define `
(DaisyMapList_find e NIL = NONE) /\
(DaisyMapList_find e ((e1,k)::el) = if expCompare e e1 = Eq then SOME k else DaisyMapList_find e el)`;
val _ = Datatype `
binTree = Node 'a binTree binTree | Leaf 'a | LeafN`;
val DaisyMapTree_insert_def = Define `
(DaisyMapTree_insert e k LeafN = Leaf (e,k)) /\
(DaisyMapTree_insert e k (Leaf (e1,k1)) =
case (expCompare e e1) of
| Lt => Node (e1,k1) (Leaf (e,k)) (LeafN)
| Eq => Leaf (e1,k1)
| Gt => Node (e1,k1) (LeafN) (Leaf (e,k))) /\
(DaisyMapTree_insert e k (Node (e1,k1) tl tr) =
case (expCompare e e1) of
| Lt => Node (e1,k1) (DaisyMapTree_insert e k tl) tr
| Eq => (Node (e1, k1) tl tr)
| Gt => Node (e1,k1) tl (DaisyMapTree_insert e k tr))`;
val DaisyMapTree_find_def = Define `
(DaisyMapTree_find e (LeafN) = NONE) /\
(DaisyMapTree_find e (Leaf (e1,k1)) =
if expCompare e e1 = Eq then SOME k1 else NONE) /\
(DaisyMapTree_find e (Node (e1,k1) tl tr) =
case (expCompare e e1) of
| Lt => DaisyMapTree_find e tl
| Eq => SOME k1
| Gt => DaisyMapTree_find e tr)`;
val DaisyMapTree_mem_def = Define `
DaisyMapTree_mem e tMap =
case (DaisyMapTree_find e tMap) of
| SOME _ => T
| _ => F`;
val DaisyMapTree_empty_def = Define `
DaisyMapTree_empty = LeafN `;
val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``);
val _ = type_abbrev ("analysisResult", ``:(real exp # ((real # real) # real)) binTree``);
val _ = export_theory();
open preamble
open simpLib realTheory realLib RealArith sptreeTheory
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyTactics
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyTactics DaisyMapTheory
val _ = new_theory "Environments";
......@@ -15,9 +15,11 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(abs (v1 - v2) <= abs v1 * (mTypeToQ m)) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x iv err.
approxEnv E1 defVars A fVars dVars E2 /\
(abs (v1 - v2) <= SND (A (Var x))) /\
DaisyMapTree_find (Var x) A = SOME (iv, err) /\
abs (v1 - v2) <= err /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (insert x () dVars) (updEnv x v2 E2))`;
......@@ -86,41 +88,41 @@ val approxEnv_fVar_bounded = store_thm (
\\ fs[]));
val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
``!E1 Gamma absenv fVars dVars E2 x v v2 m e.
approxEnv E1 Gamma absenv fVars dVars E2 /\
``!E1 Gamma A fVars dVars E2 x v v2 m iv e.
approxEnv E1 Gamma A fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
SND (absenv (Var x)) = e ==>
DaisyMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e``,
rpt strip_tac
\\ qspec_then
`\E1 Gamma absenv fVars dVars E2.
`\E1 Gamma A fVars dVars E2.
!x v v2 m.
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
SND (absenv (Var x)) = e ==>
DaisyMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e`
(fn thm => irule (SIMP_RULE std_ss [] thm))
(fn thm => destruct (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
>- (fs [emptyEnv_def])
>- (fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
>- (first_x_assum irule \\ fs[updDefVars_def]
>- (rpt conj_tac
>- (fs [emptyEnv_def])
>- (rpt strip_tac \\ fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
\\ first_x_assum irule \\ fs[updDefVars_def]
\\ rename1 `defVars x2 = SOME m2` \\ qexistsl_tac [`m2`, `x2`]
\\ fs[])
>- (rpt strip_tac \\ fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC \\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexistsl_tac [`m1`,`x1`]
\\ fs[]))
>- (fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC
\\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexistsl_tac [`m1`,`x1`]
\\ fs[])
>- (qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `m`, `x`]
\\ fs[]));
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then MATCH_ACCEPT_TAC);
val _ = export_theory ();;
......@@ -10,7 +10,7 @@ open preamble
open simpLib realTheory realLib RealArith pred_setTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory DaisyMapTheory
val _ = new_theory "ErrorValidation";
......@@ -18,42 +18,43 @@ val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val validErrorbound_def = Define `
validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)=
let (intv, err) = absenv e in
let mopt = typeMap e in
case mopt of
| NONE => F
| SOME m =>
if (0 <= err) then
validErrorbound e (typeMap: (real exp # mType) binTree) (A:analysisResult) (dVars:num_set)=
case DaisyMapTree_find e A, DaisyMapTree_find e typeMap of
| SOME (intv, err), SOME m =>
(if (0 <= err) then
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (mTypeToQ m) <= err)
| Const _ n => (maxAbs intv * (mTypeToQ m) <= err)
| Unop Neg f =>
if (validErrorbound f typeMap absenv dVars) then
err = (SND (absenv f))
else
F
| Unop Inv f => F
| Binop op f1 f2 =>
(if (validErrorbound f1 typeMap absenv dVars /\ validErrorbound f2 typeMap absenv dVars) then
let (ive1, err1) = absenv f1 in
let (ive2, err2) = absenv f2 in
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Div =>
(if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
then
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err)
else F)
| Unop Neg e1 =>
if (validErrorbound e1 typeMap A dVars)
then
case (DaisyMapTree_find e1 A) of
| SOME (_, err1) => err = err1
| _ => F
else F
| Unop Inv e1 => F
| Binop op e1 e2 =>
(if (validErrorbound e1 typeMap A dVars /\ validErrorbound e2 typeMap A dVars)
then
case DaisyMapTree_find e1 A, DaisyMapTree_find e2 A of
| SOME (ive1, err1), SOME (ive2, err2) =>
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
(case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Div =>
(if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
then
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err)
else F))
| _, _ => F
else F)
| Fma f1 f2 f3 =>
(if (validErrorbound f1 typeMap absenv dVars /\
......@@ -73,21 +74,27 @@ val validErrorbound_def = Define `
(err1 + mult_error_bound + (maxAbs (addInterval errIve1 errIntv_prod)) * (mTypeToQ m)) <= err
else F)
| Downcast m1 e1 =>
let (ive1, err1) = absenv e1 in
let rec_res = validErrorbound e1 typeMap absenv dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err)
else F`;
case DaisyMapTree_find e1 A of
| SOME (ive1, err1) =>
let rec_res = validErrorbound e1 typeMap A dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err)
else F)
| _, _ => F`;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (typeMap: real exp -> mType option) (env:analysisResult) (dVars:num_set)=
validErrorboundCmd (f:real cmd) (typeMap: (real exp # mType) binTree)
(A:analysisResult) (dVars:num_set) =
case f of
| Let m x e g =>
if (validErrorbound e typeMap env dVars /\ (env e = env (Var x))) then
validErrorboundCmd g typeMap env (insert x () dVars)
else F
(case DaisyMapTree_find e A, DaisyMapTree_find (Var x) A of
| SOME (iv_e, err_e), SOME (iv_x, err_x) =>
if (validErrorbound e typeMap A dVars /\ err_e = err_x)
then validErrorboundCmd g typeMap A (insert x () dVars)
else F
| _ , _ => F)
| Ret e =>
validErrorbound e typeMap env dVars`;
validErrorbound e typeMap A dVars`;
val err_always_positive = store_thm (
"err_always_positive",
......
......@@ -11,6 +11,7 @@ val _ = new_theory "ExpressionAbbrevs"
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``);
(* val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``); *)
val _ = export_theory()
......@@ -112,4 +112,81 @@ fun daisy_eval_tac t :tactic=
\\ fs[sptreeTheory.lookup_def]
end;
(* Daisy Compute Tactic as in Coq dev to simplify goals involving computations *)
fun iter n s f =
if n = 0 then s
else iter (n - 1) (f s) f;
fun getArgTypeList t num lst =
let val (name, list) = dest_type t in
case name of
"fun" =>
let
val (hdty, tylist) = (hd list, tl list) in
getArgTypeList (hd tylist) (num + 1) (hdty :: lst)
end
| _ => (num, rev lst)
end
fun getPatTerm t =
let
val decl_list = decls (term_to_string t);
val argTypes_list = map (fn t => getArgTypeList (#Ty (dest_thy_const t)) 0 []) decl_list in
if length decl_list = 1
then
let
val (cnt, tyList) = hd argTypes_list
in
iter cnt (hd decl_list, tyList)
(fn (t,tyList) =>
let
val var = mk_var ("_",hd tyList) in
(* val _ = print_term var; *)
(* val _ = print_term t in *)
(mk_comb (t, var), tl tyList)
end)
end
else raise ERR "Too many constants" ""
end;
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];
fun add_unevaluated_function (t:term) :unit =
eval_funs := t :: (!eval_funs);
fun Daisy_compute t =
let
val eval_thm = DB.theorem ((term_to_string t)^"_def");
val (pat,_) = getPatTerm t in
TRY (
Tactical.PAT_X_ASSUM
pat
(fn thm =>
let
val rwthm = ONCE_REWRITE_RULE [eval_thm] thm;
val compute_thm = computeLib.RESTR_EVAL_RULE (!eval_funs) rwthm in
assume_tac compute_thm end)
\\ fs[]
\\ TRY (
REPEAT (
((qpat_assum `option_CASE _ _ _`
(fn thm =>
let
val (t,t2,_) = optionSyntax.dest_option_case (concl thm) in
Cases_on `^t2` \\ fs[] end))
ORELSE
(split_pair_case_tac)) \\ fs[])))
end;
(* val Daisy_compute:tactic = *)
(* fn (g:goal) => *)
(* let *)
(* val terms_to_eval = !eval_funs in *)
(* if (length terms_to_eval = 0) *)
(* then let val _ = print "Nothing to evaluate" in ALL_TAC g end *)
(* else *)
(* Daisy_compute_steps terms_to_eval g *)
(* end; *)
end
......@@ -41,6 +41,41 @@ val mTypeToQ_pos = store_thm("mTypeToQ_pos",
val isMorePrecise_def = Define `
isMorePrecise (m1:mType) (m2:mType) = (mTypeToQ (m1) <= mTypeToQ (m2))`;
val morePrecise_def = Define `
(morePrecise M0 _ = T) /\
(morePrecise M16 M16 = T) /\
(morePrecise M32 M32 = T) /\
(morePrecise M32 M16 = T) /\
(morePrecise M64 M0 = F) /\
(morePrecise M64 _ = T) /\
(morePrecise _ _ = F) `;
val morePrecise_antisym = store_thm (
"morePrecise_antisym",
``!m1 m2.
morePrecise m1 m2 /\
morePrecise m2 m1 ==>
m1 = m2``,
rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]);
val morePrecise_trans = store_thm (
"morePrecise_trans",
``!m1 m2 m3.
morePrecise m1 m2 /\
morePrecise m2 m3 ==>
morePrecise m1 m3``,
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[morePrecise_def]);
val isMorePrecise_morePrecise = store_thm (
"isMorePrecise_morePrecise",
``!m1 m2.
isMorePrecise m1 m2 = morePrecise m1 m2``,
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2`
\\ fs[morePrecise_def, isMorePrecise_def, mTypeToQ_def]);
val M0_least_precision = store_thm ("M0_least_precision",
``!(m:mType).
isMorePrecise m M0 ==>
......@@ -62,7 +97,7 @@ val M0_lower_bound = store_thm ("M0_lower_bound",
**)
val join_def = Define `
join (m1:mType) (m2:mType) =
if (isMorePrecise m1 m2) then m1 else m2`;
if (morePrecise m1 m2) then m1 else m2`;
val join3_def = Define `
join3 (m1: mType) (m2: mType) (m3: mType) = join m1 (join m2 m3)`;
......
This diff is collapsed.
......@@ -27,6 +27,15 @@ val REAL_INV_LE_ANTIMONO_IMPR = store_thm ("REAL_INV_LE_ANTIMONO_IMPR",
``! x y. 0 < x /\ 0 < y /\ y <= x ==> inv x <= inv y``,
rpt strip_tac \\ fs[REAL_INV_LE_ANTIMONO]);
val REAL_INV_LE_ANTIMONO_IMPL = store_thm ("REAL_INV_LE_ANTIMONO_IMPL",
``! x y. x <0 /\ y < 0 /\ y <= x ==> inv x <= inv y``,
rpt strip_tac
\\ once_rewrite_tac [GSYM REAL_LE_NEG]
\\ `- inv y = inv (- y)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- inv x = inv (- x)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ ntac 2(FIRST_X_ASSUM (fn thm => once_rewrite_tac [ thm]))
\\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]);
val REAL_MUL_LE_COMPAT_NEG_L = store_thm( "REAL_MUL_LE_COMPAT_NEG_L",
``!(a:real) b c. a <= &0 /\ b <= c ==> a * c <= a * b``,
rpt strip_tac
......
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