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
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
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
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
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
>> quantHeu
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 l
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 insta
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 fe
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
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 a
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
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_
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 bei
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.
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 n
15 matches
Mail list logo
