Re: [Hol-info] Proof assistants for way more people
The assumption seems to do the job provided that it has no free variables. Then once proven it can be removed by modus ponens or other cut-like rule. I'm not seeing a problem with type variables, though it's true they must match in both parts of tm |- tm or |- tm -- tm. -Cris On Thu, Jul 19, 2012 at 9:20 AM, Konrad Slind konrad.sl...@gmail.comwrote: I wrote: It also suffers from the problem that a polymorphic formula assumed in this way can't be instantiated. Asserting an axiom is more powerful. In HOL4 axiom usage can be tracked in a similar way to how assumptions are propagated, so you can get the same effect as using an assumption. Cris then asked: Could you explain for us relative beginners a bit more what you mean here? I looked at the HOL Light code for PROVE_HYP, but the meaning and use are not clear to me. And anyway I am wondering if you mean that asserting an axiom is more powerful than _any_ ASSUME-like mechanism, or is somehow specific to PROVE_HYP. Additional enlightenment will be much appreciated. -Cris One aspect of HOL that occasionally bites is that one needs to remember that type variables are subject to similar constraints as term variables. Suppose I want to ASSUME a formula containing a type variable, getting a theorem th = tm |- tm I won't be able to instantiate said type variable in the conclusion of th without also instantiating it in the hypotheses. On the other hand new_axiom(foo,tm) returns |- tm and you don't have that limitation to deal with. Of course, you've then got a new axiom roaming around and potentially obliterating the usefulness of your formalization. Konrad. -- 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 Thu, Jul 19, 2012 at 9:54 AM, Freek Wiedijk fr...@cs.ru.nl wrote: I forgot who wrote this One way to ameliorate this problem is to compose proofs lazily. That was me. but anyway: Doesn't the Isabelle kernel now have a feature that you can postpone proving a thm and still already being allowed to use it? I think Makarius put that in the kernel especially to be able to parallelize Isabelle proof checking on multi-core machines? Can someone confirm or deny this, and give some details? My memory of the talk by Makarius in which he described this (I think I heard it twice :-)) is a bit hazy. I can confirm that I have also heard this. Don't know the details, though. I can imagine adding something similar in HOL Light. But I can also imagine just using ASSUME of the thing you plan to prove later (so any thm that uses it will get it explicitly in the assumption list), and then once you have proved it, explicitly discharging it with something like: fun th1 th2 - let tm = concl th2 in MP (DISCH tm th1) th2 I guess this function already is in HOL Light, but I don't know its name. Anyone? In HOL4 that is called PROVE_HYP. To comfortably work in a style like this you probably would want to change the thm printer though, or else you would go crazy by all the assumptions. In HOL4 you can control how much assumptions are printed with a trace called assumptions, but even the lowest setting still prints them as dots, I think. But that would be easy to change. 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, In HOL4 that is called PROVE_HYP. In HOL Light too, thanks for answering my question! (Its arguments have the opposite order from the function I wrote though :-)) In HOL4 you can control how much assumptions are printed with a trace called assumptions, HOL Light just prints them in full, I think. Ah well, as I already wrote, this way of working does not appeal too much to me anyway :-) 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 Konrad, On Thu, Jul 19, 2012 at 7:35 AM, Konrad Slind konrad.sl...@gmail.comwrote: HOL Light just prints them in full, I think. Ah well, as I already wrote, this way of working does not appeal too much to me anyway :-) Freek It also suffers from the problem that a polymorphic formula assumed in this way can't be instantiated. Asserting an axiom is more powerful. In HOL4 axiom usage can be tracked in a similar way to how assumptions are propagated, so you can get the same effect as using an assumption. Could you explain for us relative beginners a bit more what you mean here? I looked at the HOL Light code for PROVE_HYP, but the meaning and use are not clear to me. And anyway I am wondering if you mean that asserting an axiom is more powerful than _any_ ASSUME-like mechanism, or is somehow specific to PROVE_HYP. Additional enlightenment will be much appreciated. -Cris Konrad. -- 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] Proof assistants for way more people
On Thu, 19 Jul 2012, Freek Wiedijk wrote: Doesn't the Isabelle kernel now have a feature that you can postpone proving a thm and still already being allowed to use it? I think Makarius put that in the kernel especially to be able to parallelize Isabelle proof checking on multi-core machines? Yes, this concept is called proof promise. See page 5 of my PLMMS 2009 paper http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf Note that at the bottom right of page 5, the two main kernel rules (promise) and (fulfill) have been simplified later: \Pi_2 is required to be empty (all pending promises already fulfilled) and the \Pi_2 a check becomes obsolete --- it would be hard to implement anyway. Moreover note that the idea to fork proofs in one context and join later in another context hinges on the \Theta_2 = \Theta_1 test of (fulfill). This works in Isabelle thanks to theory certificates that were introduced by Larry in the 1990-ies, and refined by myself over the years. HOL4 and HOL-Light lack that concept. (John Harrison keeps asking me every 10 years what is its purpose :-) Proof promises are used for parallel proof checking, but the basic concept is independent of all that: a promise acts like a polymorphic proof constant that can be replaced later on, by substituting with its definition. This is like an implicit let-redex within the conceptual proof term language -- LCF systems usually omit that structure in memory. Contrast promises with oracles, which are polymorphic contants that are postulated but never replaced (implemented). Cf. 'sorry' in Isabelle. Contrast promises also with ASSUME, which is like a non-polymorphic lambda over the proof; it also tends to get in the way of other tools, not just the pretty printer. Cf. Shallow lazy proofs at TPHOLs 2005. My general plan is to make more aggressive use for proof promises in the Isabelle/PIDE interaction model, not just to improve parallelism, but do get top-down development by default without the user having to say 'sorry' all the time. Makarius -- 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, Later, after a long exploratory theory development, having settled on the right structures, you can go back and fill in the cheats with real proofs, Yes, for example Peter Aczel was arguing for this once too, I think. It's a tempting approach. But my experience is that whenever I try to do this kind of thing I get it wrong. I.e., when I finally go back, I find that it turns out not to be provable what I interpolated there (because I forgot about certain necessary hypotheses, for example), and that I have been building on quicksand. It might be that others are more precise than me, so that this is a personal problem. And it also might be the case that it still is not _too_ bad this way, that it still is relatively easy to repair things. But this oh my, that's not provable after all! feeling was so much a turn off to me, that I stopped trying to work in this style. Nowadays, I just prove things in their proper order, and all of it. 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
On Wed, Jul 18, 2012 at 7:49 PM, Felix Breuer fe...@fbreuer.de wrote: Hi Ramana! 2012/7/16 Ramana Kumar ramana.ku...@gmail.com One way to ameliorate this problem is to compose proofs lazily. By that, I mean when you get to a step that's obvious to you, just cheat (most proof assistants have some option to make a tagged theorem without proof). Do you (or anyone) know if there is a way to do this in HOL Light? Looking at HOL Light's kernel briefly I think the only thing you can do is call new_axiom a lot, which isn't exactly what you want, but could work: make many new_axioms when you're cheating (you could write a tactic that does this for use within a proof script), and check the list of axioms to be sure you haven't cheated after you've filled everything in. Thanks! Felix -- http://www.felixbreuer.net -- 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
One way to ameliorate this problem is to compose proofs lazily. By that, I mean when you get to a step that's obvious to you, just cheat (most proof assistants have some option to make a tagged theorem without proof). Do you (or anyone) know if there is a way to do this in HOL Light? Looking at HOL Light's kernel briefly I think the only thing you can do is call new_axiom a lot, which isn't exactly what you want, but could work: make many new_axioms when you're cheating (you could write a tactic that does this for use within a proof script), and check the list of axioms to be sure you haven't cheated after you've filled everything in. This tactic already exists in HOL Light, and is called CHEAT_TAC. I occasionally use it to compose proofs lazily, but usually follow the mode recommended by Freek of proving everything properly (because I don't trust myself to cheat truthfully). Cheers, Joe -- 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! 2012/7/16 Ramana Kumar ramana.ku...@gmail.com One way to ameliorate this problem is to compose proofs lazily. By that, I mean when you get to a step that's obvious to you, just cheat (most proof assistants have some option to make a tagged theorem without proof). Do you (or anyone) know if there is a way to do this in HOL Light? Thanks! Felix -- http://www.felixbreuer.net -- 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
Do you (or anyone) know if there is a way to do this in HOL Light? Looking at HOL Light's kernel briefly I think the only thing you can do is call new_axiom a lot How about making assumptions? Then at the end you just have to check that your theorems have no unwanted assumptions... -- 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
Freek, you're running a very interesting discussion with Mark, Felix, Chris etc. I'd like to know why Mark can't do his interface improvements on HOL Light. Responding to your points: Maybe you _would_ experience those steps very fleetingly, but you wouldn't focus at them in the way a proof assistant forces you to. Yes, I've been forced to focus in my 2600+ lines of miz3 code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz formalizing my Hilbert axiomatic geometry paper http://www.math.northwestern.edu/~richter/hilbert.pdf Often I've found that I hadn't done a good job on those those steps I experience very fleetingly. My latest example involves the supplement of angle, which sounds really easy, right? And a right angle is one whose supplement is congruent to itself. My Lemma 6.6 from my paper reads Supplements of congruent angles are congruent. An angle congruent to a right angle is a right angle. All right angles are congruent. Proof. Greenberg proves the first statement [7, Prop. 3.14]. This implies the second statement, by axiom C5. The third statement, due to Hilbert, is [7, Prop. 3.23]. How hard can that be to formalize? It took me over 200 lines! The problem was that I wasn't thinking about an angle (a subset of the plane, a union of two rays) but instead 3 points. Possibly my experts Hartshorne and Greenberg thought the same way. Straightening that out took work, and I include below all the thm defs I use for supplements and right angles, partly to shed light on And when you prove something you will need to decide on a name for your new lemma. That's something that's particularly difficult. Yes! I have a 775 line long file thmFontHilbertAxiom.ml which contains all my defs and thms, and I'd be lost without it. I'm constantly searching through it for something to cut paste and then make variable substitutions with Emacs query-replace. I definitely worried about the names of my thms defs. But I think the interface issues that Mark, Felix Chris bring up are also important. The miz3 error messages don't confuse me at all any more. Maybe I'm coding better. But I'll need to explain to my geometry audience what miz3 does. Thanks for comparing it privately to Mizar. It will take me a while to understand what you said. If John's HOLBY prover turns out to be weaker than Mizar, as you suggested, I don't necessary think that's bad. I need to understand the proof assistant, and whether it's a little too strong or a little too weak isn't as important. So why can't we understand John's HOLBY? -- Best, Bill Ray_DEF : thm = |- ∀ A B X. ray A B X ⇔ ¬(A = B) ∧ Collinear A B X ∧ ¬(A ∈ open (X,B)) Angle_DEF : thm = |- ∀ A O B. angle A O B = ray O A ∪ ray O B ANGLE : thm = |- ∀α. Angle α ⇔ (∃ A O B. α = angle A O B ∧ ¬Collinear A O B) RAY : thm = |- ∀ r. Ray r ⇔ (∃O A. ¬(O = A) ∧ r = ray O A) SupplementaryAngles_DEF : thm = |- ∀α β. α Suppl β ⇔ (∃ A O B A'. ¬Collinear A O B ∧ O ∈ open (A,A') ∧ α = angle A O B ∧ β = angle B O A') RightAngle_DEF : thm = |- ∀α. Right α ⇔ Angle α ∧ (∃ β. α Suppl β ∧ α ≡ β) SupplementExists_THM : thm = |- ∀ α. Angle α ⇒ (∃ α'. α Suppl α') SupplementImpliesAngle_THM : thm = |- ∀α β. α Suppl β ⇒ Angle α ∧ Angle β SupplementSymmetry_THM : thm = |- ∀α β. α Suppl β ⇒ β Suppl α SupplementsCongAnglesCong_THM : thm = |- ∀α β α' β'. α Suppl α' ∧ β Suppl β' ∧ α ≡ β ⇒ α' ≡ β' SupplementUnique_THM : thm = |- ∀ α β β'. α Suppl β ∧ α Suppl β' ⇒ β ≡ β' CongRightImpliesRight_THM : thm = |- ∀ α β. Angle α ∧ Angle β ∧ Right α ∧ α ≡ β ⇒ Right β RightAnglesCongruentHelp_THM : thm = |- ∀A O B A' P a. ¬Collinear A O B ∧ O ∈ open (A,A') ⇒ Line a ∧ O ∈ a ∧ A ∈ a ⇒ ¬(P ∈ a) ∧ P,B same_side a ⇒ Right (angle A O B) ∧ Right (angle A O P) ⇒ ¬(P ∈ int_angle A O B) CongRightImpliesRight_THM : thm = |- ∀α β. Angle α ∧ Angle β ∧ Right α ∧ β ≡ α ⇒ Right β RightAnglesCongruent_THM : thm = |- ∀α β. Right α ∧ Right β ⇒ α ≡ β OppositeRightAnglesLinear_THM : thm = |- ∀ A B O H h. ¬Collinear A O H ∧ ¬Collinear H O B ⇒ Right (angle A O H) ∧ Right (angle H O B) ⇒ Line h ∧ O ∈ h ∧ H ∈ h ⇒ ¬(A,B same_side h) ⇒ O ∈ open (A,B) -- 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
Hello everyone, I think the two problems Freek mentioned are indeed by far the most important obstacles to creating a truly usable proof assistant. However, there is also merit in addressing the points Mark and Cris mention: A nice system that solves all these surface usability issues, may well attract more users, even if the two core problems remain unsolved. And a critical mass of users can be very helpful in solving the two key problems as well. Note that I do not mean to imply that Freek's main problems will simply go away if the user base is large enough. These are deep research problems that will require new ideas to solve. However, attracting more users and thus more researchers to the field certainly can't hurt. To put it differently: As a working mathematician, I'd personally love to use a nice proof assistant that solves all the surface usability issues, even if the two core problems remain and need many more years to be solved. Cheers, Felix 2012/7/13 Cris Perdue c...@perdues.com Hi Freek, On Fri, Jul 13, 2012 at 5:32 AM, Freek Wiedijk fr...@cs.ru.nl wrote: Hi Cris, I was speaking from a software engineering and usability point of view. Okay, just to fix our minds: would you consider Knuth's/ Lamport's latex to be usable in this sense? Because I would strongly claim that it is. It's one of the most usable systems I know. Thanks for asking! Usability is not an absolute, it is relative to the user and the purpose. I'm glad you find latex usable as well as useful. Consider how people may come to use LaTeX. If you are an academic you may have a strong motivation to prepare papers for publication. If that means investing time and effort to learn LaTeX, you may be willing. If your colleagues use it and recommend it, if some conferences or publishers require it, all of that might reinforce your readiness to adopt it. If you like the payoff, you tend to find it usable. First-time usability can be crucial for adoption of technology that users aren't very convinced that they need or want. (For proof assistants I think this might be 99.99% of potential users.) If the potential user tries it and gets an immediate feeling of success, he or she is likely to take another step. Otherwise most potential users quit and don't come back unless maybe a friend starts gushing about how great it is. Then maybe they will give it one more try. If the product passes the user's first sniff test, the user still wants to feel that bits of additional effort will pay off nicely too. Most potential users of a new tool such as a proof assistant have some other known path toward his or her goal -- pencil and paper or a whiteboard for proofs or problem solving; testing for software development; computational approximations for engineering. The cost of learning to use this proof assistant thing might be high, and the payoff is uncertain. People have lots of other things to do. So the tool had better make a very good first impression. That is my view, and I think it's a pretty standard view on this sort of thing by people who worry about technology adoption. Maybe this is old news to you, but if so I think it's still worth saying. Best regards, Cris That's why I think that Mark's focus on things like error messages and concrete syntax is missing the point. Latex is pretty horrible in that respect, but _that doesn't matter._ 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 -- http://www.felixbreuer.net -- 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, I was speaking from a software engineering and usability point of view. Okay, just to fix our minds: would you consider Knuth's/ Lamport's latex to be usable in this sense? Because I would strongly claim that it is. It's one of the most usable systems I know. That's why I think that Mark's focus on things like error messages and concrete syntax is missing the point. Latex is pretty horrible in that respect, but _that doesn't matter._ 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
On Wed, Jul 11, 2012 at 8:38 PM, Mark m...@proof-technologies.com 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] Proof assistants for way more people
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 ramana.ku...@gmail.com wrote: On Wed, Jul 11, 2012 at 8:38 PM, Mark m...@proof-technologies.com 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] Proof assistants for way more people
On Thu, Jul 12, 2012 at 3:37 AM, Freek Wiedijk fr...@cs.ru.nl wrote: Hi Mark, It's just that no-one's done it yet! This from Mark was a reply to my comment that making a proof assistant really easy to use will be a huge challenge. I was speaking from a software engineering and usability point of view. In particular I'm thinking of usability by people who are not steeped in the culture of formal logic, people who have some exposure to math, but not to higher-order logic or even perhaps formal logic. In reality this ease of use question is many-faceted. It depends on what we mean by easy and who we think the users may be. I have a particular personal interest in having a proof assistant that is easy enough to use that way more people will decide it is their personal preferred way to get symbolic mathematics done without having to be told by a professor, and without it being an overriding requirement of a project where an error in reasoning may cost millions of dollars (or pounds, or Euro's, etc.). Freek, I do like your two points as being key, especially your point 2. Point 1 may be especially important for users who are trained mathematicians, and certainly worth stating. Point 2 I think is more a question of software design. HOL Light for example has bazillions of tactics and rules of inference and theorems, all with names to be remembered. By my definition of easy, this is much too hard. The tool needs to guide the user toward relevant options (and not to _all_ options), ideally ones that seem particularly likely to be useful as well. Even issues like being able to read a completed proof, or follow the steps or get explanations for them are things I consider important for adoption by many people. But in the end here I am agreeing with you all, and trying to clarify, not dispute. Regards, Cris 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
I was reading the following article when this message arrived. Hope some of you might find it useful. http://www.useit.com/alertbox/20030825.html On 2012-07-12, at 3:32 PM, Mark wrote: 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 ramana.ku...@gmail.com wrote: On Wed, Jul 11, 2012 at 8:38 PM, Mark m...@proof-technologies.com 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 -- 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 c...@perdues.com 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
Mark wrote: on 9/7/12 5:48 PM, Cris Perdue c...@perdues.com 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! Actually I think it is probably extraordinarily difficult. I recall a comment made about certain sorts of user interfaces (actually it was about GUIs but I think equally applicable to a certain style or philosophy of designing user interfaces for complicated software), that they make easy tasks easy and difficult tasks impossible. Theorem proving is a difficult task - or, more to the point - when you break it down into its myriad of subtasks, they are all different. The tool that does them all will not be amazingly simple to use Jeremy -- 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 c...@perdues.com 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 and not necessarily in geometry. I do not have a lot of thoughts right now on what success may be possible this way, but am following Bill Richter's experiences with much interest. Reasoning it seems to me is such a valuable tool, and computers are so well suited to supporting it, that hopefully much more
Re: [Hol-info] Proof assistants for way more people
What I am aiming at is a theorem prover that makes formalising such pen-and-paper [Undergraduate textbook] proofs quick and trivial. 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? 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: Some of the reasons Ri are labels of statements proved above. Those statements must be used exactly as they are. Other statements are theorem proved earlier. They have free variables, and we have a number of variables already defined. Our defined variables must be substituted for the free variables in all all possible ways. If we have d defined variables, and a theorem has f free variables, then there are f^d different substitutions, if we don't care about typing. As we only want to substitute variables of the same type, we will have much less than f^d substitutions. 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. Hmm, that might cause trouble if there are multiple invocations of a theorem Ri in the same by justification. Now we have a large number of actual statements that we want to combine to prove STATEMENT. The theorem statements are all of the form `this == that'. So for each theorem statement, we try to build `this' from all the known statements, and if we can, we add `that' to our list of statements. We proceed in this way until the timeout limit is reached. A smart proof assistant may be able to, as miz3 does, to assert there is an inference error, that there is no way to prove STATEMENT from R1, R2, ..., Rn. Does any of this sound right? I'll read what John says in his purple book. But this is a lot like what I do when I write proofs 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
