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:
>
>> 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?
>
> None, AFAIK. I was just telling you how to see them all with available
> tools.
>
>> 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.
>
> As Adam wrote, "notations" is the usual suspect, being sensitive to
> ordering (the last matching notation is always selected). Now I see
> that viewing all the notation (not just constructors) is useful for
> this, so I added their displaying to miz.xsl
> (http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/*checkout*/xsl4mizar/miz.xsl)
> and mizar.el
> (http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/*checkout*/mizarmode/mizar.el).
> You'll need to copy both files to your $MIZFILES, and rename miz.xsl
> to miz.xml.

Will the updated mizar.el and the new miz.xsl be added to the next
mizar release?

Jesse

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