Re: [Hol-info] Proof assistants for way more people

[Bill Richter]

   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

Re: [Hol-info] Proof assistants for way more people

[Cris Perdue]

Hi Mark,

I really do think we are excited by the same overall vision, which is
great! Shared vision I believe is probably the greatest key to building
successful collaboration.

Now come some interesting parts -- someone like me coming in with perhaps
rather different work history and from a different "technical culture", and
with limited grounding in automated deduction and formalization of math. We
may each have to (metaphorically) "speak slowly and clearly" to be
understood by others not accustomed to our way of talking. ;-)

Further comments in-line:

On Mon, Jul 9, 2012 at 2:24 AM, "Mark"  wrote:

> 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'll let people like you decide how much training it seems to take for
people to become proficient in different aspects of proof assistants. 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.


>
> 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.
>

Ouch. Speaking of ease of use!  Actually I had forgotten that this
particular example needs one hint to get the user started: Click with the
mouse on an expression in the problem statement.  That will cause a little
menu to appear. This is a very simple problem, but Khan Academy currently
has no way for students to solve practice problems online.  They basically
just give an answer. If students solve problems with an online tool, the
Khan Academy system can track every step, not just the final answer. They
analyze student skill development through behavior, so detailed tracking
should be important to them.

And yes, I do think MathXpert points the way in key aspects of usability.
The free trial version should be quite adequate for looking into this.


>
> 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.
>

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.

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). ;-)


>
> 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.
>

Cool, yes. Looking at proofs of recognizable theorems sounds good, though
some of you math heads are probably more suited to that investigation than
I am.

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 oth

Re: [Hol-info] How do I reinitialize HOL in the command window?

[Gottfried Barrow]

On 7/6/2012 7:05 AM, Makarius wrote:
http://www.tug.org/texlive/ seems to support Cygwin directly by its 
own installer, without going through the Cygwin package management.  
So it might be worth trying that.


That might be worth a try for me. MiKTeX is set to ask me if I want it 
to go retrieve an uninstalled package, so I guess TeXLive might do the 
same thing.


MiKTeX has a portable install that you could put under your contrib, and 
then call into it with Java. It's download size is 157 megabytes.


http://miktex.org/portable/about

But switching from teTex is trivial compared to porting Poly/ML to a 
native Windows.


You need a big grant from the Templeton Foundation:

http://www.templeton.org/what-we-fund/core-funding-areas

http://www.templeton.org/what-we-fund/core-funding-areas/science-and-the-big-questions/mathematical-and-physical-sciences

Spin it that 
the new action in abstract, non-applied, proof-emphasized mathematics is 
going to be driven by automated proof checking. That's the way it's 
gonna be. Research into numerical analysis and numerical solutions 
consumes much of the resources in mathematics departments; it's part of 
the PC revolution.


It's a waste of everyone's time for proofs to be "pencil and paper" from 
beginning to end. Tell the Templeton Foundation that, and you might get 
a grant, or maybe not.


Regards,
GB
--
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] Positions at ETH in concurrency & verification (ERC advanced investigator grant)

[Bertrand Meyer]

We have positions at the Chair of Software Engineering in connection with a 
recent Advanced Investigator Grant to Bertrand Meyer
from the ERC. We are building advanced practical solutions for "Concurrency 
Made Easy" and a verification-aware IDE.

 

Positions are available in my group at ETH Zurich, the Chair of Software 
Engineering. We recently received an Advanced Investigator
Grant from the European Research Council (5 years, 2.5 million euros); the 
project description is at
http://se.inf.ethz.ch/research/scoop/CME.pdf. In addition to this project 
(Concurrency Made Easy) we are recruiting for our effort
of building an advanced verification environment around Eiffel, "Verification 
As a Matter of Course" (see e.g. the slides at
http://se.ethz.ch/~meyer/publications/methodology/programming-10years-sierre.pdf,
 although the details are no longer up to date).

 

Requirements:

 

+   Good knowledge of software verification techniques

+   For the concurrency project, excellent background in concurrency

+   Good publications on relevant topics (particularly for the postdoc 
positions) 

+   Excellent mastery of object-oriented programming, including Eiffel concepts 
& Design by Contract

+   Mix of theoretical and practical (software development) talents 

+   Passion for research and determination to advance the state of software 
engineering.

 

The positions are available immediately.

 

Please send a CV to se-open-positi...@lists.inf.ethz.ch; also include a 
position statement describing (briefly, half a page to two
pages) on what topics you would like to work and what you think you can 
contribute. Obviously you should take some time to become
familiar with our work at http://se.ethz.ch, especially the Research pages.

 

-- Bertrand Meyer

 

 


--
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]

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 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
> sui

Re: [Hol-info] hol-info Digest, Vol 73, Issue 28

[Bill Richter]

Thanks, Lorenzo, and I'm sorry, I messed up. I understand Julien's
proof of Hilbert's axiom B3.  I meant to post B4, not B3.  B4 is what
Greenberg calls Hilbert's full Pasch axiom:

let B4 = new_axiom
  `! l A B C. Line l /\ ~Collinear A B C /\ 
   ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\ 
   (? X. X IN l /\ Between A X C) ==> 
   (? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;;

So if A B C are noncollinear points, and l is a line not containing A,
B or C, but l intersects the segment AC, then l must intersect either
AB or BC.  That's stronger than your inner Pasch axiom or Tarski's
alternate outer Pasch axiom.

I think Julien hadn't proved B4 the last time I looked at his code.
Thanks for offering to interpret Tarski's book.  My German is pretty
good, so if you email me some pages, maybe I can hack it.

I think your B3 code is not in your file 2391 line long Tarski-HOL
Light.hl you posted.  I think you have no other Pasch statement except
INNER_PASCH.  Maybe I don't have the latest copy of your code.  

I have trouble with your code, as I understand HOL Light poorly.  If
you want me to understand, you may have to explain your proofs in
math.  Pointers to Narboux's proofs are also good.  I tried to read
your midpoint code, and I did a lot better than I expected!

I'm puzzled at your axiom list.  Here's my segment construction axiom

let A4 = new_axiom
  `!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;

and I don't see anything like that in your axiom list.  Could it be

let SEGM_CONSTR_TAC a b c d x =
  X_CHOOSE_THEN x STRIP_ASSUME_TAC (SPECL [a;b;c;d] SEGM_CONSTRUCTION);;

I don't understand.  I also have trouble with your axiom 

let CONTINUITY = new_axiom
   `!X Y. (?a. !x y. x IN X /\ y IN Y ==> BB (a,x,y))
  ==> (?b. !x y. x IN X /\ y IN Y ==> BB (x,b,y))`;;

I believe this is Hilbert's 2nd order Dedekind cuts axiom, and not
Tarski's 1st order axiom.  In practice I'm not sure it matters much
(folks used to be really fussy about FOL before HOL), and you don't
seem to ever use it, or your EUCLID axiom.  I'm happy you don't use
your EUCLID axiom.  I have been wondering if Hilbert's Pasch axiom
requires your EUCLID axiom.  Your last theorem I think is this:

g (`!a b. ?x. MM (x,a,b)`);;

So any two points a and b have a midpoint x.  That's really cool!  I
include your code below.  Julien hadn't proved that the last time I
looked.  I can't understand your proof.  I'll tell you what I think:

tarski is the type which means point.  First you consider the case
when a = b, and then of course x = a.  And you handle that case really
easily?  I don't know what "hp1" means.  It looks like you're proving
the existence of the midpoint by constructing a perpendicular.  I
tried to do that and failed.  I think I follow this: 

let MM = new_definition
`MM (m,a,b) <=> BB (a,m,b) /\ CC (a,m) (m,b)`;;

let PER = new_definition
  `PER (a,b,c) <=> ? c'. MM (b,c,c') /\ CC (a,c) (a,c')`;;

let PERP_IN = new_definition
  `PERP_IN (x,a,b,c,d) <=> 
  ~ (a=b:tarski) /\ ~ (c=d:tarski) /\ COLL (x,a,b) /\ COLL (x,c,d) /\ 
  (! u:tarski v:tarski. (COLL (u,a,b) /\ COLL (v,c,d) ==> PER (u,x,v)))`;;

let PERP = new_definition
  ` PERP (a,b,c,d) <=> ?x. PERP_IN (x,a,b,c,d)`;;

So MM (m,a,b) means m is the midpoint of a and b.  

PER (a,b,c) means ab and bc are perpendicular, as

b is the midpoint of c & c', so c' is obtained by applying segment
construction to push c past b with bc = bc'.  Now c and c' are
equidistant from a.

BTW I recommend writing comment lines to explain your code!

Then PERP_IN (x,a,b,c,d) means a & b are distinct, c & d are distinct,
x is in the intersection of the lines ab and cd.  Now unless a, b, c &
d are collinear (your assumptions don't say they can't be), then x is
the only intersection of the lines ab and cd, by Hilbert's axiom I1,
which I proved and you must too (I'm including my proof below).  So
let's assume that x is the only intersection point of the lines ab and
cd.Then you say that if u is on line ab, and v is on line cd, then
xu and xv are perpendicular. 

Then PERP (a,b,c,d) means that lines ab and cd intersect at some point
x and then (basically) lines ab and cd are perpendicular. 

OK, back to your code, on the "hp1" line.  You're asserting that there
is a point q so that lines ab and qb are perpendicular?  I think I did
not know how to prove that.  My memory is a bit rusty.  Let me try to
remember.  Your UPPER_DIM axiom says that the points which are
equidistant from two distinct points u and v form a line, at least
they're all collinear.  So if we use segment construction to push a
past b on line ab to get a point a', with b the midpoint of a and a',
then we can look at the points equidistant from a and a'.  Well, b is
such a point, but how do we know there are any other such points, say
q?  I'm pretty sure I never knew how to prove that.  So good work!

-- 
Best,
Bill 

Lorenzo's proof of the existence of midpoints. 

let MM_EXISTENCE_AUX = top_thm ();;

g (`!a