Hi Bill,
(I'm joining this conversation late, so apologies if I've got the wrong end
of the stick here, but ...)
If you want to do the classic HOL Light proof script thing of creating
"packaged up" proofs that prove your goal in one compound ML expression,
involving various ML subexpressions for term quotations, then there is a
fairly fundamental OCaml language mechanism that restricts with what can
ultimately be achieved with contextual type inference. This is related to
the order in which OCaml evaluates subexpressions.
Specifically, if OCaml has some curried expression:
F X Y Z
then it will evaluate Z, then Y, then X before it evaluates the overall
expression. So if there is more than one term quotation in your ML
expression, the first term quotations to be evaluated will be ones occurring
later on in the expression.
The impression I get is that this is the opposite of what you want to do,
i.e. type annotate "early on" (i.e. towards the left of the ML expression)
and expect ML subexpressions "later on" (i.e. towards the right) in the same
expression to inherit the HOL type context of this "early" type annotation.
The only obvious solutions to this that occur to me are:
1. Low-tech solution A: Breaking up your proof to a series of "g" and "e"
steps, so that they get evaluated in the intended order, and then adapting
the HOL Light term quotation parser to inherit a HOL type context for
variables occurring early on in the proof (this is what ProofPower does).
However, you still have same problem here at the individual proof step
level, if a given "e" step involves more than one term quotation;
2. Low-tech solution B: Evaluating all of your term quotations up front, as
a series of term definitions, and then using an adapted HOL Light contextual
term parser as in Low-tech solution A. However, your proof script is then
less readable because all the term quotations are defined up front instead
of being embedded in the proof steps;
3. High-tech solution: Expressing your proof script not in ML but in some
special proof script language (like Isabelle's Isar), so that you are not
tied to the order in which OCaml evaluates subexpressions, because it is the
parser for your proof script language, and not OCaml, that would decide
evaluation order. However, this involves designing a proof scripting
language and writing a parser for it.
Regards,
Mark.
on 17/4/13 5:32 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> 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
>
>
>
------------------------------------------------------------------------------
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
