Re: [Hol-info] Instantiating existentials under existentials

[Thomas T. <th...@tu...>]

Hi,

there is "GEN_EXISTS_TAC "y" `5`" from bossLib. It is more general than
what was asked for here originally. It also knows about the usual
boolean connectives.

For example, it can instantiate also

?x. P x /\ ?z y. ... y ...

or with negation

?x. (P x /\ (!z y. ... y ...)) ==> Q x

"GEN_EXISTS_TAC" is a special case of  quantHeuristicsLib.QUANT_TAC.
This one allows _partially_ instantiating multiple variables in one go,
whereas "GEN_EXISTS_TAC" allows _completely_ instantiating_ one var.

With QUANT_TAC you can for example instantiate "l" in the following

`?x l. (HD l > x /\ P x l)`

with "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`l1`])]" to get

`?x l1. HD ((SUC x) :: (l1++l2)) /\ P x ((SUC x) :: (l1++l2))`

notice that "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`x`, `l1`])]" would
lead to

`?x x' l1. HD ((SUC x') :: (l1++l2)) /\ P x ((SUC x') :: (l1++l2))`

Best

Thomas


On 22.03.2016 04:08, Yong Kiam wrote:
> Out of curiosity:
> 
> How would one do the instantiation that Magnus doesn't need i.e.
> instantiate using (and under) and existential?
> 
> On Tue, Mar 22, 2016 at 4:12 AM, Ramana Kumar <Ram...@cl...
> <mailto:Ram...@cl...>> wrote:
> 
>     Yes there is:
>     CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5`
> 
>     On 22 March 2016 at 07:08, Magnus Myreen <mo...@ca...
>     <mailto:mo...@ca...>> wrote:
> 
>         Hi hol-info,
> 
>         Quick question: is there a tactic for instantiating a nested
>         existential based on a name? Example: for a goal such as
> 
>           ?x y z. ... y ...
> 
>         I want to use a tactic foo_tac `y` `5` and get:
> 
>           ?x z. ... 5 ...
> 
>         Is there such a foo_tac tactic? I suspect this functionality is
>         there
>         somewhere already. If not, then I'll implement it.
> 
>         Note: I don't need the advanced feature of being able to instantiate
>         it with `x+z+1` where the variables refer to the other existentially
>         quantified variables.
> 
>         Many thanks,
>         Magnus
> 
>         ------------------------------------------------------------------------------
>         Transform Data into Opportunity.
>         Accelerate data analysis in your applications with
>         Intel Data Analytics Acceleration Library.
>         Click to learn more.
>         http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
>         _______________________________________________
>         hol-info mailing list
>         hol...@li...
>         <mailto:hol...@li...>
>         https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
>     ------------------------------------------------------------------------------
>     Transform Data into Opportunity.
>     Accelerate data analysis in your applications with
>     Intel Data Analytics Acceleration Library.
>     Click to learn more.
>     http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
>     _______________________________________________
>     hol-info mailing list
>     hol...@li... <mailto:hol...@li...>
>     https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> 
> ------------------------------------------------------------------------------
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140
> 
> 
> 
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>