[mizar] Re: RELPREM,RELINFER and *603,*604,*605

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Sun, 30 Dec 2007, rk1 wrote:
>
>> RELINFER, however, gives me over 400 errors in my file.
>>
>> Thanks to your example, now I see what all those errors mean: my
>> style of proof writing is rather "incremental" and I like to use one
>> fact at a time to go from one statement to the next.  You and
>> RELINFER are telling me I can condense many of these incremental
>> groups of statements into single steps.
>>
>> Do I absolutely have to remove all the RELINFER *604 and *605 errors to
>> prepare my file for submission to the MML?
>
> As far as I know (and the MML web page says so), the MML submission
> procedure requires all such errors be removed. So if you don't want to
> risk rejecting your article by a picky reviewer, you'd better get rid
> of them before submission.

When I was "polishing" an article of mine a few months ago using the
irrelevant utilities (an ironic name), I also had literally hundreds of
"errors".  Many of those errors, when fixed, did simplify my text (I too
work in a fine-grained, step-by-step way that, in some places, is even
more anal-retentive than the checker).  But many of those "errors", if
fixed, would transform my text in a way that I thought would go against
my intentions for the article.  Metaphorically speaking, relinfer was
acting like an editor who wanted me to transform my text in ways that I
thought unacceptable.

In "Writing a MIZAR article in nine easy steps" (from which I gained
much of my knowledge of MIZAR), Freek Wiedijk says:

  "Please take note that the relinfer program is dangerous! Not because
   your proofs will break but because they might become ugly. relinfer
   encourages you to cut steps that a human might want to see."

I agree.

>> I removed all the *602 and *603 from RELPREM as I agree those make
>> my proof clearer, but I think condensing many of my chosen steps as
>> RELINFER suggests would make my proof harder to read.
>
> I agree, I don't really like doing this bit of cleansing myself ;-)
> But what one finds easier to read, others may find boring, so I think
> it's better to rely on the checker's notion of obviousness.
> And 400 errors is not that bad, after all. Also, removing them by hand
> can help you improve your style and then write articles faster knowing
> better what inferences Mizar can accept.

RELPREM, TRIVDEMO, RELITER, and INACC are great tools.  But sometimes
it seems right to ignore RELINFER's advice.

Jesse

-- 
Jesse Alama (alama@stanford.edu)