[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Re: thank you very much and two more questions...
Hi Adem,
On Thu, 10 Apr 2008, Ozyavas, Adem wrote:
1) I tried the below complete mizar article:
environ
vocabularies ARYTM_3,
ORDINAL2, ::natural
ARYTM; ::number
notations NAT_D, ::format for divides
ORDINAL1; ::format for natural and number
constructors NAT_D, ORDINAL1;
requirements SUBSET, NUMERALS;
registrations ORDINAL1; ::to register natural number cluster
begin
theorem for n being natural number holds 2 divides n*(n+1);
::> *165,165
::>
::> 165: Unknown functor format
mizar returns with error 165, because n*(n+1) is not of type Nat (it is a complex
number) where "divides" predicate expects two arguments of type Nat. Following one
example, I added NAT_1 to the notations and constructors directives and it
worked except for the fact that #4 error is reported, that is, a justification is
needed and no problem with that...
Now, my question is that "what is it in the NAT_1 article that removes the typing error
#165? I checked the contents of NAT_1 and only two redefinitions of + and * caught
my attention but they require different types than natural number which is the type of n
in the example article above but the redefinitions of + and * in the NAT_1 article need Nat and
Element of Nat for the two arguments respectively or vice versa.
As I wrote before, this can be quite a black art, in which (as it seems
to me) you got lucky with this example. If you try proving in your article
the following:
theorem for n being natural number holds n*(n+1) is natural number;
it will succeed, but if you try:
theorem for n,m being natural number holds n*(n+m) is natural number;
you will get parse errors. The difference is that the Mizar verifier
"knows too much" about the numeral 1 (it knows that it is Element of NAT),
and as a result both the + and * redefinitions in NAT_1 work in that
example. The verifier does not know this about n (nor m in the second
example).
This is quite subtle, I had to use an explanation provided by the E
automated theorem prover on your article to see it (hopefully I'll make
this functionality publicly available soon, some static explanations
for a couple of existing articles can be browsed by clicking at the "by"
keywords at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_bytst/).
A general advice for novices is not to construct the environment by
themselves, and just copy it from a related article. This is the worst
kind of problems with writing Mizar articles, and unfortunately we still
have not provided some easy and safe options for construction of the
environment.
2) my second question is related to the first one which is about types in mizar. I have
been reading papers, notes I could find in journals and on the internet about mizar and
writing articles. I could not comprehend the difference among Nat, Element of Nat,
natural number. My understanding is that they are semantically the same, that is, a
variable of type any of these 3 is a natural number. I do not quite figure out which
one to prefer in articles and why?
For general issues with the environment I really recommend reading at
least section 1.4 in Freek Wiedijk's Mizar tutorial:
http://mizar.org/project/mizman.pdf . The type Nat is now just a syntactic
sugar for "natural number"
(http://mmlquery.mizar.org/mml/4.100.1011/nat_1.html#NM1, keyword "is"
defines the new type just as a syntactic macro). Type Element of NAT is
stronger in the type hierarchy than "natural number": the conditional
registration from ORDINAL1
(http://mmlquery.mizar.org/mml/4.100.1011/ordinal1.html#CC7) :
cluster -> natural Element of omega ;
automates that direction (every Element of omega is natural), but there is
currently no automation in the opposite direction (though as you say, the
semantics is the same). I really don't know what the current recommended
MML policy is: I thought that the usage of Element of NAT was discouraged
in favour of "natural number", but clearly sometimes things still work
better with Element of NAT.
Josef