Hello everyone,
I have another question on HOL-Light. This time I am stuck with some
rewriting in a proof.
I have defined an inductive type and want to prove an "inversion" lemma
for it:
g `!eps env v val.
eval_exp eps env (Var v) val ==> val = env v`;;
I have been able to do the proof until I arrive at a subgoal which I
think is easy to proof but I cannot find the appropriate tactic to do it:
val it : xgoalstack = 1 subgoal (4 total)
0 [`val = env v2`] (val_eq)
1 [`v = v2`]
`v = v2`
The script I used is:
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env v val; cases");;
e (REMOVE_THEN "cases" (DESTRUCT_TAC "var | const | bin"));;
(* Var case *)
e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));;
e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN
ONCE_REWRITE_TAC[injectivity "exp"]]);;
e (DISCH_TAC);;
e (EXPAND_TAC "v2");;
e (ONCE_REWRITE_TAC[ASSUME `v = v2`]);
Since the last two tactics do not change the goal in any way my
questions in this case are:
1) How can I use the assumption 1 and rewrite it inside my goal?
2) Is there an easier way of closing the proof, since I already derived
the goal I have?
3) (A little unrelated) Can I make HOL-Light annotate all terms in my
goal with their derived type?
I have added my formalization below.
Thank you (once again) in advance.
Best regards,
Heiko
------------------------------------------------------------
let binop_IND, binop_REC = define_type
"binop = Plus | Sub | Mult | Div ";;
(*
Define an evaluation function for binary operators.
*)
let eval_binop = new_recursive_definition binop_REC
`(eval_binop Plus v1 v2 = v1 + v2) /\
(eval_binop Sub v1 v2 = v1 - v2) /\
(eval_binop Mult v1 v2 = v1 * v2) /\
(eval_binop Div v1 v2 = v1 / v2)`;;
let exp_IND, exp_REC= define_type
"exp = Var num
| Const V
| Binop binop exp exp";;
let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
new_type_abbrev ("env_ty",`:num->real`);;
let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
`(!eps env v.
eval_exp eps env (Var v) (env v)) /\
(!eps env n delta.
abs delta <= eps ==>
eval_exp eps env (Const n) (perturb n delta)) /\
(!eps env b e1 e2 v1 v2 delta.
eval_exp eps env e1 v1 /\
eval_exp eps env e2 v2 /\
abs delta <= eps ==>
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2)
delta))`;;
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
