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

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

2013-02-11 Thread Vincent Aravantinos


Hi Ramana, sure, I'll do it asap.

Le 11/02/2013 10:15, Ramana Kumar a écrit :

Any chance you'll check this in to the HOL4 repository, Vincent?


On Sat, Dec 29, 2012 at 12:35 AM, Vincent Aravantinos 
mailto:vincent.aravanti...@gmail.com>> 
wrote:


Le 28/12/12 08:20, Michael Norrish a écrit :

I think my first reaction to a clean implementation with test
cases (in a selftest.sml file, say) and documentation (a .doc
file) would be to accept first and ask questions later. If it
turns out that something really is redundant or otherwise
unloved given other facilities in the system it can always be
removed. Michael

Ok. For now, here is a fast translation of HINT_EXISTS_TAC for HOL4:


fun HINT_EXISTS_TAC g =
  let
val (hs,c) = g
val (v,c') = dest_exists c
val (vs,c') = strip_exists c'
fun hyp_match c h =
  if exists (C mem vs) (free_vars c)
  then fail ()
  else (match_term c h,h)
val ((subs,_),h) = tryfind (C tryfind hs o hyp_match)
(strip_conj c')
val witness =
  case subs of
 [] => v
|[{redex = u, residue = t}] =>
if u = v then t else failwith "GEN_HINT_EXISTS_TAC not
applicable"
|_ => failwith "GEN_HINT_EXISTS_TAC not applicable"
  in
(EXISTS_TAC witness THEN ASM_REWRITE_TAC[]) g
  end;



Cheers,
V.

-- 
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University,

Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/





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

--
Free Next-Gen Firewall Hardware Offer
Buy your Sophos next-gen firewall before the end March 2013 
and get the hardware for free! Learn more.
http://p.sf.net/sfu/sophos-d2d-feb___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2013-02-11 Thread Ramana Kumar

Any chance you'll check this in to the HOL4 repository, Vincent?


On Sat, Dec 29, 2012 at 12:35 AM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:

> Le 28/12/12 08:20, Michael Norrish a écrit :
>
>> I think my first reaction to a clean implementation with test cases (in a
>> selftest.sml file, say) and documentation (a .doc file) would be to accept
>> first and ask questions later. If it turns out that something really is
>> redundant or otherwise unloved given other facilities in the system it can
>> always be removed. Michael
>>
> Ok. For now, here is a fast translation of HINT_EXISTS_TAC for HOL4:
>
>
> fun HINT_EXISTS_TAC g =
>   let
> val (hs,c) = g
> val (v,c') = dest_exists c
> val (vs,c') = strip_exists c'
> fun hyp_match c h =
>   if exists (C mem vs) (free_vars c)
>   then fail ()
>   else (match_term c h,h)
> val ((subs,_),h) = tryfind (C tryfind hs o hyp_match) (strip_conj c')
> val witness =
>   case subs of
>  [] => v
> |[{redex = u, residue = t}] =>
> if u = v then t else failwith "GEN_HINT_EXISTS_TAC not
> applicable"
> |_ => failwith "GEN_HINT_EXISTS_TAC not applicable"
>   in
> (EXISTS_TAC witness THEN ASM_REWRITE_TAC[]) g
>   end;
>
>
>
> Cheers,
> V.
>
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Group
> http://users.encs.concordia.**ca/~vincent/
>
>
--
Free Next-Gen Firewall Hardware Offer
Buy your Sophos next-gen firewall before the end March 2013 
and get the hardware for free! Learn more.
http://p.sf.net/sfu/sophos-d2d-feb___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2013-01-15 Thread Thomas Tuerk

Dear Vincent,

>I see. I'll have a look for my culture, but I think in the end that it 
> will be simpler, if I need it, to just translate my current HINT_EXISTS_TAC to
> HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at
> quantHeuristicsLib when I get the time though, because maybe the
> my problem will actually happen to be useless in the end.

this makes sense. Using quantHeuristicsLib or consequence conversions would 
provide 
you with a bit more power. However, to solve exactly the problem you described,
it is really easier to just port your OCaml code.

I might be interested in your problem in general, though. I still look for
users for my quantifier heuristic library. I implemented this library as
an extensible one than can easily be extended by the user. 
What kind of quantifier problems do you have?
Is there some other kind of automation you might be interested in. 

Best

Thomas


On Fri, 2012-12-28 at 07:18 -0500, Vincent Aravantinos wrote:
> Hi Thomas,
> 
> Le 27/12/12 07:30, Thomas Tuerk a écrit :
> > On Thu, 2012-12-27 at 19:55 +0800, Ramana Kumar wrote:
> >> There might be something in quantHeuristicsLib that can help, but I'm
> >> not sure.
> > quantHeuristicsLib can do it (see below), but has other restrictions.
> >
> > SATISFY_ss allows to instantiate multiple variables at the same time.
> > So, it can for example handle:
> >
> > ?x y. P x y /\ Q y x
> > -
> > 0. P 1 2
> > 1. !x. Q 2 x
> >
> > Notice, assumption 1. SATISFY_ss does not use matching but unification
> > with restriction to the variables occurring all-quantified
> > in an assumption or existentially in the current goal.
> > quantHeuristicsLib can currently only handle one variable at a time.
> I thought of this problem (handling more than 1 variable at a time) while
> writing HINT_EXISTS_TAC but came to the conclusion that I just wanted
> a pragmatic solution that does not claim to solve all the problems but
> just to be useful in many situations. Therefore, solving for one variable
> only seemed sufficient to me.
> 
> > However, using consequence conversions it can do your kind of
> > instantiation guessing also at subpositions.
> >
> > Getting quantHeuristicLib to do what you want requires writing some
> > ML-code, though. By default, it only searches for guesses with
> > justification, i.e. it only instantiates a quantifier, if it can
> > prove that the resulting term is really equivalent.
> > For example:
> >
> > ?x. P x /\ Q x
> > ---
> > P 2
> >
> > would not be instantated with 2, because Q 2 might be false, but there
> > may still be a "x" that satisfies both. In order to get it working for
> > your case, you need to "tell" it to use unjustified guesses for
> > conjunction. Given ?x. X x /\ Y x, it should search for guesses for X x
> > and Y x and return all found guesses, even if it can't prove that they
> > are not guesses for the overall conjunct.
> >
> > "implication_concl_qp" in
> > "src/quantHeuristicsLib/quantHeuristicsParameter" does this for the
> > right hand side of implications. One could use that code as a basis or
> > generalise it.
> 
I see. I'll have a look for my culture, but I think in the end that it 
> will be
> simpler, if I need it, to just translate my current HINT_EXISTS_TAC to
> HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at
> quantHeuristicsLib when I get the time though, because maybe the
> my problem will actually happen to be useless in the end.
> 
> Thanks,
> V.
> 



--
Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS
and more. Get SQL Server skills now (including 2012) with LearnDevNow -
200+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only - learn more at:
http://p.sf.net/sfu/learnmore_122512
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2012-12-28 Thread Vincent Aravantinos

Le 28/12/12 08:20, Michael Norrish a écrit :
> I think my first reaction to a clean implementation with test cases 
> (in a selftest.sml file, say) and documentation (a .doc file) would be 
> to accept first and ask questions later. If it turns out that 
> something really is redundant or otherwise unloved given other 
> facilities in the system it can always be removed. Michael 
Ok. For now, here is a fast translation of HINT_EXISTS_TAC for HOL4:


fun HINT_EXISTS_TAC g =
   let
 val (hs,c) = g
 val (v,c') = dest_exists c
 val (vs,c') = strip_exists c'
 fun hyp_match c h =
   if exists (C mem vs) (free_vars c)
   then fail ()
   else (match_term c h,h)
 val ((subs,_),h) = tryfind (C tryfind hs o hyp_match) (strip_conj c')
 val witness =
   case subs of
  [] => v
 |[{redex = u, residue = t}] =>
 if u = v then t else failwith "GEN_HINT_EXISTS_TAC not 
applicable"
 |_ => failwith "GEN_HINT_EXISTS_TAC not applicable"
   in
 (EXISTS_TAC witness THEN ASM_REWRITE_TAC[]) g
   end;


Cheers,
V.

-- 
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://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. SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122912
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2012-12-28 Thread Vincent Aravantinos

Le 28/12/12 08:01, Thomas Tuerk a écrit :
> Dear Vincent,
>
>> I see. I'll have a look for my culture, but I think in the end that it
>> will be simpler, if I need it, to just translate my current HINT_EXISTS_TAC 
>> to
>> HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at
>> quantHeuristicsLib when I get the time though, because maybe the
>> my problem will actually happen to be useless in the end.
> this makes sense. Using quantHeuristicsLib or consequence conversions would 
> provide
> you with a bit more power. However, to solve exactly the problem you 
> described,
> it is really easier to just port your OCaml code.
>
> I might be interested in your problem in general, though. I still look for
> users for my quantifier heuristic library. I implemented this library as
> an extensible one than can easily be extended by the user.
> What kind of quantifier problems do you have?
> Is there some other kind of automation you might be interested in.
I don't know yet. It will depend on my practical needs. I'll tell you if 
I find something that can be of interest.


Cheers,
V.

--
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2012-12-28 Thread Michael Norrish

On 28/12/2012, at 23:07, Vincent Aravantinos  
wrote:

> Le 27/12/12 06:55, Ramana Kumar a écrit :
>> 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.
> 
> I'd totally be ready to do this, but I would like, first of all, to be sure 
> people share my interest in the features of HINT_EXISTS_TAC: I don't want to 
> pollute the repo with new tactics that I am the only one to find useful.

> In particular, it seems from this discussion that there are several "close" 
> solutions in HOL4.
> However, none of them allows to just make progress in a goal without solving 
> it completely.
> In my opinion, that's an essential aspect of HINT_EXISTS_TAC, but I'm not 
> sure this opinion is shared by any of you guys? :-)

I think my first reaction to a clean implementation with test cases (in a 
selftest.sml file, say) and documentation (a .doc file) would be to accept 
first and ask questions later.  If it turns out that something really is 
redundant or otherwise unloved given other facilities in the system it can 
always be removed.

Michael
--
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2012-12-28 Thread Vincent Aravantinos

Hi Thomas,

Le 27/12/12 07:30, Thomas Tuerk a écrit :
> On Thu, 2012-12-27 at 19:55 +0800, Ramana Kumar wrote:
>> There might be something in quantHeuristicsLib that can help, but I'm
>> not sure.
> quantHeuristicsLib can do it (see below), but has other restrictions.
>
> SATISFY_ss allows to instantiate multiple variables at the same time.
> So, it can for example handle:
>
> ?x y. P x y /\ Q y x
> -
> 0. P 1 2
> 1. !x. Q 2 x
>
> Notice, assumption 1. SATISFY_ss does not use matching but unification
> with restriction to the variables occurring all-quantified
> in an assumption or existentially in the current goal.
> quantHeuristicsLib can currently only handle one variable at a time.
I thought of this problem (handling more than 1 variable at a time) while
writing HINT_EXISTS_TAC but came to the conclusion that I just wanted
a pragmatic solution that does not claim to solve all the problems but
just to be useful in many situations. Therefore, solving for one variable
only seemed sufficient to me.

> However, using consequence conversions it can do your kind of
> instantiation guessing also at subpositions.
>
> Getting quantHeuristicLib to do what you want requires writing some
> ML-code, though. By default, it only searches for guesses with
> justification, i.e. it only instantiates a quantifier, if it can
> prove that the resulting term is really equivalent.
> For example:
>
> ?x. P x /\ Q x
> ---
> P 2
>
> would not be instantated with 2, because Q 2 might be false, but there
> may still be a "x" that satisfies both. In order to get it working for
> your case, you need to "tell" it to use unjustified guesses for
> conjunction. Given ?x. X x /\ Y x, it should search for guesses for X x
> and Y x and return all found guesses, even if it can't prove that they
> are not guesses for the overall conjunct.
>
> "implication_concl_qp" in
> "src/quantHeuristicsLib/quantHeuristicsParameter" does this for the
> right hand side of implications. One could use that code as a basis or
> generalise it.

I see. I'll have a look for my culture, but I think in the end that it 
will be
simpler, if I need it, to just translate my current HINT_EXISTS_TAC to
HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at
quantHeuristicsLib when I get the time though, because maybe the
my problem will actually happen to be useless in the end.

Thanks,
V.

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


--
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

2012-12-28 Thread Vincent Aravantinos


Le 27/12/12 06:55, Ramana Kumar a écrit :
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.


I'd totally be ready to do this, but I would like, first of all, to be 
sure people share my interest in the features of HINT_EXISTS_TAC: I 
don't want to pollute the repo with new tactics that I am the only one 
to find useful.
In particular, it seems from this discussion that there are several 
"close" solutions in HOL4.
However, none of them allows to just make progress in a goal without 
solving it completely.
In my opinion, that's an essential aspect of HINT_EXISTS_TAC, but I'm 
not sure this opinion is shared by any of you guys? :-)


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 :)
On Thu, Dec 27, 2012 at 6:48 PM, Vincent Aravantinos 
mailto: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 mailto: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"
mailto: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.

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

2012-12-27 Thread Konrad Slind

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  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  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
>>> f

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

2012-12-27 Thread Ramana Kumar

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  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 (fr

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

2012-12-27 Thread Vincent Aravantinos


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 > 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" 
> 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 foc

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

2012-12-26 Thread Michael Norrish

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  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" 
>  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
--
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5,

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

2012-12-26 Thread Vincent Aravantinos


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" 
mailto: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




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

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

2012-12-26 Thread Ramana Kumar

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

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

2012-12-26 Thread Vincent Aravantinos

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

15 matches

Site Navigation

Mail list logo

Footer information