[mizar] Re: puzzling errors

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Sun, 11 Mar 2007, Jesse Alama wrote:
>
>> In the article I'm working on, the formula
>>
>>  bounding-0-circuit-space(p) is Subspace of 0-circuit-space(p)
>>
>> is flagged with *101 ("Unknown mode") underneath the use of Subspace.
>> At the stage where this formula occurs in my article, the term
>> bounding-0-circuit-space is just a VectSpStr over F2 (the field {0,1}
>> with the usual operations).  I'm trying to establish that it has type
>> VectSp of F2 by proving and then appealing to
>>
>> for G being Field,
>>    U being VectSp of G,
>>    X being non empty Subset of the carrier of U,
>>    f being BinOp of X,
>>    l being Function of [:the carrier of G,X:],X,
>>    z being Element of X
>>  st f = (the add of U)||X &
>>     l = (the lmult of U)|[:the carrier of G,X:] &
>>     z = the Zero of U
>>  holds VectSpStr (# X, f, z, l #) is Subspace of U;
>>
>> What surprises me is that this formula is flagged only with *4; it is
>> not flagged with *101.  That suggests that the last formula
>>
>>  VectSpStr (# X, f, z, l #) is Subspace of U
>>
>> is well-formed (in the sense that the use of Subspace there isn't
>> flagged with *101).  Why is my theorem about Subspaces not flagged
>> with *101 but my claim about bounding-0-circuit-space(p) is flagged
>> with that error?
>
> I guess the term '0-circuit-space(p)' is the culprit here - it seems its
> type doesn't widen to 'Vectsp of F', where F is some field.

You're right -- it turns out that 0-circuit-space(p) didn't have the
right type.  But there's a little twist in this story.

I proved earlier in my article that the term 0-circuit-space(p) has
type VectSp of F2, and F2 has type Field.  But what's required for
formulas of the form

  X is Subspace of Y

is that Y has type

(*)  non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of GF

where GF has type

  non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr.

(This comes from VECTSP_4.)  I have a registration

(**) registration let p be polyhedron;
  cluster 0-circuit-space(p) -> VectSp of F2;
  coherence by <some theorem>;
end;

So 0-circuit-space(p) has type VectSp of F2.  But, to my surprise, it
didn't automatically get the adjectives in (*).  By adding a new
registration

(***) registration let p be polyhedron;
  cluster 0-circuit-space(p) -> non empty Abelian add-associative right_zeroed right_complementable VectSp-like;
  coherence by <some theorem>;
end;

the *101 error I described goes away.  This surprises me because the
mode VectSp of F is expandable; I thought that any term of type VectSp
of F automatically got all the adjectives in (*).  This is reinforced
by the failure of the coherence of registration (***) to go through
when I omit the reference to <some theorem>, even though (**) occurs
before (***).  Is this a feature or a bug?

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*116: Invalid "qua" (http://www.mizar.org)