Oops, my Low-tech solution B doesn't require an adapted HOL Light term quotation parser.
Mark. on 17/4/13 10:08 AM, Mark <m...@proof-technologies.com> wrote: > 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
