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

Refactor some proofs into prove calls, add old apply proofs to attic

parent bd8d9fd6
g `!eps env v val.
eval_exp eps env (Var v) val ==> val = env v`;;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env v val; cases_exp");;
e (destruct "cases_exp" "varc | constc | binopc");;
e (destruct "varc" "@v2. var_eq val_eq");;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
e (destruct "constc" "@n. @d. var_eq _ _");;
e (contradiction `Var (v:num) = Const (n:real)` "exp");;
e (destruct "binopc" "@b. @e1. @e2. @v1. @v2. @d. var_eq _ _ _ _");;
e (contradiction `Var (v:num) = Binop (b:binop) (e1:(real)exp) (e2:(real)exp)` "exp");;
let var_inv = top_thm();;
g `!eps env n v.
eval_exp eps env (Const n) v ==> ?d. v = perturb n d /\ abs d <= eps`;;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env n v; cases_exp");;
e (destruct "cases_exp" "varc | constc | binopc");;
e (destruct "varc" "@v. const_eq _");;
e (lcontradiction "const_eq" "exp");;
e (destruct "constc" "@n2. @d. c_eq v_eq abs_less");;
e (EXISTS_TAC `d:real`);;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
e (destruct "binopc" "@b. @e1. @e2. @v1. @v2. @d. const_eq _ _ _ _");;
e (lcontradiction "const_eq" "exp");;
let const_inv = top_thm();;
......@@ -53,51 +53,72 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
abs delta <= eps ==>
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;;
g `!eps env v val.
eval_exp eps env (Var v) val ==> val = env v`;;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env v val; cases_exp");;
e (destruct "cases_exp" "varc | constc | binopc");;
e (destruct "varc" "@v2. var_eq val_eq");;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
e (destruct "constc" "@n. @d. var_eq _ _");;
e (contradiction `Var (v:num) = Const (n:real)` "exp");;
e (destruct "binopc" "@b. @e1. @e2. @v1. @v2. @d. var_eq _ _ _ _");;
e (contradiction `Var (v:num) = Binop (b:binop) (e1:(real)exp) (e2:(real)exp)` "exp");;
let var_inv = top_thm();;
let var_inv =
prove
(`!eps env v val.
eval_exp eps env (Var v) val ==> val = env v`,
ONCE_REWRITE_TAC
[eval_exp_CASES] THEN
INTRO_TAC "!eps env v val; cases_exp" THEN
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | constc | binopc") THENL
[REMOVE_THEN "varc" (DESTRUCT_TAC "@v2. var_eq val_eq") THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "constc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN
SUBGOAL_TAC "" `F`
[MP_TAC (ASSUME `Var (v:num) = Const (n:real)`) THEN
ASM_REWRITE_TAC [distinctness "exp"]];
REMOVE_THEN "binopc"
(DESTRUCT_TAC "@b. @e1. @e2. @v1. @v2. @d. var_eq _ _ _ _") THEN
SUBGOAL_TAC "" `F`
[MP_TAC
(ASSUME
`Var (v:num) = Binop (b:binop) (e1:(real)exp) (e2:(real)exp)`) THEN
ASM_REWRITE_TAC [distinctness "exp"]]] THEN
FIRST_ASSUM CONTR_TAC);;
g `!eps env n v.
eval_exp eps env (Const n) v ==> ?d. v = perturb n d /\ abs d <= eps`;;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env n v; cases_exp");;
e (destruct "cases_exp" "varc | constc | binopc");;
e (destruct "varc" "@v. const_eq _");;
e (lcontradiction "const_eq" "exp"));;
e (destruct "constc" "@n2. @d. c_eq v_eq abs_less");;
e (EXISTS_TAC `d:real`);;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
e (destruct "binopc" "@b. @e1. @e2. @v1. @v2. @d. const_eq _ _ _ _");;
e (lcontradiction "const_eq" "exp"));;
let const_inv = top_thm();;
let const_inv =
prove
(`!eps env n v.
eval_exp eps env (Const n) v ==> ?d. v = perturb n d /\ abs d <= eps`,
ONCE_REWRITE_TAC
[eval_exp_CASES] THEN
INTRO_TAC "!eps env n v; cases_exp" THEN
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | constc | binopc") THENL
[REMOVE_THEN "varc" (DESTRUCT_TAC "@v. const_eq _") THEN
REMOVE_THEN "const_eq"
(fun th ->
SUBGOAL_TAC "" `F`
[MP_TAC th THEN ASM_REWRITE_TAC [distinctness "exp"]] THEN
FIRST_ASSUM CONTR_TAC);
REMOVE_THEN "constc" (DESTRUCT_TAC "@n2. @d. c_eq v_eq abs_less") THEN
EXISTS_TAC `d:real` THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "binopc"
(DESTRUCT_TAC "@b. @e1. @e2. @v1. @v2. @d. const_eq _ _ _ _") THEN
REMOVE_THEN "const_eq"
(fun th ->
SUBGOAL_TAC "" `F`
[MP_TAC th THEN ASM_REWRITE_TAC [distinctness "exp"]] THEN
FIRST_ASSUM CONTR_TAC)]);;
g `!eps env b e1 e2 v.
eval_exp eps env (Binop b e1 e2) v ==>
?d v1 v2.
v = perturb (eval_binop b v1 v2) d /\
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 /\
abs d <= eps`;;
e (INTRO_TAC "!eps env b e1 e2 v; cases_exp");;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE[eval_exp_CASES]));;
e (destruct "cases_exp" "varc | constc | binopc ");;
e (destruct "varc" "@v. b_eq _");;
e (lcontradiction "b_eq" "exp"));;
e (destruct "constc" "@n. @d. b_eq _ _");;
e (lcontradiction "b_eq" "exp");;
e (destruct "binopc" "@b2. @e1'. @e2'. @v1. @v2. @d. b_eq v_eq eval_e1 eval_e2 abs_delta");;
e (EXISTS_TAC `d:real` THEN EXISTS_TAC `v1:real` THEN EXISTS_TAC `v2:real`);;
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
let binop_inv = top_thm();;
let binop_inv =
prove
( `!eps env b e1 e2 v.
eval_exp eps env (Binop b e1 e2) v ==>
?d v1 v2.
v = perturb (eval_binop b v1 v2) d /\
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 /\
abs d <= eps`,
INTRO_TAC "!eps env b e1 e2 v; cases_exp"
THEN RULE_ASSUM_TAC (ONCE_REWRITE_RULE[eval_exp_CASES])
THEN destruct "cases_exp" "varc | constc | binopc "
THENL [
destruct "varc" "@v. b_eq _" THEN lcontradiction "b_eq" "exp";
destruct "constc" "@n. @d. b_eq _ _" THEN lcontradiction "b_eq" "exp";
destruct "binopc" "@b2. @e1'. @e2'. @v1. @v2. @d. b_eq v_eq eval_e1 eval_e2 abs_delta"
THEN EXISTS_TAC `d:real` THEN EXISTS_TAC `v1:real` THEN EXISTS_TAC `v2:real`
THEN RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]]);;
(*
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
......@@ -116,21 +137,18 @@ let abs_leq_0_impl_zero =
THEN MP_TAC (ASSUME `abs d = &0`)
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
g `!e:(real)exp v1:real v2:real env.
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`;;
g (`!e:(real)exp v1:real v2:real env.
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`);;
e (MATCH_MP_TAC exp_IND);;
e (STRIP_TAC);;
(* Var Case *)
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
(* Var Case *)
e (SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real` [ALL_TAC]);;
e (MATCH_MP_TAC var_inv);;
e (EXISTS_TAC `&0`);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v2_eq_env_a" `v2:real = (env (a:num)):real` [ALL_TAC]);;
e (MATCH_MP_TAC var_inv);;
e (EXISTS_TAC `&0`);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real`
[MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_env_a" `v2:real = (env (a:num)):real`
[MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]);;
e (ASM_REWRITE_TAC[]);;
(* Const Case *)
e (STRIP_TAC);;
......@@ -138,10 +156,6 @@ e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
e (SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (MATCH_MP_TAC const_inv);;
e (EXISTS_TAC `env:num->real`);;
e (STRIP_ASSUME_TAC const_inv);;
e (ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_a" "@d1. v1_eq abs");;
......
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