Re: [Hol-info] HOL Light set comprehensions

[Bill R. <ri...@ma...>]

Rob, I think the answer to your interesting question involves more complicated set abstractions like {y + 6 | y < 0}.  I think here we see the merit of the HOL Light invisible variables, as this simple proof shows: 

   g `EMPTY = {y + 6 | y < 0}`;;
   e(REWRITE_TAC[SETSPEC; GSPEC]);;
   e(REWRITE_TAC[LT; EMPTY]);;

   `{} = (\GEN%PVAR%459. ?y. y < 0 /\ GEN%PVAR%459 = y + 6)`

   # val it : goalstack = No subgoals

Let's replace the computer-generated invisible variable GEN%PVAR%451 with a for clarity: 

`{} = (\a. ?y. y < 0 /\ a = y + 6)`

I think that's correct, because I think the meaning of 
{y + 6 | y < 0}
is
{a | ?y. y < 0 /\ a = y + 6}
so HOL Light should generate an invisible variable automatically for {y + 6 | y < 0}.

BTW Michael Norish's response a year ago is quite relevant:
http://article.gmane.org/gmane.comp.mathematics.hol/2118
Sorry it took me so long to respond, and I still don't understand parser.ml well enough, but I bet Michael does.

RDA> This is idle curiosity on my part about HOL Light: why are the
RDA> constants that support set comprehensions defined in such a way
RDA> that the parser has to generate an invisible bound variable?

RDA> This results in surprising behaviour like:

RDA> # `{x | x > 9}` = `{x | x > 9}`;;
RDA> val it : bool = false

First, the constants SETSPEC and GSPEC are defined in sets.ml in a way that involves no invisible bound variables: 

let GSPEC = new_definition
  `GSPEC (p:A->bool) = p`;;

let SETSPEC = new_definition
  `SETSPEC v P t <=> P /\ (v = t)`;;

I bet Michael understands these definitions.  So the invisible bound variables that you and Michael's post refer to must come from the HOL Light parser making sense of the curly braces, and I think that involves these lines of parser.ml:

  || a (Resword "{") ++

  let pgenvar =
    let gcounter = ref 0 in
    fun () -> let count = !gcounter in
              (gcounter := count + 1;
               Varp("GEN%PVAR%"^(string_of_int count),dpty)) in

  let pmk_setcompr (fabs,bvs,babs) =
    let v = pgenvar() in
    let bod = itlist (curry pmk_exists) bvs
                     (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs)) in
    Combp(Varp("GSPEC",dpty),Absp(v,bod)) in

So HOL Light must use parser.ml to turn a set abstraction
{ ... | ... }
into a combination involving GSPEC, SETSPEC and your invisible variables.  Here's evidence:

g `EMPTY = {y | y < 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;

`{} = (\GEN%PVAR%450. ?y. y < 0 /\ GEN%PVAR%450 = y)`

Let's rewrite the lambda abstraction for clarity as, changing GEN%PVAR%450 to a:

(\a. ?y. y < 0 /\ a = y)

Maybe your point is that HOL Light should instead use this simpler lambda abstraction

(\y. y < 0)

There you'd be making a really good point, but with more complicated set abstraction above, I think we see the value of invisible variables.

BTW note that my simple proof above did not use IN_ELIM_THM, and I got away with that because IN_ELIM_THM has a large intersection with 
REWRITE_TAC[SETSPEC; GSPEC].
-- 
Best,
Bill