Re: [Hol-info] Rewriting and Types in HOL-Light

[Marco M. <ma...@ma...>]

Dear Heiko,

I see two main problem in your proof:

1. When you open the subgoal, you have to be sure about the types of your
terms.  I.e., here you have to add the annotation :num beside v or v2:

e (SUBGOAL_TAC "v_eq_v2" `v:num = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN
ONCE_REWRITE_TAC[injectivity "exp"]]);;

2. About your proof strategy, you surely want to make use of injectivity
and distinctness of constructors.  This is what I would do in this case:

g `!eps env v val.
   eval_exp eps env (Var v) val ==> val = env v`;;
e (REPEAT GEN_TAC);;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
(* Use distinctness of constructors. *)
e (REWRITE_TAC[distinctness "exp"]);;
(* Use injectivity of constructors. *)
e (REWRITE_TAC[injectivity "exp"]);;
(* Now you can easy conclude with MESON_TAC, or, if you wish, with. *)
e (DISCH_THEN STRUCT_CASES_TAC);;
e REFL_TAC;;

Marco




2016-07-05 12:02 GMT+02:00 Heiko Becker <s9h...@st...>:

> 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...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>