Rob, I learned a lot from your post! My conclusion is that in both HOL Light
and HOL4,
{f x | R x} = λa. ∃x. R x ∧ a = f x
for some variable a than is not free in R x or f x. I judge both HOL
approaches to have pluses & minuses, and can't rate one above the other:
1) In HOL Light, the proof of this equation is immediate, as parser defines {f
x | R x} to be the RHS. However, we always generate a fresh variable, ones
with odd-sounding (although unseen) names like GEN%PVAR%1066.
2) In HOL4, the parser's definition of {f x | R x} involves no fresh variables,
but calculating a in the above equation was beyond my skill/patience here, as
there are many cases to consider.
# dest_comb `{f x | R x}`;;
val it : term * term =
(`GSPEC`, `\GEN%PVAR%1066. ?x. SETSPEC GEN%PVAR%1066 (R x) (f x)`)
I like this approach for its simplicity: ``Let's choose a fresh variable,
whether we need it or not, without studying the free & bound variables.'' The
HOL4 approach, as you explained it, looks more elegant, but if you want to
understand what alpha-conversions take place, you need a serious investigation
that I couldn't complete here. Let me make a two minor changes to your code:
# let HOL4_GSPEC = new_definition `HOL4_GSPEC = (\f. (\v. ?r. f r = (v, T)))`;;
Let's study your {f x | R x} = HOL4_GSPEC (λx. (f x, R x)) :
HOL4_GSPEC (λx. (f x, R x))
=
(λf. (λv. ∃r. f r = (v, T))) (λx. (f x, R x))
=
λv. ∃r. (λx. (f x, R x)) r = (v, T)
as long as v and r are not free in (λx. (f x, R x)). Assuming this, and that r
is not a bound variable in (f x, R x), we have
= λv. ∃r. (f r, R r) = (v, T)
=
λv. ∃r. f r = v ∧ R r
and that's correct! But if any of the assumptions above don't hold, we'll have
to alpha-convert if we want to make it this far. I couldn't figure the whole
story out, but here are three alpha-conversion examples, the first when r is
bound in (f x, R x).
needs "RichterHilbertAxiomGeometry/readable.ml";; (* extensively commented *)
let HOL4_GSPEC = NewDefinition `; HOL4_GSPEC = (λf. (λv. ∃r. f r = (v, T)))`;;
interactive_goal `;
f = (λx. (λr. r + x)) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x))
`;;
interactive_proof `;
intro_TAC fDef;
rewrite SETSPEC GSPEC HOL4_GSPEC PAIR_EQ;
`;;
`(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = f x) = (\v. ?r. f r = v /\ R r)`
The whole point is the next step, where I expected alpha-conversion of the
outer (existential) r:
interactive_proof `;
rewrite fDef;
`;;
`(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = (\r. r + x)) =
(\v. ?r. (\r'. r' + r) = v /\ R r)`
I was wrong; it was the inner (abstraction) r that was alpha-converted.
Here's an example with ¬(r = x) and r free in (f x, R x):
interactive_goal `;
f = (λx. r + x) ⇒ {f x | R x} = HOL4_GSPEC (\v. (f v, R v))
`;;
interactive_proof `;
intro_TAC fDef;
rewrite fDef;
rewrite HOL4_GSPEC PAIR_EQ;
`;;
`{r + x | R x} = (\v. ?r'. r + r' = v /\ R r')`
Now the outer (existential) r was alpha-converted.
Here's an example where ¬(v = x), v is free in (f x, R x), and r is not free in
(λx. (f x, R x)).
interactive_goal `;
f = (λx. v + x) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x))
`;;
interactive_proof `;
intro_TAC fDef;
rewrite fDef HOL4_GSPEC PAIR_EQ ;
`;;
`{v + x | R x} = (\v'. ?r. v + r = v' /\ R r)`
I finally got what I wanted, and HOL Light-type alpha-conversion. Let's make
it look even nicer:
interactive_proof `;
∀y. v + y = f y [fApplied] by fol fDef;
rewrite fApplied;
`;;
`{f x | R x} = (\v'. ?r. f r = v' /\ R r)`
Let me address my lack of skill/patience. Alpha-conversion will be needed iff
¬(v = x) and v is free in (f x, R x)
\/
¬(r = x) and r is free in (f x, R x)
\/
r is bound in (f x, R x).
I guess that's only 4 cases, as the 2nd and 3rd disjuncts are disjoint, and my
3 examples touched on all 4. I should try to work this exercise. I suppose
after all this I should re-prove your theorem:
let thm1 = theorem `;
{f x | R x} = HOL4_GSPEC (\x. (f x, R x))
proof
rewrite HOL4_GSPEC PAIR_EQ EXTENSION IN_ELIM_THM;
fol;
qed;
`;;
val thm1 : thm = |- {f x | R x} = HOL4_GSPEC (\x. f x,R x)
The HOL4 design sees two abstractions here: `\(x, y, z). f x y z`
and `\(x, y, z). R x y z` and combines them together into one
abstraction `\(x, y, z). (f x y z, R x y z)`. This contains all
the information needed to construct the set comprehension and the
HOL4 formulation of GSPEC captures that construction.
Wow, that's cool! Is this due to Konrad and Michael, or does it go way back?
I never would have thought of such stunts. Here's two proof:
HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z))
=
(λv. ∃r. (λ(x, y, z). (f x y z, R x y z)) r = (v, T))
=
Now r must be a triple r = (a, b, c), and then
=
(λv. ∃a b c. v = f a b c ∧ R a b c)
=
{f x y z | R x y z}
let thm3 = theorem `;
{f x y z | R x y z} = HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z))
proof
rewrite HOL4_GSPEC PAIR_EQ IN_ELIM_THM EXISTS_PAIR_THM EXTENSION
IN_ELIM_THM;
fol;
qed;
`;;
Warning: inventing type variables
0..0..0..solved at 3
0..0..0..solved at 3
val thm3 : thm =
|- {f x y z | R x y z} = HOL4_GSPEC (\(x,y,z). f x y z,R x y z)
Actually I got a pretty-printer error that seems serious enough to switch to
standard usage:
let HOL4_GSPEC = new_definition `HOL4_GSPEC = (\f. (\v. ?r. f r = (v, T)))`;;
g `{f x y z | R x y z} = HOL4_GSPEC (\(x, y, z). (f x y z, R x y z))`;;
e(REWRITE_TAC [HOL4_GSPEC; PAIR_EQ; IN_ELIM_THM; EXISTS_PAIR_THM; EXTENSION;
IN_ELIM_THM]);;
`!x. (?x y z. R x y z /\ x = f x y z) <=>
(?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)`
That looks like a variable capture error (on top of the repeated p1), one that
we know (since the theorem was proved) didn't actually take place. The
pretty-printer ought to have printed
`!x'. (?x y z. R x y z /\ x' = f x y z) <=>
(?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)`
I see the same pretty-printer error occurred in your theorem:
interactive_goal `;
{f x | R x} = HOL4_GSPEC (\x. (f x, R x))
`;;
interactive_proof `;
rewrite HOL4_GSPEC PAIR_EQ EXTENSION IN_ELIM_THM;
`;;
# val it : goalstack = 1 subgoal (1 total)
`!x. (?x. R x /\ x = f x) <=> (?r. f r = x /\ R r)`
Does anyone understand the HOL Light pretty-printing of freshly generated
variables, or know where it's done?
--
Best,
Bill
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
