Hello Keiko,
On 05/07/2016 11:02, Heiko Becker wrote:
> 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?
Do you mean to rewrite the assumption itself or use the assumption to
rewrite the goal?
The former can be accomplished with RULE_ASSUM_TAC (REWRITE_RULE [...]).
This will rewrite all assumptions (there are more complicated ways that
allow more control).
For the latter you can use ASM_REWRITE_TAC. For simple variable
substitutions you can also use FIRST_X_ASSUM SUBST1_TAC.
> 2) Is there an easier way of closing the proof, since I already derived
> the goal I have?
The problem is in your SUBGOAL_TAC step. When you introduce the subgoal
`v = v2`, HOL Light does not know the context of v and v2 so it assigns
them variable types. The resulting subgoal is unprovable.
Instead you can use:
e(SUBGOAL_TAC "v_eq_v2" `v:num = v2` [...
(The answer to your 3rd question may help with such problems in the future.)
There is a number of other ways to deal with this proof. For example:
e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);;
> 3) (A little unrelated) Can I make HOL-Light annotate all terms in my
> goal with their derived type?
>
This snippet* has come in handy in numerous occasions:
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."));;
* Slightly modified from original source:
https://code.google.com/archive/p/flyspeck/wikis/TipsAndTricks.wiki#Investigating_Types
Use "show_types();;" to make HOL Light print out the types of all variables.
Use "hide_types();;" to restore the original behaviour.
Hope this helps.
Regards,
Petros
>
> ------------------------------------------------------------
>
> 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
>
--
Petros Papapanagiotou, Ph.D.
CISA, School of Informatics
The University of Edinburgh
Email: p...@ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
