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

[Vincent A. <vin...@gm...>]

Hi Ramana,

HINT_EXISTS_TAC allows not to type `P` explicitly. Indeed the good thing 
about this tactic, in my opinion, is that you don't need to type any 
term explicitly and just let the prover find them for you. And it's 
shorter of course.
On the other hand, it has maybe the disdvantage of being specialized: 
one might prefer the more general mechanism provided by 
MATCH_ASSUM_ABBREV_TAC.

In any case, thanks a lot, you taught me some HOL4 commands I was not 
aware of :-) (namely, MATCH_ASSUM_ABBREV_TAC and Abbr); I'm more 
familiar with HOL Light...

Cheers,
V.

Le 26/12/12 19:42, Ramana Kumar a écrit :
>
> 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... <mailto: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/
>     <http://users.encs.concordia.ca/%7Evincent/>
>
>
>     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... <mailto:hol...@li...>
>     https://lists.sourceforge.net/lists/listinfo/hol-info
>


-- 
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/