[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: strict



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" 


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).
Note that before any HTML browsing, you should call the verifier (it produces the XML used by the browser). 

Josef