Re: [mizar] definitions for incomparable (?) types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Jesse,

On Wed, 3 Jan 2007, Jesse Alama wrote:

> I recently came across the definition of the attribute left_unital for
> non-empty multLoopStr's.  The definition is in VECTSP_1:
>
> definition let IT be non empty multLoopStr;
> attr IT is left_unital means
> for x being Element of IT holds 1.IT * x = x;
> end;
>
> When I browse the semantic HTML presentation of the MML the link from
> the "1." in the formula above goes to the definition in GROUP_1:
>
> definition let G be non empty HGrStr such that A1: G is unital;
> func 1.G -> Element of G means
>  for h being Element of G holds h * it = h & it * h = h;
> existence;
> uniqueness;
> end;
>
> The functor "1." requires its argument to be a unital HGrStr.

No, it does not. There is a syntactic difference that matters between:

definition let G be non empty unital HGrStr;

and

definition let G be non empty HGrStr such that A1: G is unital;

The first definition would really syntactically force the argument of "1." 
to be of type "non empty unital HGrStr", i.e. the Mizar type checking 
module would give an error, if it would not succeed in widening the 
argument of "1." to that type.

The second definition does not put the assumption of "being unital" to the 
type system (for whatever reason, see some previous discussions on mizar 
forum about the type system). The semantics (hidden in the Mizar 
implementation) of "assume A1: G  is unital;" is that the defined functor 
"1." is still total on the whole domain of its (syntactic) argument type 
(i.e. "non empty HGrStr"), but the only thing we know about its values on 
"non unital" arguments is that they have the result type stated in the 
definition (i.e. "Element of G"). The definitional theorem created here 
contains the "unitality" assumption (click on ":: deftheorem Def5 defines 
1. GROUP_1:def 5 :" at 
http://mmlquery.mizar.org/mml/4.66.942/group_1.html#K2 to see it):

for G being non empty HGrStr st G is unital holds
for b2 being Element of G holds
( b2 = 1. G iff for h being Element of G holds
( h * b2 = h & b2 * h = h ) );

So you cannot use the "definiens" of "1." in non unital cases.

> But it
> doesn't look like the type "non empty multLoopStr" widens to the type
> "unital HGrStr".  (I'm not sure if I'm using the term "type" and
> "widen" correctly here; please let me know if I should express myself
> differently.)

I think you use the terms as they are normally used in Mizar context.

> Thus, I'm not sure how the definition of the attribute
> left_unital makes sense.  What's going on here?  I'm thoroughly
> confused; any clarification would be appreciated!

Usually it's just one way how to deal with partial functors in Mizar, 
though sometimes abused. Its side effect is the axiom of choice built-in 
directly into the Mizar type system (see the "choose" functor at 
http://mmlquery.mizar.org/mml/4.66.942/subset_1.html#K10

Best,
Josef