Hello Petros and Marco,
thank you for your replies.
With your help I was able to finish the subgoal.
Regards,
Heiko
On 07/05/2016 04:59 PM, Petros Papapanagiotou wrote:
> 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
>>
>
------------------------------------------------------------------------------
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
