[mizar] Re: trouble with a term not having the expected type

[Jesse Alama <alama@stanford.edu>]

Jesse Alama <alama@stanford.edu> writes:

> I'm working on a proof in which I'd like to use the treatment of sums
> of finite sets of elements of a field as given in FVSUM_1.  That is,
> I'm trying to use the symbol `Sum' whose meaning is defined in
> FVSUM_1:def 8.  But the meaning attached to `Sum' in my proof comes
> from RLVECT_1:def 12 rather than FVSUM_1:def 8.  I've confirmed this
> by looking at the constructor explanation for the existence claim for
> a definition of mine that uses `Sum', as well as by looking at the XML
> file generated by the verifier.
>
> Here's the definition I'm looking at:
>
> definition let p be polyhedron, c be 0-chain of p;
>   func boundary(p,c) -> -1-chain of p means :Def26:
>   for x being -1-polytope of p
>     holds it.x = Sum T(p,c,x);
>
> The operator T in that definition is defined as:
>
> definition let p be polyhedron, c be 0-chain of p, x be -1-polytope of p;
>   func T(p,c,x) -> FinSequence of the carrier of F2 means
>   ex f being FinSequence st
>     rng f = V(p) &
>     dom it = V(p) &
>     for i being Element of NAT st i in V(p)
>       ex v being vertex of p
>         st v = f.i & it.i = cc(p,x,v);
>
> F2 is a term of type Field (it represents the field whose carrier is
> {0,1} and with the usual operations and constants).
>
> The definition of the unary functor Sum in RLVECT_1 requires its
> argument F to be of type
>
>   FinSequence of the carrier of V,
>
> where V has type
>
>   non empty LoopStr.
>
> The definition of the unary functor Sum in FVSUM_1 requires its
> argument F to be of type
>
>   FinSequence of the carrier of K,
>
> where K has type 
>
>   non empty Abelian add-associative right_zeroed right_complementable LoopStr.
>
> I've set up the constructors environment in my file to be in MML.LAR
> order; more precisely, it is
>
>  constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1,
>    ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2,
>    RLVECT_1, LATTICES, GROUP_1, VECTSP_1, VECTSP_9, INT_1, STRUCT_0,
>    BINOP_1, MCART_2, FRAENKEL, ENUMSET1, RELSET_1, PARTFUN1, REALSET1,
>    FINSEQ_1, FINSOP_1, FVSUM_1, VECSP_9;
>
> How can I ensure that the constructor attached to the symbol `Sum' in
> my definition of boundary is the one in FVSUM_1 rather than the one in
> RLVECT_1?

My mistake: I should have included my notations directive instead of the constructors directive:

 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
   PARTFUN1, MCART_1, FUNCT_2, BINOP_1, ORDINAL2, FINSET_1, NUMBERS, XCMPLX_0,
   NAT_1, INT_1, CARD_1, FINSEQ_1, MCART_2, FINSOP_1, REALSET1, STRUCT_0,
   LATTICES, RLVECT_1, GROUP_1, VECTSP_1,  FVSUM_1, VECTSP_9;

What I'm wondering about is that it seems that there are two possible
meanings that one could assign to `Sum': one comes from RLVECT_1 and
the other from FVSUM_1.  Somehow, the one from RLVECT_1 is chosen.
How can I get the verifier to choose the other one?

Thanks again,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*14: Too many terms in an inference (http://www.mizar.org)