[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Functions between the positive real numbers?

Dear Freek,
would me send the attempts that you made. Then I could analyse what's the problem. 

Some remarks now:
Positive reals are introduced in GRPAH_5 (probably should be moved to concrete mathematics) : 

  func Real>=0 -> Subset of REAL equals
:: GRAPH_5:def 12
  { r where r is Real : r >=0 };

Actually, they are introduced also in ARYTM_2

 func REAL+ equals
:: ARYTM_2:def 2
 RAT+ \/ DEDEKIND_CUTS \ {{ s: s < t}: t <> {}};
but making the definition in GRAPH_5 a redefinition of ARYTM_2:def 2 looks like a horror. The ARYTM_2 should be encapsulated, anyway. 

I would introduce an attribute

 'positive-preserving'

maybe under a better name. It seems to be useful.

All the best,
Andrzej


Freek Wiedijk wrote:

Dear Mizar community,

I'm currently teaching a Mizar course, and a problem came up
that I haven't been able to solve.  Please help me with this.

I ask the students as an exercise to formalize the solution
of a puzzle from the international mathematical olympiads
that talks about a function from the positive real numbers
to the positive real numbers:

<http://www.cs.ru.nl/~freek/courses/pa-2007/exercises/exercise-mizar.pdf>

In the solution to this exercise, we would like to be able
to use the notions from LIMFUNC1.  So the simplest approach
is just to use something like

  reserve f for PartFunc of REAL,REAL

and then have conditions like

  for x being positive Real holds x in dom f

and

  for x being positive Real holds f.x is positive Real

That works.  However, it is not very elegant.

So both me and two of my students have tried to make
redefinitions and clusters such that we could use

  reserve f for Function of posREAL,posREAL

where

  posREAL -> Subset of REAL

is the set of positive real numbers, and then -- because of
those redefinitions/clusters -- have f _also_ automatically
be of type "PartFunc of REAL,REAL".  However, we have
failed dismally.  Worse, we got _very_ mystifying errors.

So I have three (or in fact four, as one of the students
has tried two different approaches) attempts that I have
questions about.  But before bothering the list with these
files, maybe someone (Andrzej?) can just tell us how to
do this?  Or is not possible?

I would like to show my group how nice the Mizar type
system is (as it is!).  So not getting this to work is
frustrating...

Freek