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