Re: [mizar] A quote

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Piotr,

>> I think I agree with this.  With properly automated
>> computations you can throw away all of the AXIOMS and [X]REAL_*
>> and XCMPLX_* series of articles.  I _hate_ searching through
>> those articles for lemmas that I know are there, but that I
>> can't find.
>
>Searching these articles drives me nuts at times yet I do not see how
>you plan to eliminate them.  Could you elaborate please?

Well, the magic word is "decision procedures".  I learned
from a nice talk by Shanker (the big one of the PVS system, I
think it was at TPHOLs in Oregon) that that kind of
automation is the most important thing for a proof checker.

So for our library we wrote a tactic called "Rational" (which
is almost identical in functionality to another Coq tactic
called "Field") that can prove any equation that you can
establish by "multiplying out everything and bringing
everything under a common denominator".  For instance it can
prove for you that

  (x + y)^2 = x^2 + 2*x*y + y^2

I guess that in Mizar that's a theorem, but the point is that
you don't need to search for it: you just say "Rational" and
it's proved.

Now I realize that in the REAL_* etc. articles there is much
more than this (inequalities, equalities that need
assumptions, etc.) but you can easily imagine a decision
procedure that is a generalization of this "Rational" thing
and that _can_ do all the things in those articles.

The technical term for this is "quantifier elimination", I
think.  For real problems that is completely unpractical,
double exponential or so, but for the things from REAL_*
etc., I guess it will do very well.

So in Mizar you could image a "requirements QUANELIM" that
would give you this.

Freek