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

[Vincent A. <vin...@gm...>]

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/