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

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Dear Vincent,

I think you are right about SATISFY_ss - it can only prove a goal, not
refine it.
There might be something in quantHeuristicsLib that can help, but I'm not
sure.

Do you have a clone of the HOL4 git repository? You could make a pull
request on github after adding HINT_EXISTS_TAC in an appropriate place.

In addition to match_assum_abbrev_tac, there is match_assum_rename_tac.
Both of them could do with some improvement, e.g. see
https://github.com/mn200/HOL/issues/81. If you happen to delve into this
code, your patches would be warmly welcomed :)

Ramana

On Thu, Dec 27, 2012 at 6:48 PM, Vincent Aravantinos <
vin...@gm...> wrote:

>  Hi Michael,
>
> I'm regularly amazed by the pearls that HOL4 contains...
> I did not know about the SatisfySimps module!
>
> Now, from my first tests, this can only be used to conclude a goal.
> Concretely, if I have a goal of the following form:
>
> ?x. P x /\ Q x
> --------------------
>   0. P t
>   ...
>
> where Q x cannot be solved immediatly (assume it can be solved from other
> theorems or the other assumptions, but not automatically).
> Then SATISFY_ss won't do anything because of Q x.
> On the other hand, HINT_EXISTS_TAC will instantiate x by t, just leaving Q
> t as a new goal to prove (of course the new goal is not equivalent to the
> previous one, but the purpose of the tactic is just to make some progress
> and help the user reducing parts of the goal easily).
>
> Am I right about this behaviour of SATISFY_ss or did I miss something?
>
> V.
>
> Le 26/12/12 23:17, Michael Norrish a écrit :
>
> HOL4’s SATISFY_ss (from SatisfySimps) should solve this problem
> (particularly now that Thomas Türk has fixed a bug in its code).
>
> Michael
>
> On 27/12/2012, at 11:42, Ramana Kumar <ra...@me...> wrote:
>
>   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
>>
>
> ------------------------------------------------------------------------------
> Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
> MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
> with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
> MVPs and experts. ON SALE this month only -- learn more at:
> http://p.sf.net/sfu/learnmore_122712
>
>  _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Grouphttp://users.encs.concordia.ca/~vincent/
>
>