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

Re: [mizar] unused loci

Hi,

On Wed, 21 Feb 2007, Jesse Alama wrote:


In my proof of Euler's polyhedron formula, I'm considering functors
like this:

definition let p be polyhedron,
              f be enumeration of vertices(p),
              c be 0-chain of p;
 func Sum c -> Element of F2 means
 ex s being Element of V(p)-tuples_on the carrier of F2
   st f,s represents c & it = Sum s;

This definition gives rise to error 100 ("unused locus").  A working
definition is

definition let p be polyhedron,
              c be 0-chain of p;
 func Sum c -> Element of F2 means
 ex f being enumeration of vertices(p),
    s being Element of V(p)-tuples_on the carrier of F2
   st f,s represents c & it = Sum s;

It doesn't matter so much whether I use the first or the second
definition.  The first option, though, is nicer, since in its
uniqueness proof I can appeal to the fact (proved earlier) that

 f,s represents c & f,t represents c implies s = t

But in the uniqueness proof for the second case, I have to use the fact
(also proved earlier) that

 f,s represents c & g,t represents c implies Sum s = Sum t

(the antecedent implies that s is a permutation of t, and then I use
invariance of sums under permutations).

Apart from the mathematical niceness of being able to use the first
definition instead of the second, why is it that I get the unused
locus error?  I don't see why it's OK to write "Sum c" even though
there is a hidden parameters (p, the polyhedron) that doesn't need to
get expressed, but yet "Sum c" with two implicit parameters (the
polyhedron p and the enumeration f of the vertices of p) is malformed.
What's going on here?
The implicit parameters must be somehow deducible from the explicit ones - that's the case with 'p' which is reconstructed using 'c'. Otherwise there's no way to specify which 'f' you have in mind when you use 'Sum c'. 
And if you mean 'any f', then it must be stated as such in the definiens:

func Sum c -> Element of F2 means
for f being enumeration of vertices(p) ...

or as you propose (which is even better to use later)

func Sum c -> Element of F2 means
for f being enumeration of vertices(p) ...
And I don't see why this should be 'less elegant' than the formulation with a fictitious parameter ;-) 

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================