Re: [mizar] the carrier of and [#]

[Jesse Alama <alama@stanford.edu>]

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

> On Wed, 4 Apr 2007, Jesse Alama wrote:
>
>> Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
>>
>>> On Wed, 4 Apr 2007, Jesse Alama wrote:
>>>
>>>> I faced a surprising problem recently concerning a seeming lack of
>>>> equality of
>>>>
>>>>  [#]V
>>>>
>>>> and
>>>>
>>>>  the carrier of V,
>>>>
>>>> where V has type VectSp of F, and F has type Field.  Specifically, the
>>>> statement
>>>>
>>>>  consider G being FinSequence of [#]V such that
>>>>    G is one-to-one and
>>>>    rng G = Carrier l and
>>>>    x - y = Sum (l (#) G) by VECTSP_6:def 9;
>>>> ::>                  *103
>>>>
>>>> where l is type Linear_Combination of A, A has type Subset of V, and x
>>>> and y have type Element of V, is rejected.  For reference,
>>>> VECTSP_6:def 9 is
>>>>
>>>>  definition let GF be non empty LoopStr;
>>>>             let V be non empty VectSpStr over GF;
>>>>             let L be Linear_Combination of V;
>>>>   assume A1: V is Abelian add-associative right_zeroed right_complementable;
>>>>   func Sum(L) -> Element of V means
>>>>    :Def9: ex F being FinSequence of the carrier of V st
>>>>      F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
>>>>
>>>> However, by changing "[#]V" to "the carrier of V", my statement is
>>>> accepted.  This surprised me, since, according to STRUCT_0:def 3, we
>>>> have [#]V = the carrier of V, and my original statement is rejected
>>>> even if I cite STRUCT_0:def 3.  What might be going on?
>>>
>>> Is STRUCT_0 listed in the 'definitions' directive? - only then the
>>> equals' definition works automatically - adding a subsequent reference
>>> to a universal sentence (the definitional theorem of STRUCT_0:def 3)
>>> won't help since the checker is able to use only one such universal
>>> premise in one disjunct in an inference.
>>
>> Yes, STRUCT_0 is in my definitions directive.  Any other ideas for
>> what might be going on?
>
> Sorry, I didn't give this enough thought - the error *103 is reported
> by the analyzer, the second pass of the verifier which checks the
> syntactic ant type correctness - it knows nothing of the equality of
> [#]G' and 'the carrier of G' - they are made equal only in the
> equalizer. So you can't use '[#]G' where the type correctness of '(#)'
> requires an argument of the type 'Finsequence of the carrier of G'.

OK, I understand now why I got the error.  Would it be possible to
incorporate the equalizer into the analyzer, so that statements like
the ones I made would be acceptable?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)