Re: [mizar] weak types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

Freek Wiedijk wrote:

>
> So I'm not sure exactly what a Mizar-like system that's build
> on these principles should look like.  But I do think that
> sqrt x > a should _not_ be an abbreviation of
> x >= 0 & sqrt x > a.  Instead I think that to be allowed to
> write down sqrt x > a you should be required to prove
> x >= 0.  Apart from that you could use the existing
> (permissive) semantics of Mizar as far as I'm concerned.

With a permissive definition like (NATTRA_1:def 8):

 let A,B be Category, F1,F2 be Functor of A,B;
 assume F1 is_naturally_transformable_to F2;
 mode natural_transformation of F1,F2 -> transformation of F1,F2 means
  for a,b being Object of A st Hom(a,b) <> {}
   for f being Morphism of a,b holds it.b*F1.f = F2.f*it.a;

when one proves that a transformation is a natural transformation, then one
has to prove first the guard (the assumption in the definition) and then the
definiens, like in the proof of coherence in NATTRA_1:def 9

    t2`*`t1 is natural_transformation of F,F2
   proof thus F is_naturally_transformable_to F2 by A1,A2,Th25;
    thus thesis by A3,A4,A5,Lm2;
   end;

And if one refers to NATTRA_1:def 8, one has also to refer to the fact that
  F1 is_naturally_transformable_to F2
and, of course to the definiens.

So the difference seems to be in the fact, that you want to state the guard,
if you just write
      T is natural_transformation
and in Mizar we need guard only when the definition is actually used. It is
something like lazy evaluation.
I believe it is the main argument for the permissiveness.

Andrzej