Commit 2232ce0f authored by Heiko Becker's avatar Heiko Becker
Browse files

Add unary negation to validated error bounds, since it is used in some of Daisys benchmarks.

Remove currently unused dependency on cakeml which came from merging with translation branch
Remove currently unu
parent 2ea56862
......@@ -23,7 +23,11 @@ Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):=
else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n =>
Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
|Unop _ _ => false
|Unop Neg e =>
if (validErrorbound e absenv dVars)
then Qeq_bool err (snd (absenv e))
else false
|Unop Inv e => false
|Binop b e1 e2 =>
if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars))
then
......@@ -80,7 +84,9 @@ Proof.
andb_to_prop validErrorbound_e.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- inversion R.
- destruct u; simpl in *; try congruence.
andb_to_prop R.
apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
Qed.
......@@ -1961,7 +1967,26 @@ Proof.
- unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error.
andb_to_prop valid_error.
inversion R.
destruct u; try congruence.
env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
rename R into valid_error.
andb_to_prop valid_error.
apply Qeq_bool_iff in R.
apply Qeq_eqR in R.
rewrite R.
destruct iv as [e_lo e_hi].
inversion eval_real; subst.
inversion eval_float; subst.
unfold evalUnop.
apply bound_flip_sub.
eapply IHe; eauto.
simpl in valid_intv.
rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
auto.
instantiate (1 := e_hi).
instantiate (1 := e_lo).
rewrite absenv_e; auto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
......
......@@ -24,7 +24,13 @@ val validErrorbound_def = Define `
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * machineEpsilon <= err)
| Const n => (maxAbs intv * machineEpsilon <= err)
| Unop op f => F
| Unop Neg f =>
if (validErrorbound f absenv dVars)
then
err = (SND (absenv f))
else
F
| Unop Inv f => F
| Binop op f1 f2 =>
(if (validErrorbound f1 absenv dVars /\ validErrorbound f2 absenv dVars)
then
......@@ -76,7 +82,7 @@ val err_always_positive = store_thm ("err_always_positive",
val validErrorboundCorrectVariable_ind = prove (
``!(E1 E2:env) absenv fVars dVars.
approxEnv E1 absenv fVars dVars E2 ==>
! (v:num) (nR nF err nlo nhi:real) (P:precond).
!(v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validIntervalbounds (Var v) absenv P dVars /\
......@@ -151,8 +157,8 @@ val validErrorboundCorrectVariable_ind = prove (
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
>- (rpt strip_tac
\\ rpt( first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin dVars ==> _` `v' IN domain dVars`
\\ rpt(first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domain dVars ==> _` `v' IN domain dVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
......@@ -180,7 +186,7 @@ val validErrorboundCorrectVariable_ind = prove (
>- (fs [validIntervalbounds_def, lookup_insert])
>- (fs [validErrorbound_def, lookup_insert])
>- (rpt strip_tac
\\ specialize `!v. v = _ \/ v IN domain _ ==> _` `v'`
\\ specialize `!v'. (v' = _) \/ v' IN domain _ ==> _` `v'`
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
......@@ -190,7 +196,7 @@ val validErrorboundCorrectVariable_ind = prove (
\\ fs [domain_insert]))
>- (rpt strip_tac
\\ rpt (first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin fVars ==> _` `v' IN domain fVars`
\\ specialize `v' IN domain fVars ==> _` `v' IN domain fVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
......@@ -2132,8 +2138,25 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ qpat_x_assum `absenv _ = _` (fn thm => fs[thm])
\\ first_x_assum match_mp_tac
\\ fs [usedVars_def, SUBSET_DEF])
>- (qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => fs[thm]))
>- (qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ qpat_x_assum `absenv _ = _` (fn thm => fs[thm])
\\ Cases_on `u` \\ fs []
\\ rveq
\\ Cases_on `absenv e`
\\ fs[]
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases
\\ fs [evalUnop_def]
\\ once_rewrite_tac [real_sub] \\ once_rewrite_tac [GSYM REAL_NEG_ADD]
\\ once_rewrite_tac [ABS_NEG]
\\ once_rewrite_tac [GSYM real_sub]
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`E1`, `E2`, `absenv`, `P`, `FST q`, `SND q`, `fVars`, `dVars`]
\\ fs [Once usedVars_def]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ fs []
\\ Cases_on `absenv e` \\ Cases_on `absenv (Unop Neg e)`
\\ fs [])
>- (rename1 `Binop op e1 e2`
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ rename1 `eval_exp 0 _ e1 nR1`
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -19,7 +19,6 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
Subproject commit df1790a2ee43b9d3c00d7b036784285b8f491c0f
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib std_preludeTheory;
val _ = new_theory "realProg";
val _ = translation_extends "std_prelude";
(* real_of_int *)
val real_of_int_def = Define `
real_of_int (i:int) = if i < 0 then - & (Num (-i)) else & (Num i):real`;
val real_of_int_num = store_thm("real_of_int_num[simp]",
``real_of_int (& n) = &n``,
rewrite_tac[real_of_int_def]
\\ Cases_on `&n`
\\ fs []);
val real_of_int_add = store_thm("real_of_int_add[simp]",
``real_of_int (m + n) = real_of_int m + real_of_int n``,
Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
\\ fs [integerTheory.INT_ADD_CALCULATE]
\\ rw [] \\ fs [] \\ fs [GSYM NOT_LESS,realTheory.add_ints]);
val real_of_int_neg = store_thm("real_of_int_neg[simp]",
``real_of_int (-m) = -real_of_int m``,
Cases_on `m` \\ fs [real_of_int_def]);
val real_of_int_sub = store_thm("real_of_int_sub[simp]",
``real_of_int (m - n) = real_of_int m - real_of_int n``,
fs [integerTheory.int_sub,realTheory.real_sub]);
val real_of_int_mul = store_thm("real_of_int_mul[simp]",
``real_of_int (m * n) = real_of_int m * real_of_int n``,
Cases_on `m` \\ Cases_on `n` \\ fs [real_of_int_def] \\ rw []
\\ fs [integerTheory.INT_MUL_CALCULATE]);
(* -- *)
val REAL_TYPE_def = Define `
REAL_TYPE (r:real) =
\v. ?(n:int) (d:num). (r = (real_of_int n) / (real_of_num d)) /\
PAIR_TYPE INT NUM (n,d) v /\ d <> 0`;
val _ = add_type_inv ``REAL_TYPE`` ``:(int # num)``;
val pair_of_num_def = Define `
pair_of_num n = ((& (n:num)):int, 1:num)`;
val pair_of_num_v_thm = translate pair_of_num_def;
val Eval_REAL_NUM = Q.prove(
`!v. (NUM --> PAIR_TYPE INT NUM) pair_of_num v ==>
(NUM --> REAL_TYPE) ($&) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ qexists_tac `& x` \\ qexists_tac `1`
\\ fs [pair_of_num_def] \\ fs [real_of_int_def])
|> (fn th => MATCH_MP th pair_of_num_v_thm)
|> add_user_proved_v_thm;
val pair_le_def = Define `
pair_le (n1,d1) (n2,d2) = (n1 * & d2 <= n2 * & d1)`;
val pair_le_v_thm = translate pair_le_def;
val Eval_REAL_LE = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> BOOL) pair_le v ==>
(REAL_TYPE --> REAL_TYPE --> BOOL) ($<=) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_le_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [BOOL_def] \\ rw [] \\ rveq
\\ EQ_TAC \\ rw []
\\ fs [realTheory.le_rat]
\\ Cases_on `n` \\ fs [real_of_int_def]
\\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rfs [realTheory.REAL_MUL_LNEG,integerTheory.INT_MUL_CALCULATE]
\\ qpat_x_assum `(_ <= _:int)` mp_tac
\\ fs [integerTheory.INT_NOT_LE])
|> (fn th => MATCH_MP th pair_le_v_thm)
|> add_user_proved_v_thm;
val pair_lt_def = Define `
pair_lt (n1,d1) (n2,d2) = (n1 * & d2 < n2 * & d1)`;
val pair_lt_v_thm = translate pair_lt_def;
val Eval_REAL_LT = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> BOOL) pair_lt v ==>
(REAL_TYPE --> REAL_TYPE --> BOOL) ($<) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_lt_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [BOOL_def] \\ rw [] \\ rveq
\\ EQ_TAC \\ rw []
\\ fs [realTheory.lt_rat]
\\ Cases_on `n` \\ fs [real_of_int_def]
\\ Cases_on `n'` \\ fs [real_of_int_def]
\\ rfs [realTheory.REAL_MUL_LNEG,integerTheory.INT_MUL_CALCULATE]
\\ qpat_x_assum `(_ <= _:int)` mp_tac
\\ fs [integerTheory.INT_NOT_LE])
|> (fn th => MATCH_MP th pair_lt_v_thm)
|> add_user_proved_v_thm;
val pair_add_def = Define `
pair_add (n1:int, d1:num) (n2, d2) = ((n1 * &d2) + (n2 * &d1),d1 * d2)`;
val pair_add_v_thm = translate pair_add_def;
val Eval_REAL_ADD = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_add v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($+) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_add_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * &d' + n' * &d`
\\ qexists_tac `d * d'`
\\ fs[real_of_int_add]
\\ fs [REAL_ADD_RAT]
\\ qspecl_then [`&d`, `real_of_int n'`] (fn thm => fs[Once thm]) REAL_MUL_COMM)
|> (fn th => MATCH_MP th pair_add_v_thm)
|> add_user_proved_v_thm;
val pair_sub_def = Define `
pair_sub (n1:int, d1:num) (n2, d2) = ((n1 * &d2) - (n2 * &d1),d1 * d2)`;
val pair_sub_v_thm = translate pair_sub_def;
val Eval_REAL_SUB = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_sub v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($-) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_sub_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * &d' - n' * &d`
\\ qexists_tac `d * d'`
\\ fs[real_of_int_sub]
\\ fs [real_sub, real_div, REAL_NEG_LMUL]
\\ fs [GSYM real_div]
\\ fs [REAL_ADD_RAT]
\\ qspecl_then [`&d`, `- real_of_int n'`] (fn thm => fs[Once thm]) REAL_MUL_COMM)
|> (fn th => MATCH_MP th pair_sub_v_thm)
|> add_user_proved_v_thm;
val real_neg_lem = prove(
``!(x:real). - x = 0 - x``,
fs[]);
val pair_neg_v_thm = translate real_neg_lem;
val pair_mul_def = Define `
pair_mul (n1,d1) (n2,d2) = (n1 * n2:int, d1 * d2:num)`;
val pair_mul_v_thm = translate pair_mul_def;
val Eval_REAL_MUL = Q.prove(
`!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_mul v ==>
(REAL_TYPE --> REAL_TYPE --> REAL_TYPE) ($*) v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
\\ disch_then (qspec_then `refs2` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ pop_assum mp_tac
\\ ntac 2 (qpat_x_assum `~_` mp_tac)
\\ rpt (pop_assum kall_tac)
\\ fs [PAIR_TYPE_def]
\\ rw [] \\ rveq \\ fs []
\\ qexists_tac `n * n'` \\ fs []
\\ qexists_tac `d * d'` \\ fs []
\\ fs [real_of_int_mul]
\\ match_mp_tac REAL_EQ_RMUL_IMP
\\ qexists_tac `&(d * d')`
\\ `&(d * d') 0:real` by fs []
\\ drule REAL_DIV_RMUL
\\ simp_tac std_ss [] \\ fs [] \\ rw []
\\ qabbrev_tac `n1 = real_of_int n`
\\ qabbrev_tac `n2 = real_of_int n'`
\\ once_rewrite_tac [EQ_SYM_EQ]
\\ `n1 / &d * (n2 / &d') * &(d * d') =
((n1 / &d) * &d) * ((n2 / &d') * &d')` by
(fs [AC REAL_MUL_ASSOC REAL_MUL_SYM]
\\ fs [REAL_MUL_ASSOC]
\\ fs [AC REAL_MUL_ASSOC REAL_MUL_SYM])
\\ pop_assum (fn th => rewrite_tac [th])
\\ `&d <> 0:real /\ &d' <> 0:real` by fs []
\\ fs [REAL_DIV_RMUL])
|> (fn th => MATCH_MP th pair_mul_v_thm)
|> add_user_proved_v_thm;
val pair_inv_def = Define `
pair_inv (n1,d1) =
(if n1 < 0 then - & d1 else & d1,num_of_int n1)`;
val pair_inv_v_thm = translate pair_inv_def;
val Eval_REAL_INV = Q.prove(
`PRECONDITION (r <> 0) ==>
!v. (PAIR_TYPE INT NUM --> PAIR_TYPE INT NUM) pair_inv v ==>
(Eq REAL_TYPE r --> REAL_TYPE) inv v`,
SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
pair_mul_def,FORALL_PROD,Eq_def,PRECONDITION_def] \\ rw [] \\ res_tac
\\ pop_assum (strip_assume_tac o SPEC_ALL)
\\ fs [] \\ asm_exists_tac \\ fs []
\\ rw [] \\ first_x_assum drule
\\ disch_then (qspec_then `refs` mp_tac)
\\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
\\ fs [realTheory.REAL_EQ_LDIV_EQ] \\ rveq
\\ fs [pair_inv_def,real_of_int_def]
\\ Cases_on `n` \\ fs []
THEN1
(qexists_tac `&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr])
THEN1
(qexists_tac `-&d`
\\ qexists_tac `n'` \\ fs []
\\ rewrite_tac [realTheory.REAL_INV_1OVER]
\\ fs [realTheory.div_ratr]
\\ fs [realTheory.neg_rat]))
|> UNDISCH
|> (fn th => MATCH_MP th pair_inv_v_thm)
|> add_user_proved_v_thm;
val _ = (next_ml_names := ["pair_div"])
val pair_div_v_thm = translate realTheory.real_div;
val pair_div_side_def = pair_div_v_thm
|> hyp |> hd |> rand |> repeat rator |> DB.match [] |> hd |> snd |> fst;
val pair_div_v_thm =
pair_div_v_thm
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val _ = export_theory();
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