Re: [Hol-info] Improve EXISTS_TAC with by taking hints from the assumption list

[Ramana K. <ra...@me...>]

For what it's worth, my usual move in this situation is to do

qmatch_assum_abbrev_tac 'P t' >>
qexists_tac 't' >>
simp[Abbr'X']

Note that P is a metavariable, i.e. I have to type it out, but I avoid
typing the large term abbreviated by t. The X stands for pieces of P I want
unabbreviated after.

HINT_EXISTS_TAC might still be an improvement.

Sorry for no proper backquotes, using my phone.
 On Dec 26, 2012 10:57 PM, "Vincent Aravantinos" <
vin...@gm...> wrote:

> Hi list,
>
> here is another situation which I don't like and often meet (both in
> HOL-Light and HOL4), and a potential solution.
> Please tell me if you also often meet the situation, if you agree that
> it is annoying, and if there is already a solution which I don't know of
> (I'm pretty sure there is no solution in HOL-Light, but I'm not familiar
> with all its extensions over there).
>
> SITUATION:
>
>    goal of the form `?x. ... /\ P x /\ ...`
>    + one of the assumptions is of the form `P t` (t is a big a term)
>    + one wants to use t as the witness for x
>
>
> USUAL MOVE:
>
>    e (EXISTS_TAC `t`)
>    (*Then rewrite with the assumptions in order to remove the now
> trivial P t:*)
>    e(ASM_REWRITE_TAC[])
>
>
> PROBLEM WITH THIS:
>
>    Annoying to write explicitly the big term t.
>    Plus the subsequent ASM_REWRITE_TAC is trivial and can thus be
> systematized.
>    Not really annoying if it only appears from time to time, but I
> personally often face this situation.
>
>
> SOLUTION:
>
>    A tactic HINT_EXISTS_TAC which looks for an assumption matching one
> (or more) of the conjuncts in the conclusion and applies EXISTS_TAC with
> the corresponding term.
>
>
> EXAMPLE IN HOL-LIGHT:
>
>   (* Consider the following goal:*)
>
>      0 [`P m`]
>      1 [`!x. P x ==> x <= m`]
>
>    `?x. P x`
>
>    (* Usual move: *)
>    # e (EXISTS_TAC `m:num`);;
>    val it : goalstack = 1 subgoal (1 total)
>
>      0 [`P m`]
>      1 [`!x. P x ==> x <= m`]
>
>    `P m`
>
>    # e (ASM_REWRITE_TAC[]);;
>    val it : goalstack = No subgoals
>
>    (* New solution, which finds the witness automatically and removes
> the trivial conjunct : *)
>
>    # b (); b (); e HINT_EXISTS_TAC;;
>    val it : goalstack = No subgoals
>
>    (* Notes:
>     * - The use case gets more interesting when m is actually a big term.
>     * - Though, in this example, the tactic allows to conclude the goal,
> it can also be used just to make progress in the proof without necessary
> concluding.
>     *)
>
> A HOL-Light implementation for HINT_EXISTS_TAC is provided below the
> signature.
> One for HOL4 can easily be implemented if anyone expresses some interest
> for it.
>
> Cheers,
> V.
>
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Group
> http://users.encs.concordia.ca/~vincent/
>
>
> let HINT_EXISTS_TAC (hs,c as g) =
>    let hs = map snd hs in
>    let v,c' = dest_exists c in
>    let vs,c' = strip_exists c' in
>    let hyp_match c h =
>      ignore (check (not o exists (C mem vs) o frees) c);
>      term_match (subtract (frees c) [v]) c (concl h), h
>    in
>    let (_,subs,_),h = tryfind (C tryfind hs o hyp_match) (binops `/\` c')
> in
>    let witness =
>      match subs with
>        |[] -> v
>        |[t,u] when u = v -> t
>        |_ -> failwith "HINT_EXISTS_TAC not applicable"
>    in
>    (EXISTS_TAC witness THEN REWRITE_TAC hs) g;;
>
>
>
> ------------------------------------------------------------------------------
> LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
> Remotely access PCs and mobile devices and provide instant support
> Improve your efficiency, and focus on delivering more value-add services
> Discover what IT Professionals Know. Rescue delivers
> http://p.sf.net/sfu/logmein_12329d2d
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>