|
« Return to Thread: PATE deadline extended to April 11, 2007
Re: Functions between the positive real numbers?
by trybulec
::
Rate this Message:
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
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
« Return to Thread: PATE deadline extended to April 11, 2007
| Free embeddable forum powered by Nabble | Forum Help |
