FYI. Somewhat related functionality is in Q.REFINE_EXISTS_TAC, which
can be used to partially instantiate an existential. But you have to
supply a witness, instead of saying "find a witness in the assumptions".
Konrad.
On Thu, Dec 27, 2012 at 5:55 AM, Ramana Kumar <ram...@member.fsf.org> wrote:
> 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 <
> vincent.aravanti...@gmail.com> 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 <ram...@member.fsf.org> 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" <
>> vincent.aravanti...@gmail.com> 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-info@lists.sourceforge.net
>>> 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-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>> --
>> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
>> Verification Grouphttp://users.encs.concordia.ca/~vincent/
>>
>>
>
>
> ------------------------------------------------------------------------------
> 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-info@lists.sourceforge.net
> 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-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
