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?