[Hol-info] Research Associate at the University of Kent, Canterbury, UK
Apply in either of these places: https://www.jobs.ac.uk/job/DBV331/research-associate-cems-236-23 https://jobs.kent.ac.uk/Vacancy.aspx?ref=CEMS-236-23 Salary: £36,386 to £40,931 Contract Type: Fixed Term - 36 months Deadline: 4th September The School of Computing at Kent in the UK wishes to appoint a qualified and highly motivated researcher to work as a Research Associate. This 36 month post is funded by two grants led by Professor Mark Batty ( m.j.ba...@kent.ac.uk): Transparent pointer safety: Rust to Lua to OS Components from Innovate UK and Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT) from the EPSRC. This project is in partnership with Sheffield and Surrey. Applicants should have a strong mathematical background and knowledge of how to reason about systems. This must be evidenced by high-quality research publications or artifacts in programming languages, formal verification, distributed systems, security, or computer architecture. Experience in hand proof, mechanised theorem proving tools (i.e. Isabelle/HOL, Coq, or similar) or familiarity with model checkers and SMT solvers is highly desirable. As Research Associate you will: 1. develop formal models for the expression of the behaviours of advanced architectures, 2. develop reasoning techniques (proof, mechanical proof, model checking, automated tools) for proving properties about these systems, and 3. apply these techniques to establish system properties including memory safety, security properties and functional correctness. To be successful in this role you will: 1. have or be about to complete a PhD in a relevant discipline, or equivalent professional experience, 2. have a track record of peer-reviewed publications at scientific workshops, competitions, conferences or journals, and 3. have excellent mathematical skills relevant to analysing computer-system behaviour. The university of Kent is walking distance from the charming historic city of Canterbury, it has a high speed connection to London, and travel to Europe is convenient by rail or car. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] proof replay?
Hi Dan, So, in a nutshell, you've got N proof scripts in HOL Light that you want to fit together as one coherent proof in a single session, but that would take far too much processing to do so in practice. So you want to execute these in N parallel HOL Light sessions, recording the kernel-level steps as they happen, and export these, and replay them all in a single HOL Light session. This is basically known as "proof recording", and an exported proof is known as a "proof object". There have been various attempts at proof recording in HOL Systems over the years, including Wong (1990s), Skalberg & Obua (2000s), Kaliszyk & Krauss (2010s), Hurd's Open Theory project (2010s) and my Common HOL project (2010s). Section 4.5 of my paper on proof auditing includes a brief overview of these. As you say, most recording systems are designed for either porting proofs between two specific proof systems (either two proof assistants or a proof assistant and its sister proof checker), but Open Theory and Common HOL were designed for porting between any two HOL systems (including back into the same system). You're absolutely right that the replay has potential to be much faster than executing the original proof scripts, given that search does not need to be replicated during replay. But there are numerous challenges to overcome to make it tractable. Even though a basic proof recording system can be written in a few hundred lines of ML, recording a large proof would probably use up huge amounts of RAM/diskspace, and probably not result in that much of a speed up during replay. However, some recording systems do much better than that. I'm not sure about the latest developments for other systems, but back in 2015 my recording system for Common HOL recorded the "text formalisation" part of Flyspeck in HOL Light (1.3bn primitive proof steps) using modest RAM/CPU, and managed to get replay in HOL Light down by a factor of 7, and I think that this could go down by another factor of 2 (so perhaps 15 in total) with a bit of extra work, but this is nowhere near the 100x speedup you envisage. Would that meet your requirements? May I ask what the application is? Mark. On 25/01/2021 13:40, D. J. Bernstein wrote: I have another newbie question regarding HOL Light; again happy to hear about other HOL variants if those have easier answers. I'm in the typical post-human-proof situation where a program found a "proof" that's too tedious for a human to verify (in the conventional sense, not PCPs). For verification, I'm converting the "proof" into a HOL Light proof: auto-generating the whole chain of intermediate steps as definitions, and auto-generating all the theorems linking the definitions. This works fine on scaled-down examples, and extrapolation suggests that the CPU time for HOL Light will still be affordable when scaled up to the full theorem, in the ballpark of 1 core-hours. It's no problem to farm the separate proof steps out to separate cores, each using its own subset of the relevant definitions, at which point I have one instance of HOL Light printing out a theorem saying A implies B, and a separate instance of HOL Light printing out a theorem saying B implies C, and so on. This brings me to the question: how can I have HOL Light printing out the combined theorem saying that A implies Z, without waiting 1 hours for HOL Light on one core to serially run through proving all the lemmas? I'd guess that >99% of the CPU time I'm seeing comes from HOL Light searching for proofs (e.g., the computation in REAL_LINEAR_PROVER), and that far less is spent by the HOL Light kernel verifying the proofs. Is there a generic mechanism to record merely what the kernel is doing--- i.e., to automatically write down a proof in the conventional sense--- and then replay this proof in another HOL Light instance that has the same definitions? The papers I've found on the problem of exporting libraries of theorems from one system to another sound like that's only partially solved, but that's also a conceptually more difficult problem than simply replaying the lowest level of proof within a single system. I did various other searches for answers and didn't find anything---sorry if I missed something obvious. In general the small kernel makes me think that tracing proofs wouldn't be touching many lines of code, but I haven't studied the kernel closely enough to be confident about this. In case this (1) doesn't exist and (2) is hard to build, my backup plan is to modify the program printing out the proof tactics to do its own searches for lower-level proof steps. Conceptually this would be copying the searches implemented in HOL Light, so presumably the speed will end up similar, but the searches would then be easily distributable precomputation,
Re: [Hol-info] Visualizing subgoals in a proof script
Hi Mario, Yes, as Freek says, Tactician would do the sort of thing you need, but is only for HOL Light. It works on the vast majority of tactic proofs as they are typically written in HOL Light, say perhaps 1 in every 1,000 proof script lines might trip it up. It could be ported to HOL4, but this would not be easy to get working as well as it does for HOL Light, because it plays about with the innards of OCaml and equivalent tweaking of PolyML would be required. Mark. On 07/08/2020 10:02, Freek Wiedijk wrote: Dear Mario, Hello. In HOL4 is there a way to generate something like the entries in Metamath proof explorer for the subgoals generated within a proof and the tactics used to solve them? Example: <http://us.metamath.org/mpeuni/eluniab.html> For HOL Light there is Mark Adams's "tactician" which I expect would make something like this possible (even though I expect it only would work on the majority of proofs, and not be guaranteed to work on all of them). But that's HOL Light, not HOL4. Freek ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] grammar for HOL Light terms
And for HOL Zero there is Appendix C of the User Manual that gives a formal grammar of the HOL Zero concrete syntax. Again, this is fairly similar to HOL Light's and HOL4's, but there are numerous small differences. Note that the formal grammar hasn't actually been checked (as far as I'm aware) by a parser generator. http://www.proof-technologies.com/holzero/ Mark. On 09/11/2019 15:48, Petros Papapanagiotou wrote: Hi Brando, The HOL4 description manual has quite a bit of information, a lot of which is shared with HOL Light: http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-description.pdf/download I am not sure if there is a similar document for HOL Light. You can see the HOL Light term structure as it is defined here: https://github.com/jrh13/hol-light/blob/a1ca1f31539c8e9bd40d324c14951e3c76836787/fusion.ml#L99 Hope this helps! Regards, Petros On 08/11/2019 15:48, Miranda, Brando wrote: Hi, This is my first message to the HOL list so hope its not out of the rules for the list (couldn’t find the rules). I wanted to find the formal grammar for generating terms (formulas) in HOL (Light). I was wondering were I could find such a specification? Thanks! Brando ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Dr. Petros Papapanagiotou Chancellor's Fellow in Digital Technologies CISA, School of Informatics, The University of Edinburgh Academic Coordinator IoT Research & Innovation Service http://homepages.inf.ed.ac.uk/ppapapan/ --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] 0 / 0 = 0 ???
I think there is definitely an advantage in keeping ``x/y`` undefined (even granted that it will always be possible to prove ``?y. x/0 = y``), namely that it means that your proofs are much more likely to directly translate to other formalisms of real numbers where '/' is not total. Of course there is also a disadvantage, in that it makes proof harder. But then, arguably, being forced to justify that we are staying within the "normal" domain of the function is probably a good thing (in a similar way as being forced to conform to a type system is a good thing). I understand that, historically, it is this disadvantage of harder proofs that was the reason for making ``0/0=0`` in HOL. It's much easier for automated routines if they don't have to consider side conditions. Mark. On 15/02/2019 08:56, Chun Tian (binghe) wrote: Thanks to all kindly answers. Even I wanted ``0 / 0 = 0`` to be excluded from at least "extreal_div_def" (in extrealTheory), I found no way to do that. All I can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's going to happen, I do case analysis instead. --Chun Il 14/02/19 18:12, Konrad Slind ha scritto: It's a deliberate choice. See the discussion in Section 1.2 of http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692&rep=rep1&type=pdf On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) mailto:binghe.l...@gmail.com>> wrote: Hi, in HOL's realTheory, division is defined by multiplication: [real_div] Definition ⊢ ∀x y. x / y = x * y⁻¹ and zero multiplies any other real number equals to zero, which is definitely true: [REAL_MUL_LZERO] Theorem ⊢ ∀x. 0 * x = 0 However, above two theorems together gives ``0 / 0 = 0``, as shown below: > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div); val it = ⊢ 0 / 0 = 0: thm How do I understand this result? Is there anything "wrong"? (The same problems happens also in extrealTheory, since the definition of `*` finally reduces to `*` of real numbers) Regards, Chun Tian ___ hol-info mailing list hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] String of term with type information?
Hi, I don't know of any function in HOL Light (although I'm don't know about most recent versions). To write your own, a simple approach would be to print primitive term syntax, with all constants and variables annotated with their type, and to put parentheses around everything at every level. This would be unreadable for anything but small terms, but would parse back in. However, even this would have its problems: (1) If you have generated type variables (e.g. `:?20147`) then HOL Light cannot parse these back in; (2) Any irregular names of constants and variables would cause problems for the parser; (3) Variables overloaded with constants would not get parsed properly. But I suppose you are assuming that the original term was successfully parsed in by HOL Light's parser. If so, then only (1) is a problem. Mark. But other if you are not concerned about type variables, On 29/06/2018 15:26, Yaqing Jiang wrote: Hi, Anyone knows if there is a function in HOL Light that convert terms to strings so that I can save the term and load it the next time? If I do string_of_term `x:num` I only got "x", but I need "x:num". If there's none I'll make one myself anyway. Thanks -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Fwd: Re: Tracking lemmas used by REWRITE_CONV
Hi Yaqing, Try this below - it returns a minimal thm list, based on the "black box" technique. But I haven't tested it properly.. Apply it like this: shrink_rewrite_list REWRITE_CONV [th1;th2;th3;th4] tm;; Cheers, Mark. (* Utils *) let remove_nth_elem n xs = let (xs1,xs2) = chop_list (n-1) xs in (xs1 @ tl xs2);; let remove_one_combs xs = map (C remove_nth_elem xs) (1 -- length xs);; let smaller xs1 xs2 = if (length xs1 <= length xs2) then xs1 else xs2;; let smallest xss = end_itlist smaller xss;; (* shrink_arg_list *) let rec shrink_arg_list (eqr:'a->'a->bool) (f:'b list -> 'a) (xs:'b list) : 'b list = let y = f xs in (* fails overall if fails on original list *) let xss1 = remove_one_combs xs in let foo xs1 = try let y' = f xs1 in (eqr y' y) with Failure _ -> false in let xss2 = filter foo xss1 in if (xss2 = []) then xs else let xss3 = map (shrink_arg_list eqr f) xss2 in smallest xss3;; (* thm_eq *) let list_eq eqr xs1 xs2 = try forall (uncurry eqr) (zip xs1 xs2) with Failure _ -> false;; let thm_eq th1 th2 = let (hs1,c1) = dest_thm th1 in let (hs2,c2) = dest_thm th2 in (list_eq aconv hs1 hs2) && (aconv c1 c2);; (* shrink_rewrite_list *) let shrink_rewrite_list (rewrite_fn:thm list -> 'a -> thm) (ths:thm list) (arg:'a) : thm list = shrink_arg_list (thm_eq) (fun ths -> rewrite_fn ths arg) ths;; On 31/01/2018 15:56, Yaqing Jiang wrote: Hi Mark, Sure, you help me a lot early 2015. Time flies! I think you'll incorporate dependency tracking in a systematic way, so I'll just try the black box method myself (I won't be using this very often and the accuracy is not quite important). I saw a directory Proofrecording in the root directory of HOL Light. There's also anther implementation of dependency tracking as part of anther project here [1] These might be helpful, just in case you need. Thanks for the advice. Best, Yaqing On 31/01/18 15:38, Mark Adams wrote: Hi Yaqing, Good to know someone's been using it! This has always been in my list of things to do, since Tactician is about both refactoring and dependency. I was going to treat REWRITE_CONV (or potentially some other function) like a black box. I think tweaking the REWRITE_CONV code could also be a valid technique, but would require a bit of investment understanding the implementation (which is not trivial!). Best, Mark. On 31/01/2018 15:25, Yaqing Jiang wrote: Hi Mark, Thanks for the quick reply. You (and Tactician) have really helped me a lot these years! I wonder if this feature is in your update plan?If not, I think I should do this myself. Now I'm not sure which method should be considered. I saw most proof recording methods using a way that hacks the fusion.ml, and they don't even touch any functions related to REWRITE_CONV. I found it very low efficient to figure out how these functions in kernel finally used in REWRITE_CONV. I was also thinking to just use a direct way you mentioned. Now that you think it's a solution, I'll try this. I'd like to have the minimal subset of the theorems(lemmas) used by REWRITE_CONV. With the idea you mentioned, there are still 2 levels: 1. Treat REWRITE_CONV as a black box and use another functions to minimise the lemma list 2. If there's a loop inside REWRITE_CONV, and the theorems are passed in serial, maybe I can track the results each time, which might be faster. Best wishes, Yaqing On 31/01/18 14:58, Mark Adams wrote: Hi Yaqing, I could enhance my Tactician tool to do this sort of thing. In fact, a new release is long overdue, so I'll try to find the time to do this soon (but am too busy in the next few weeks). But you say you're looking for a quick patch. One approach would be to apply the original conversion, and then try taking out members of the theorem list and keeping the same result. I can probably knock up the code for this tonight. Note that this idea gives you something a slightly different from removing unused theorems - it's a list that removes any unused theorems plus potentially others that have no effect on the overall result (whether the original rewrite used them or not). Which of these two are you interested in (or does it make no difference to you)? Best, Mark. On 31/01/2018 12:49, Yaqing Jiang wrote: Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term, not all the theorems in th1,th2,... are used. Anyone knows if there is a simple way of finding out which theorems were actually applied? I know there are methods that tracking the entire dependencies of a proven theorem, but a small patch of REWRITE_CONV would work for me. By the way, I'm using HOL Light, so things might be di
Re: [Hol-info] Tracking lemmas used by REWRITE_CONV
Hi Yaqing, I could enhance my Tactician tool to do this sort of thing. In fact, a new release is long overdue, so I'll try to find the time to do this soon (but am too busy in the next few weeks). But you say you're looking for a quick patch. One approach would be to apply the original conversion, and then try taking out members of the theorem list and keeping the same result. I can probably knock up the code for this tonight. Note that this idea gives you something a slightly different from removing unused theorems - it's a list that removes any unused theorems plus potentially others that have no effect on the overall result (whether the original rewrite used them or not). Which of these two are you interested in (or does it make no difference to you)? Best, Mark. On 31/01/2018 12:49, Yaqing Jiang wrote: Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term, not all the theorems in th1,th2,... are used. Anyone knows if there is a simple way of finding out which theorems were actually applied? I know there are methods that tracking the entire dependencies of a proven theorem, but a small patch of REWRITE_CONV would work for me. By the way, I'm using HOL Light, so things might be different. I should be able to adapt the idea to HOL Light. Best regards, Yaqing -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] INST
Hi Michael, Yes, Konrad's right about how types are determined in term quotations, and I too don't know of an INST in HOL Light that unifies the types of its arguments. To get a listing of the types of the free variables in 'th', you can do: map dest_var (frees th);; or to return the type of a given variable, where 'x' is the variable name: assoc x (map dest_var (frees th));; Mark. On 07/01/2018 17:36, Konrad Slind wrote: Hi Michael, What I think is happening is that each quoted element is being parsed separately. This means that the type of the x in `x` is a type variable while the type of `2` is :num. Since INST (I think) just fails if the two types aren't identical, you get the displayed behaviour. There may well be a version of INST in Hol Light that normalizes the arguments but I don't know it. Konrad. On Thu, Jan 4, 2018 at 8:04 PM, Michael Beeson wrote: an example from the tutorial let th1 = REFL `x+1`;; val th1 : thm = |- x + 1 = x + 1 # let th3 = INST [`2`,`x:num`] th1;; val th3 : thm = |- 2 + 1 = 2 + 1 Fine. But if we leave off the type information about x it doesn't work. # let th3 = INST [`2`,`x`] th1;; Warning: inventing type variables Exception: Failure "vsubst: Bad substitution list". I don't understand why this fails. In general you might not know what type x has in th1 (eg., has prioritize_real() or prioritize_vector() been done just before this?) .Is there a command I can issue to ask for "the type of `x` in th1 " ? Michael Beeson -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] [Metamath] Articles on Hale's Kepler Conjecture proof
Hi Ken,
On 20/06/2017 12:38, Ken Kubota wrote:
This 2017 article by Thomas Hales et al. at _Forum of Mathematics, Pi_
seems to be identical with the 2015 article at:
https://arxiv.org/pdf/1501.02155.pdf
Yes, as far as I am aware, if there are any differences they are tiny.
Arxiv is a preprint service.
What I find even more interesting, is Mark's notion of
_faithfulness_,
Unfortunately my definition of "faithfulness" is a bit vague. See
below.
developing further Freek Wiedijk's notion of
_Pollack-consistency_ ("being able to correctly parse formulas that
it printed itself", quoted on p. 8).
Strictly speaking from Freek's original paper, being able to correctly
parse back printed formulas (i.e. forall tm. parse (print tm) = tm), is
called having a "well-behaved" parser/printer. In his paper,
"Pollack-consistency" is about not being able to derive "false" from
assuming the equality of formulae that get printed the same. But when
discussed, these concepts usually all get bundled together and described
as "Pollack-consistency".
It seems as if Mark’s HOL Zero and my R0 are the only
implementations that have this property of Pollack-consistency.
It's good to see that these properties are being taken seriously.
In the case of R0, this even holds for full proofs, and the
property of faithfulness is also implemented:
"Generally, definitions once introduced cannot be removed or
redefined (implementing the notion of 'faithfulness' as defined by
Mark Adams..)"
The intention with my use of the term "faithfulness" was to capture what
I understand others in the theorem proving community mean by the term.
Freek's defintions are really basic properties of parsers/printers that
users might naturally expect to hold, e.g. that parsing printed output
always results in the original internal term. But if a printer printed
"false" as "true" and "true" as "false", and the parser correspondingly
parsed "true" as "false" and "false" as "true", then this would satisfy
Freek's "well-behaved" property. So we need "faithfulness" to cover
that sort of thing. Banning deletion or redefinition of theory isn't
what I meant.
Mark.
Am 19.06.2017 um 23:15 schrieb Norman Megill :
Some of you may be interested in the following.
A writeup of Hale's computer proof ("Flyspeck project") of the
Kepler sphere-packing conjecture has just been published:
T. Hale et. al, A Formal Proof of the Kepler Conjecture
https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
A blog entry on this:
http://blog.journals.cambridge.org/2017/06/12/proving-the-kepler-conjecture/
The following paper discusses auditing issues for several proof
languages in the context of the above proof:
M. Adams, Proof Auditing Formalised Mathematics
http://www.proof-technologies.com/papers/qed_paper.html
Norm
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to metamath+unsubscr...@googlegroups.com.
To post to this group, send email to metam...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero
Unfortunately, and embarrassingly, there is not yet a system description paper for HOL Zero. I plan to write one soon (but I think I said that a few years ago..). I should take a good look at R0 some time and could then comment on it, but good to hear that steps have been taken to address concerns about pretty printing. Clearly the qualities enumerated in Freek's paper are all desirable, but remember that there is also "faithfulness", which isn't fully addressed by the concept of Pollack-consistency. You could print something wrongly but also parse it back in correspondingly wrongly (so, for example, print & parse "true" as "false" and vice versa). Mark. On 13/02/2017 15:38, Ken Kubota wrote: > Dear List Members, > > Through Mark Adams' paper "HOL Zero's Solutions for > Pollack-Inconsistency" > (2016) linked at the HOL Zero homepage, I became aware of the notion of > Pollack-consistency coined by Freek Wiedijk for the property of "a > system being > able to correctly parse formulas that it printed itself": > > Freek Wiedijk: Pollack-inconsistency > http://doi.org/10.1016/j.entcs.2012.06.008 > http://www.cs.kun.nl/~freek/pubs/rap.pdf > > It is amusing to see how the parsing and printing functions of John's > HOL Light > are put on the rack and stretched quite a bit. > Also Isabelle and other systems are examined. > > The interesting point for me was to see that somebody had the same > idea. In the > R0 implementation, not only a formula, but whole printed proofs can be > parsed > again. In fact, if it is compiled and started with "make check", R0 > loops > through all proofs, and this is done twice, with the output of the > first run as > the input of the second, stopping immediately with an error message if > a proof > fails or if the output of the two runs differ. This was implemented > quite > early, so the system was designed from the very beginning to comply > with a > notion of Pollack-consistency not only in terms of formulae, but in > terms of > whole proofs. Like for HOL Zero, this was done in order "to achieve the > highest > levels of reliability and trustworthiness through careful design and > implementation of its core components" - quoted from: > > Mark Adams: HOL Zero's Solutions for Pollack-Inconsistency > http://doi.org/10.1007/978-3-319-43144-4_2 > http://www.proof-technologies.com/holzero/hzsyntax_itp2016.pdf > > > Concerning HOL4 and HOL Zero, I am looking for introductions to them in > the > literature. The appropriate candidates seem to be, at the first glance > (without > having read them already): > > Mark Adams: Introducing HOL Zero (Extended Abstract) > http://doi.org/10.1007/978-3-642-15582-6_25 > > Konrad Slind, Michael Norrish: A Brief Overview of HOL4 > http://doi.org/10.1007/978-3-540-71067-7_6 > > The latter I found as reference no. 14 of Mark's 2016 paper. > > Please let me know if you have other suggestions. > > > Kind regards, > > Ken Kubota > > > > Ken Kubota > http://doi.org/10./100 -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family
Hello Ken,
Not wanting to crowd your diagram too much, but I think maybe HOL Zero
(my system!) deserves a mention. It is a bare bones implementation of
the logic, and is designed to be highly trustworthy and robust.
http://www.proof-technologies.com/holzero.html
It can be used to create simple natural deduction proofs, but is mainly
intended as a proof checker to replay (via some proof recording
mechanism) formal proofs performed on other systems. It has
successfully replayed two quarters of the Flyspeck Project, for example,
that were originally performed in HOL Light in 1.4 billion primitive
inference steps. Another intended role is a pedagogical example of a
basic HOL system, with a simple coding style and lots of code comments
explaining what is going on, which also helps trustworthiness.
Mark Adams.
On 22/10/2016 03:41, Ken Kubota wrote:
> … I have now added the quotes on the genesis of Church's simple theory
> of types,
> and on the invention of λ-calculus and the origin of the λ-notation
> in the "Historical Notes" section at:
> http://dx.doi.org/10./100.111
>
> Also interesting might be Freek Wiedijk's criticism
> concerning the (current) HOL family quoted in the "Criticism" section.
>
> Ken Kubota
>
>
>
> Ken Kubota
> doi: 10./100
> http://dx.doi.org/10./100
>
>
>
>> Anfang der weitergeleiteten Nachricht:
>>
>> Von: Ken Kubota
>
>> Concerning Roger Jones' remarks, let me first note that a legend
>> ("significance of the shape of boxes")
>> can be found on top of the 2nd page, as it doesn't fit on the first
>> anymore.
>>
>> Please also note the arrow from lambda calculus (LC) to simple type
>> theory (STT), narrowing the
>> interest to theories based on LC. The purpose is mainly to distinguish
>> the logics based on LC
>> by their expressiveness in terms of their syntactic features, where
>> STT is characterized by having no
>> type variables in their object language at all. From this perspective,
>> the very early developments
>> prior to LC can be neglected, as Church's 1940 paper is the today's
>> standard reference.
>> For me, even Church's 1940 logic is baroque, as I grew up with
>> Andrews' Q0, which is much more
>> elegant, cleaner, and natural.
>> However, for historical accuracy, I already considered adding a quote
>> mentioning Ramsey and Chwistek from
>>
>> http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf
>>
>> (p. 12)
>> in the Historical Notes section. Note that Church mentions both, and
>> Carnap, in the first footnote
>> of his 1940 article.
>
>
>>> Am 18.10.2016 um 15:34 schrieb Roger Bishop Jones :
>
>>> Credit for the Simple Theory of Types
>>> ===
>>>
>>> Ken's diagram makes it look like this theory begins with Church.
>>>
>>> Its not entirely uncontroversial as to who should have credit for
>>> devising this system.
>>> Most frequently credit has been given to Ramsey, but though he seems
>>> to have had the
>>> idea pretty early on, he never formulated the logical system in
>>> detail (and one might think
>>> that the idea of simplifying Russell's ramified theory would have
>>> occurred to others).
>>>
>>> Recent scholarship suggests that the first fully detailed account of
>>> STT as a formal
>>> system is due to Rudolf Carnap, who, in the course of writing a
>>> logistics textbook
>>> to facilitate the application of formal logic in mathematics and
>>> science, decided to
>>> base it around the simplified rather than the ramified type theory.
>>> I think this particular formulation may have escaped attention
>>> because the book
>>> "Abriss der Logistik" was written in German and has never been
>>> translated into
>>> English.
>>> Until recently the more widely know text by Hilbert and Ackermann was
>>> thought
>>> to be the first formal account of the simple theory of types.
>>> STT appears I believe, only in the second edition of their text, so
>>> though the
>>> first edition (1928) precedes Carnap's (1929) text, he still was in
>>> first with STT.
>>> There were many later textbooks which presented this version of STT
>>> (not based on the lambda-calculus and having "power set" as the
>>> primitive
>>> type constructor), wh
Re: [Hol-info] Type checking issue
Hello Abid, The term quotation fails type checking simply because the types of LHS and RHS of the equality are different: `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M) `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M) As I understand it (I may be wrong here), there is no way of getting the HOL type system to let you express this associativity property about 'horz_conct1'. If you want to express these kinds of properties, I think you need to define your function in a different way, not using types like this. Mark. On 02/07/2016 10:30, Abid Rauf wrote: > Dear All, > > I am having the following type checking issue with a definition in the Matrix > theory of HOL-Light. It seems the double application of the function leads to > an unknown dimension of the matrix, which is causing the problem. I would > appreciate if someone can please help me out with us. > > let horz_conct1 = new_definition > `(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda a b > . > if (b<=dimindex(:N)) > then (A$a$b) else (B$a$(b-(dimindex(:N`;; > > Now if i want to prove that > > g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)= > horz_conct1 (A) (horz_conct1 B C)`;; > > it gives following error > > Exception: Failure "typechecking error (initial type assignment)". > > So the definition is accepted but the proof goal using the function gives the > problem. > > Best Regards, > > Abid Rauf > Ph.D Scholar (CS) & RA SAVe Labs, > School of Electrical Engineering and Computer Science (SEECS), > National University of Science and Technology (NUST), H-12, Islamabad, > Pakistan > -- > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San > Francisco, CA to explore cutting-edge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info-- Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] A question about the theorem in HOL4?
It's a bit confusing. The expressions you enter in the session are not actually in HOL - they are in the functional programming language ML. This is the language used to implement HOL4. You are in an ML toplevel (also called "read-eval-print loop" or "REPL"), with HOL4 already incorporated. ML expressions that you enter in the session get evaluated by the toplevel. These may include standard library functions that are provided by ML, or functions provided by HOL4, or a mixture of both. This is a very powerful paradigm, and allows the user to extend the theorem prover as much as they like with their own facilities. You are able to input HOL expressions (called "terms") by surrounding them with two backquote characters at the start and end, like this: `` FST (1,2) ``; which results in: val it = ``FST (1,2)``: term Inference rules are provided by HOL4 as ML functions that return theorems, for example 'REWRITE_CONV': REWRITE_CONV [pairTheory.FST] ``FST (1,2)``; results in: val it = |- FST (1,2) = 1: thm As Ramana says, there happens to be an ML function called 'fst', which directly corresponds to the HOL function 'FST'. But when you enter the following into the ML session: fst (1,2); to result in val it = 1: int you are not doing theorem proving, you are just doing functional programming. Hope this makes sense. Mark. On 22/06/2016 09:24, Ramana Kumar wrote: > FST is a function in logic, not in ML. > > In this case, there does happen to be a similar function, called fst, in ML. > > Are you trying to specify/prove something in logic? Or are you trying to > write an ML program? > > On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote: > >> Hi,guys >> I am working with HOL4. >> FST is in pairTheory, its definition is >> >> [FST] Theorem >> >> |- ∀x y. FST (x,y) = x >> >> But, When I use it like following: >> >> val n = FST (1,2); >> >> It responses: >> >> ! Toplevel input: >> ! val n = FST (1,2); >> ! ^^^ >> ! Type clash: expression of type >> ! thm >> ! cannot have type >> ! 'a -> 'b >> >> What is the reason? Does anyone know how to use it? >> >> Thanks! >> -- >> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San >> Francisco, CA to explore cutting-edge tech and listen to tech luminaries >> present their vision of the future. This family event has something for >> everyone, including kids. Get more information and register today. >> http://sdm.link/attshape >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > -- > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San > Francisco, CA to explore cutting-edge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info-- Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Fwd: Re: HOL-Light Beginner Questions
I think the problem now is that the syntactic form of the HOL term you supply to 'new_inductive_definition' does not fit what is allowed by the command, because you are not allowed to have compound implications (see the HOL Light reference manual entry for 'new_inductive_definition'). So I think you should get what you intend by transforming it to something logically equivalent, i.e. change "A ==> B ==> C" to "A /\ B ==> C". The error messages could be much better here. Mark. On 17/06/2016 10:51, Heiko Becker wrote: > Hello, > On 06/16/2016 01:45 PM, Mark Adams wrote: > >> Hi Heiko, >> >> That's strange, your corrected version goes through fine on my computer. Do >> you still get the same problem if you restart HOL Light and enter the >> corrected script? What version of HOL Light are you using? >> >> Mark. > > It turns out, that I accidentally loaded both commands. The sstep definition > and the next one. And the failure came from the next one. But I am unable to > fix it currently: > > let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition > `(!(x:num) (e:exp) (s1:cmd) (s2:cmd) (env:num->real) (v:real). > exp_eval e env = v ==> > bstep s1 (upd_env x v env) s2 ==> > bstep (Ass x e s1) env s2) /\ > (!(c:bexp) (s1:cmd) (s2:cmd) (t:cmd) (env:num->real). > bval c env = T ==> > bstep s1 env s2 ==> > bstep (Ite c s1 t) env s2) /\ > (!(c:bexp) (s:cmd) (t1:cmd) (t2:cmd) (env:num->real). > bval c env = F ==> > bstep t1 env t2 ==> > bstep (Ite c s t1) env t2)`;; > Exception: Failure "dest_var: not a variable". > > I have tried removing some parts of the definition to see if I have an > undefined variable lying around but could not arrive at some obvious failure. > > Best regards, > > Heiko > > On 16/06/2016 10:01, Heiko Becker wrote: > > Forwarded Message > > SUBJECT: > Re: [Hol-info] HOL-Light Beginner Questions > > DATE: > Thu, 16 Jun 2016 10:59:44 +0200 > > FROM: > Heiko Becker > > TO: > Ramana Kumar > > CC: > hol-info > > On 06/16/2016 01:57 AM, Ramana Kumar wrote: > I expect it could be because the Boolean constants are spelled "T" and "F" > rather than "true" and "false" in the logic, so the latter are being treated > as free variables. > > Thank you for your explanation. I am getting closer to getting my definition > working. > I have changed it as follows: > > let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition > `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v > env)) /\ > (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\ > (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;; > > But now HOL-Light complains about some construct not being a variable: > Exception: Failure "dest_var: not a variable". > > Can you maybe help me again? > > Best regards, > > Heiko > > On 16 June 2016 at 01:09, Heiko Becker wrote: > > My formalization: > > let exp_INDUCT, exp_REC= define_type > "exp = Var num > | Const real > | Plus exp exp > | Sub exp exp > | Mult exp exp > | Div exp exp";; > > let exp_eval_SIMPS = define > `(exp_eval (Var x) E = E x) /\ > (exp_eval (Const r) E = r) /\ > (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\ > (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\ > (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\ > (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;; > > let bexp_INDUCT, bexp_REC = define_type > "bexp = leq exp exp > | less exp exp";; > > let bval_SIMPS = define > `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\ > (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;; > > let cmd_INDUCT, cmd_REC = define_type > "cmd = Ass num exp cmd > | Ite bexp cmd cmd > | Nop";; > > let upd_env_simps1 = define > `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E > y)`;; > > let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition > `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v > E)) /\ > (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\ > (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;; > > When loading the sstep definitions I get the following failure: > Exception: Failure "new_definition: term not closed". Forwarding my message. Send from wrong mail account intially. --
Re: [Hol-info] Fwd: Re: HOL-Light Beginner Questions
Hi Heiko, That's strange, your corrected version goes through fine on my computer. Do you still get the same problem if you restart HOL Light and enter the corrected script? What version of HOL Light are you using? Mark. On 16/06/2016 10:01, Heiko Becker wrote: > Forwarded Message > > SUBJECT: > Re: [Hol-info] HOL-Light Beginner Questions > > DATE: > Thu, 16 Jun 2016 10:59:44 +0200 > > FROM: > Heiko Becker > > TO: > Ramana Kumar > > CC: > hol-info > > On 06/16/2016 01:57 AM, Ramana Kumar wrote: > >> I expect it could be because the Boolean constants are spelled "T" and "F" >> rather than "true" and "false" in the logic, so the latter are being treated >> as free variables. > > Thank you for your explanation. I am getting closer to getting my definition > working. > I have changed it as follows: > > let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition > `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v > env)) /\ > (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\ > (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;; > > But now HOL-Light complains about some construct not being a variable: > Exception: Failure "dest_var: not a variable". > > Can you maybe help me again? > > Best regards, > > Heiko > > On 16 June 2016 at 01:09, Heiko Becker wrote: > > My formalization: > > let exp_INDUCT, exp_REC= define_type > "exp = Var num > | Const real > | Plus exp exp > | Sub exp exp > | Mult exp exp > | Div exp exp";; > > let exp_eval_SIMPS = define > `(exp_eval (Var x) E = E x) /\ > (exp_eval (Const r) E = r) /\ > (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\ > (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\ > (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\ > (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;; > > let bexp_INDUCT, bexp_REC = define_type > "bexp = leq exp exp > | less exp exp";; > > let bval_SIMPS = define > `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\ > (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;; > > let cmd_INDUCT, cmd_REC = define_type > "cmd = Ass num exp cmd > | Ite bexp cmd cmd > | Nop";; > > let upd_env_simps1 = define > `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E > y)`;; > > let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition > `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v > E)) /\ > (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\ > (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;; > > When loading the sstep definitions I get the following failure: > Exception: Failure "new_definition: term not closed". Forwarding my message. Send from wrong mail account intially. -- What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interface-level. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multi-vendor support for NetFlow, J-Flow, sFlow and other flows. Make informed decisions using capacity planning reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info-- What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interface-level. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multi-vendor support for NetFlow, J-Flow, sFlow and other flows. Make informed decisions using capacity planning reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421&iu=/41014381___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] types issue
Hi Asad,
This is an intended design feature of HOL Light. Unique
numerically-named type variables are created as part of parsing in term
quotations, for term/constants that have undetermined types.
So, for example, if you entered the term quotation `x`, then the parser
wouldn't know which type is intended for "x", and so gives it a unique
type variable, which your printer would show as:
`x:?1143114`
whereas if you entered `x:A`, then the type of "x" is determined, and
your printer would print as:
`x:A`
Mark.
On 16/05/2016 07:38, Asad Ahmed wrote:
> Hi everybody,
> I am working on the VirtualBox 4.02/Ubuntu 12.04 LTS, windows 10 as
> guest OS. I installed the HOL Light following the isntruction on link:
>
> https://bitbucket.org/akrauss/hol-light-workbench
>
> It uses Ocaml version 3.12.1/camlp5-5.15, a slight modification in the
> setup script for downloading the Hol Light from
>
> git clone https://github.com/jrh13/hol-light.git
>
> I use following code fregment for showing types:
>
> let print_typed_var fmt tm =
> let s,ty = dest_var tm in
> pp_print_string fmt ("("^s^":"^string_of_type ty^")") in
> install_user_printer("print_typed_var",print_typed_var);;
>
> When I upload the "Multivariate/make_complex.ml" or simply some other
> theory (let us say "Multivariate/topology.ml"), and want to know about
> the types I come up with datatypes of numerical attributes, e.g,
>
> # TENDSTO_REAL;;
> val it : thm =
> |- ((s:?1143113->real) ---> (l:real)) =
> (lift o (s:?1143113->real) --> lift (l:real))
> I have emacs23.
>
> Thanks in advance
>
> --
> Mobile security can be enabling, not merely restricting. Employees who
> bring their own devices (BYOD) to work are irked by the imposition of MDM
> restrictions. Mobile Device Manager Plus allows you to control only the
> apps on BYO-devices by containerizing them, leaving personal data untouched!
> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
--
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How to transform the proof form
For HOL Light I've got a tool called Tactician that would be ideal for that:
http://www.proof-technologies.com/tactician/
but it doesn't work for HOL4. One day I hope to port it, but that's
unlikely to be done in the near future.
Mark.
on 27/11/15 8:20 AM, Ada wrote:
> Hey guys,
>
> I am learning to use HOL. Here is some code.
>
> load "abs_tools";
>
> open abs_tools;
> val _ = type_abbrev ("num_field", ``:complex -> bool``);
> (* -- *)
> (* Definition of number field.*)
> (* -- *)
>
> val s = ``s : num_field``;
>
> val nf_carrier = ``s SUBSET univ(:complex) /\ s <> {}:complex -> bool``;
> val nf_constant = ``0c IN s /\ 1c IN s``;
> val nf_operation = ``!a:complex b:complex. a IN s /\ b IN s
> ==> (a+b IN s) /\ (a-b IN s) /\
> (a*b IN s)
> /\ (if a <> 0 then b/a IN s
> else a = 0c)``;
>
> val is_num_field_def = Define `
> num_field ^s =
> ^nf_carrier
> /\ ^nf_constant
> /\ ^nf_operation `;
> (* We work on an abstract number field s *)
>
> val _ = set_assums [ ``num_field ^s`` ];
>
> (* prove the coditions of number field *)
>
> val nf_proj_tac =
>
> POP_ASSUM MP_TAC THEN RW_TAC arith_ss [is_num_field_def] THEN STRIP_TAC;
> val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac);
> val constant =
>
> asm_store_thm("constant",nf_constant,nf_proj_tac);
> val operation =
> asm_store_thm("operation",nf_operation,nf_proj_tac);
>
> Now, I want to write the prove in another way. For example, how to
> transform
>
> "val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac); "
>
> into the form of
>
> "g(...)
> e(...)
> e(...)
> "
> Thanks! --Wish.
>
>
>
>
>
> --
>
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] proof structure in Coq
Just to be clear, Tactician (only for HOL Light at the moment) goes between the three styles: - g and e - prove with THEN/THENL/etc - Flyspeck's 'prove_by_refinement', which is a hybrid of the above two Mark. on 18/11/15 8:54 AM, Ramana Kumar wrote: > I usually use ">>" instead of literally "THEN". Arguably that's still too > much "shift". > > Yes I think you're right about tactician - it's for going back and forth > between those styles. > > On 18 November 2015 at 08:41, Freek Wiedijk wrote: > >> Hi Ramana, >> >> >Apparently Coq somewhat recently gained the ability to be explicit about >> >proof structure: >> >http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html >> >(Of course that comes naturally when using tacticals like THEN, THEN1, >> etc.) >> >> Not _very_ recently. It was introduced in 8.4, which is >> from late 2011. And maybe Ssreflect had it long before >> that already? (In my opinion Ssreflect is a much underrated >> proof language, even if it looks like perl.) >> >> Of course in Flyspeck many (most?) proofs are the other >> way around, where there is just a list of tactics that is >> processed like you would successively "e" them interactively. >> I think Mark Adams tactician is exactly about converting >> a THEN-THEN proof to that format? >> >> But I agree that a more structured "bulleted" proof is nicer. >> Even though ergonomically of course having to type THEN >> is monstrous. >> >> Freek >> > > > > > > > -- > > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Emacs Macros for HOL Light Proof
Hi Petros/Joe,
I must admit that I'm not particularly familiar with any of these Emacs/etc
modes for HOL Light and HOL4, although I have seen Proof General, and
ProofTree that interacts with it. How do these other facilities compare?
> Tactician is more general and gives you a full breakdown of the
> packaged proof in interactive steps (and vice-versa), at the cost
> of having to reconstruct core HOL Light data structures. Of course
> Mark would be much better at explaining more details.
That's right, a goal tree is maintained as a tactic proof executes, with
each node storing a goal and a description of the tactic used on it. Goals
are adjusted to carry a pointer to their tree node, and tactics are adjusted
to work with these goals and update the tree. Theorems are also adjusted,
to enable them to be described if they occur as tactic arguments. This all
enables a flattened ("g" and "e" style) or packaged "prove" style) version
of a tactic proof script to be outputted upon user request. A goal tree
graph, with tactics as the nodes, can also be outputted as a .dot file. A
planned enhancement is to output graphs that also show the goal sequent as
you hover the mouse over a node.
So I suppose one could envisage an Emacs mode where the user selected a
packaged proof script to result in a window showing the flattened proof
script and/or the goal tree graph, which would be suitable for stepping
through interactively. The user could edit the proof in this window and
then the packaged proof would get updated accordingly. I think generally
users would be more comfortable editing flattened proof scripts rather than
packaged up ones.
> One advantage that I can think of is when you wish to go through the
> proof of one particular subgoal. This may be confusing if you are
> executing packaged proof steps (e.g. if other subgoals are proven
> simultaneously).
Yes, if the user just sees/edits the packaged proof script, there is the
challenge of how to design a GUI for stepping through this. I suppose the
goal tree graph could highlight the set of nodes that correspond to a given
highlighted tactic in the script, and the graph could be automatically
recalculated as the user edits the script.
Mark.
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Question about camlp5
Hi Robert, Could you provide more information about the circumstances when it fails? Specifically, which versions of OCaml and Camlp5 are you using? Execute the following in a terminal window: ocaml -version camlp5 -v Does this error arise when building HOL Light from source in an OCaml session? Are you starting the session from scratch, or rebuilding HOL Light on top of an existing session that had HOL Light already built? Are you using a very recent download of HOL Light? Do you know the SVN release number, or roughly the date you downloaded? Mark. on 28/5/15 7:13 PM, Robert White wrote: > Dear all, > > I wonder if there is a way I can get rid of the error of : > Error: Unbound value set_jrh_lexer > > Sometimes it is working sometimes it is not. I am very confused. > Is there any advice? > > Thanks a lot! > > -- > Regards, > Robert > > > > > > > -- > > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Question about proof of law of excluded middle.
I forgot to say that the theorem is 'excluded_middle_thm' and its proof is in file 'src/boolclass.ml'. Mark. on 18/5/15 5:17 PM, Mark wrote: > Hello Robert, > > If you're interested in the proof itself, rather than how in how the HOL > Light one works, then there's also a proof in HOL Zero which could help. > This follows the same idea but is a "forwards proof" in terms of basic > inference rule steps rather than tactics, but might (or might not..) be more > understandable. Download the HOL Zero source distribution from: > http://www.proof-technologies.com/holzero/ > > Best, > Mark. > > on 15/5/15 11:22 PM, Robert White wrote: > >> Dear Sir/Madam, >> >> I wonder if you could explain a bit of the last step of the proof of law > of >> excluded middle (in the file class.ml). I am not sure how the rewriting >> magically converted >> >> 0 [`F <=> (@x. (x <=> F) \/ t)`] >> 1 [`T <=> (@x. (x <=> T) \/ t)`] >> 2 [`t`] >> >> `~((@x. (x <=> T) \/ t) <=> (@x. (x <=> F) \/ t)) ==> (@x. (x <=> F) \/ > t)` >> >> to `t \/ ~t` >> >> The proof is as follows: >> >> let EXCLUDED_MIDDLE = prove >> (`!t. t \/ ~t`, >> GEN_TAC THEN SUBGOAL_THEN >> `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T) \/ >> t)` >> MP_TAC THENL >> [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL >> [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN >> DISJ1_TAC THEN REFL_TAC; >> DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN >> TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN >> DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN >> PURE_ONCE_ASM_REWRITE_TAC[] THEN >> *ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;* >> >> PS: Is there a way I can print out how it is done step by step form OCaml >> Toplevel? >> >> Thanks very much! >> -- >> >> Regards, >> Robert >> >> >> >> >> >> > >> -- >> One dashboard for servers and applications across Physical-Virtual-Cloud >> Widest out-of-the-box monitoring support with 50+ applications >> Performance metrics, stats and reports that give you Actionable Insights >> Deep dive visibility with transaction tracing using APM Insight. >> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y >> >> >> >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> > > > > -- > One dashboard for servers and applications across Physical-Virtual-Cloud > Widest out-of-the-box monitoring support with 50+ applications > Performance metrics, stats and reports that give you Actionable Insights > Deep dive visibility with transaction tracing using APM Insight. > http://ad.doubleclick.net/ddm/clk/290420510;117567292;y > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- One dashboard for servers and applications across Physical-Virtual-Cloud Widest out-of-the-box monitoring support with 50+ applications Performance metrics, stats and reports that give you Actionable Insights Deep dive visibility with transaction tracing using APM Insight. http://ad.doubleclick.net/ddm/clk/290420510;117567292;y ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Question about proof of law of excluded middle.
Hello Robert, If you're interested in the proof itself, rather than how in how the HOL Light one works, then there's also a proof in HOL Zero which could help. This follows the same idea but is a "forwards proof" in terms of basic inference rule steps rather than tactics, but might (or might not..) be more understandable. Download the HOL Zero source distribution from: http://www.proof-technologies.com/holzero/ Best, Mark. on 15/5/15 11:22 PM, Robert White wrote: > Dear Sir/Madam, > > I wonder if you could explain a bit of the last step of the proof of law of > excluded middle (in the file class.ml). I am not sure how the rewriting > magically converted > > 0 [`F <=> (@x. (x <=> F) \/ t)`] > 1 [`T <=> (@x. (x <=> T) \/ t)`] > 2 [`t`] > > `~((@x. (x <=> T) \/ t) <=> (@x. (x <=> F) \/ t)) ==> (@x. (x <=> F) \/ t)` > > to `t \/ ~t` > > The proof is as follows: > > let EXCLUDED_MIDDLE = prove > (`!t. t \/ ~t`, > GEN_TAC THEN SUBGOAL_THEN > `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T) \/ > t)` > MP_TAC THENL > [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL > [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN > DISJ1_TAC THEN REFL_TAC; > DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN > TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN > DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN > PURE_ONCE_ASM_REWRITE_TAC[] THEN > *ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;* > > PS: Is there a way I can print out how it is done step by step form OCaml > Toplevel? > > Thanks very much! > -- > > Regards, > Robert > > > > > > > -- > One dashboard for servers and applications across Physical-Virtual-Cloud > Widest out-of-the-box monitoring support with 50+ applications > Performance metrics, stats and reports that give you Actionable Insights > Deep dive visibility with transaction tracing using APM Insight. > http://ad.doubleclick.net/ddm/clk/290420510;117567292;y > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- One dashboard for servers and applications across Physical-Virtual-Cloud Widest out-of-the-box monitoring support with 50+ applications Performance metrics, stats and reports that give you Actionable Insights Deep dive visibility with transaction tracing using APM Insight. http://ad.doubleclick.net/ddm/clk/290420510;117567292;y ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Theorems Produced by Type Definitions
Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with current HOL Light, and it's always better to have closed formulae coming out of definition commands. One small point: the formulae as written in the linked message do not have the intended syntactic form (due to bracketing), and should of course be written as this: (\a. abs (rep a)) = \a. a P = (\r. rep (abs r) = r) Mark. on 16/10/14 5:19 PM, Ramana Kumar wrote: > Hi all, > > There has been an interesting discussion on the OpenTheory mailing list > recently regarding how to simplify the two theorems produced by a type > definition in HOL Light and remove their free variables. The latest message > in the thread, which shows the suggestions by Mario Carneiro can be found > here: > http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html. > > I'm cross-posting to this list because I think using Mario's suggestions > would be an improvement to both HOL Light and Opentheory. I hope the > respective authors of those systems might agree and implement the changes, > and that anyone else with an interest might voice their opinion. > > Cheers, > Ramana > > > > > > > -- > Comprehensive Server Monitoring with Site24x7. > Monitor 10 servers for $9/Month. > Get alerted through email, SMS, voice calls or mobile push notifications. > Take corrective actions from your mobile device. > http://p.sf.net/sfu/Zoho > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Comprehensive Server Monitoring with Site24x7. Monitor 10 servers for $9/Month. Get alerted through email, SMS, voice calls or mobile push notifications. Take corrective actions from your mobile device. http://p.sf.net/sfu/Zoho ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?
Nela, These versions should definitely work together. Just realised - what you presumably did is first try the HOL Light 'make' using other versions of OCaml or Camlp5. So what you needed to do was first do make clean before doing make I would be very surprised if this doesn't work. Mark. on 17/9/14 1:14 PM, Nela Cicmil wrote: > @ Mark: I used the svn download command only this week so probably it has > the most recent version of HOL Light. On svn download, I get the output > "Checked out revision 198", and the CHANGES document inside the hol_light > directory is dated 9th Sept 2014. Here are my ocaml and camlp5 versions: > > hol_light nc$ ocaml -version > The OCaml toplevel, version 4.01.0 > hol_light nc$ camlp5 -v > Camlp5 version 6.11 (ocaml 4.01.0) > > @ Ramana: I'm looking into the pa_j*.ml files, but it's not clear to me how > to write one to work with the ocaml version 4.01.0/camlp5 v 6.11 combo. > > Thanks! > > Best wishes, > Nela > > > Nela Cicmil, D.Phil > Dept. Physiology, Anatomy & Genetics, > University of Oxford > > From: marco.magg...@gmail.com [marco.magg...@gmail.com] on behalf of Marco > Maggesi [magg...@math.unifi.it] > Sent: 17 September 2014 08:15 > To: Mark Adams > Cc: Nela Cicmil; hol-info@lists.sourceforge.net > Subject: Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on > Mac OS X 10.8.5? > > Hi Nela, > > I use the Nix package manager (http://nixos.org/nix/) and it works well for > me. I use Nix both on Max and on Linux. It is nice because it makes the > installation of HOL Light completely independent from the versions of ocaml, > camlp5 (or any other software indeed) installed in your machine. > > If you want to try, here is what you have to do: > > 1. Install Nix. Follow the instructions from the nix manual > (http://nixos.org/nix/manual). Basically you have to type the following > four commands in a terminal: > > > $ bash <(curl https://nixos.org/nix/install) > source /usr/local/etc/profile.d/nix.sh > > > nix-channel --add http://nixos.org/channels/nixpkgs-unstable > nix-channel --update > > 2 > . > Then you can install HOL Light with a single command (no need to install > OCaml or Camlp5) > > > nix-env -i hol_light > > For more serious work you probably need to use checkpointing which is > available only on Linux. For this I use a NixOS (http://nixos.org) > VirtualBox appliance. Do not esitate to ask for more details if you are > interested. > > Best, > Marco > > 2014-09-17 5:50 GMT+02:00 "Mark Adams" > mailto:m...@proof-technologies.com>>: > Hi Nela, > > There have been various problems over the years, but I get no problems with > recent versions of HOL Light (downloaded since May 2014, including SVN > version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11 > running on Fedora 17. > > Do you know the HOL Light SVN version (or otherwise, what date did you > download)? > > And can you please check your OCaml and Camlp5 versions by executing the > following from the same terminal window from which you are trying the HOL > Light make?: > ocaml -version > camlp5 -v > > Mark. > > on 16/9/14 4:45 PM, Nela Cicmil > mailto:nela.cic...@dpag.ox.ac.uk>> wrote: > >> Dear HOL Light users, >> >> Would anyone be able to please advise me on how to install HOL Light on my >> Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5. >> >> My trouble is that I can't seem to get compatible versions of Ocaml, > camlp5 >> and HOL Light installed on my system, mainly because the Ocaml version > that >> comes with OPAM, v 4.01.0, seems to be too recent to run with the slighter >> older camlp5 versions compatible with HOL Light. >> >> Has anyone recently installed HOL Light on a Mac, and has advice on which >> versions of Ocaml and camlp5 to install, and which procedure to use to >> install them? In particular, is it possible to install an older version of >> Ocaml, e.g. v 3.12, using OPAM? >> >> The specific issues I've encountered are detailed below. Any advice would > be >> much appreciated. >> >> Thank you, >> >> Best wishes, >> Nela >> >> Nela Cicmil, D.Phil >> Dept. Physiology, Anatomy & Genetics, >> University of Oxford >> >> >> After various attempts to install Ocaml on the Mac, I installed (using >> homebrew) the latest version of OPAM, which comes with Ocaml version > 4.01.0. >> On basic testing at the terminal, Ocaml se
[Hol-info] Flyspeck Project completion
For those to whom the news has not already reached, Tom Hales' Flyspeck Project is now complete! This establishes a formal proof of Hales' 1998 Kepler Conjecture proof, and is a landmark in the formalisation of mathematics. The formal proof was mainly done in HOL Light, but with one part (the classification of tame hypermaps) done in Isabelle/HOL. It involves hundreds of thousands of lines of proof script, resulting in billions of primitive inferences. I include below Hales' original announcement from 5 weeks ago. Mark. - We are pleased to announce the completion of the Flyspeck project, which has constructed a formal proof of the Kepler conjecture. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than the face-centered cubic packing. It is the oldest problem in discrete geometry. The proof of the Kepler conjecture was first obtained by Ferguson and Hales in 1998. The proof relies on about 300 pages of text and on a large number of computer calculations. The formalization project covers both the text portion of the proof and the computer calculations. The blueprint for the project appears in the book "Dense Sphere Packings," published by Cambridge University Press. The formal proof takes the same general approach as the original proof, with modifications in the geometric partition of space that have been suggested by Marchal. A formal proof is a mathematical proof that has been checked by computer from the foundational axioms of mathematics and primitive inference rules. A formal proof provides a much higher degree of certification than traditional standards of rigor and peer review by referees. The formal proof has been constructed in a combination of the Isabelle and HOL Light formal proof assistants. The Isabelle portion of the formalization, which was carried out by Bauer and Nipkow, classifies all tame graphs. This enumerates the combinatorial structures of potential counterexamples to the Kepler conjecture. This classification theorem has been translated directly by hand into a corresponding term `import_tame_classification` in the HOL Light proof assistant. At a conceptual level, the classification theorem could be formulated as a large SAT problem, and SAT problems pass easily from one proof assistant to another. The rest of the formalization has been carried out in HOL Light, producing a formal theorem |- import_tame_classification /\ the_nonlinear_inequalities ==> the_kepler_conjecture where `the_kepler_conjecture` is defined as the following term `(!V. packing V ==> (?c. !r. &1 <= r ==> &(CARD(V INTER ball(vec 0,r))) <= pi * r pow 3 / sqrt(&18) + c * r pow 2))` In standard mathematical language, this states that for every packing V (which is identified with the set of centers of balls of radius 1), there exists a constant c controlling the error term, such that for every radius r that is at least 1, the number of ball centers inside a spherical container of radius r is at most pi * r^3 / sqrt(18), plus an error term of smaller order. As r tends to infinity, this gives the density bound pi / sqrt(18) = 0.74+, which is the density of the face-centered-cubic packing. The term `the_nonlinear_inequalities` is defined as a conjection of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours. Almost all verifications were made in parallel with 32 cores, hence the real time is about 5000 / 32 = 156.25 hours. Nonlinear inequalities were verified with compiled versions of HOL Light and the verification tool developed in Solovyev's 2012 thesis. To check that no pieces were overlooked in the distribution of inequalities to various cores, the pieces have been reassembled in a specially modified version of HOL Light that allows the import of theorems from other sessions of HOL light. In that version, we obtain a formal proof of the theorem |- the_nonlinear_inequalities The code for the project is available for download from http://afp.sourceforge.net/devel-entries/Flyspeck-Tame.shtml (Isabelle tame graphs) https://code.google.com/p/flyspeck/ (HOL Light Flyspeck project). There have been many contributors to the project as indicated in the credits below. Many of them will be co-authors of the published account of the formal proof. Sincerely, Thomas Hales, Alexey Solovyev, Hoang Le Truong, and the Flyspeck Team August 10, 2014 CREDITS Project Director: Thomas Hales Project Managers: Ta Thi Hoai An, Mark Adams HOL Light libraries and support: Jo
Re: [Hol-info] advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?
Hi Nela,
There have been various problems over the years, but I get no problems with
recent versions of HOL Light (downloaded since May 2014, including SVN
version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
running on Fedora 17.
Do you know the HOL Light SVN version (or otherwise, what date did you
download)?
And can you please check your OCaml and Camlp5 versions by executing the
following from the same terminal window from which you are trying the HOL
Light make?:
ocaml -version
camlp5 -v
Mark.
on 16/9/14 4:45 PM, Nela Cicmil wrote:
> Dear HOL Light users,
>
> Would anyone be able to please advise me on how to install HOL Light on my
> Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.
>
> My trouble is that I can't seem to get compatible versions of Ocaml,
camlp5
> and HOL Light installed on my system, mainly because the Ocaml version
that
> comes with OPAM, v 4.01.0, seems to be too recent to run with the slighter
> older camlp5 versions compatible with HOL Light.
>
> Has anyone recently installed HOL Light on a Mac, and has advice on which
> versions of Ocaml and camlp5 to install, and which procedure to use to
> install them? In particular, is it possible to install an older version of
> Ocaml, e.g. v 3.12, using OPAM?
>
> The specific issues I've encountered are detailed below. Any advice would
be
> much appreciated.
>
> Thank you,
>
> Best wishes,
> Nela
>
> Nela Cicmil, D.Phil
> Dept. Physiology, Anatomy & Genetics,
> University of Oxford
>
>
> After various attempts to install Ocaml on the Mac, I installed (using
> homebrew) the latest version of OPAM, which comes with Ocaml version
4.01.0.
> On basic testing at the terminal, Ocaml seemed to be working fine. I then
> installed camlp5 version 6.11, using ./configure --transitional mode, and
> that seemed to be running fine as well. When I then attempted to install
HOL
> Light, using the svn checkout http://hol-light.googlecode.com/svn/trunk/
> hol_light procedure, and got the following error on "make":
>
> File "pa_j.ml", line 112, characters 72-74:
> Error: This expression has type (string * MLast.ctyp) list
> but an expression was expected of type
> ('a * MLast.ctyp) list Ploc.vala
> make: *** [pa_j.cmo] Error 2
>
> - On reading various previous posts, it seemed that the latest versions of
> camlp5 could be at fault. I attempted to install older versions of camlp5,
> version 6.02.0 and 5.15, but I got the following error on ./configure
> --transitional:
>
> Sorry: the compatibility with ocaml version "4.01.0"
> is not yet implemented. Please report.
> Information: directory ocaml_stuff/4.01.0 is missing.
> Configuration failed.
>
> - With campl5 version 6.06 it's the following error (I'm not sure what the
> preprocessor is here):
>
>>> Fatal error: OCaml and preprocessor have incompatible versions
> Fatal error: exception Misc.Fatal_error
> make[2]: *** [versdep.cmo] Error 2
> make[1]: *** [core] Error 2
> make: *** [world.opt] Error 2
>
> - So then I attempted to install an earlier version of Ocaml, version
> 3.12.1, in the hope that it would be compatible with the earlier versions
of
> camlp5. This did not seem possible with OPAM so I downloaded the original
> source distribution tar.gz from http://ocaml.org/releases/3.12.1.html. I
> believe my system has the necessary dependencies in the form of Xcode
5.11,
> gcc and gnumake running. However, the "make world" installation command
> exits on the following error:
>
> make coldstart
> cd byterun; make all
> gcc -DCAML_NAME_SPACE -O -fno-defer-pop -no-cpp-precomp -Wall
> -D_FILE_OFFSET_BITS=64 -D_REENTRANT-c -o interp.o interp.c
> clang: error: unknown argument: '-fno-defer-pop'
> [-Wunused-command-line-argument-hard-error-in-future]
> clang: note: this will be a hard error (cannot be downgraded to a warning)
> in the future
> make[2]: *** [interp.o] Error 1
> make[1]: *** [coldstart] Error 2
> make: *** [world] Error 2
>
>
>
> --
> Want excitement?
> Manually upgrade your production database.
> When you want reliability, choose Perforce.
> Perforce version control. Predictably reliable.
>
http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
--
Want excitement?
Manually upgrade your production database.
When you want reliability, choose Perforce
Perforce version control. Predictably reliable.
http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill
These are nice explanations, but here are a few comments and
corrections:
> * 1) the definitions of type bool and the constant =
*
>
You're still using the terminology "definition" for 'bool'
and '=', whereas they are only *declared* in each of the HOL systems'
axiomatisations, and not *defined*. Declare is when you just introduce
an entity to the theory, define is when you declare something and
constrain it (beyond type constraints). The HOL Light command
'new_constant' declares a new constant, whereas 'new_definition' defines
a new constant.
> * 2) sequents, new_basic_definition and the HOL
Light inference rules
>
> Similar code is found in the 150 line
segment of the file thm.ml
> module Hol : Hol_thm_primitives = struct
>
[...]
> end;;
> but I won't discuss this. My guess is that the fusion.ml
definitions are
> used first for some basic theorem and then the thm.ml
definitions are used
> for more sophisticated or faster handling of
theorems.
Actually fusion.ml replaces type.ml, term.ml and thm.ml, but
these unused source code files are still hanging around in the HOL Light
source directory.
> So a theorem is of the form Sequent ([a1;...;an],
t), which we will write as
>
> {a1,...,an} |- t
>
> It will turn out
that t will always have HOL type bool.
And a1,..,an will also always
have HOL type bool.
> Sequent is an Ocaml constructor defined in the
module Hol. Thus we have no
> way to produce theorems except by
sequent-producing functions defined in
> Hol ...
The crucial point is
that OCaml type 'thm' is an abstract datatype, and so its only
constructors are those supplied in the module interface (which are the
sequent-producing functions defined in Hol).
> ...
> including
new_basic_definition,
> ...
>
> Another way to produce sequents is
with the Hol module function
> new_basic_type_definition.
>
> The only
other way to produce sequents is with 10 Hol module functions which
>
produce theorems from earlier theorems:
Actually, there is also
'new_axiom'.
> ...
> The term T is are defined to have type bool by
>
> let T_DEF = new_basic_definition
> `T = ((p:bool. p) = (p:bool.
p))`;;
>
> Note a subtlety about = here which I messed up in a previous
post. The
> first = is the Ocaml =, meaning that T_DEF is bound in Ocaml
to the value of
> the new_basic_definition expression. Each of the other
two =s is the
> constants = of type A->A->bool. Therefore the RHS
(p:bool. p) = (p:bool.
> p) has type bool, and therefore T has type
bool.
To use the correction terminology, we say "are instances of the
constant '=', which has generic type `:A->A->bool` ".
> I think the
parser treats prefixes in a special way, but I'm not sure what
> it
is.
Prefix operators bind differently from nonfix operators, and less
tightly, so that `~ ~ p` is the double negation of `p`, and `~ P x` is
the negation of `P x`. If '~' were nonfix, you'd need to supply extra
parentheses in these expressions.
Best,
Mark. --
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill,
on 21/3/14 4:28 PM, Bill Richter wrote:
> ... BTW where is the constant = defined in HOL Light? I see now that
> the line in bool.ml override_interface ("<=>",`(=):bool->bool->bool`);;
> just means that <=> is being defined as a synonym for = in this special
> case. In general = has type A->A-bool.
That's right, the line in bool.ml is just defining an alias. The constant
'=' is *declared* (there is a difference in meaning between the words
"declare" and "define") in fusion.ml, in the line that sets the ML binding
'the_term_constants' (approx line 206). The type constants 'bool' and 'fun'
are declared similarly in fusion.ml in the line that sets
'the_type_constants' (approx line 114).
Mark.
--
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
I should have said '@' instead of '?' here. The constant '?' is actually defined in these axiomatisations (using '@'). Mark. on 21/3/14 9:10 AM, Mark Adams wrote: > ... In HOL Light's axiomatisation, the only such entities are the 'bool' and > 'fun' type constants and the '=' constant (the other axiomatisations also > have the '==>' and '?' constants) -- Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/13534_NeoTech ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill, on 21/3/14 6:19 AM, Bill Richter wrote: > ... > > T = ((λxbool . x) = (λxbool . x)) > > So it looks to me that HOL Light is defining Tom's primitive = in terms of > the Ocaml =. Is that correct? And maybe that just means that the HOL Light > primitive = is "represented" in Ocaml as the ordinary =? No, not at all. The above is defining the constant 'T'. The constant '=' does not have a definition in HOL Light, or in any of the HOL axiomatisations. We have to start somewhere with entities that don't have definitions but are just declared. In HOL Light's axiomatisation, the only such entities are the 'bool' and 'fun' type constants and the '=' constant (the other axiomatisations also have the '==>' and '?' constants). In the logic, the meaning of such entities is not captured in definitions, but instead "drops out" from the aggregation of the axioms and primitive inference rules. Best, Mark. -- Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/13534_NeoTech ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill, Have you tried looking at the HOL Zero source code? I think you will find it illustrative for your purposes. It has a simple core like HOL Light, but the source code explains more of what is going on. In file 'corethy.ml' I try to motivate the axioms and constant definitions used in the axiomatisation. I try to use terminology as carefully as possible, and to define everything precisely in the bundled HOL glossary, although I'm always looking for suggestions for improvements (it's changed a lot over the years, thanks to the suggestions of Rob, John and others). And all derived theorems and inference rules (e.g. in bool.ml') have annotations in comments that explain what is going on in the derivation (although I've just spotted a couple of theorems that don't). HOL Zero has a different axiomatisation of the HOL logic than the one used in HOL Light and the one used in HOL4 and ProofPower. In a nutshell, it is the same as HOL4 with the same primitive constants, except that it has 3 basic primitive inference rules (EQ_MP, INST and MK_COMB) in place of the rather complicated SUBST (making it close to HOL Light's set of primitive inference rules), and that it derives BOOL_CASES_AX (using the Beeson-like proof) instead of IMP_ANTISYM_AX (whereas HOL Light derives both). So it's axiomatisation is between that of HOL4 and HOL Light, but somewhat closer to HOL4's "classic" axiomatisation that HOL Light's. Best, Mark. The source code comments explain a of what is going on. on 21/3/14 6:19 AM, Bill Richter wrote: > Thanks, Konrad! You seem to agree with me here, that the > typed-LC-implies-FOL isn't actually important: > > My personal feelings on this foundational aspect are that the > actual set of axioms isn't that important provided the usual > introduction and elimination rules of predicate calculus can be > derived from them. > > Now you're encouraging me to go read Church's typed LC paper more carefully, > and see if I can work out the apparent difference between Church and what I > quoted Andrews as saying about Church: > > My recollection (don't have citations to hand) is that Church > originally wanted the untyped lambda calculus to serve as a > foundation for logic, but that was discovered to be > inconsistent. Something like Russell's paradox would be easy to > code up in it. However, the simply typed lambda calculus worked > better, i.e., it supports the derivation of the expected FOL-like > rules, as we see in HOL theorem provers, and it is sound. > > Here's a some dumb questions about HOL4 and HOL Light. > > On p 29 of LOGIC, you write that there are constants > Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have written > that as > T:bool and ∀:(α→bool)→bool > Are the apparent subscripts supposed to indicate colons, or does HOL4 not > use colons for type annotations? > > I'm having trouble seeing your derivation of the expected FOL-like rules in > HOL Light. Is there a paper where somebody explained these HOL derivations, > or is it perhaps easier to understand in HOL4? > > Tom Hales writes on p 6 of > http://www.ams.org/notices/200811/tx081101370p.pdf > > The system [HOL Light] has only two primitive constants. One of them is the > equality symbol (=) of type :A->A->bool. So = is primitive, and p 5 lists > the HOL Light axioms about the properties of =. Let's try to find this in > the HOL Light sources. In > hol_light/bool.ml > it seems to me that first the type bool is defined, > then = and <=> are defined to have type bool->bool->bool and to be the same > as each other, > then T is defined as > > let T_DEF = new_basic_definition > `T = ((\p:bool. p) = (\p:bool. p))`;; > > That's your first HOL axiom on p 29 (again without colons): > > T = ((λxbool . x) = (λxbool . x)) > > So it looks to me that HOL Light is defining Tom's primitive = in terms of > the Ocaml =. Is that correct? And maybe that just means that the HOL Light > primitive = is "represented" in Ocaml as the ordinary =? > > -- > Best, > Bill > > > > -- > Learn Graph Databases - Download FREE O'Reilly Book > "Graph Databases" is the definitive new guide to graph databases and their > applications. Written by three acclaimed leaders in the field, > this first edition is now available. Download your free book today! > http://p.sf.net/sfu/13534_NeoTech > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo
Re: [Hol-info] More on set comprehensions
Ah yes, point taken.
on 8/1/14 10:13 AM, Rob Arthan wrote:
> Mark,
>
> On 8 Jan 2014, at 03:22, Mark Adams wrote:
>
>> Not wanting to be too picky here (because I very much agree with the
> thrust
>> of what Rob is saying), but isn't ProofPower term quotation parsing
>> sensitive to the subgoal package state (specifically, free variables in
> term
>> quotations pick up the types of existing free variables in the subgoal
>> package proof)?
>
> Yes. That's why I mentioned a context when I said "the same string of
> symbols should always parse to the same
> term in any given context".
>
> Regards,
>
> Rob.
>
>>
>> Mark.
>>
>> on 7/1/14 5:04 PM, Rob Arthan wrote:
>>
>>> Bill,
>>>
>>>> On 4 Jan 2014, at 05:17, Bill Richter wrote:
>>> ...
>>>
>>> On 7 Jan 2014, at 16:22, Rob Arthan wrote:
>>>> I think we will just have to agree differ about this. Let me just make
>> two
>>> comments:
>>>>
>>>
>>> Something very odd happened with my e-mail client which caused it to
>> discard
>>> the
>>> two comments. They were as follows:
>>>
>>> (a) Too much mathematical notation is explained away as short-hands,
> i.e.,
>>> as syntactic abbreviations. This is a consequence of the traditional
>>> pretence that mathematics is founded on first-order set theory and
>>> of the inexpressiveness of first-order languages. In a higher-order
>>> logic you can generally replace these short-hands by first class
>>> mathematical
>>> citizens that you can reason about in their own right. This often
>>> fits in well with a categorical way of thinking about what you are
>>> doing. In the case in point, the categorical account of set
> comprehensions
>>> would be in the category of sets and relations. Let me write R : X <-> Y
>>> to mean that R is a relation between the sets X and Y and let BOOL
>>> be the two-point set {F, T}. Given a relation R:X <-> BOOL, we
>>> associate the subset R^{-1}({T}). Given a function f : X -> Y and
>>> a function p : X -> BOOL, we get a relation R : Y <-> BOOL
>>> in the obvious way by defining R = p o f^{-1} and hence
>>> the associated subset R^{-1}({T}) of Y. Note there are no bound
variables
>>> in this categorical description of {f x | p x}: they are all hidden in
> the
>>> definitions of relational composition, relational image and
>>> relational inverse. From what you say above you would
>>> presumably object to that.
>>>
>>> (b) My original objection was that something like
>>> `{x | x > 0}` = `{x | x > 0}` evaluates to false in HOL Light
>>> because the two terms use a different name for the
>>> hidden bound variable that you are so fond of. I now
>>> realise that things like `x` = `x` also evaluate false
>>> because you get different type variables. I can only conclude
>>> that the HOL Light parser does not share what I know was
>>> a design goal of the ProofPower-HOL parser which was that
>>> the same string of symbols should always parse to the same
>>> term in any given context. I suspect this is also a design goal
>>> of the HOL4 parser (which, like ProofPower-HOL, uses
>>> 'a, 'b, 'c etc. for invented type variables).
>>>
>>> Regards,
>>>
>>> Rob.
>>
>>
>
> --
>> 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
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
>
>
>
> --
> 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. Sta
Re: [Hol-info] More on set comprehensions
Not wanting to be too picky here (because I very much agree with the thrust
of what Rob is saying), but isn't ProofPower term quotation parsing
sensitive to the subgoal package state (specifically, free variables in term
quotations pick up the types of existing free variables in the subgoal
package proof)?
Mark.
on 7/1/14 5:04 PM, Rob Arthan wrote:
> Bill,
>
>> On 4 Jan 2014, at 05:17, Bill Richter wrote:
> ...
>
> On 7 Jan 2014, at 16:22, Rob Arthan wrote:
>> I think we will just have to agree differ about this. Let me just make
two
> comments:
>>
>
> Something very odd happened with my e-mail client which caused it to
discard
> the
> two comments. They were as follows:
>
> (a) Too much mathematical notation is explained away as short-hands, i.e.,
> as syntactic abbreviations. This is a consequence of the traditional
> pretence that mathematics is founded on first-order set theory and
> of the inexpressiveness of first-order languages. In a higher-order
> logic you can generally replace these short-hands by first class
> mathematical
> citizens that you can reason about in their own right. This often
> fits in well with a categorical way of thinking about what you are
> doing. In the case in point, the categorical account of set comprehensions
> would be in the category of sets and relations. Let me write R : X <-> Y
> to mean that R is a relation between the sets X and Y and let BOOL
> be the two-point set {F, T}. Given a relation R:X <-> BOOL, we
> associate the subset R^{-1}({T}). Given a function f : X -> Y and
> a function p : X -> BOOL, we get a relation R : Y <-> BOOL
> in the obvious way by defining R = p o f^{-1} and hence
> the associated subset R^{-1}({T}) of Y. Note there are no bound variables
> in this categorical description of {f x | p x}: they are all hidden in the
> definitions of relational composition, relational image and
> relational inverse. From what you say above you would
> presumably object to that.
>
> (b) My original objection was that something like
> `{x | x > 0}` = `{x | x > 0}` evaluates to false in HOL Light
> because the two terms use a different name for the
> hidden bound variable that you are so fond of. I now
> realise that things like `x` = `x` also evaluate false
> because you get different type variables. I can only conclude
> that the HOL Light parser does not share what I know was
> a design goal of the ProofPower-HOL parser which was that
> the same string of symbols should always parse to the same
> term in any given context. I suspect this is also a design goal
> of the HOL4 parser (which, like ProofPower-HOL, uses
> 'a, 'b, 'c etc. for invented type variables).
>
> Regards,
>
> Rob.
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
Oops. That last email contains an error in the detail. The HOL Light adaption of 'plexer.ml' and 'pa_o.ml' is called 'pa_j.ml'. Mark. on 15/10/13 2:29 PM, Mark Adams wrote: > Hi Rob, > > Yes, you not only need a sufficiently recent version of Camlp5 for your > version of OCaml, you also need to create a sufficiently recent > adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code > files etc/). You are right that you can work out what adaptions to do by > diffing corresponding older versions of the unadapted and adapted Camlp5 > files. These Camlp5 files are 'lib/lexer.ml' and 'etc/pa_o.ml', but the > adaption for HOL Light is combined into one file called 'pa_o.ml'. Note > that Camlp5 6.07 or later is required for OCaml 4.00, and Camlp5 6.11 or > later is required for OCaml 4.01. > > I think the warnings you get may be from superfluous #load directives in > your adapted 'pa_j.ml' file, so comment out the following two lines in the > adapted 'pa_o.ml' file and everything should go smoothly: > #load "pa_extend.cmo";; > #load "q_MLast.cmo";; > > Note that HOL Zero (also implemented in OCaml) does a similar thing to HOL > Light, in that it uses Camlp5 to adjust the OCaml lexical syntax for HOL > quotations (although in HOL Light there are also changes to the OCaml > syntax). Installation works smoothly for HOL Zero for all versions of > OCaml. Also, the HOL Zero distribution has relatively detailed comments in > Section 2 of INSTALL and Section 2 of 'etc/README', if you want to > understand a little more about what is going on. > > Mark. > > on 14/10/13 2:07 PM, Rob Arthan wrote: > >> >> On 14 Oct 2013, at 12:53, Rob Arthan wrote: >> >>> Can anyone help me with building HOL light? I get the following when I > run >> make: >>> >>> File "pa_j.ml", line 1918, characters 35-43: >>> While expanding quotation "str_item": >>> Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' >> (in >>> [str_item]) >>> Error while running external preprocessor >>> Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > >> /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df >>> >>> I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 > of >> the HOL light source. >>> >>> Regards, >>> >>> Rob. >> >> By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light > to >> compile. I can provide a patch if anyone wants it, but it still gives >> warnings, so it really needs attention from someone who understands it. > It >> seems a shame that this involves so much copy/paste/tweak re-use of the >> camlp5 source. >> >> Regards, >> >> Rob. >> >> > >> -- >> October Webinars: Code for Performance >> Free Intel webinars can help you accelerate application performance. >> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most >> from >> the latest Intel processors and coprocessors. See abstracts and register > >> > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> > > > > -- > October Webinars: Code for Performance > Free Intel webinars can help you accelerate application performance. > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most > from > the latest Intel processors and coprocessors. See abstracts and register > > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Trouble building HOL light
Hi Rob, Yes, you not only need a sufficiently recent version of Camlp5 for your version of OCaml, you also need to create a sufficiently recent adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code files etc/). You are right that you can work out what adaptions to do by diffing corresponding older versions of the unadapted and adapted Camlp5 files. These Camlp5 files are 'lib/lexer.ml' and 'etc/pa_o.ml', but the adaption for HOL Light is combined into one file called 'pa_o.ml'. Note that Camlp5 6.07 or later is required for OCaml 4.00, and Camlp5 6.11 or later is required for OCaml 4.01. I think the warnings you get may be from superfluous #load directives in your adapted 'pa_j.ml' file, so comment out the following two lines in the adapted 'pa_o.ml' file and everything should go smoothly: #load "pa_extend.cmo";; #load "q_MLast.cmo";; Note that HOL Zero (also implemented in OCaml) does a similar thing to HOL Light, in that it uses Camlp5 to adjust the OCaml lexical syntax for HOL quotations (although in HOL Light there are also changes to the OCaml syntax). Installation works smoothly for HOL Zero for all versions of OCaml. Also, the HOL Zero distribution has relatively detailed comments in Section 2 of INSTALL and Section 2 of 'etc/README', if you want to understand a little more about what is going on. Mark. on 14/10/13 2:07 PM, Rob Arthan wrote: > > On 14 Oct 2013, at 12:53, Rob Arthan wrote: > >> Can anyone help me with building HOL light? I get the following when I run > make: >> >> File "pa_j.ml", line 1918, characters 35-43: >> While expanding quotation "str_item": >> Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' > (in >> [str_item]) >> Error while running external preprocessor >> Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > > /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df >> >> I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174 of > the HOL light source. >> >> Regards, >> >> Rob. > > By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light to > compile. I can provide a patch if anyone wants it, but it still gives > warnings, so it really needs attention from someone who understands it. It > seems a shame that this involves so much copy/paste/tweak re-use of the > camlp5 source. > > Regards, > > Rob. > > > -- > October Webinars: Code for Performance > Free Intel webinars can help you accelerate application performance. > Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most > from > the latest Intel processors and coprocessors. See abstracts and register > > http://pubads.g.doubleclick.net/gampad/clk?id=60134071&iu=/4140/ostg.clktrk > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- October Webinars: Code for Performance Free Intel webinars can help you accelerate application performance. Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from the latest Intel processors and coprocessors. See abstracts and register > http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
>> HOL Light and HOL Zero don't use OCaml's lexing facilities, but >> implement their own from scratch. > > Wow, I didn't know that! Where can I learn about HOL Light lexing > facilities? HOL Light's nice, simple and compact, but is a bit light on source code comments. It's got a snappy little lexer, implemented towards the start of parser.ml. If you can't understand this, then take a look at HOL Zero's. Part of the point of HOL Zero is to have more explanation in the source code, so that non-experts stand a chance of understanding what's going on. Another is that quotation syntax is carefully designed to avoid issues related to parser/printer completeness/soundness, so that any valid HOL name can be parsed in and unambiguously pretty printed. So the lexer, implemented in lexer.ml, is more lengthy but is well commented. >> All exceptions are pretty printed in OCaml, > > I don't think that's right. Before I wrote my > > let PrintErrorFail s = > open_box 0; print_string s; close_box (); print_newline (); fail();; > > I was always getting strings with double-quotes and \n instead of newlines > when I used failwith. Well, it's very simple pretty printing. It's still pretty printing though. > and I thought the whole point of your post was that you weren't > happy with this pretty printing for Failure exceptions, and so I > explained how to override it just for Failure exceptions and keep > the pretty printer for all other exceptions exactly the same. > > I wasn't happy with how failwith printed any error message, and the main > exception for me is Not_found. Now my only problem is the minor one of > seeing > Exception "". What about instead of printing out your failure message followed by using fail(), just using failwith applied to a string argument that is your failure message? >> Regarding what the OCaml reference manual says: OCaml's Pervasives >> module is initially opened, but not its Format module. > > Ah, but I think section 20.2 Module Pervasives (p 318) says that > print_string and print_newline are pervasive anyway, even though, as you > say, the entire Format module is not opened. Yes, but 'print_string' and 'print_newline' are in *both* modules: Pervasives and Format. All the other formatting stuff is not in Pervasives. Mark. -- Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill, > Let me try to explain. My only objection to my PrintErrorFail is minor: > it prints Exception: Failure "". at the end, but arguably this is a good > error message. What you do is print out the message regardless of whether the exception bubbles up to the toplevel. The solution I'm suggesting only prints the message if the exception hits the toplevel. I don't know which functionality you want. > "fail" has an link in the HOL Light reference manual, and "failwith" is > only explain in the "fail" link: 'failwith' is part of OCaml itself, but 'fail' is a just a HOL Light thing. > I think that you understood a great deal more about pretty-printing error > messages, and I advise you to try to write up what you know.We need good > documentation.Perhaps you understand printer.ml well enough to recommend > some change by which all HOL Light error messages are pretty-printed. I > certainly don't see how to do this. Yes we do, and that's on of the things I'm aiming to do with HOL Zero. My hands are full with various projects of my own, and I don't really have time to document HOL Light. > I just looked at your Tactician sources, and I have some non-expert > responses: This from mlconcrete.ml > > > let exec x > (ignore o Toploop.execute_phrase false Format.std_formatter o > !Toploop.parse_toplevel_phrase o Lexing.from_string) x;; > > looks pretty similar to the code I borrowed from miz3.ml. Can you explain > it? Is this different from the Roland Zumkeller's Flyspeck code you > mention in autopromote.ml? Is this explained in Flyspeck somewhere? I know what it's doing but don't know the detailed functionality about each of the functions used. I got it as a cut-and-paste from update_database.ml! Roughly speaking it takes a string, turns it into lexical tokens, turns this into abstract syntax and then executes it. > I see that in termparser.ml you have > > let enable_flyspeck_parsing () > let env = Obj.magic !Toploop.toplevel_env > > I bet it would be a really good programming exercise for me to really > understand how Toploop/Obj.magic/Lexing code is used in the Ocaml sources, > or Flyspeck, or your Tactician. But I'd rather you explain it to me so I > can read Voevodsky's book. I think it's a better idea to get really familiar with the main parts of OCaml, which are explained in the reference manual. Dabbling with Toploop and Obj is a bit advanced and is very difficult to find good documentation about. I've only got a partial understanding, which is good enough for my purposes in Tactician. Mark. -- Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill, > By grepping, I see occurrences of Format.print_string and > Format.print_newline commands in e.g. make.ml, but isn't the Format > prefix here unnecessary, because they're pervasive? Isn't that > explained in section 20.2 Module Pervasives : The initially opened > module of the ocaml reference manual, and p 318 for print_string and > print_newline? Yes, the use of the "Format" prefix in HOL Light's make.ml is unnecessary because it's already included as a result of printer.ml in hol.ml. But it does no harm being there. Regarding what the OCaml reference manual says: OCaml's Pervasives module is initially opened, but not its Format module. > Your failwith idea sounds great, but I didn't understand it. I think just look at my last two emails again - it should be pretty clear. And look at the HOL Zero source code in the places I suggested. I can't really think how to explain it better. > For instance, should all error messages be pretty-printed? If not, do I > really want to override the standard printer? All exceptions are pretty printed in OCaml, and I thought the whole point of your post was that you weren't happy with this pretty printing for Failure exceptions, and so I explained how to override it just for Failure exceptions and keep the pretty printer for all other exceptions exactly the same. > I grepped through your Tactician sources and I see a lot, so I bet you > understand this quite well... Not really. My starting point was Zumkeller's code in HOL Light's update_database.ml, and then I searched a bit on the web for info about Obj, etc. My Tactican code examines the memory representation of ML bindings to have a guess at the ML type of these bindings. There may be a better way of doing this. I don't really have time to examine Freek's code, but it looks like he's done a similar thing to me in terms of using update_database.ml as a starting point. Yes, the Toploop and Lexing stuff is taking a string and running it as OCaml. I don't really know much about the OCaml Lexing module, I'm afraid. My use of it in Tactician's mlconcrete.ml is just a cut-and-pasting. HOL Light and HOL Zero don't use OCaml's lexing facilities, but implement their own from scratch. > BTW I looked at your HOL Zero page > http://www.proof-technologies.com/holzero/index.html, and remind me of > something I should know: Does your HOL Zero do type quantification? No it doesn't. You need HOL-Omega for that. This and many other aspects of HOL are covered in my glossary. Mark. -- Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill, > Thanks, Mark! That sounds like a good tip, but can you be more specific? I > produce error message with this function > > let PrintErrorFail s = > open_box 0; print_string s; close_box (); print_newline (); fail();; > > > But I only want to change the OCaml exception printer for my function > PrintErrorFail. You put a call to PrintErrorFail where the "" was in my last email, i.e. in the pretty printer for exceptions. Don't put it in each function - just raise the exception in each funciton and let the pretty printer print it out when it bubbles to the toplevel. So in each function there is no need to have "try ... with ... -> PrintErrorFail" in each function - instead you have "try ... with ... -> failwith (the error message that you want...)". Take a look at HOL Zero if you want to see it in practice. Like I said, see 'exn.ml' and holzero.ml' (although these do it for my own HolFail exceptions, not for Failure exceptions). And take at look at other files, like 'lib.ml' to see exceptions getting raised and trapped. > BTW I do not understand why this works, why I don't have to say > Format.open_box and Format.close_box, > which would follow Freek's miz3.ml usage. I know print_string and > print_newline are pervasive, so you didn't need to write > Format.print_string. This is about modules. Things declared inside the Format module would normally need to be prefixed by their module name, but a module can be "included" or "opened" to avoid having to use the module prefix. John "includes" the 'Format' module in printer.ml, so you don't have to prefix from that point onwards. > BTW do you understand either of the undocumented Ocaml features that Freek > uses, Toploop or Object.magic? Is there an Ocaml list I ought to posting > questions on instead of hol-info? The OCaml developers want to keep these modules (by the way, it's Obj not Object) low key and don't publish any details about them. OCaml is used in the implementation of OCaml (!), and as I understand it, they exist for this purpose. The only source of info I can find is by Google searches. I only know a bit about them, but enough to use them in my Tactician utility. Grep Tactician's source code for Obj and Toploop if you want to find out more. Mark. -- See everything from the browser to the database with AppDynamics Get end-to-end visibility with application monitoring from AppDynamics Isolate bottlenecks and diagnose root cause in seconds. Start your free trial of AppDynamics Pro today! http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill,
You can overwrite the OCaml exception printer if you want, like I do in HOL
Zero in 'exn.ml' and the main build file 'holzero.ml', where the error
message is part of the exception and gets printed out if/when the exception
bubbles to the top. You could do something like this:
let print_exn e =
match e with
Failure msg
-> (* Special printing for Failure exceptions *)
| _ -> Format.print_string (Printexc.to_string e);; (* Otherwise
revert to normal OCaml printing *)
#install_printer print_exn;;
You would get something like this printed out:
Exception:
So this doesn't stop "Exception" getting printed out at the start, but you
have control over everything else after that. There is probably also a way
to stop "Exception" getting printed, but I just don't know enough about
OCaml to do this.
Mark.
on 26/7/13 1:48 PM, Bill Richter wrote:
> Vince, I figured out how to print error messages without double-quotes and
> with actual newlines! This and a lot more is explained in the ocaml doc
in
> "Module Format", which I got the idea to use after looking at Freek's
> miz3.ml. I'd like to get rid of a trailing message Exception: Failure "".
>
> #load "str.cma";;
>
> let StringRegexpEqual r s = Str.string_match r s 0 &&
> s = Str.matched_string s;;
>
> let rec FindMatch sleft sright s =
> let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)") and
> left = (Str.regexp sleft) in
> let rec FindMatchPosition s count =
> if count = 1 then 0 else
> try
> ignore(Str.search_forward test s 0);
> let endpos = Str.match_end() in
> let rest = Str.string_after s endpos and
> increment =
> if StringRegexpEqual left (Str.matched_group 1 s) then -1 else 1
> in
> endpos + (FindMatchPosition rest (count + increment))
> with Not_found -> open_box 0; print_string
> ("\n no matching right bracket operator "^ sright ^
> " to left bracket operator "^ sleft ^" in "^ s ^"\n");
> close_box (); print_newline (); fail() in
> FindMatchPosition s 0;;
>
> let s = ";abc]edf" in Str.string_before s (FindMatch "\[" "\]" s);;
> let s = ";1234[abc]]xyz" in Str.string_before s (FindMatch "\[" "\]" s);;
> let s = ";12345[abc]lmnop]xyz" in Str.string_before s (FindMatch "\[" "\]"
> s);;
> let s = ";123456[abc]lmnop[abc]pqrs]xyz" in Str.string_before s (FindMatch
> "\[" "\]" s);;
> let s = ";123[45[abc]lm]nop!!]xyz" in Str.string_before s
(FindMatch
> "\[" "\]" s);;
> let s = ";123456[abc]lmn[op[abc]pq]rs!!]xyz" in Str.string_before
s
> (FindMatch "\[" "\]" s);;
> let s = ";123456[abc]lmn[op[abc]pq]rs!![]xyz" in Str.string_before
s
> (FindMatch "\[" "\]" s);;
>
> Output:
>
> val it : string = ";abc]"
> # val it : string = ";1234[abc]]"
> # val it : string = ";12345[abc]lmnop]"
> # val it : string = ";123456[abc]lmnop[abc]pqrs]"
> # val it : string = ";123[45[abc]lm]nop!!]"
> # val it : string = ";123456[abc]lmn[op[abc]pq]rs!!]"
> #
> no matching right bracket operator \] to left bracket operator \[ in xyz
>
> Exception: Failure "".
>
> I'm responding to your post on Jul 2:
>
>> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>>
>> with Not_found -> failwith("missing initial \"proof\" or final \"qed;\"
> in "^ s)
>>
>> It would be nice to at least have an actual newline before the string
> s.
>
> Not to my knowledge.
>
> Here's another example:
>
> let rec FindSemicolon s =
> try
> let rec FindMatchPosition s pos =
> let start = Str.search_forward (Str.regexp ";\|\[") s pos in
> if Str.matched_string s = ";" then start
> else
> let rest = Str.string_after s (start + 1) in
> let MatchingSquareBrace = FindMatch "\[" "\]" rest in
> let newpos = start + 1 + MatchingSquareBrace in
> FindMatchPosition s newpos in
> FindMatchPosition s 0
> with Not_found -> open_box 0; print_string
> ("\n no final semicolon in " ^ s ^"\n");
> close_box (); print_newline (); fail();;
>
> let s = "123456[abc]lmn[op[a; b; c]pq]rs!![];xyz" in
> Str.string_before s (FindSemicolon s);;
> let s = "123456[abc]lmn[op[a; b; c]pq]rs!![]xyz" in
> Str.string_before s (
Re: [Hol-info] tactic works only once
I think a good start to tracking it down would be to remove tactics from the
end of 't' (starting with 't2') until it doesn't fail. Then check that the
resulting goal states are alpha-equivalent. If they are then the culprit
should be the next tactic, otherwise carry on going back until the goal
states are alpha-equivalent.
Mark.
on 17/6/13 2:11 PM, Ramana Kumar wrote:
> Yes, I was not claiming that b() is the problem. I am just curious as to
> why the tactic fails when I apply it a second time, since I can't find any
> explicit use of references, and I think I'm only using tactics from
bossLib
> (and lcsymtacs).
>
> On Mon, Jun 17, 2013 at 1:58 PM, Konrad Slind
wrote:
>
>> If that top_goal was the "original", then the tactic simply fails,
>> and it has nothing to do with the use of b().
>>
>> Konrad.
>>
>>
>>
>> On Mon, Jun 17, 2013 at 6:38 AM, Ramana Kumar
> wrote:
>>
>>> t (top_goal());
>>> val it = ([], fn): goal list * validation
>>> t (top_goal());
>>> Exception- HOL_ERR {message = "first subgoal not solved by second
>>> tactic", origin_function = "THEN1", origin_structure = "Tactical"}
raised
>>>
>>> I didn't think there were any refs touched by t, but I'll have a look
>>> more closely...
>>>
>>>
>>> On Sun, Jun 16, 2013 at 10:21 PM, Konrad Slind
> wrote:
>>>
>>>> > Could you perhaps tell me what could possibly be behind the behaviour
>>>> above?
>>>>
>>>> Superficial answer: refs
>>>>
>>>> Do you get the same behaviour if you invoke t away from the goalstack?
>>>>
>>>> t (top_goal()) = t (top_goal())
>>>>
>>>>
>>>> Konrad.
>>>>
>>>>
>>>> On Sun, Jun 16, 2013 at 3:03 PM, Ramana Kumar
>>> > wrote:
>>>>
>>>>> I have run into strange problem:
>>>>> e(t); (* succeeds and proves the goal *)
>>>>> b(); (* return to original goal *)
>>>>> e(t); (* fails *)
>>>>>
>>>>> I'll copy the code for t below, but there's a lot of required context,
>>>>> which I won't go into in this first message... Could you perhaps tell
> me
>>>>> what could possibly be behind the behaviour above?
>>>>>
>>>>> My t is (tac >> t2), where
>>>>> val t2 = metis_tac[RTC_TRANSITIVE,transitive_def]
>>>>> val tac =
>>>>> rpt gen_tac >>
>>>>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >>
>>>>>
>>>>>
>
qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`](Q.X_CHOOSE_THEN`cb`
> strip_assume_tac)(CONJUNCT1
>>>>> (CONJUNCT2 compile_append_out)) >>
>>>>> simp[Abbr`cs1`] >>
>>>>> REWRITE_TAC[Once SWAP_REVERSE] >>
>>>>> simp[] >> strip_tac >>
>>>>> qpat_assum`(A.out = cb ++ B)`mp_tac >>
>>>>> Q.PAT_ABBREV_TAC`cs1:compiler_result = X exp` >> strip_tac >>
>>>>> qabbrev_tac`tt = case t of TCNonTail => t | TCTail j k =>
>>>>> TCTail j (k + 1)` >>
>>>>>
>>>>>
>
qspecl_then[`cmnv`,`CTLet(sz+1)::cenv`,`tt`,`sz+1`,`cs1`,`exp'`](Q.X_CHOOSE_
> THEN`cd`strip_assume_tac)(CONJUNCT1
>>>>> compile_append_out) >>
>>>>> first_x_assum(qspecl_then[`rd'`,`cmnv`,`cs1`,`CTLet
>>>>> (sz+1)::cenv`,`sz+1`,`csz`,`bs2`,`bce`,`bcr`
>>>>> ,`bc0 ++ REVERSE cc`
>>>>> ,`REVERSE cd`,`(DROP (LENGTH cd)
>>>>> (REVERSE cb))++bc1`]mp_tac) >>
>>>>> discharge_hyps >- (
>>>>> simp[TAKE_APPEND1,TAKE_APPEND2,Abbr`bs2`] >>
>>>>> conj_asm1_tac >- (
>>>>>
>>>>>
> qspecl_then[`cmnv`,`cenv`,`t`,`sz`,`exp'`,`0`,`cs1`,`1`,`cb`,`cd`]mp_tac
>>>>> compile_bindings_thm >>
>>>>> simp[DROP_APPEND1,DROP_LENGTH_NIL_rwt] ) >>
>>>>> conj_tac >- PROVE_TAC[] >>
>>>>>
>>>>>
>
fs[Cenv_bs_def,s_refs_def,SUM_APPEND,FILTER_APPEND,ALL_DISTINCT_APPEND,FILTE
> R_REVERSE,EVERY_REVERSE]
>>>>> >>
>>>>>
>>
Re: [Hol-info] Learning HOL Light
Hill Bill, > ... > > 0 [`!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)`] (A) > 1 [`p * p = 2 * q * q`] (B) > > Now a mathematicians would think this means that we have chosen arbitrary > elements of the set that num denotes, and that the variables p and q will > refer to these fixed, but arbitrary, elements from now on. But I think > that's not what HOL is doing! I think HOL is just saying that the > assumptions and the goals are now written in terms of the free variables p & > q. And I guess HOL and FOL are designed this way because that's the way > math works, but I never saw that before. Tha'ts right, a variable in HOL is just an arbitrary value of its type. If 'p' and 'q' were free variables in a given theorem, then you could use INST to come up with many different instantiations of this theorem, each giving 'p' and 'q' different values. Constants are different: they are for fixed values. This is no equivalent of INST for constants. However, type variables complicate the matter. These are for parametric polymorphism, and constants as well as variables can have type variables. INST_TYPE instantiates the type variables in constants as well as in variables. > ... > > I bet the information that p, q, and m have type num is stored somewhere. I > know we can infer the type num from the assumptions, but that's not always > true. Can you tell me where this type information is stored? Yes this information is stored somewhere, and it is actually in the term itself. What I mean is in the "internal representation" of the term (of ML datatype 'term', defined in 'fusion.ml'). Each occurrence of a variable has a name and a type. This representation is normally hidden from the user during interaction due to the term parser and pretty printer, but these can be turned off to reveal to true data structures (which are quite unreadable for large terms). Mark. -- Try New Relic Now & We'll Send You this Cool Shirt New Relic is the only SaaS-based application performance monitoring service that delivers powerful full stack analytics. Optimize and monitor your browser, app, & servers with just a few lines of code. Try New Relic and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Not sure what's going on there. The 2nd message I sent to hol-info didn't seem to get through, and so my 3rd message, saying ignore the previous message, wrongly looks like it's saying ignore the 1st message. Just having one of those days... Mark. on 17/4/13 1:43 PM, Mark wrote: > Oops again, ignore my last email. Momentarily forgot what I was talking > about there. > > Mark. > > on 17/4/13 1:30 PM, Mark 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 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
Re: [Hol-info] Learning HOL Light
Oops again, ignore my last email. Momentarily forgot what I was talking about there. Mark. on 17/4/13 1:30 PM, Mark 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 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
Re: [Hol-info] Learning HOL Light
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 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 ty
Re: [Hol-info] Learning HOL Light
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 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 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 "
[Hol-info] hol4 relocatable build
kananaskis-8/bin/unquote * RWX --- --- usr/share/hol-kananaskis-8/bin/hol.builder0 * RWX --- --- usr/share/hol-kananaskis-8/bin/mkmunge.exe * RWX --- --- usr/share/hol-kananaskis-8/bin/hol.builder * RWX --- --- usr/share/hol-kananaskis-8/src/num/termination/numheap * RWX --- --- usr/share/hol-kananaskis-8/src/TeX/mkmunge.exe * !WX --- --- usr/share/hol-kananaskis-8/src/TeX/mkmunge.o * RWX --- --- usr/share/hol-kananaskis-8/tools/mllex/mllex.exe * RWX --- --- usr/share/hol-kananaskis-8/tools/mlyacc/src/mlyacc.exe * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/makebase.exe * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Txt.exe * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Html.exe * RWX --- --- usr/share/hol-kananaskis-8/help/src-sml/Doc2Tex.exe I already tried patching -Wa,--noexecstack into machine_flags in tools-poly/configure.sml: val machine_flags = ["-Wl,--hash-style=gnu", "-Wl,-O1", "-Wl,--as-needed", "-Wa,--noexecstack"] I patched polyml: --- polyml.5.5-orig/libpolyml/x86asm.asm2012-05-03 21:07:59.0 +1000 +++ polyml.5.5/libpolyml/x86asm.asm 2012-09-19 17:41:51.767737295 +1000 @@ -3003,4 +3003,7 @@ dd Mask_assign_byte ;# 254 dd Mask_assign_word ;# 255 +#if defined(__linux__) && defined(__ELF__) +.section .note.GNU-stack,"",%progbits +#endif END I could try some other things, like: - trying to splice "-Wa,--noexecstack" into some other flags. - patching or linking in some assembler code. Thanks, Mark -- LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial Remotely access PCs and mobile devices and provide instant support Improve your efficiency, and focus on delivering more value-add services Discover what IT Professionals Know. Rescue delivers http://p.sf.net/sfu/logmein_12329d2d ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill,
> Your NOTIN suggestion made great sense, but that's not the problem, it
> seems, because FunctionSpace/---> worked. I think HOL Light doesn't like
my
> weird infix -bb-->. HOL Light won't even take this as a function:
>
> let FunctionddSpace = new_definition
> `! s t. -dd--> s t = {f | (! x. x IN s ==> f x IN t) /\
> ! x. x NOTIN s ==> f x = @y. T}`;;
Yes, I missed that. The name "-dd-->" is irregular (it mixes symbolic and
alpha-numeric characters), and won't get parsed correctly in term quotations
in HOL Light. You have to construct terms involving "-dd-->" using the
syntax constructor functions (mk_comb, mk_eq, etc).
> How do you handle precedence in your HOL Zero? I'd guess it's similar
> to the way HOL Light does precedence.
I did a major review of HOL concrete syntax when designing HOL Zero, and
numerous details are handled differently from the other HOL systems.
Precedence is similar to HOL Light's, but type annotation generally requires
parentheses (although there are a few exceptions) - so `f a : A` in HOL
Light is `f (a:A)` in HOL Zero. Pairs are a special syntactic category,
where "," is a separator instead of being an infix operator, and outer
parentheses are mandatory - so `a,b,c` in HOL Light is `(a,b,c)` in HOL
Zero.
Mark.
--
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill,
> Why don't we try to prove your precedence order is correct for HOL Light.
> Don't we just have to understand parser.ml?
Yes, but that's easier said than done! Parsers can be subtle things.
> I just realized I don't need type annotations if use tactics:
>
> let CartesianProduct = new_definition
> `! X Y. X times Y = {x,y | x IN X /\ y IN Y}`;;
>
> let IN_CartesianProduct = prove
> (`! X Y x y. x,y IN X times Y <=> x IN X /\ y IN Y`,
> REWRITE_TAC[IN_ELIM_THM; CartesianProduct] THEN MESON_TAC[PAIR_EQ]);;
The term defining CartesianProduct has a type variable (automatically
generated). It's good practice to explicitly type-annotate your terms with
any type varaibles, rather than to get HOL Light to generate type variables
for you. As you say, it helps readability.
Your proof above works because you don't need to supply term quotations that
involve the generated type variable. If such term quotations were needed,
then you would have to annotate them with the nasty generated type variable
name.
> However, that doesn't work in miz3!!! I get the error #6 underspecified
> types hol with
>
> So miz3 is doing something funny.
I don't know about miz3, but I'm guessing it doesn't allow type variables to
be generated.
> Milner type inference surely tells us that no type annotations were needed
above.
Milner type inference tells us that type annotations are never needed! It
always either fails (because the term is ill-typed) or succeeds with the
most general types possible (generating type variables that are not
explicitly supplied in type annotations).
> Here's a place where my type inference intuition doesn't work, and I get
the
> error
> Exception: Failure "typechecking error (initial type assignment)":
>
> parse_as_infix("-bb-->",(13,"right"));;
>
> let FunctionbbSpace = new_definition
> `! s t. s -bb--> t = {f | (! x. x IN s ==> f x IN t) /\
> ! x. x NOTIN s ==> f x = @y. T}`;;
>
> HOL Light seems to insist on the type annotation f: A->B. But I can't see
> why. A and B just mean arbitrary types. The sub-term x IN s shows that s
> has type A->bool and x has type A, for some type A. and the sub-term f x
> IN t shows that t has type B->bool and f x has type B, for some type B.
> Thus f has type A->B. What am I missing?
Your reasoning is correct, but I don't know the full theory context in which
this exists. Crucially, has 'NOTIN' been declared as an infix? (whether it
is has been declared/defined as a constant is actually not important for the
purposes of type inference)
Mark.
--
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Learning HOL Light
Hi Bill,
It can get quite confusing sometimes, especially when "," is involved. I
think people (or those that are not already super-familiar with the syntax)
intuitively expect mandatory surrounding parentheses around pairs/tuples.
But anyway, this should help you. In the following list for HOL Light,
higher items bind more tightly (i.e. have higher "precedence") than lower
items:
- function application
- type annotation
- all prefixes
- "," separators in set enumeration (i.e. { a, b, c })
- all infixes, including "," for pairs
- all binders, including "\" and "let", and "if"
- ";" separators in list enumeration (i.e. [ a; b; c ])
Note that this is just my own informal list, derived from observed
behaviour, and there might be errors in it. Please someone say if they find
an error!
Mark.
on 6/12/12 5:14 AM, Bill Richter wrote:
> I'm trying to learn HOL Light by reading the tutorial, and I keep running
> into things I don't understand. Maybe it's a good idea to have a thread
for
> the experts to straighten out beginners like me. Here's my latest
problem,
> about parenthesis and maybe precedence. I have an improved proof of the
> universal property of the Cartesian product below (John's code, with my
> modified definition of composition), but I don't understand why it works.
I
> knew this worked:
>
> parse_as_infix("timesp",(20, "right"));;
>
> let CartesianProductp = new_definition
> `! X Y. X timesp Y = {pair:A#B | ? x y. pair = x,y /\ x IN X /\ y IN
> Y}`;;
>
> let IN_CartesianProduct = thm `;
> ! X Y x:A y:B.
> x,y IN X timesp Y <=> x IN X /\ y IN Y
> by CartesianProductp, SET_RULE, PAIR_EQ`;;
>
> But why do I need the variable pair? I wanted
>
> parse_as_infix("timeb",(20, "right"));;
>
> let CartesianProductb = new_definition
> `! X Y. X timeb Y = {x,y:A#B | x IN X /\ y IN Y}`;;
>
> let IN_CartesianProductb = thm `;
> ! X Y x:A y:B.
> x,y IN X timeb Y <=> x IN X /\ y IN Y
> by CartesianProductb, SET_RULE, PAIR_EQ`;;
>
> But this theorem earns a #8 syntax or type error hol. So let's try
> parentheses, as John does in the tutorial (the bug problem, p 64 ff):
>
> parse_as_infix("timec",(20, "right"));;
> let CartesianProductc = new_definition
> `! X Y. X timec Y = {(x,y):A#B | x IN X /\ y IN Y}`;;
>
> let IN_CartesianProductc = thm `;
> ! X Y x:A y:B.
> x,y IN X timec Y <=> x IN X /\ y IN Y
> by CartesianProductc, SET_RULE, PAIR_EQ`;;
>
> Now this works! In spite of the fact that the def is printed without
> parentheses:
> # val CartesianProductc : thm = |- !X Y. X timec Y = {x,y | x IN X /\ y
IN
> Y}
> What's going on? Is this related to the parentheses here, which are
> printed:
>
> FST;;
> val it : thm = |- !x y. FST (x,y) = x
>
> The comma infix "," has precedence 14. Is that lower than the precedence
of
> function application? There's a lot written in the tutorial about
> precedence, but I found nothing about the precedence of function
> application, forall, exists or lambda. Here's my improved code, which is
> due to John except my definition of composition, first with the statements
> using math characters:
>
> (*
> parse_as_infix("∉",(11, "right"));;
> parse_as_infix("∏",(20, "right"));;
> parse_as_infix("∘",(20, "right"));;
> parse_as_infix("→",(13,"right"));;
>
> ∉ |- ∀a l. a ∉ l ⇔ ¬(a ∈ l)
>
> CartesianProduct
> |- ∀ X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}
>
> IN_CartesianProduct
> |- ∀ X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
>
> FunctionSpace
> |- ∀ s t. s → t =
> {f | (∀ x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∉ s ⇒ f x = @y. T}
>
> IN_FunctionSpace
> |- ∀ s t f. f ∈ s → t ⇔
> (∀ x. x ∈ s ⇒ f x ∈ t) ∧ ∀ x. x ∉ s ⇒ f x = @y. T
>
> FunctionComposition
> |- ∀ x f s g. (g ∘ (f,s)) x = (if x ∈ s then g (f x) else @y. T)
>
> UniversalPropertyProduct
> |- ∀ M A B f g.
> f ∈ M → A ∧ g ∈ M → B
> ⇒ (∃! h. h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g)
> *)
>
> horizon := 0;;
> timeout := 50;;
>
> parse_as_infix("NOTIN",(11, "right"));;
> parse_as_infix("times",(20, "right"));;
> parse_as_infix("composition",(20, "right"));;
> parse_as_infix("--->",(13,"right"));;
>
> let NOTIN = new_definition
> `! a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
>
> let CartesianProduct = new_definition
> `! X Y. X times Y = {(x,y):A#B | x IN X /\ y IN Y}`;;
>
> let IN_CartesianProduct = thm `;
> !
Re: [Hol-info] Is there a good reason for not using Ocaml modules in HOL Light?
Hi Vincent, That's a good question. I think it's mainly down to history. HOL Light was originally implemented in Caml Light, and was ported to OCaml when it was already quite a substantial system. Caml Light didn't have a module system, and modules were not added in the port (except for the inference kernel). There are another few things about HOL Light that are explained by this: - Caml Light used '&' and 'or' instead of OCaml's '&&' and '||' (although OCaml still allows the old operator names, so HOL Light kept them); - Caml Light's lexical syntax was different (which explains most of the point of using Camlp4/Camlp5 to change the OCaml lexical syntax). Mark. on 16/8/12 10:21 PM, Vincent Aravantinos wrote: > Hi list, > > is there a good reason for not using Ocaml modules in HOL Light? > > This would yield a better name management, and shorter and more readable > proofs. > > For instance, instead of having: > > # REAL_ADD_SYM;; > val it : thm = |- !x y. x + y = y + x > # REAL_ADD_LID;; > val it : thm = |- !x. &0 + x = x > # REAL_ADD_ASSOC;; > val it : thm = |- !x y z. x + y + z = (x + y) + z > # ... > > We could have: > > module Real : sig > val ( ADD_SYM ) : thm > val ( ADD_LID ) : thm > val ( ADD_ASSOC ) : thm > ... > end > > And similarly: > > module Complex : sig > val ( ADD_SYM ) : thm > val ( ADD_LID ) : thm > val ( ADD_ASSOC ) : thm > ... > end > > Then, if in a context where real numbers are prominent, one could just > open the Real module, but still access Complex theorems by using the dot > notation. > > Going further, we could even use the local opening > (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc77) or > aliasing > (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc74) of > modules. But both seem incompatible with the current camlp5 extension > used by HOL Light. > > -- > Vincent Aravantinos > Postdoctoral Fellow, Concordia University, Hardware Verification Group > http://users.encs.concordia.ca/~vincent > > > > -- > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi Bill,
> Isn't this supposed to be about sets?
No, HOL is about types. Tom is informally explaining what the HOL logic is,
rather than explaining it in terms of some other formal notation (e.g. ZFC
set theory).
> Can you explain how the set abstraction/enumerations of sets.ml are
lambdas?
It's like I said - a set abstraction is (of course) a set, and so is a set
enumeration. Sets in HOL Light and HOL4 are functions to boolean (i.e.
"predicates"). A lambda is a function. So therefore one can understand
how, in HOL Light and HOL4, a set abstraction or enumeration might be a
lambda. Maybe I'm misunderstanding what your misunderstanding is...
I think a problem for you here is that, in HOL Light, it's sometimes not
easy to see through the syntactic sugar. The parser will automatically
parse a set enumeration as ` { 1, 2, 3 }`, whereas it is actually internally
represented as `1 INSERT (2 INSERT (3 INSERT EMPTY))` (and parsing this
longhand will give precisely the same internal term). The pretty printer
will always print out this internal representation as `{ 1, 2, 3 }`. To get
around this in HOL Light and see the true internal representation, I think
you need to use the destructors 'dest_comb' and 'dest_abs'. Then, if you
want to know the definitions of the HOL constants used in the internal
representation, you can examine the ML state variable 'the_definitions',
which lists all constant definitions that have been made.
> Does HOL4 have anything comparable to sets.ml?
Yes it will have, and it will probably be spread over many source code
files, but I'm afraid I don't know where this is in the HOL4 source. This
is a question for HOL4 community, Michael et al. I'm more of a HOL Light
and HOL Zero person.
Mark.
on 13/8/12 5:53 AM, Bill Richter wrote:
> Thanks, Mark! I looked at Tom Hales's Notices article, as you suggested
> www.ams.org/notices/200811/tx081101370p.pdf
> Now Tom is a great mathematician (he's the main reason I'm here), but Tom
is
> now an HOL Light expert, and I think mathematicians can't be expected to
> understand him. He starts out great:
>
> Much day-to-day mathematics is written at a level of abstraction
> that is indifferent to its exact representation as sets.
>
> This layer of abstraction is good news, because it allows us to
> shift from Zermelo-Fraenkel- Choice (ZFC) set theory to a different
> foundational system with equanimity and ease.
>
> HOL Light is a new axiomatic foundation with types, different from
> the usual ZFC.
>
> That sounds great, but here I want more details:
>
> The types are presented in the HOL Light System box.
>
> Terms are the basic mathematical objects of the HOL Light system. The
> syntax is based on Church’s lambda-calculus [to define functions]
>
> What is a type? Compared to a set, I think. What is a term?
>
> 1. Types: The collection of types is freely generated from type
> variables :A,:B,... and type constants :bool (boolean), :ind
> (infinite type), joined by arrows
>
> Isn't this supposed to be about sets? My code (largely written by John)
> doesn't obviously obey Tom's rule:
> new_type("point",0);;
> new_type_abbrev("point_set",`:point->bool`);;
> new_constant("Between",`:point->point->point->bool`);;
> new_constant("Line",`:point_set->bool`);;
>
> Maybe I need to read something by Church.
>
> 2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not
> sure why you are pointing to the definition of "INSERT" (which is
> used in the representation of set enumerations) and then talking
> about set abstractions.
>
> Because it was about all that was explained about sets in the tutorial,
and
> because I was intrigued that INSERT was explicitly defined as a lambda in
> sets.ml.
>
> But anyway, any set enumeration or set abstraction is of course a
> set, and, in HOL Light, any set is a function (as explained by 1.),
> which is what a lambda is, so there should be no surprise that a
> set abstraction/enumeration can be expressed as a lambda in HOL
> Light.
>
> Can you explain how the set abstraction/enumerations of sets.ml are
lambdas?
> Does HOL4 have anything comparable to sets.ml?
>
> Sorry, I had two typos in my last post. I meant to say
>
> let I1 = new_axiom
> `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
> says there is a unique "line" containing any two DISTINCT "points".
>
> if A, B refer to "points" a & b, then open (A,B) refers to the
> subset of point consisting of all "points" between a and b.
>
> --
> Best,
> Bill
>
>
>
--
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi Bill,
It's important to understand that the HOL4 Logic Manual gives a
(more-or-less) formal semantics of a formal logic. That's two levels of
formal! None of the set theory given in this document is actually part of
the HOL logic itself. Rather the set theory is a formal way of portraying
to the reader what the HOL logic is. This is a valuable document, making
crystal clear in minute detail exactly what the HOL logic is meant to be.
But it is not necessarily the best document to be reading for newcomers
wanting to get a good solid intuitive grasp.
By the way, I have a glossary of HOL terminology on my website which I think
will be of use to you, both in reading other documents about HOL, and as a
self-contained description of HOL (which can be read like an encyclopedia,
skipping between definitions). It tries to explain clearly, concisely and
consistently all the concepts that you need to know. Even though it is
written for HOL Zero, it applies to all HOL systems, and clearly states
where it is talking specifically about HOL Zero. Unfortunately it is only a
text document at the moment, but one day I will make it HTML if anyone shows
any interest in it. Get it here:
http://www.proof-technologies.com/misc/Glossary.txt
Mark.
on 13/8/12 5:18 AM, Bill Richter wrote:
> Thanks, Michael! I will treat the Logic Manual as a true description of
the
> HOL in HOL Light, and I will try harder to read it. I have a lot of
trouble
> with your 3 sentences:
>
> Sets in HOL Light and HOL4 are predicates over their respective
> types. Types correspond to non-empty sets (as already discussed).
> So, because any predicate bounded above corresponds to a ZFC set,
> the sets in HOL do also correspond to ZFC sets.
>
> One question would be: how does HOL Light turn my code into ZFC FOL? That
> sounds like a tough question which I'm interested in, but it's not my real
> question. I need to talk about sets to my audience of mathematicians in
my
> paper I'll submit soon to the Amer Math Monthly. I have 3900 lines of
code
>
>
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGe
> ometry.tar.gz
> and I want to tell them something about which sets I'm using. My first 4
> lines of code are
>
> new_type("point",0);;
> new_type_abbrev("point_set",`:point->bool`);;
> new_constant("Between",`:point->point->point->bool`);;
> new_constant("Line",`:point_set->bool`);;
>
> I think that says I told HOL Light to define a set called point and two
> functions
> Between: point x point x point ---> {True, False}
> Line: P(point) ---> {True, False}
> These sets & functions will be specified more closely by my axioms. We
then
> (in our heads) define a "point" to be an element of point, and a "line" to
> be a subset of point (i.e. element of P(point)) which Line sends to True.
> I think my first axiom
> let I1 = new_axiom
> `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
> says that given two elements of the set point, there is a unique line
> containing them. I often write
> let A B C be point;
> I think that means that A, B and C are variables referring to "points",
and
> so (in our heads) we say that if
> Between A B C = True
> then the middle "point" is "between" the two outer "points".
> I have a definition
>
> let Interval_DEF = new_definition
> `! A B. open (A,B) = {X | Between A X B}`;;
>
> I think that says if A, B refer to two elements of a & a of the set point,
> then open (A,B) refers to the subset of point consisting of all "points"
> between a and a.
>
> Now is my interpretation of my own code correct? I'm happy to cite the
> Logic Manual in my paper, but need to give audience more to go on. Are
> there any examples in the Logic Manual that are as "concrete" as my
> description above? I'm not too worried right now about how HOL Light is
> able to prove my statements about such sets are actually true.
>
> I have technical questions about sets defined by {...}, whether they're
> abstractions or enumerations (thanks for the new terminology, Mark). My
> first theorem is
>
> let IN_Interval = prove
> (`! A B X. X IN open (A,B) <=> Between A X B`,
> REWRITE_TAC[IN_ELIM_THM; Interval_DEF]);;
>
> Here's the code in sets.ml for IN_ELIM_THM:
>
> let IN_ELIM_THM = prove
> (`(!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ (x = t))) /\
> (!p x. x IN GSPEC (\v. ?y. SETSPEC v (p y) y) <=> p x) /\
> (!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ (x = t))) /\
> (!p x. GSPEC (\v. ?y. SETSPEC v (p y) y) x <=> p x) /\
> (!p x. x IN (\y
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi Bill, > ... My main problem is that I don't understand HOL, so I don't know what > theorems HOL Light is proving for me. The HOL4 Logic manual looks like > a very respectable CS document, but I haven't been able to read it yet, and > it's not a HOL Light document. And it's not a particularly light HOL document either! I agree we are missing a neat self-contained informal explanation of the HOL language and logic. I'm trying to think of a good paper to point you to. Maybe Tom Hale's AMS paper from 2008. Alternatively, chapters 3 & 4 of my incomplete HOL Zero manual (bundled with the HOL Zero system) explain everything, but then this is for HOL Zero and not for HOL Light, although it may still be helpful for your purposes. > With my Tarski code, I would be happy to > say (though I don't quite understand it) that HOL Light was verifying my FOL > proofs using Tarski's geometry axioms. But there's real HOL in my Hilbert > code funneled through sets.ml. Of course I know what results I meant to > prove, and my results use sets as mathematicians customarily use sets. I > figure that's the result that HOL Light proved for me, but I'm missing the > translation. I'm not sure exactly what you mean when you say "translation". Specifically, a translation from what to what? The "from" or the "to" could conceivably be: HOL Light term quotation syntax HOL Light primitive term syntax HOL Light miz3 proof scripts HOL Light inference rules conventional mathematical notation some formal mathematical logic that is not HOL Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi Bill,
There are a few points which you may or may not already realise. Sorry if
these are obvious, but I haven't been following the (very lengthy!) thread
in detail.
1. Just checking you understand this: In HOL Light and HOL4 (but not
ProofPower HOL), sets are represented as functions to booleans, so a set
with elements of type A is represented as a function from A to bool. Enter
the following in a HOL Light session to confirm this:
type_of ` { 10 }`;;
> The tutorial then explains {A, B} is syntactic sugar for A INSERT B INSERT
> {}. INSERT is defined in sets.ml as
>
> let INSERT_DEF = new_definition
> `x INSERT s = \y:A. y IN s \/ (y = x)`;;
>
> That kinda sounds like saying a set abstraction is a lambda ...
2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not sure why
you are pointing to the definition of "INSERT" (which is used in the
representation of set enumerations) and then talking about set abstractions.
But anyway, any set enumeration or set abstraction is of course a set, and,
in HOL Light, any set is a function (as explained by 1.), which is what a
lambda is, so there should be no surprise that a set abstraction/enumeration
can be expressed as a lambda in HOL Light.
> ... kinda sounds like saying a set abstraction is a lambda, but that
> can't be, because p 100 of the HOL Light tutorial says something I
> need to understand:
>
> Since MESON’s handling of lambdas is a bit better than its handling
> of set abstractions,
3. Lambdas are used in the representation of set abstractions, but the
representation is quite complicated and also involves a few other things,
and presumably it is these other things that MESON is not so good at.
Hope this helps.
Mark.
on 12/8/12 3:45 AM, Bill Richter wrote:
> I made real progress on my set theory problem, but I'd like to do even
> better. My 3860 lines of miz3 Hilbert axiomatic geometry code
>
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGe
> ometry.tar.gz now uses set abstraction to define rays:
>
> let Ray_DEF = new_definition
> `! A B. ray A B = {X:point | ~(A = B) /\ Collinear A B X /\ A NOTIN open
> (X,B)}`;;
>
> This works because of the theorem I then prove, following sets.ml
>
> let IN_Ray = prove
> (`! A B X:point. X IN ray A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN
> open (X,B)`,
> REWRITE_TAC[IN_ELIM_THM; Ray_DEF]);;
>
> I then replaced every occurrence of `IN, Ray_DEF' with the
sets.ml-friendly
> `IN_Ray'. I have no idea why IN_Ray works, and I borrowed code from
> sets.ml:
>
> let UNION = new_definition
> `s UNION t = {x:A | x IN s \/ x IN t}`;;
>
> let IN_UNION = prove
> (`!s t (x:A). x IN (s UNION t) <=> x IN s \/ x IN t`,
> REWRITE_TAC[IN_ELIM_THM; UNION]);;
>
> This is partly explained on p 91--92 of the HOL Light tutorial:
>
> In order to eliminate the set abstraction from a term of the form
> x ∈ {t | p}, rewrite with the theorem IN_ELIM_THM [of sets.ml], which
> will
> nicely eliminate the internal representation of set abstractions, e.g.
>
> # REWRITE_CONV[IN_ELIM_THM]
> ‘z IN {3 * x + 5 * y | x IN (:num) /\ y IN (:num)}‘;;
> val it : thm =
> |- z IN {3 * x + 5 * y | x IN (:num) /\ y IN (:num)} <=>
> (?x y. (x IN (:num) /\ y IN (:num)) /\ z = 3 * x + 5 * y)
>
> The tutorial then explains {A, B} is syntactic sugar for A INSERT B INSERT
> {}. INSERT is defined in sets.ml as
>
> let INSERT_DEF = new_definition
> `x INSERT s = \y:A. y IN s \/ (y = x)`;;
>
> That kinda sounds like saying a set abstraction is a lambda, but that
can't
> be, because p 100 of the HOL Light tutorial says something I need to
> understand:
>
> Since MESON’s handling of lambdas is a bit better than its handling
> of set abstractions,
>
> If anyone can explain any of these mysteries, I'd be happy to listen. But
> what I'd really like is a way to prove IN_Ray in miz3.
>
> --
> Best,
> Bill
>
>
>
> --
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape ha
Re: [Hol-info] HOL and the axiom of choice
Hi Cris, I'm not sure about the original motivation for using the axiom of choice in the HOL logic, and would be interested to know. But given that the HOL logic has this, and given that excluded middle is provable from this, we may as well not have excluded middle as an axiom. The philosophy is to make the logical core as minimalist as possible, and not have axioms that can be proved from other axioms and inference rules. The early HOL systems (HOL88, HOL90 and ProofPower) had 5 axioms, including both SELECT_AX (the axiom of choice) and BOOL_CASES_AX (effectively the law of the excluded middle) as axioms. HOL Light has an alternative formulation of the HOL logic, and proves the law of the excluded middle using the axiom of choice. This was based on a relatively recent result in mathematical logic by Radu Diaconescu. HOL Zero uses another alternative formulation, but excluded middle is derived like it is in HOL Light. HOL4's formulation of the HOL logic is much the same as in the early systems, but does away with a different axiom (IMP_ANTISYM_AX), proving this using excluded middle. I wonder whether HOL Zero's or HOL4's formulations could be further minimalised... Mark. on 5/8/12 10:33 PM, Cris Perdue wrote: > In a post earlier today Rob Arthan commented that "in HOL you are working > in a model of Zermelo set theory with choice", which certainly seems to be > true of HOL Light. I'm a bit surprised that HOL Light (and HOL Zero, and > Proof Power, etc.) has this as a rather fundamental part. > > John Harrison goes on to say that HOL Light's choice axiom makes the law of > excluded middle provable in HOL Light, so maybe that was the motivation. > > In the end I'm quite curious to know: is there some philosophical or > engineering reason not to introduce the law of the excluded middle > separately from an axiom of choice in HOL logics? Or is it mostly an > accident of history that the axiom of choice is treated as being rather > fundamental? > > Also -- for comparison, in Peter Andrews' quite similar Q0 there is a > weaker description operator that basically only promises to give the back > the single element of a singleton. Is there some notable concern or > disadvantage seen in this description operator compared with a choice > operator? > > Q0 has been my introduction to these logics, so I'm very interested in > points of comparison. > > thanks much, > Cris > > > > > > > -- > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Tactician 1.3 release
Hi Peter, Thanks for the interest. Porting to HOL4 is very feasible. Especially if someone could fund me to do this! Mark. on 27/7/12 3:18 PM, Peter Vincent Homeier wrote: > Hello, Mark. > > Are you interested in porting this technology to the HOL4 system? > > Peter > > On Wed, Jul 25, 2012 at 11:05 PM, "Mark" wrote: > >> Tactician is a free and open source utility for refactoring HOL Light >> tactic proof scripts. Version 1.3 is out now and can be downloaded >> from the Tactician webpage: >> >> www.proof-technologies.com/tactician/index.html >> >> HOL Light's source code contains hundreds of tactic proofs that have >> each been neatly packaged up into a single-tactic proof. Although >> concise, it can be difficult to step through these proofs >> tactic-by-tactic, which is what every user wants to do if they want to >> understand a proof. It becomes almost impossible for large tactic >> proofs that branch into many subgoals. >> >> However, with Tactician this becomes easy. Just load Tactician into >> the HOL Light session immediately before the proof you want to step >> through, then process the proof as normal, and then simply execute the >> Tactician command "print_flat_proof ();;". This will print out to >> screen a flattened version of the proof script that can be stepped >> through, with ML comments pointing out where the proof branches. >> >> For example, the following original proof: >> >>let REAL_POW_LT = prove >> (`!x n. &0 < x ==> &0 < x pow n`, >>REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN >>INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LT_01] THEN >>MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);; >> >> Gets flattened out to this: >> >>g `!x n. &0 < x ==> &0 < x pow n`;; >>e (REPEAT STRIP_TAC);; >>e (SPEC_TAC (`n:num`,`n:num`));; >>e (INDUCT_TAC);; >>(* *** Subgoal 1 *** *) >>e (REWRITE_TAC [real_pow;REAL_LT_01]);; >>(* *** Subgoal 2 *** *) >>e (REWRITE_TAC [real_pow;REAL_LT_01]);; >>e (MATCH_MP_TAC REAL_LT_MUL);; >>e (ASM_REWRITE_TAC []);; >> >> Mark. >> >> >> > > -- >> Live Security Virtual Conference >> Exclusive live event will cover all the ways today's security and >> threat landscape has changed and how IT managers can respond. Discussions >> will include endpoint security, mobile security and the latest in malware >> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ >> ___ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > -- > "In Your majesty ride prosperously > because of truth, humility, and righteousness; > and Your right hand shall teach You awesome things." (Psalm 45:4) > > > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Tactician 1.3 release
Tactician is a free and open source utility for refactoring HOL Light tactic proof scripts. Version 1.3 is out now and can be downloaded from the Tactician webpage: www.proof-technologies.com/tactician/index.html HOL Light's source code contains hundreds of tactic proofs that have each been neatly packaged up into a single-tactic proof. Although concise, it can be difficult to step through these proofs tactic-by-tactic, which is what every user wants to do if they want to understand a proof. It becomes almost impossible for large tactic proofs that branch into many subgoals. However, with Tactician this becomes easy. Just load Tactician into the HOL Light session immediately before the proof you want to step through, then process the proof as normal, and then simply execute the Tactician command "print_flat_proof ();;". This will print out to screen a flattened version of the proof script that can be stepped through, with ML comments pointing out where the proof branches. For example, the following original proof: let REAL_POW_LT = prove (`!x n. &0 < x ==> &0 < x pow n`, REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LT_01] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);; Gets flattened out to this: g `!x n. &0 < x ==> &0 < x pow n`;; e (REPEAT STRIP_TAC);; e (SPEC_TAC (`n:num`,`n:num`));; e (INDUCT_TAC);; (* *** Subgoal 1 *** *) e (REWRITE_TAC [real_pow;REAL_LT_01]);; (* *** Subgoal 2 *** *) e (REWRITE_TAC [real_pow;REAL_LT_01]);; e (MATCH_MP_TAC REAL_LT_MUL);; e (ASM_REWRITE_TAC []);; Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
Hi Freek, I agree that these are very very important, but there are certainly other things wrong in my opinion. Here's a small list of things that are at the top of my head: - lack of exact control of imperative-style commands - lack of support for various styles of proof commonly used on paper (e.g. a "transitive" style) - poor error messages - poor ability to control what is and what is not displayed - poorly designed concrete syntax/pretty printer, that means Pollack Inconsistency becomes a problem - there are various other things I can't think of at the moment Note that not every system suffers badly from all of these problems, but in my opinion, every existing system suffers from most. I'm not suggesting that any in my list are individually as important as the two in your list, but sometimes the combination of many small problems is greater than their sum. Sometimes, because of one limitation, the user finds they have to use some less natural technique, and in pursing that they might encounter another problem or two, and it is the combination of these problems that conspire to present to the user a difficult challenge in how to complete a proof that is really quite straightforward on paper. I don't know about other users, but I used to get this all the time. I believe that by making 20 relatively small improvements to usability, the net effect can be a massive jump in usability. Mark on 12/7/12 11:38 AM, Freek Wiedijk wrote: > Hi Mark, > >>It's just that no-one's done it yet! > > There are just two things that make proof assistants > difficult to use: > > 1. There is not sufficient automation of trivial stuff. > > I.e., you generally need to break down your reasoning into > smaller steps than how you would experience things when > you wouldn't be dealing with a proof assistant. Maybe you > _would_ experience those steps very fleetingly, but you > wouldn't focus at them in the way a proof assistant > forces you to. It's like doing math vr > slllwwlyyy. > > If some step in a proof is obvious to you, you want to be > able to just say "well, that's obvious" and nothing more. > That's unfortunately not how it seems to work right now. > Even if there's automation in a system that can solve > such a problem, you need to be aware _what_ automation > to invoke. > > 2. You need to be able to find things in a library, or > establish that the thing you think you need is not > there yet. > > And you need to be able to keep your library > well-organised and in sync with the versions of your > systems. Not easy. > > Random example: suppose you want to use Schwarz's > inequality in a proof. So _here's_ your formalisation > that you're working on, and _there's_ the library of your > system. Now what? You will need to give search commands, > or switch windows to look at lists of things you might > need, or try to remember what the lemma was called and > what was its exact shape... it's all irritating overhead. > > And when you prove something you will need to decide > on a name for your new lemma. That's something that's > particularly difficult. > > There are no other reasons proof assistants are difficult. > So will these be the two things you'll be addressing? > > Of course these two things are related. And Sledgehammer > clearly is trying to address these problems. But yes, > it's not fully "done yet". > > Freek > > > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
Hi Ramana, I'm not quite sure how to interpret your question. Are you suggesting that HOL4's user interface, with it's existing provision for mixing declarative and imperative styles, is perfectly good already, or are you suggesting that it's difficult to get any better (regardless of whether it's perfectly good)? I disagree with both, but it's difficult for me to defend my position without an actual implementation of my system to back me up. Mark. on 12/7/12 8:11 AM, Ramana Kumar wrote: > On Wed, Jul 11, 2012 at 8:38 PM, "Mark" wrote: > >> I intend to cater for both the declarative style (i.e. stating the result >> of >> the step) and the imperative style (i.e. stating what operation to apply >> next), and a mixture of both. I think that this is a huge subject that > has >> not been properly explored yet by existing systems. > > I would say one can write proof scripts in a mixture of imperative and > declarative styles already in HOL4, in particular using things like "by", > "TRY", and the various matching, renaming, and abbreviating tactics for the > declarative parts. It's a matter of self-discipline how much you want to > explicitly state formulae you're proving or manipulating. Is there > something more to declarative proofs that I'm missing? -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Common HOL Platform, definition?
Hi Cris, The Common HOL Platform is my attempt at a basis for enabling easy interchange of proofs and source code between HOL systems. It consists of a very precisely defined ML API and an equivalent for HOL theory. I'm afraid I haven't yet produced a coherent document describing it yet (although I have a collection of files that capture it for my personal use). However HOL Zero does conform to the platform, and from version 0.5.0 onwards has an ML module interface for the Common HOL API (commonhol.mli). The behaviour of each ML binding in HOL Zero's ML user interface (which in fact consists of little more than this API) is described in the user manual A-appendices (however these are only 50% complete). Of course the behaviour can also be determined by examining the source code, but this is hardly satisfactory for people. I plan to finish the user manual later this year hopefully. The platform actually predates HOL Zero by about two years. Part of the motivation for building HOL Zero was producing a clear example of the platform. Mark. on 12/7/12 2:48 AM, Cris Perdue wrote: > Hello Mark and All, > > I noticed Mark's publication "Introducing HOL Zero", and the abstract > mentions a Common HOL Platform. Can anyone point me to a definition of this? > > Thanks, > Cris -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
on 9/7/12 5:48 PM, Cris Perdue wrote: > > > What I was talking about though is ease of use of software products, > and a proof assistant is definitely a software product. To get many > people to use a software product, especially one that is not just a > minor variation on one they know, it has to be amazingly simple to > use. This of course will be a huge challenge for this kind of technology. Actually I don't think it's particularly difficult to do. It's just that no-one's done it yet! > For those who have read this far, I'd very much like to learn what options > there may be for using ML (or I presume OCaml) for building Web > applications. I'm more than happy to discuss the question, but this proof > assistant is going to need to become a Web application, for a number of > reasons. I'm not sure the web application itself would be written in ML, perhaps just the core engine. I suppose it would be nice if it could all be in ML, but I'm afraid I don't know much about that sort of thing. > Going on to your further points, yes I totally agree that getting serious > adoption requires a lot more than just programming of a core engine. In > fact it will require considerable work figuring out how to hide 99.9% of > the complexity from 99% of the users (numbers approximate). ;-) Well this would be a fundamental aspect of the ML program. > Your various comments about requirements sound good to me, including the > issue of limiting jumps in reasoning. Beeson's retrospective paper "Design > Principles of MathPert" ( > http://www.michaelbeeson.com/research/papers/hisc.pdf) I think is well > worth a read. It addresses this and various other issues in educational > math software. He focuses on assisting solution of math problems, but it > his system does rigorous proofs under the hood and the paper seems > perfectly relevant to assisting with proofs of theorems. Thanks very much for this pointer. Someone once mentioned this paper to me before, I seem to remember, but it somehow slipped through the net. This guy is definitely thinking about it in a similar way. I wholeheartedly agree with all of his principles in section 2. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
on 10/7/12 4:50 AM, Bill Richter wrote: > Mark, since this is an HOL newsgroup, can you say something about how > you're going to do this? Why is your classic "LCF-style" interactive > theorem prover going to be better than HOL Light & miz3, which is not > suitable yet for such quick and trivial formalising? Above the low level stuff (the inference kernel, the parser/printer, the derivation of its low-level inference rules), it will be implemented in a completely different way to the existing systems. I don't expect anyone to believe me in how effective it will be until I've actually implemented it and > I thought a little about why I mean by the "trivial" stuff I want the > proof assistant to do. Perhaps this is exactly what miz3 does. > Suppose I have a line > > STATEMENT by R1, R2, ..., Rn; > > miz3 ought to check this, I hazily imagine, by: ... > > Perhaps a more rudimentary proof assistant ought to require the user > to specify how to substitute our defined variables for the free > variables in the theorems. I intend to cater for both the declarative style (i.e. stating the result of the step) and the imperative style (i.e. stating what operation to apply next), and a mixture of both. I think that this is a huge subject that has not been properly explored yet by existing systems. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
Hi Cris, Thanks for the enthusiastic endorsement! I know what you mean about years of training instead of months of training. I was erring on the side of understatement rather than overstatement! I'm not sure if I've got the webpage working properly on the Khan Academy website. What is supposed to happen on the page? I haven't taken a good look at MathXpert yet, but I should defnitely do that. Thanks very much for you offer of help. What I want to do first is a classic "LCF-style" interactive theorem prover in an ML toplevel, that will act as the logical brain of the system. But after that, to get serious adoption, there will be a tonne of supporting stuff that needs doing, including user interfaces, webpages, training manuals etc, and any help here would be extremely useful. Also, just getting input from people about what the requirements should be is always useful. But this is all a few years away - it will be several months before I can even resume work on it. In terms of design, I think the way to go is, as you suggest, to look at proofs of recognisable theorems in mathematics. It should be possible to get step-for-step correspondence between textbook proofs and theorem prover proofs. Undergraduage textbooks mix English prose with lines of mathematical notation, but it is straightforward to extract out identifiable proof steps and turn this into a rigorous symbolic pen-and-paper proof, with steps at the same level as the original. What I am aiming at is a theorem prover that makes formalising such pen-and-paper proofs quick and trivial. It should also be possible to restrict the kinds of jumps in reasoning that the user is allowed to do in one step, so that the same system can be suited to both formalising undergraduate textbooks and policing much more basic high school proofs. I don't see why professional mathematicians and school children can't be using the same system. I certainly think that theorem provers will never get widely adopted until such a system exists. Actually, a very interesting exercise was Freek's challenge at ICMS 2006, where he asked expert users of various theorem provers, including HOL Light, Mizar, Coq and Isabelle/HOL Isar, to formalise a classic textbook proof. http://www.cs.ru.nl/~freek/demos/index.html Regards, Mark. on 7/7/12 12:59 AM, Cris Perdue wrote: > Mark and all, > > Yay! That's a beautiful description of key characteristics of tools that I > believe will have great benefit and impact when they arrive on the scene. > Reading through it a couple more times, I'm not sure there is any point > where I do not heartily agree. This is something I want to contribute to > with my software skills and enthusiasm for logic. It is also the motivation > behind the Prooftoys (http://prooftoys.org/) work to date, and it is a > vision I am prepared to contribute to as much as I am able in the future. I > would like to call out at least one point: > > "not require months of training" > > This is an understatement. My too-many years of experience with software > technology are hollering deafeningly that making adoption drop-dead easy is > the real target. OK, "Proof is not that simple" you say, and of course you > know what you are talking about. Rather than harangue you all further on > the subject, I'd like to point you to a couple of examples. > > Using Prooftoys I have made a proof of concept demo that works in the Khan > Academy math exercise framework, at > > http://sandcastle.khanacademy.org/media/castles/crisperdue:cris-testing/exer > cises/expression_expansion.html > . > Or get a trial version of Michael Beeson's MathXpert and do just about > anything. MathXpert steps are all mathematically correct, and it manages > the "side conditions" behind the scenes unless they "block" a step or you > go out of your way to look at them. And I would say a bright high school > student could pick it up pretty darned fast if he or she actually tries it. > > Of course I'm talking about adoption by individual users, not be schools or > teachers, which is vastly different and in the end will only be possible > following much adoption by individuals. > > One serious question is whether it is possible to work up by baby steps > from there to more serious sorts of proofs so adopters can easily work up > from there to "actual proofs", fuller use of the logic, and ability to > express classic styles of informal reasoning (or in Mark's words "proof on > paper"). I absolutely think it is possible, but definitely an issue. > Clearly a lot more could be said here. > > Another approach might be to start immediately with proofs of recognizable > theorems, in the spirit of Euclid's Elements, but formal of course
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi Bill, I understand exactly what you are looking for (or at least I think I do!) - a theorem prover with very clearly defined functionality, that automates what is "trivial" and does not automate what is not "trivial", and that is easy to use, caters for all the classic styles of doing (symbolic) proof on paper and does not require months of training. And if this system is also a "serious" system involved in the formalisation of mathematics, and is highly trustworthy, then all the better. You see such a system as being an excellent way of teaching students how to do proof. As you say, Mizar and miz3 (and don't forget Isar) perhaps come about the closest of any current systems to what you want. I've had in mind for many years a design of a system that does exactly what you want, but have been too busy with other stuff to develop this up till now. I suppose this doesn't really help you until it's been implemented, but I just wanted to tell you that! I suppose a problem with using existing systems is that they are trying to do something different - to enable proofs to be proved with minimal amount of user effort. Sometimes the approach they use to achieving this means that they come close to your goals, but they will never be perfect for what you want. By the way, "malicious" proofs are not proofs that use a theorem prover's automatic facilities when they are not intended to be used. Malicious proofs are proofs that deliberately take advantage of unsoundness (or other trustworthiness issues) in the theorem prover, to prove a fallacy, or to appear to prove a fallacy. Mark. on 6/7/12 7:45 AM, Bill Richter wrote: > My question is: What kind of proof is miz3 saying I have? Recall that > my long-term purpose is to teach a rigorous axiomatic high school > Geometry course. There must be powerful theorem provers that could > prove every result in the course! Josef got Vampire to prove most of > my Tarski miz3 results. So I'd like to know that miz3 isn't powerful > enough to make it useless for teaching Geometry! I think miz3 is just > about right, from my experience of 2350 lines of Hilbert axiomatic > code and 985 lines of Tarski code, but I'll never be sure until I know > what miz3 calls a proof. Part of the problem is that there's no > documentation for exactly what a Mizar proof is. Again, from my > original Tarski code experience, I think Mizar is about the right > level of power. But I don't know, and can't explain it in my paper. > > > > Here's my hazy idea. I more or less know what an FOL proof is, and I > think writing them down is tedious, and we'd like a proof assistant to > automate the tedious details (substituting variables etc) , so we're > left with the interesting part of the FOL proof. I think this is what > Mizar, John's Mizar-like FOL, and miz3 all do. But I'd like to know > for sure, and more precisely, exactly what automation they do. > > It's never happened that when I ``intentionally'' wrote up a miz3 > proof, that miz3 proved the theorems before I thought I had completed > the proof. That's what I want. But once I goofed in my miz3 proof, > miz3 approved a proof that I didn't think was a proof. Freek > explained that MESON is quite powerful, and explained how MESON proved > my result. So as long as I don't goof like that, I'm OK. But could > my students exploit the power of MESON to hand in miz3 proofs that I > wouldn't call proofs? I know issues like this get discussed here, > maybe it's called `malicious' proofs. I'm not really worried about > malice, and I'd be thrilled to have any students, but the teacher > ought to know what the proof assistant will accept as a proof. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
I see, and the printer always inserts spaces presumably. What about if
there is no longest (e.g. if "-b-" and "b->" were both infixes, but not
"-b->")?
on 27/6/12 12:23 PM, Michael Norrish wrote:
> By taking the longest match against the set of known "keywords". If you
> want those other interpretations you introduce some extra spaces.
>
> x - b -> y
>
> for example.
>
> On 27/06/12 9:03 PM, "Mark" wrote:
>> How does the HOL4 parser deal with the associated potential ambiguities?
>> E.g. ``x -b-> y`` getting parsed as infix "-b->" applied to ``x`` and
> ``y``,
>> as opposed to (say) infix "->" applied to ``x - b`` and ``y``?
>>
>> Mark.
>>
>> on 27/6/12 11:22 AM, Michael Norrish
wrote:
>>
>>> On 27/06/2012, at 18:21, "Mark" wrote:
>>>
>>>> The name "seg<" is irregular, in that it combines both alpha-numeric
and
>>>> symbolic characters. Any names can be used for constants and variables
>> in
>>>> the HOL logic, but HOL Light (and HOL4 I think) have no mechanism for
>>>> *parsing* irregular names. So defining a constant called "seg<" by
>>>> supplying a term quotation won't work.
>>>
>>> As it happens HOL4 will parse "irregular names" of the sort you
describe.
>>> The trick is to define the underlying constant with a nice name, and to
>> then
>>> do something like
>>>
>>> val _ = overload_on ("seg<", ``seglt``)
>>>
>>> where seglt is the "nice name". For example, my theory of the lambda
>>> calculus uses -b-> as an infix beta-reduction arrow. With Unicode on,
> you
>>> can get the same arrow with an inserted Greek beta.
>>>
>>> Michael
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
How does the HOL4 parser deal with the associated potential ambiguities?
E.g. ``x -b-> y`` getting parsed as infix "-b->" applied to ``x`` and ``y``,
as opposed to (say) infix "->" applied to ``x - b`` and ``y``?
Mark.
on 27/6/12 11:22 AM, Michael Norrish wrote:
> On 27/06/2012, at 18:21, "Mark" wrote:
>
>> The name "seg<" is irregular, in that it combines both alpha-numeric and
>> symbolic characters. Any names can be used for constants and variables
in
>> the HOL logic, but HOL Light (and HOL4 I think) have no mechanism for
>> *parsing* irregular names. So defining a constant called "seg<" by
>> supplying a term quotation won't work.
>
> As it happens HOL4 will parse "irregular names" of the sort you describe.
> The trick is to define the underlying constant with a nice name, and to
then
> do something like
>
> val _ = overload_on ("seg<", ``seglt``)
>
> where seglt is the "nice name". For example, my theory of the lambda
> calculus uses -b-> as an infix beta-reduction arrow. With Unicode on, you
> can get the same arrow with an inserted Greek beta.
>
> Michael
>
>
> --
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
The name "seg<" is irregular, in that it combines both alpha-numeric and
symbolic characters. Any names can be used for constants and variables in
the HOL logic, but HOL Light (and HOL4 I think) have no mechanism for
*parsing* irregular names. So defining a constant called "seg<" by
supplying a term quotation won't work.
To define such a constant using 'new_definition' you would have construct
the definition term argument, using syntax constructors (such as 'mk_var',
'mk_eq', 'mk_comb', etc). This would mean that terms involving your new
constant would get pretty printed as you desire. But you still have the
problem that you can't parse in term quotations involving the new constant -
they would always require syntax constructors.
Mark.
on 27/6/12 8:10 AM, Bill Richter wrote:
>
>
> parse_as_infix("seg_less",(12, "right"));;
>
> let SegmentOrdering_DEF = new_definition
> `s seg_less t <=>
> ? A B C D X. s = Segment A B /\ t = Segment C D /\
> X IN open (C,D) /\ Segment A B === Segment C X`;;
>
>
>
> BTW I would have preferred to call it seg<, to go with angle< later,
> but HOL Light didn't let me do that. Does anyone know why?
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] HOL Light tactic proof refactoring
Hi everyone, I've written a utility for refactoring HOL Light tactic proofs, called Tactician and available here: http://www.proof-technologies.com/tactician/index.html This page includes download, installation instructions and example usage. It is loaded into a normal HOL Light session, and records proofs internally as they are executed and outputs refactored versions upon user request. Refactoring operations include: - packaging up a tactic proof into a single tactic using THEN and THENL; - flattening out a packaged-up proof into a series of single-tactic steps. Flattening out is particularly useful for those wishing learn from the hundreds of packaged-up proofs that come with the HOL Light release. Mark -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants and high school math
Hi Cris, I agree with you and Freek that it's a good idea to concentrate on "high school math". Can I ask, which of the following 3 are you specifically talking about: a) getting students to use theorem provers to perform interactive formal proofs; b) getting students to use theorem provers as advanced calculators; c) concentrating on "high school math" as a way of improving theorem prover usability (without any necessary intention of actually getting high school students to use this)? Also can I ask are you specifically talking about high school students, or perhaps undergrad students instead/as well? If you are looking to support actual high school students, which countries are you thinking of? Do they even still do proof at high school in the USA, for example? It seems that it's almost been banished from the cirriculum in the UK, I found out at an education conference a few years ago. I don't know about other countries. Of course this sort of thing would still be very useful to undergrad courses around the world. Mark. on 24/5/12 1:56 AM, Cris Perdue wrote: > Reading Freek Wiedijk's paper "Formal Proofs: Getting > Started<http://www.ams.org/notices/200811/tx081101408p.pdf>" > has been very interesting for me, but raised a question that seems > important to some of my goals, and it seems to me that he and other members > of this group are probably a great resource that can help. > > Please bear with me through a bit of background. My ongoing personal > project is the Prooftoys visual proof assistant (http://prooftoys.org/). > Its biggest goal from the start has been to help popularize use of proof > assistants by being easy to try out, learn and use. It is a Web application > and immediately available through its graphical user interface to anyone > visiting a suitable web page. > > As I have continued working on it and learned more about the field, I have > come increasingly to feel that application to high school-level math and > math problems may be the best short-term opportunity to advance this > particular cause. (In fact I have taken some concrete steps in this > direction.) Good proof assistants can do a lot of math these days, so the > chances have looked very good to me, though of course there will be many > details to work out in functionality, usability, and other areas. > > But Freek's paper says: > > However, currently steps in a proof that even a high school student can > easily take without much thought often take many minutes to formalize. This > lack of automation of “high school mathematics” is the most important > reason why formalization currently still is a subject for a small group of > computer scientists, instead of it having been discovered by all > mathematicians. > > This could be a genuine obstacle to what I have in mind! Now I am a > relative newcomer to proof assistant software, and it is significant work > for me to implement things like rewriting rules to take care of common > simplifications and such, but I have tended to assume it was just me. > > So I am asking you to help me understand how true Freek's statement may be. > Can some of you give examples of steps that would tend to be obvious to > high school students but not easily handled by a proof assistant? Or steps > that could reasonably appear in examples in a high school textbook, but be > not simple for a proof assistant? (I'm thinking particularly of algebra, > trigonometry, maybe even up to calculus, but I do not understand the issues > of formalizing geometry well enough to absorb comments about assisting with > geometry problems. And I'm not really thinking of students who have > aptitude as potential professional mathematicians ... ) > > Any guidance or thoughts in this area will be very greatly appreciated. > > Cheers, > Cris > > > > > > > -- > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has cha
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi John/Ramana,
John Harrison wrote:
> I shouldn't have tempted fate by mentioning you! But I'm not yet
> completely convinced. It's true that it would create a type operator
> with recorded arity 0, but (at least in the HOL Light implementation)
> it would still end up applied to the sorted list of type variables
> ("tyvars") as if it had arity 2^31. That's not to say this is an ideal
> situation, but it seems to fall into the "anomalous" cetegory rather
> than the actually inconsistent. Or am I missing something?
Ah yes, you're absolutely right - the theorem still has the correct arity
and so this is not a route to unsoundness. Phew!
But I still get a fundamental sense of unease that types can be constructed
that are not well-formed (i.e. where the arities are wrong), so I'll adapt
HOL Zero to stop this.
John Harrison wrote:
> Mark wrote:
>> I always thought that this would be impossible to exploit in practice,
>> but now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable ...
>
> Well, I hope that's impossible for pragmatic reasons: wraparound on
> 2^31 would only happen on a 32-bit platform, and then I don't think
> you could address enough memory directly to put this to the test since
> pointers are also 32-bit. And on a 64-bit machine the bar becomes
> much higher because integers won't wrap till 2^63. But perhaps there
> is some weird way of setting up OCaml where pointers are 64-bit but
> type int is 32-bit?
Yes, you're right again. 64-bit machines will have 63-bit integers unless
using special tricks, and 32-bit machines won't be able to address enough
RAM unless using special tricks. So looks like it couldn't be a problem in
practice. (note that my bounty qualification criteria aim to ban what I
mean by "special tricks")
Ramana Kumar wrote:
> And what about switching to big integers? (for HOL Zero and/or HOL Light)
> I thought HOL Zero might be switching to SML at some point anyway?
Yes, big integers is the other possibility. I'm trying to do it as light
weight as possible, and yet keeping the user interface "conventional" (using
the classic types so that integer literals supplied by the user do not have
to be wrapped with 'Int'). However, the HOL Zero natural number syntax
functions already use big integers, and so there is already an inconsistency
in style here, and so maybe I should follow your suggestion. And yes, I
will be switching to SML, but this is several months away, and in any case,
I want everything to be as watertight as possible in the OCaml
implementation.
Mark.
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Ramana Kumar wrote: > Mark wrote: >> Yes, big integers is the other possibility. ... > > Sounds good. > For your information, I am currently working on a verified compiler for > (currently a pure subset of) SML. > But it is also probably several months away from completion :) Yes, I heard about this. Sounds great stuff! Would be nice if it could have some sort of simple mechanism for disallowing overwriting of certain ML and pretty printer bindings (e.g. a compiler directive that could be applied for a given binding, which would set a one-way flag on the binding). This would stop 'thm' and its pretty printer being overwritten by the user, for example, and would be an easy way of eliminating this long-standing vulnerability of LCF-style systems that run in a simple classic top level ML session. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
John Harrison wrote: > * Each type constructor has an int for its arity and when the user > tries to construct a type with it, this value is compared with the > length (also as an int) of the list of type arguments. So in > principle you could declare a type constructor with arity n and > later give it n + 2^31 arguments (on a 32-bit platform). This is > a bit of a rough edge, but of somewhat academic interest, and I > don't think it implies a soundness problem (you could imagine > allowing type constructors with the same name but different > arities). Still, maybe Mark Adams will find a flaw in that > reasoning and then I'll change to using unit list instead of int! You've got me worried now. This use of integers could be exploited when defining a new type operator. In general, the input theorem to type operator definition is: |- ?x. P x or in HOL Light as |- P x Imagine the type of 'x' is, say, cartesian product with 2^31 dimensions and a type variable for each dimension, and 'P' is, say, `\x. true`. Then the resulting type operator will be given arity 0 (because the OCaml int length of the list of type variables will be 2^31, which wraps round as 0 in OCaml), and the theorem that defines it will state that this 0-dimensioned type constant is in bijection with the the entire 2^31-dimensioned representation type (with its 2^31 type parameters). Inconsistency should be derivable by using two different type instantiations of this definition theorem. HOL Zero is just as vulnerable as HOL Light here, because it also used OCaml's int for type arities. I always thought that this would be impossible to exploit in practice, but now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable in principle with a machine with something like 100 GB of RAM (although inefficiencies in the 'union' operation used to compile a term's type variables would mean the execution would surely take years). Does this mean unit lists in HOL Light? :) I'm thinking of adding a check that there are no more than 2^30-1 type variables in the input theorem. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Makarius wrote: > * avoidance of unspecific exception handlers -- no dreaded > "handle _ => ..." that would let bad weather intrude program semantics > (I've seen this occasionally in the HOL Zero sources) These were taken out of HOL Zero some time ago. But if you know of any instances, please let me know. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Makarius wrote: > I didn't know you are still planning to switch back to SML. Anyway, what > did you find nicer about OCaml? Oh, little things in the syntax. Anonymous functions can have multiple curried arguments (fun a b -> a+b), "match" statement cases can carry more than one alternative (match x with (A n | B n) -> n-1), less indentation in the way that the let/in construct gets used as opposed to SML's let/val/in/end construct. Makarius wrote: > For the moment my main observations are: > > > * Still too many obvious attacks are simply declared as forbidden in the > Bounty.txt. Here is the copy from holzero-0.5.4 for the record: > > - building HOL Zero from a non-standard ML session state (e.g. with > parallelism) > - overwriting key ML objects (e.g. the 'thm' datatype or 'get_all_axioms') > - overwriting the pretty printer for key ML datatypes (e.g. 'thm' or 'list') > - circumventing the ML language proper or its type system (e.g. 'Obj.magic') > - circumventing, reconfiguring or interfering with the ML interpreter > - exploiting bugs in the ML interpreter > - changing the operating system environment in which the ML interpreter runs The immediate priority for me is to get it all written down somewhere, so that an auditor has a basis to work from. This hasn't been done before (or at least not comprehensively) for other theorem provers, as far as I am aware (and I would very much like to know if it ever has been done before). As far as convincing themselves that they can trust whatever comes out of a given theorem prover, all the proof auditor has to do is convince themselves that none of the above happens in a given proof script that supposedly establishes a given result. Once they've done that, the LCF approach means that they can then ignore the contents of the proof script and concentrate on the state of the theorem prover having processed the script (I call this "black box" proof auditing). The point of the $100 bounty is to help give assurance that the list of dodgy things catches everything. > For example, ML with parallel threads should now be standard, not > non-standard as declared above. It is merely a historical accident that > OCaml is still sequential by default. Your code will require some > additional refinements to make it thread-safe, which requires some "piling > up of more stuff". An alternative would be to nail down the environment > to be always sequential. Yes, in the future I hope to chip away at some of the items in the list, and I agree that catering for parallel threads must be a high priority one. I think I know how to do this already, but I'm a bit stretched for time at the moment to change anything fundamental. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Sorry for being a little late to join the discussion. At the risk of going down a side alley, I feel I need to respond to some points related to trustworthiness and/or HOL Zero. Makarius wrote: > A system like HOL-Light has the advantage that the reader gets > quickly an impression what the basic logic functionality is > meant to be. This gives some certainty under additional > assumptions, i.e. that the ML really is what it seems at first > sight, and that certain bad things are not done in practice. Yes, and, inspired by HOL Light, I took this further with HOL Zero, by trying to make the source code even easier to follow, and by giving extensive source code comments explaining exactly what is going on. Freek wrote: > Surely in every practical programming language you can > "cheat" in some way if you try hard enough. For instance by > poking the memory, either internally through some Obj.magic > like interface, or if you don't get that from your language > by poking in /dev/mem? Yes, but if we can push these vulnerabilities into as small as possible corner of the programming language toplevel (e.g. OCaml's Obj.magic and the C and OS interfaces), then this gives us something useful. We can have a well-defined subset of dodgy stuff, where everything else is safe. For those of us that have concern about soundness (e.g. anyone trying to audit a massive industrial safety-critical formal verification project), this is a considerably better situation than simply throwing our hands up in the air and saying "well, we can never be certain about anything" (apologies for over-simplifying your stance, Freek). So this is what I've been trying to do with HOL Zero - to define as clearly as possible what is and what isn't safe, and to maximise this safe subset of behaviour. This definition is not perfect yet, but the safe subset is considerably larger and considerably better defined than in any other proof system I know of. And if anyone finds a problem and tells me about it, I award them with $100 and the problem gets published on my website (even the ones I find, although I don't bother giving myself $100). Makarius wrote: > Mark Adams occasionally promotes an even more aggressive > scenario for HOL Zero where he wants to admit potentially > malicious users, an army of paid proof-workers who want to > cheat. (I am not really following him here, we are not that > far yet.) Yes, I do. I think we are already close to this. Freek wrote: > So the possibility of cheating if you really try does not > seem an interesting one to me. What's important is that > you won't "cheat" accidentally, by misunderstanding how > things work. In my experience, in some large industrial formal verifications, where you are writing 15,000 lines of bespoke ML extension to a theorem prover, to automate the proof of 1,000-line automatically-generated conjectures, it is virtually impossible to define what is and what isn't feasibly accidental. I certainly came across situations that I had subconsciously dismissed as impossible, or that I thought would never occur in practice. I think we should be striving to make it as difficult as possible to cheat, whether maliciously or accidentally. Makarius wrote: > This Obj stuff is absent in SML. Yes and I plan to port HOL Zero to SML. SML is fundamentally safer and better defined than OCaml. I think I would have used SML from the onset if I knew about these OCaml vulnerabilities. Although OCaml is nicer in other ways .. Makarius wrote: > Moreover, as I have explained to Mark Adams already in a > similar discussion, one can seal up the toplevel > interpreter loop, to isolate user scripts from any such > built-in nonsense. ... A managed ML toplevel is again > one of these layers that would complicate a prover > implementation, but make it more reliable. These techniques have the effect of removing vulnerabilities, but at the expense of greatly complicating the implementation, perhaps introducing their own vulnerabilities. What I would really like is an ML interpreter with a toplevel that can be configured to disallow all nasty stuff (e.g. overwriting the 'thm' datatype, or overwriting its pretty printer). Makarius wrote: > I've looked at holzero-0.4.1 before and just today at > holzero-0.5.4. (I am still hoping to see a really > convincing independent proof checker for the HOL family > of systems.) In what sense is HOL Zero not a convincincly independent implementation of the HOL logic? Its development was sponsored by no-one other than myself. Its core system (inference kernel + parser/printer + core theory) was all genuinely written from scratch - it took about 5 iterations to get variable instantiation right!! Its architecture involves the innovation of an inner (or "language") ker
Re: [Hol-info] newbie questions
Hi Felix, > 7) When using the compact way of writing proofs, e.g. > > let rewrite_x_lemma = prove > (`~(x:num=0) ==> ?n:num. x = n + 1`, > DISCH_TAC THEN (EXISTS_TAC `x - 1`) THEN ASM_SIMP_TAC[ARITH_RULE > `~(x=0) ==> x >= 1`;ARITH_RULE `x >= 1 ==> x - 1 + 1 = x`]);; > > is there a way to generate a "long form" of this with all intermediate > subgoals? Or would I have to rewrite the whole thing manually using g() and > e()? I've been working on a mechanism to flatten HOL Light proofs into "g"s and "e"s and to package them up into a "prove" proof. I'm just tidying it up a little now. So I'll announce to the HOL list when it's ready to use (any week now). Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Cannot Make HOL on OCaml 3.12 in Cygwin
This is due to do with Camlp5. I'm not sure whether HOL Light properly
supports the Camlp5 6.x versions (i.e. the latest versions). Which Camlp5
version are you using, as a matter of interest?
camlp5 -v
I've never known HOL Light to successfully build with Camlp5 6.x, but
according to the previous posting at least Camlp5 version 6.02.3 works for
some people (note that 6.02.3 requires a patch, for which you must have the
'patch' program installed):
http://sourceforge.net/mailarchive/message.php?msg_id=28674314
However this does not seem to work for me! Presumably you are getting the
same problem as me. I recommend Camlp5 version 5.15. Old versions are
available towards the bottom of the Camlp5 page:
http://cristal.inria.fr/~ddr/camlp5/
This works for me with the latest HOL Light SVN download.
Mark.
on 14/3/12 5:19 PM, Adam Golding wrote:
> Hi, thanks for your help,
>
> I downloaded the new hol light via svn, and, while there are several ml
> files that begin with 'pa_j_3.1x', they all give me this error:
>
> File "pa_j.ml", line 112, characters 71-73:
> Error: This expression has type (string * MLast.ctyp) list
> but an expression was expected of type
> ('a * MLast.ctyp) list Ploc.vala
> Makefile:33: recipe for target `pa_j.cmo' failed
> make: *** [pa_j.cmo] Error 2
>
> On 14 March 2012 06:28, "Mark" wrote:
>
>> You are not the first to have had trouble!
>>
>> The first thing is that you are trying to install HOL Light. When people
>> say "HOL" they mean HOL4, which is another HOL theorem prover.
>>
>> The problem you get is due to there being significant changes between
> OCaml
>> 3.11.X and 3.12.X, and the version of HOL Light you have (presumably the
>> snapshot from 10th Jan 2010?), does not cater for OCaml 3.12.X. Versions
>> of
>> HOL Light since the 10th Jan 2010 snapshot are only available as a
>> Subversion snapshot.
>>
>> There are 3 possible solutions:
>> 1. Download the latest HOL Light Subversion shapshot (see the HOL Light
>> webpage). For this you need to install Subversion.
>> 2. Tweak the version of HOL Light you have to work with OCaml 3.12.X.
> This
>> doesn't take long, and I can tell you how if needed.
>> 3. Install an older version of OCaml. I've had problems installing OCaml
>> 3.11.X (and OCaml 3.12.0) on 64-bit Linux, so perhaps OCaml 3.10.2 is the
>> safest choice.
>>
>> I recommend solution 1. Another thing to remember is that you must do a
>> "make clean" before reattempting a "make" in the same HOL Light
directory.
>> And another thing is that you need the right version of Camlp5 (do
"camlp5
>> -v" to find out).
>>
>> Note that there was a similar posting a few months ago:
>> http://sourceforge.net/mailarchive/message.php?msg_id=28674314
>>
>> Hope this helps,
>>
>> Mark.
>>
>>
>> on 14/3/12 9:23 AM, Adam Golding wrote:
>>
>> > My Situation:
>> > Windows 7 64-bit Ultimate
>> > Cygwin (with the Cygwin version of OCaml 3.12.1)
>> >
>> > Since there is no pa_j_3.12.ml file I copied pa_j_3.11.ml to pa_j.ml
>> >
>> > I get the following error when trying to 'make' HOL:
>> >
>> > $ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I
>> +camlp5
>> > pa_j.ml
>> > File "pa_j.ml", line 1689, characters 37-56:
>> > While expanding quotation "class_expr":
>> > Parse error: ']' or [expr] expected after '[' (in [expr])
>> > File "pa_j.ml", line 1, characters 0-1:
>> > Error: Preprocessor error
>> >
>> > Not having the first clue about OCaml, I don't know how to proceed from
>> > here..
>> >
>> > Many Thanks :-)
>> > Adam Golding
>> >
>> >
>> >
>> >
>> >
>> >
>>
>>
>
>> > --
>> > Virtualization & Cloud Management Using Capacity Planning
>> > Cloud computing makes use of virtualization - but cloud computing
>> > also focuses on allowing computing to be delivered as a service.
>> > http://www.accelacomm.com/jaw/sfnl/114/51521223/
>> >
>> >
>> >
>> > ___
>> > hol-info mailing list
>> > hol-info@lists.sourceforge.net
>> > https://lists.sourceforge.net/lists/listinfo/hol-info
>> >
>> >
>> >
>>
>
>
>
--
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Cannot Make HOL on OCaml 3.12 in Cygwin
You are not the first to have had trouble! The first thing is that you are trying to install HOL Light. When people say "HOL" they mean HOL4, which is another HOL theorem prover. The problem you get is due to there being significant changes between OCaml 3.11.X and 3.12.X, and the version of HOL Light you have (presumably the snapshot from 10th Jan 2010?), does not cater for OCaml 3.12.X. Versions of HOL Light since the 10th Jan 2010 snapshot are only available as a Subversion snapshot. There are 3 possible solutions: 1. Download the latest HOL Light Subversion shapshot (see the HOL Light webpage). For this you need to install Subversion. 2. Tweak the version of HOL Light you have to work with OCaml 3.12.X. This doesn't take long, and I can tell you how if needed. 3. Install an older version of OCaml. I've had problems installing OCaml 3.11.X (and OCaml 3.12.0) on 64-bit Linux, so perhaps OCaml 3.10.2 is the safest choice. I recommend solution 1. Another thing to remember is that you must do a "make clean" before reattempting a "make" in the same HOL Light directory. And another thing is that you need the right version of Camlp5 (do "camlp5 -v" to find out). Note that there was a similar posting a few months ago: http://sourceforge.net/mailarchive/message.php?msg_id=28674314 Hope this helps, Mark. on 14/3/12 9:23 AM, Adam Golding wrote: > My Situation: > Windows 7 64-bit Ultimate > Cygwin (with the Cygwin version of OCaml 3.12.1) > > Since there is no pa_j_3.12.ml file I copied pa_j_3.11.ml to pa_j.ml > > I get the following error when trying to 'make' HOL: > > $ ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 > pa_j.ml > File "pa_j.ml", line 1689, characters 37-56: > While expanding quotation "class_expr": > Parse error: ']' or [expr] expected after '[' (in [expr]) > File "pa_j.ml", line 1, characters 0-1: > Error: Preprocessor error > > Not having the first clue about OCaml, I don't know how to proceed from > here.. > > Many Thanks :-) > Adam Golding > > > > > > > -- > Virtualization & Cloud Management Using Capacity Planning > Cloud computing makes use of virtualization - but cloud computing > also focuses on allowing computing to be delivered as a service. > http://www.accelacomm.com/jaw/sfnl/114/51521223/ > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Virtualization & Cloud Management Using Capacity Planning Cloud computing makes use of virtualization - but cloud computing also focuses on allowing computing to be delivered as a service. http://www.accelacomm.com/jaw/sfnl/114/51521223/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Problem building HOL Light
HOL Light requires Camlp5 for OCaml versions >=3.10. The problem is that
HOL Light doesn't cater for Camlp5 versions 6.X, so you must use a 5.X
version. Also note that only Camlp5 version 5.15 works for OCaml 3.12.
So, given that you have OCaml 3.12, the solution is to install Camlp5
version 5.15. Go to the Camlp5 webpage:
http://pauillac.inria.fr/~ddr/camlp5/
and scroll down towards the bottom for a link to previous versions.
Mark.
on 3/1/12 7:33 AM, Cris Perdue wrote:
> I am looking for suggestions on successfully running "make" to install the
> current version of HOL Light.
>
> On an Ubuntu 11.10 system, with:
>
> $ ocaml -version
> The Objective Caml toplevel, version 3.12.0
> $ camlp5 -v
> Camlp5 version 6.02.2 (ocaml 3.12.0)
>
> # Running "make" I get:
>
> $ make
> if test `ocamlc -version | cut -c3` = "0" ; \
> then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo"
> -I +camlp4 pa_j.ml; \
> else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
> q_MLast.cmo" -I +camlp5 pa_j.ml; \
> fi
> File "pa_j.ml", line 112, characters 72-74:
> Error: This expression has type (string * MLast.ctyp) list
> but an expression was expected of type
> ('a * MLast.ctyp) list Ploc.vala
> make: *** [pa_j.cmo] Error 2
>
> This was done in the root directory after syncing this afternoon to the
SVN
> directory at Google code.
>
> The README suggests that the default location of the camlp5 library in in
> /usr/local. I have done:
>
> $ export CAMLP5LIB=/usr/lib/ocaml/camlp5
>
> # camlp5 library:
>
> $ echo $CAMLP5LIB
> /usr/lib/ocaml/camlp5
> cris@cris-netbook:~/src/hol-light-read-only$ ls !$
> ls $CAMLP5LIB
> camlp5.agramext.mli pa_extend.o pa_macro.cmx
> pa_pragma.oploc.cmi pr_null.cmo prtools.cmi
> camlp5.cma gramlib.apa_extfold.cmo pa_macro.o pa_r.cmo
> ploc.cmx pr_null.cmx prtools.mli
> camlp5.cmxa gramlib.cma pa_extfold.cmx pa_mkast.cmopa_r.cmx
> ploc.mli pr_null.o q_ast.cmo
> camlp5o.cma gramlib.cmxa pa_extfold.o pa_mkast.cmx
> pa_reloc.cmo pprintf.cmi pr_o.cmoq_ast.cmx
> camlp5r.cma grammar.cmi pa_extfun.cmopa_mkast.o
> pa_reloc.cmx pprintf.cmx pr_o.cmxq_ast.o
> camlp5sch.cma grammar.cmx pa_extfun.cmxpa_mktest.cmo
> pa_reloc.o pprintf.mli pr_o.o q_MLast.cmo
> camlp5_top.cma grammar.mli pa_extfun.o pa_mktest.cmx pa_r.o
> pr_depend.cmopr_op.cmo q_MLast.cmx
> diff.cmilib.sml pa_extprint.cmo pa_mktest.o
pa_rp.cmo
> pr_depend.cmxpr_op.cmx q_MLast.o
> diff.cmxMETA pa_extprint.cmx pa_o.cmo
pa_rp.cmx
> pr_depend.o pr_op.o q_phony.cmo
> diff.mlimLast.cmipa_extprint.opa_o.cmxpa_rp.o
> pr_dump.cmo pr_r.cmoq_phony.cmx
> eprinter.cmimLast.mlipa_fstream.cmo pa_o_fast.cmx
> pa_scheme.cmo pr_dump.cmx pr_r.cmxq_phony.o
> eprinter.cmxocpp.cmo pa_fstream.cmx pa_o_fast.o
> pa_scheme.cmx pr_dump.opr_r.o quotation.cmi
> eprinter.mliodyl.a pa_fstream.o pa_o.o
> pa_scheme.opretty.cmi pr_ro.cmo quotation.mli
> extfold.cmi odyl.cma pa_lefteval.cmo pa_oop.cmo
> pa_sml.cmo pretty.cmx pr_ro.cmx reloc.cmi
> extfold.cmx odyl.cmo pa_lefteval.cmx pa_oop.cmx
> pa_sml.cmx pretty.mli pr_ro.o reloc.mli
> extfold.mli odyl.cmx pa_lefteval.opa_oop.opa_sml.o
> pr_extend.cmopr_rp.cmo stdpp.cmi
> extfun.cmi odyl.cmxapa_lexer.cmo pa_op.cmo
pcaml.cmi
> pr_extend.cmxpr_rp.cmx stdpp.cmx
> extfun.cmx odyl.o pa_lexer.cmx pa_op.cmx
pcaml.mli
> pr_extend.o pr_rp.o stdpp.mli
> extfun.mli pa_extend.cmipa_lexer.o pa_op.o
> plexer.cmi pr_extfun.cmopr_scheme.cmo token.cmi
> fstream.cmi pa_extend.cmopa_lisp.cmo pa_pprintf.cmo
> plexer.cmx pr_extfun.cmxpr_scheme.cmx token.cmx
> fstream.cmx pa_extend.cmxpa_lisp.cmx pa_pprintf.cmx
> plexer.mli pr_extfun.o pr_scheme.o token.mli
> fstream.mli pa_extend_m.cmo pa_lisp.opa_pprintf.o
> plexing.cmipr_extprint.cmo pr_schemep.cmo versdep.cmi
> gramext.cmi pa_extend_m.cmx pa_macro.cmi pa_pragma.cmo
> plexing.cmxpr_extprint.cmx pr_schemep.cmx versdep.cmx
> gramext.cmx pa_extend_m.opa_macro.cmo pa_pragma.cmx
> plexing.mlipr_extprint.opr_schemep.o
>
> Thanks much for any help.
>
> Regards,
> -Cris
>
&
Re: [Hol-info] Problem understanding (and translating to isabelle) a theorem in realax.ml
There's a typo in my last message. It should read
let [v1;v2] = (snd o strip_comb o snd o dest_conj o snd o
dest_exists o snd o dest_abs o snd o dest_comb o snd o dest_eq) (concl
real_neg);;
Mark.
on 9/11/11 1:59 PM, Mark wrote:
> Apologies for joining this discussion rather late.
>
> Jonathan, To answer one of your questions in the last posting, I think
there
> are neater ways than to disable the pretty printer for terms. In HOL
Light
> there is a function called 'variables', which lists all the variables that
> occur in a term (either bound variables or free variables). Using this on
> the conclusion of 'real_neg' gives 2 variables called 'x1' (with different
> HOL types). So the thing to do is apply 'dest_var' on each of the
variables
> returned by 'variables':
>
> map dest_var (variables (concl real_neg));;
>
> which returns:
>
> [("x1", `:hreal#hreal`); ("u", `:hreal#hreal`); ("x1", `:real`)]
>
> So you can use HOL Light's 'vsubst' to rename the free 'x1' if you wish
(or
> INST if dealing with a theorem).
>
> An alternative but rather cumbersome approach is to use HOL Light's term
> destructors to pull apart the expression piece-by-piece:
>
> let (tm1,tm2) = dest_eq (concl real_neg);;
> let (tm3,tm4) = dest_comb tm2;;
> etc, etc .
>
> or if you just want to get to a specific subterm buried deep within, use a
> chain of destructors composed together:
>
> let (_,[v1;v2]) = (snd o strip_comb o snd o dest_conj o snd o
> dest_exists o snd o dest_abs o snd o dest_comb o snd o dest_eq) (concl
> real_neg);;
>
> I should point out that there is another HOL system called HOL Zero that
> deals with this problem of parsing/printing overloaded variables in term
> quotations. It uses an adapted form of Hindley-Milner type inference when
> parsing, so any sufficiently-type-annotated term will get successfully
> parsed. Also, the pretty printer type-annotates its output so that there
is
> no ambiguity about the types of any variables or constants, so any output
of
> the pretty printer can be cut-and-pasted back for parser input. Your
> example term would parse without requiring any type annotation, because it
> is clear from the type of 'dest_real' that the `x1` first argument to
> 'dest_real' is of type `:real` and the `x1` second argument is of type
> `:hreal#hreal`. If you did wish to see the types excplicitly, HOL Zero
has
> a display option to display the types of all printed variables.
>
> Mark.
>
> on 13/10/11 9:57 AM, Jonathan von Schroeder
> wrote:
>
>> Hi Czeray,
>> thanks for the clarification. Looking at src/HOL/Import/* I couldn't
> really
>> figure out how to invoke the automatic generation myself. Can you give me
>> any hints?
>>
>> I'd also greatly appreciate if you could tell me how to pragmatically
>> distinguish these two variables to be able to rename them (maybe you can
>> point me to how it's done in the automatic translation). The only
approach
> I
>> can currently think of is to do it by looking at the types and renaming
> all
>> variables that have the same name but incompatible types since on the rhs
>> both variables are "below" the existential quantification:
>>
>> # #remove_printer print_qterm;;
>>> # concl (real_neg);;
>>> val it : term >> Comb
>>>(Comb (Const ("=", `:real->real->bool`),
>>> Comb (Const ("real_neg", `:real->real`), Var ("x1", `:real`))),
>>>Comb (Const ("mk_real", `:(hreal#hreal->bool)->real`),
>>> Abs (Var ("u", `:hreal#hreal`),
>>> Comb (Const ("?", `:(hreal#hreal->bool)->bool`),
>>> Abs (Var ("x1", `:hreal#hreal`),
>>>Comb
>>> (Comb (Const ("/\\", `:bool->bool->bool`),
>>> Comb
>>>(Comb (Const ("treal_eq", `:hreal#hreal->hreal#hreal->bool`),
>>> Comb (Const ("treal_neg", `:hreal#hreal->hreal#hreal`),
>>> Var ("x1", `:hreal#hreal`))),
>>>Var ("u", `:hreal#hreal`))),
>>> Comb
>>> (Comb (Const ("dest_real", `:real->hreal#hreal->bool`),
>>>Var ("x1", `:real`)),
>>> Var ("x1", `:hreal#hreal`
>>
>> Jonathan
>>
>> On 12 October 2011 03:38, Cezary Kaliszyk
> wrote:
>>
>>> 20
Re: [Hol-info] Problem understanding (and translating to isabelle) a theorem in realax.ml
Apologies for joining this discussion rather late.
Jonathan, To answer one of your questions in the last posting, I think there
are neater ways than to disable the pretty printer for terms. In HOL Light
there is a function called 'variables', which lists all the variables that
occur in a term (either bound variables or free variables). Using this on
the conclusion of 'real_neg' gives 2 variables called 'x1' (with different
HOL types). So the thing to do is apply 'dest_var' on each of the variables
returned by 'variables':
map dest_var (variables (concl real_neg));;
which returns:
[("x1", `:hreal#hreal`); ("u", `:hreal#hreal`); ("x1", `:real`)]
So you can use HOL Light's 'vsubst' to rename the free 'x1' if you wish (or
INST if dealing with a theorem).
An alternative but rather cumbersome approach is to use HOL Light's term
destructors to pull apart the expression piece-by-piece:
let (tm1,tm2) = dest_eq (concl real_neg);;
let (tm3,tm4) = dest_comb tm2;;
etc, etc .
or if you just want to get to a specific subterm buried deep within, use a
chain of destructors composed together:
let (_,[v1;v2]) = (snd o strip_comb o snd o dest_conj o snd o
dest_exists o snd o dest_abs o snd o dest_comb o snd o dest_eq) (concl
real_neg);;
I should point out that there is another HOL system called HOL Zero that
deals with this problem of parsing/printing overloaded variables in term
quotations. It uses an adapted form of Hindley-Milner type inference when
parsing, so any sufficiently-type-annotated term will get successfully
parsed. Also, the pretty printer type-annotates its output so that there is
no ambiguity about the types of any variables or constants, so any output of
the pretty printer can be cut-and-pasted back for parser input. Your
example term would parse without requiring any type annotation, because it
is clear from the type of 'dest_real' that the `x1` first argument to
'dest_real' is of type `:real` and the `x1` second argument is of type
`:hreal#hreal`. If you did wish to see the types excplicitly, HOL Zero has
a display option to display the types of all printed variables.
Mark.
on 13/10/11 9:57 AM, Jonathan von Schroeder
wrote:
> Hi Czeray,
> thanks for the clarification. Looking at src/HOL/Import/* I couldn't
really
> figure out how to invoke the automatic generation myself. Can you give me
> any hints?
>
> I'd also greatly appreciate if you could tell me how to pragmatically
> distinguish these two variables to be able to rename them (maybe you can
> point me to how it's done in the automatic translation). The only approach
I
> can currently think of is to do it by looking at the types and renaming
all
> variables that have the same name but incompatible types since on the rhs
> both variables are "below" the existential quantification:
>
> # #remove_printer print_qterm;;
>> # concl (real_neg);;
>> val it : term =
>> Comb
>>(Comb (Const ("=", `:real->real->bool`),
>> Comb (Const ("real_neg", `:real->real`), Var ("x1", `:real`))),
>>Comb (Const ("mk_real", `:(hreal#hreal->bool)->real`),
>> Abs (Var ("u", `:hreal#hreal`),
>> Comb (Const ("?", `:(hreal#hreal->bool)->bool`),
>> Abs (Var ("x1", `:hreal#hreal`),
>>Comb
>> (Comb (Const ("/\\", `:bool->bool->bool`),
>> Comb
>>(Comb (Const ("treal_eq", `:hreal#hreal->hreal#hreal->bool`),
>> Comb (Const ("treal_neg", `:hreal#hreal->hreal#hreal`),
>> Var ("x1", `:hreal#hreal`))),
>>Var ("u", `:hreal#hreal`))),
>> Comb
>> (Comb (Const ("dest_real", `:real->hreal#hreal->bool`),
>>Var ("x1", `:real`)),
>> Var ("x1", `:hreal#hreal`
>
> Jonathan
>
> On 12 October 2011 03:38, Cezary Kaliszyk
wrote:
>
>> 2011/10/11 Jonathan von Schroeder :
>> > Hi all,
>> > im currently having a problem figuring out the meaning of the following
>> > theorem (from realax.ml):
>> >>
>> >> # real_neg;;
>> >> val it : thm =
>> >> |- --x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1
>> x1)
>>
>> You can also look at the version automatically translated to Isabelle
>> by HOL/Import. In the isabelle source the file:
>> src/HOL/Import/HOLLight/HOLLight.thy
>> You can find the following:
>>
>> definition real_neg :: "hollight.r
Re: [Hol-info] hol-light , is this a bug of BETA_CONV
on 16/5/11 10:14 AM, Roger Bishop Jones wrote: > Even though I am not particularly concerned with > trustworthyness (at your level) it is still a awkwardness in > my own use of ProofPower that I cannot get unambiguous and > concise theory listings, partly because I get either too > much or too little type information, or because of the > effects of type abbreviations and aliasing. > It sounds as if HOL4 and HOL zero have made some > improvements in these areas. Yes, the main reason for HOL Zero not supporting type abbreviations or aliasing (other than boolean equality) is to keep things simple and avoid confusion for the user. I've gone to great lengths to try to ensure no ambiguity whatsoever in anything outputted by the pretty printer (assuming knowledge of all declared constants, type operators and fixity settings). I was bitten too many times in the past by subtle problems in large projects, misreading ambiguous output that I subconsciously assumed meant "the obvious". Mark -- Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] hol-light , is this a bug of BETA_CONV
> Surely the ideal would be to avoid having ambiguous names by > renaming as necessary? I would think so, yes. But I'm talking about the pretty printer: given any internal representation of a theorem (with whatever confusing forms of overloading that it has), ensuring that the pretty printer output faithfully represents that internal representation, so as not to mislead the user. This is the pertinent question when it comes to theorem prover trustworthiness (other than the logical soundness of internal deductions and the architecture of the inference kernel). Mark. -- Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] hol-light , is this a bug of BETA_CONV
> HOL4's output is: > >> BETA_CONV ``(λx. ∃y. (x = a) ∧ (y = b)) y``; > <> > val it = > |- (λx. ∃y. (x = a) ∧ (y = b)) y ⇔ ∃y'. (y = a) ∧ (y' = b) > : thm Yes the HOL4 pretty printer is better than HOL Light's in various respects. So is ProofPower's (but not in this respect). But neither distinguish between overloaded variables when both/all of them are free (although in HOL4 you can hover the mouse in Emacs or use full type annotation mode). Mark. -- Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] hol-light , is this a bug of BETA_CONV
In fact HOL Zero is the only HOL system with a pretty printer specially designed to avoid all possible confusing results like that. For this situation, it returns Rob's "ideal output": # beta_conv `(\x. ?y. x = a /\ y = b) y`;; val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?(y:'2). (y:'1) = a /\ (y:'2) = b) But note that HOL Zero only supports a very basic style of interactive proof, and doesn't come with the advanced automated and interactive facilities that the other HOL systems have. Mark Adams. >> I'm a new user of hol-light and I find the following thing strange : >> >> # BETA_CONV `(\x. ?y. x = a /\ y = b) y`;; >> Warning: inventing type variables >> val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b) >> >> the ?y is not renamed in the substitution , is this a bug ? >> or am I wrong at some where? > > It isn't a bug and you aren't doing anything wrong. The variables x and y in > your lambda-term will have been assigned different types. In the HOL logic > two variables with the same name but different types are distinct. The > result of the beta conversion contains two distinct variables both named > "y". Unfortunately, the pretty-printer isn't showing you the distinction. > Ideally it would have printed something like "?y: 'b.(y: 'a) = a /\ (y: 'b) > = b". -- Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] HOL glossary
Dear HOL users, An updated version of my glossary of HOL-related terminology is now available from the Proof Technologies website at: http://www.proof-technologies.com/Glossary It significantly improves on the version of the glossary sent out on the holinfo mailing list last October, by adding around 50 entries and various links and improving many existing entries. The biggest area of change has been in adding various entries for background mathematical logic concepts. Please feel free to e-mail me with any comments or opinions. I do not consider the glossary as closed, and am open to suggestions for improvement and/or debate about appropriate choice of names/descriptions/scope. Mark Adams -- Benefiting from Server Virtualization: Beyond Initial Workload Consolidation -- Increasing the use of server virtualization is a top priority.Virtualization can reduce costs, simplify management, and improve application availability and disaster protection. Learn more about boosting the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Design decisions
I think you ask an interesting question, and I would also like to know the answer. It seems that these definitions have been handed down, but it's difficult to find the original reasons why they were done the way they were. Or maybe there's some crucial document I don't know about.. Interestingly, HOL Light deviates from the other HOL systems for the definitions for some constants (e.g. conjunction, implication and existential quantification), enabling a smaller logical core. In HOL Zero, I just stuck with the conventional definitions of HOL88, HOL90, ProofPower HOL, HOL4, etc. I did, however, attempt to give informal English explanations of the logical core's definitions and axioms in source code comments, but this didn't stretch to falsity and logical negation (but I would like it to!). Mark. On Wed, 23 Feb 2011 13:40:54 +, Russell Wallace wrote: > Hi all, > > I'm looking at some of the Light source code, and curious about some > of the design decisions. > > For example, this seems straightforward enough, given F: > > let NOT_DEF = new_basic_definition > `(~) = \p. p ==> F`;; > > ... but on the face of it, it would seem even simpler to have done > > let NOT_DEF = new_basic_definition > `(~) = \p. p <=> F`;; > > Is there a reason implication was chosen over equality for this > definition? > > And this one I'm also not clear about: > > let F_DEF = new_basic_definition > `F = !p:bool. p`;; > > falsehood is defined as "all propositions are true"... which is > certainly false, though on the face of it would seem a little > roundabout... does it have some particular felicitous properties, or > is it just a case of it being the simplest way to define false given > lambda and equals as primitives? > > Is there any documentation anywhere on the reasoning behind these > decisions? > > > -- > Free Software Download: Index, Search & Analyze Logs and other IT > data in > Real-Time with Splunk. Collect, index and harness all the fast moving > IT data > generated by your applications, servers and devices whether physical, > virtual > or in the cloud. Deliver compliance at lower cost and gain new > business > insights. http://p.sf.net/sfu/splunk-dev2dev > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info -- Free Software Download: Index, Search & Analyze Logs and other IT data in Real-Time with Splunk. Collect, index and harness all the fast moving IT data generated by your applications, servers and devices whether physical, virtual or in the cloud. Deliver compliance at lower cost and gain new business insights. http://p.sf.net/sfu/splunk-dev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] HOL on MAC OS x
Yes you do need a C compiler to install Poly/ML from source. GCC is perfectly suitable. For Mac OS X, this is not installed by default, but is available on the Install CD that comes bundled with your Mac, in the Xcode directory. Mark. on 15/2/11 7:50 AM, waqar ahmed wrote: > Thanks for help , I have problem installing the Polyml.5.4 . After > downloading and unpacking, i am launching the ./configure . it shows the > following error. > > localhost:polyml.5.4 waqar$ ./configure > machecking for a BSD-compatible install... ke/usr/bin/install -c > checking whether build environment is sane... yes > checking for a thread-safe mkdir -p... ./install-sh -c -d > checking for gawk... no > checking for mawk... no > checking for nawk... no > checking for awk... awk > checking whether make sets $(MAKE)... no > checking build system type... i386-apple-darwin10.4.0 > checking host system type... i386-apple-darwin10.4.0 > checking for style of include used by make... none > checking for gcc... no > checking for cc... no > checking for cl.exe... no > configure: error: in `/Users/waqar/desktop/polyml.5.4': > configure: error: no acceptable C compiler found in $PATH > See `config.log' for more details > > Do I need to install a compiler for C ? > > --Waqar > > On Mon, Feb 14, 2011 at 3:45 AM, Robert Baron > wrote: > >> I had no problem building HOL4 Kanaskis-6 on OS X 10.5 (I have a PPC >> mac) using Poly/ML. >> >> Rob. >> >> On Wed, Feb 9, 2011 at 12:35 AM, Michael Norrish >> wrote: >> > On 07/02/11 18:48, waqar ahmed wrote: >> >> I am trying to run HOL on my MAC OSx . Can you help me in this regard. >> > >> > HOL4 Kananaskis-6 should install and run as per the installation >> instructions, using either Moscow ML or Poly/ML. >> > >> > See http://hol.sourceforge.net/InstallKananaskis.html >> > >> > Best, >> > Michael >> > >> > >> > > -- >> > The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio > XE: >> > Pinpoint memory and threading errors before they happen. >> > Find and fix more than 250 security defects in the development cycle. >> > Locate bottlenecks in serial and parallel code that limit performance. >> > http://p.sf.net/sfu/intel-dev2devfeb >> > ___ >> > hol-info mailing list >> > hol-info@lists.sourceforge.net >> > https://lists.sourceforge.net/lists/listinfo/hol-info >> > >> > > -- > Waqar Ahmed > Senior Lecturer, > Location: Faculty Cubicles, XC-Building > Department of Computer and Software Engineering, > Bahria University, Sector E-8, Islamabad, Pakistan. > Voice : +92.51.9260002.348 > > > > > > > -- > The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE: > Pinpoint memory and threading errors before they happen. > Find and fix more than 250 security defects in the development cycle. > Locate bottlenecks in serial and parallel code that limit performance. > http://p.sf.net/sfu/intel-dev2devfeb > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE: Pinpoint memory and threading errors before they happen. Find and fix more than 250 security defects in the development cycle. Locate bottlenecks in serial and parallel code that limit performance. http://p.sf.net/sfu/intel-dev2devfeb ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] identity of constants
It should be noted that this uniqueness applies to the internal, canonical name of a constant in a given theory (i.e. the name returned by 'dest_thy_const'), as opposed to names for a constant that can appear in term quotations. In HOL4 term quotations, constants can be aliased, and these aliases can be overloaded, even for constants of the same theory. Mark. on 11/1/11 9:41 PM, Michael Norrish wrote: > On 12/01/11 12:16 AM, Ramana Kumar wrote: >> Are HOL4 theories allowed to have constants with the same name but >> different types? > > No. > >> In other words, is a HOL4 constant uniquely identified by the Thy and >> Name fields in the record returned by dest_thy_const, or does the Type >> field matter too? > > The former. > >> Same question for type operators: is the Args field in the record >> returned by dest_thy_type relevant when identifying the type operator? > > The Args field is not relevant; the analogous question would actually be > whether or not the arity (length of Args) of the operator was relevant. > > In summary: > > The thy-name combination uniquely identifies HOL constants and type > operators. > > The Type.op_arity and Term.prim_mk_const functions would not make sense > otherwise. > > Michael > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Protect Your Site and Customers from Malware Attacks Learn about various malware tactics and how to avoid them. Understand malware threats, the impact they can have on your business, and how you can protect your company and customers by using code signing. http://p.sf.net/sfu/oracle-sfdevnl ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] HOL Zero - corrected URL
I've been kindly informed that the URL in my HOL Zero announcement email was wrong (missing .html). Apologies for that. This is the correct URL for downloading HOL Zero: http://www.proof-technologies.com/holzero.html Mark. -- Beautiful is writing same markup. Internet Explorer 9 supports standards for HTML5, CSS3, SVG 1.1, ECMAScript5, and DOM L2 & L3. Spend less time writing and rewriting code and more time creating great experiences on the web. Be a part of the beta today http://p.sf.net/sfu/msIE9-sfdev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Subject: Announcing HOL Zero - the theorem prover with a bounty!
Dear HOL users, HOL Zero is a new, lightweight HOL theorem prover, implemented from scratch in OCaml. It is a simple but highly trustworthy interactive system intended for checking proofs and pedagogical roles, rather than for developing large proofs. It is free and open source (GNU General Public License v3.0). Version 0.4.1, out today, is the first version intended for general release, and can be downloaded from here: http://www.proof-technologies.com/holzero It is currently limited to Unix-like operating systems. Assuming OCaml and Camlp5 are already installed, it takes less than a minute to get running (unpack the tarball, change to its 'src' directory, start an 'ocaml' toplevel session and enter '#use "holzero.ml";;'). Basic usage is similar to HOL Light (but there is no subgoal package - only forward inference is supported). Many of the ML commands have similar names in HOL Light and HOL4 (except that rules have lowercase names and end in "_rule"). Its HOL language is very similar to HOL Light's and HOL4's, with the exception that the constants for true/false are called `true` and `false` (instead of `T` and `F`). It is notable in the following respects: - Its parser and pretty printer are complete, in the sense that any internal term can be displayed and then parsed back in (without the use of antiquotation) to result in the same internal term; - Its LCF-style inference kernel uses the novel concept of a nested language kernel to boost robustness; - Its source code is written in an extremely clear and simple style and with extensive comments, making independent review feasible; - The proofs of its 100+ derived theorems make no use of automated techniques such as rewriting, and are all written out in a natural deduction style intended to convey understanding to the reader; - Consistent and unambiguous use of terminology is taken very seriously, and an extensive glossary explaining technical jargon is included (this is an updated version of the one issued on hol-info last month); - There is a $100 bounty reward for uncovering "soundness-related" flaws - i.e. problems in the design/implementation of the logic or the pretty printer that make it appear that an unsound theorem has been established. This bounty has so far been successfully claimed twice (see website for details). Please note that this is an early release of HOL Zero, and, although largely complete, there are a few unfinished areas. Most notably, the pretty printer does not do multi-line formatting, and the user manual is missing some sections. Mark Adams Proof Technologies Ltd. -- Centralized Desktop Delivery: Dell and VMware Reference Architecture Simplifying enterprise desktop deployment and management using Dell EqualLogic storage and VMware View: A highly scalable, end-to-end client virtualization framework. Read more! http://p.sf.net/sfu/dell-eql-dev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] A Question About the Reciprocal of Real_0
This is a good question, and I am not best placed to fully answer it, but hopefully can help. It's first necessary to realise that all functions (i.e. things of type `:A->B` for some A and B) in HOL are total, and so any value in the domain type maps to some value. This differs from conventional mathematics, where certain functions such as reciprocal do not include all values in their domain. So given that `inv 0` maps to some value, there is a choice of whether to specifically tie down what that value is, or to leave it "unspecified" (i.e. it is some real number value, but impossible to determine which one). Not that even if it is unspecified, then, given that it takes some value, it is still possible to prove some results that may (or may not) seem surprising, e.g. |- !x y. x * inv 0 + y * inv 0 = inv 0 * (x + y) What they have done in HOL4 (and HOL Light) is chosen to pin it down to a specific value. It is considered that this is harmless in terms of soundness. I understand that the value is chosen so that it conveniently fits with various algebraic properties, such as: |- !x y. inv x = inv y <=> x = y[ HOL4's REAL_INV_INJ ] |- !x. inv (inv x) = x [ HOL4's REAL_INV_INV ] This means it's possible to prove certain property theorems without non-zero side conditions, and so apply these theorems in a proiof without having to prove side conditions, making interactive and automated theorem proving easier and quicker. I'm not sure why other properties, such as 'REAL_INV_MUL' keep side conditions when they don't need them. For example: |- !x y. x <> 0 /\ y <> 0 ==> inv x * inv y = inv (x * y) [ HOL4's REAL_INV_MUL ] |- !x y. inv x * inv y = inv (x * y)[ HOL Light 's REAL_INV_MUL ] This is perhaps for historical reasons - I think HOL did not previously tie down the value, but then HOL Light did and influenced HOL4 (I may be wrong about this). Perhaps some theorems in HOL4 have not yet been updated. Personally I'm not sure whether I'm comfortable with the idea of tying down the value (but am willing to be convinced), and so am not its greatest advocate! I'm not exactly sure what makes me feel more uncomfortable with this compared to not tying it down to a specific value (which still makes me feel a little uncomfortable!), but I think it's related to the increased risk of users writing formal specifications with unintentional meaning. Mark Adams on 28/10/10 2:10 PM, liliminga wrote: > Hello, > > When I read realTheory, I see the REAL_INV_0 theorem. Its content is inv 0 = 0, > according to my understanding, it means that the reciprocal of real_0 > is real_0. But it is contradictory to the knowledge of maths. The definition > of inv in realaxTheory. How to understand inv 0 = 0? I want to know the > advantages of such a definition. > > > > > > > -- > Nokia and AT&T present the 2010 Calling All Innovators-North America contest > Create new apps & games for the Nokia N8 for consumers in U.S. and Canada > $10 million total in prizes - $4M cash, 500 devices, nearly $6M in marketing > Develop with Nokia Qt SDK, Web Runtime, or Java and Publish to Ovi Store > http://p.sf.net/sfu/nokia-dev2dev > > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Nokia and AT&T present the 2010 Calling All Innovators-North America contest Create new apps & games for the Nokia N8 for consumers in U.S. and Canada $10 million total in prizes - $4M cash, 500 devices, nearly $6M in marketing Develop with Nokia Qt SDK, Web Runtime, or Java and Publish to Ovi Store http://p.sf.net/sfu/nokia-dev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] HOL glossary
I have written an extensive glossary of HOL terminology (see attached text file), for those wishing to understand the HOL logic and how theorem provers work. It forms part of the documentation of my forthcoming HOL Zero theorem prover, which is free and open source. Please feel free to use this for whatever purpose you wish. I would be most grateful for any feedback anyone has. It defines about 180 concepts relevant to basic HOL system usage (e.g. "quotation", "fixity", "variable capture") and implementation (e.g. "preterm", "LCF-style", "lexical analysis"), together with some relevant background in ML programming and formal mathematics (e.g. "abstract datatype", "formal language"). It aims to reflect consensus usage in the HOL community, although there are a few notable revisions (e.g. "abstraction term", "assertion") and a few new concepts (e.g. "language kernel", "proof auditing"). It does not aim to cover non-basic aspects of HOL theorem proving that are not used in HOL Zero (e.g. "rewriting", "subgoal package", "meson"), although maybe I could produce a general HOL version if there is enough interest. Mark Adams GLOSSARY.gz Description: GNU Zip compressed data -- Beautiful is writing same markup. Internet Explorer 9 supports standards for HTML5, CSS3, SVG 1.1, ECMAScript5, and DOM L2 & L3. Spend less time writing and rewriting code and more time creating great experiences on the web. Be a part of the beta today. http://p.sf.net/sfu/beautyoftheweb___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] HOL problem
Use a function that computes the result as an intermediate value, but throws it away. The ML interpreter does not optimise this out and still does the computation. So: time (fn tm => let val _ = defCNF.DEF_CNF_VECTOR_CONV tm in () end) ; Mark Mark Adams, Proof Technologies Ltd. on 12/12/09 3:05 AM, Khaza Anuarul Hoque wrote: > I have a big file of DNF which has 500 clause, each clause has upto 50 > literals. now i > was trying to do the cnf conversion using HOL4 Kan4 release. > > load "tautLib"; > open tautLib; > load "defCNF"; > open defCNF; > > time defCNF.DEF_CNF_VECTOR_CONV ; > > Whenever i do this it returns me an exception "Ptetty Printer: > out_of_memory". > Seems like this is a problem because HOL is running out of memory > while printing the output on screen. So is there any way to do the > computation in background rather in printing on screen ?? All i need > is the time of that cnf computation, i dont need to see the output. I > am sure there is a way to do this... can anyone help me ?? Its more > than urgent > > regards > -- > Khaza Anuarul Hoque, B.Sc Engr > M.A.Sc Student, Dept. of ECE > Concordia University, Montreal, Canada > Web: http://users.encs.concordia.ca/~k_hoque > > > > -- > Return on Information: > Google Enterprise Search pays you back > Get the facts. > http://p.sf.net/sfu/google-dev2dev > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > -- Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2dev ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
