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

Re: [mizar] Re: strict



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. 


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?


http://mizar.uwb.edu.pl/forum/archive/0612/msg00012.html


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?".


yes, done in the CVS version of mizar.el

Josef