Thanks, Vince! Here's an example of a free variable occurrence in the scope of
a variable binding whose type is not inferred, from
hol_light/Examples/inverse_bug_puzzle_tac.ml. I picked a long proof so you can
clearly see. I apologize is my ML-like terminology isn't correct in HOL:
let reachableN_CLAUSES = prove
(`! p p'. (reachableN p p' 0 <=> p = p') /\
! n. reachableN p p' (SUC n) <=> ? q. reachableN p q n /\ move q p'`,
INTRO_TAC "!p p'" THEN
consider "s0 such that" `s0 = \m:num. p':triple` [MESON_TAC[]] "s0exists"
THEN
SUBGOAL_TAC "0CLAUSE" `reachableN p p' 0 <=> p = p'`
[HYP MESON_TAC "s0exists" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp1"
`! n. reachableN p p' (SUC n) ==> ? q. reachableN p q n /\ move q p'`
[INTRO_TAC "!n; H1" THEN
consider "s such that"
`s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m))`
[HYP MESON_TAC "H1" [LE_0; reachableN]] "sDef" THEN
consider "q such that" `q:triple = s n` [MESON_TAC[]] "qDef" THEN
HYP MESON_TAC "sDef qDef" [LE_0; reachableN; LT]] THEN SUBGOAL_TAC "Imp2"
`!n. (? q. reachableN p q n /\ move q p') ==> reachableN p p' (SUC n)`
[INTRO_TAC "!n" THEN REWRITE_TAC[IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN
INTRO_TAC "!q; nReach; move_qp'" THEN
consider "s such that"
`s 0 = p /\ s n = q /\ !m. m < n ==> move (s m) (s (SUC m))`
[HYP MESON_TAC "nReach" [reachableN; LT; LE_0]] "sDef" THEN
REWRITE_TAC[reachableN; LT; LE_0] THEN
EXISTS_TAC `\m. if m < SUC n then s m else p':triple` THEN
HYP MESON_TAC "sDef move_qp'" [LT_0; LT_REFL; LT; LT_SUC]] THEN
HYP MESON_TAC "0CLAUSE Imp1 Imp2" []);;
Using Petros's and Marco's ideas, I defined consider so that the first s0 of
consider "s0 such that" `s0 = \m:num. p':triple`
did not need a type annotation. But the free variable p' should need a type
annotation, as it is in the scope of the binding given by
INTRO_TAC "!p p'"
so p and p' have type triple, because reachableN has type
triple -> triple -> num -> bool.
That's also true for the function
`\m. if m < SUC n then s m else p':triple`
near the end.
In
consider "q such that" `q:triple = s n`
the free variable q should not need a type annotation, because the free
variable s is in the scope of the variable binding given by
consider "s such that"
`s 0 = p /\ s (SUC n) = p' /\ !m. m < SUC n ==> move (s m) (s (SUC m))`
where s is given the type
num -> triple
because move has type
triple -> triple -> bool.
Now Petros taught me here long ago to put these type annotations, but it would
be nice to not need them. If you look at the analogous proof in
Examples/inverse_bug_puzzle_miz3.ml, there's only one type annotation, in
consider s0 such that
s0 = \m:num. p';
That's a necessary type annotation for m, because it tells us that s0 has type
num -> triple
and we wouldn't know that otherwise.
> That's great you're changing your Q-like module right now to use
> the parser instead of strings.
I'll do it if the new preterm parser gets integrated in HOL Light.
Wow, I meant it was great you were using the parser in HOL4! But that's even
better, if you're porting your HOL4 Q-like module to HOL Light. Am I getting
something wrong? Assuming I'm getting you right, why don't you help me with
what I'm doing, see if I can sell your quotexpander modification to John, and
then you can do a great deal more with Q-like modules.
--
Best,
Bill
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
