Re: [mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> On Tue, 9 Jan 2007, Adam Naumowicz wrote:
>
>> On Tue, 9 Jan 2007, Jesse Alama wrote:
>>
>>> Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
>>>
>>>> BTW: it's better to state such properties of F2 as functorial
>>>> registrations rather than theorems - this way they could be used
>>>> automatically by the checker when one would import your registrations.
>>>
>>> I see your point, and when I was looking in the MML for examples on
>>> which I could base my definition of F2, I found that functorial
>>> registrations were the customary way of accomplishing my task.
>>> Although I don't want to break with the custom and I understand the
>>> value for the checker if I follow it, I do think that it is more
>>> natural to express the properties of a new term as theorems rather
>>> than as functorial registrations.  By expressing properties in terms
>>> of functorial registrations, one is writing for the MIZAR checker, not
>>> for human readers.  It seems to me that using functorial registrations
>>> takes MIZAR away from rather than toward the mathematical vernacular.
>>> (Though perhaps one could argue that the MIZAR custom of functorial
>>> registrations is actually captures what's going on in the mathematical
>>> vernacular.)
>>
>> Yes, it's a clear-cut example of a trade-off between sticking close
>> to the mathematical vernacular and adding more automation with new
>> language constructs. In this case, however, the registrations look
>> painfully technical in their *.miz form, but various forms of
>> presentation may 'smooth' them a bit - e.g. the relevant theorems
>> could be printed in the *.xml presentation next to the
>> registrations. And in the TEX'ed form of Formalized Mathematics the
>> presentation looks more or less like a mathematical statement, e.g.:
>> "One can verify that ... is ...".
>
> I think you can have both the theorem and the registration (trivially
> justified by the theorem). Another "more human" way would be just to
> have a theorem-property (analogy of definitional properties like
> "symmetry"), which would tell the checker to use the theorem for the
> automations. Perhaps a better word than "property" would be Andrzej's
> "pragma" in this case (e.g. keyword "register"). But I think the
> current explicit writing of registrations does not hurt much, and the
> explicit writing has its advantages. Also, in the example, wasn't it
> possible to put "strict" directly in the result type of F2 instead of
> having an extra registration for it?

In the example I indeed could have written

definition
  func F2 -> strict doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2,  zero2 #);
  coherence;
end;

rather than

definition
  func F2 -> doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2,  zero2 #);
  coherence;
end;

but I chose to isolate the proof of strictness (I had thought that
this was a "first-order" property like, e.g., commutative) and put it
in a separate theorem because I wanted to keep as separate as possible
the proofs of the various properties of F2.  Now I realize that the
attribute strict is different from other attributes.  Imagine, though,
that I had written, say,

definition
  func F2 -> commutative doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
  coherence;
end;

rather than

definition
  func F2 -> doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #);
  coherence;
end;

theorem
F2 is commutative;

In the latter case, we can give a label to the theorem and refer to it
later, whereas in the former case, the property of commutativity is
part of the definition of F2, which seems to me to be unnatural.
There may be cases where it *is* natural to put properties of a term
into its definition and then prove that the term has those properties
in the correctness proofs, but in general that seems to me to be an
unnecessary tangling.

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference