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

Start adding more lemmata about expression evaluation

parent 3c89d8d1
......@@ -54,27 +54,40 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;;
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);;
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);;
let var_equiv =
prove (
`!eps env v val. eval_exp eps env (Var v) val <=> val = env v`,
intros "!eps env v val"
THEN EQ_TAC
THENL[
intros "eval_exp_var"
THEN MATCH_MP_TAC var_inv
THEN EXISTS_TAC `eps:real`
THEN ASM_REWRITE_TAC[];
intros "val_eq"
THEN ASM_REWRITE_TAC[eval_exp_RULES]]);;
let const_inv =
prove
......
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