Re: [mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

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

> On Tue, 9 Jan 2007, Jesse Alama wrote:
>
>> Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
>>
>>> On Tue, 9 Jan 2007, Jesse Alama wrote:
>>>
>>>> The error definitely lies with the theorem, not with the summaries of
>>>> the error messages at the bottom of the file:
>>>>
>>>> theorem
>>>> F2 is strict;
>>>> ::>        *4
>>>
>>> Yes, it couldn't be that easy ;-)
>>>
>>>> Here's my environment; it's nasty:
>>>>
>>>> vocabularies FINSET_1, POLYFORM, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1,
>>>> SUBSET_1, TARSKI, BOOLE, MCART_1, RELAT_1, NAT_1, XCMPLX_0,
>>>> ORDINAL2, VECTSP_1, VECTSP_9, INT_1, BINOP_1, MCART_2, RLVECT_1,
>>>> GROUP_1; notations FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2,
>>>> ZFMISC_1, CARD_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS,
>>>> XCMPLX_0, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1,
>>>> LATTICES, MCART_2, RLVECT_1, GROUP_1;
>>>> constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1,
>>>> ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2,
>>>> VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2,
>>>> FRAENKEL, ENUMSET1, RLVECT_1, GROUP_1;
>>>> registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2,
>>>> RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0;
>>>> requirements NUMERALS, BOOLE, ARITHM, SUBSET;
>>>> definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2,
>>>> ENUMSET1, RLVECT_1, BINOP_1, STRUCT_0, GROUP_1; theorems XBOOLE_0,
>>>> FUNCT_1, RELAT_1, XBOOLE_1, TARSKI, ZFMISC_1, MCART_1, SUBSET_1,
>>>> FUNCT_2, MCART_2, ENUMSET1, BINOP_1, STRUCT_0, GROUP_1; schemes
>>>> FUNCT_1, BINOP_1;
>>>
>>>> Could it be that something in my environment is messed up?
>>>
>>> Exactly - the offending part are the notations imported from RLVECT_1
>>> after VECTSP_1 - this way your "strict" is the one automagically
>>> defined for LoopStr instead for doubleLoopStr! The order of imported
>>> notations is relevant, and it's best to use the 'mml.lar' list to
>>> control it - please see the thread at:
>>>
>>> http://mizar.uwb.edu.pl/forum/archive/0609/msg00071.html
>>>
>>> If your work dosn't depend on this unfortunate transposition, you
>>> should be able to just change the order of these two directives
>>> without any other changes to your article and get rid of the *4.
>>
>> It turns out that transposing RLVECT_1 and VECTSP_1 in the
>> constructors directive doesn't eliminate the *4.  Are there some other
>> "strict"'s that are being imported here that I don't know about?
>
> yes many, in Emacs menu, select Mizar->Browse as HTML->Browse
> environmental constructors, wait a while (for the XSLT processing),
> and search for "strict"

OK, that helps, thanks.  There are indeed a bunch of "strict"'s being
used here, but I'm not sure how to use the results.  What is the
significance of the order of the items in this file?  I ask because in
it I see

let a1 be doubleLoopStr ;
attr a1 is strict;

before

let a1 be 1-sorted , a2 be VectSpStr of a1;
attr a2 is strict;

let a1 be L10();
attr a1 is strict;

let a1 be L11();
attr a1 is strict;

let a1 be L12();
attr a1 is strict;

My first guess is that LATTICES is "stealing" strict, but I'm not sure.

>> How
>> did you find out that it was the order of RLVECT_1 and VECTSP_1 that
>> might be the source of the problem?
>
> again, try Mizar->Browse as HTML->Browse current article, and see to
> what article is the symbol "strict" linked (I should probably change
> the linking to $MIZFILES/html, for people who decide to install the
> HTML-ized library - then it would be even easier).

Where can one get the HTML-ized library?

> Note that before any HTML browsing, you should call the verifier (it
> produces the XML used by the browser).

Perhaps that could be done automatically in the sense that if the
buffer has changed, then a warning is given: "Run verifier before
browsing HTML?".

Jesse

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