Commit 2cc0bc48 authored by Heiko Becker's avatar Heiko Becker
Browse files

Easiert tactics, prove inversion lemmata

parent 16edd049
......@@ -21,3 +21,11 @@ let eq_give_right eq impl = eq_give_goal eq impl snd;;
let contradiction (t:term) (ty:string) =
SUBGOAL_TAC "" `F` [MP_TAC (ASSUME t) THEN ASM_REWRITE_TAC [distinctness ty]]
THEN FIRST_ASSUM CONTR_TAC;;
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 destruct (asm:string) (patt:string) =
REMOVE_THEN asm (DESTRUCT_TAC patt);;
let print_varandtype fmt tm =
let hop,args = strip_comb tm in
let s = name_of hop
and ty = type_of hop in
if is_var hop & args = [] then
(pp_print_string fmt "(";
pp_print_string fmt s;
pp_print_string fmt ":";
pp_print_type fmt ty;
pp_print_string fmt ")")
else fail() ;;
let show_types,hide_types =
(fun () -> install_user_printer ("Show Types",print_varandtype)),
(fun () -> try delete_user_printer "Show Types"
with Failure _ -> failwith ("hide_types: "^
"Types are already hidden."));;
......@@ -52,6 +52,53 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
eval_exp eps env e2 v2 /\
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();;
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();;
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();;
(*
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
......
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