PATE deadline extended to April 11, 2007

[Adam Naumowicz]

Dear All,

I hope this deadline extension can help some of you to contribute
papers for this workshop.

Best regards,

Adam Naumowicz

=============================================================================
Final call for papers, the deadline for submission has been extended to
April 11, 2007.

=====================================================================

                Call for Papers

        RDP (RTA 07 + TLCA 07) Workshop PATE

       Proof Assistants and Types in Education

               June 25 2007

           http://www.rdp07.org/pate.html
=====================================================================

This workshop is supported by the EU Types Coordination Action.

The purpose of the workshop is to bring together
researchers and lecturers interested in applying
type theory and proof assistants in teaching.

Contributions are solicited in the following subject areas
and related topics:

- type theory as a language for (teaching) mathematics and programming;
- computer assisted informal reasoning;
- tools and languages for teaching math and logic;
- experience in using proof assistants in class.

Submissions and Publication
-----------------------------
Authors are invited to submit a paper (max 15 pages) by e-mail to
Pierre.Courtieu@... by April 11, 2007. Preliminary proceedings will
be available at the workshop. Submissions should be in PostScript or
PDF format, using ENTCS style files.

Important Dates
-----------------
    Submission deadline:  April 11, 2007
    Notification: May 15, 2007
    Pre-proceedings version due: June 7, 2007
    Workshop: June 25, 2007

Programme Committee
--------------------
Pierre Courtieu CNAM Paris (Co-Chair)
Herman Geuvers Nijmegen (Co-Chair)
Hugo Herbelin INRIA Paris
Adam Naumowicz Bialystok
Claudio Sacerdoti Coen Bologna
Pawel Urzyczyn Warsaw

[Freek Wiedijk]

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

[Jesse Alama]

Freek Wiedijk <freek@...> writes:

> 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.

What environment are you using?  (I can't count how many hours I've
been blocked by mystifying errors that are just due to something being
wrong or missing in my environment.  There has got to be a way to make
getting the environment right not so unpleasant!  Perhaps we can have
a separate discussion about that.)

Jesse

--
Jesse Alama (alama@...)
*950: Too many schemes (http://www.mizar.org)

[Freek Wiedijk]

Hi Jesse,

>What environment are you using?

The environment of my personal attempt at a solution (that
didn't work) was:

 vocabularies ARYTM, PARTFUN1, ARYTM_1, RELAT_1, ARYTM_3, FUNCT_1, ABSVALUE,
  FINSEQ_1, LIMFUNC1, ASYMPT_0, ORDINAL2, RCOMP_1, BORSUK_5, FUNCT_2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
  SEQ_1, RELSET_1, PARTFUN1, XXREAL_0, NAT_1, IRRAT_1, FUNCT_1,
  FUNCT_2, BORSUK_5, LIMFUNC1;
 constructors REAL_1, COMPLEX1, LIMFUNC1, POWER, SEQ_1, FUNCT_2;
 registrations XREAL_0, MEMBERED, XXREAL_0, NAT_1, REAL_1, PARTFUN1, FUNCT_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

>There has got to be a way to make getting the environment
>right not so unpleasant!  Perhaps we can have a separate
>discussion about that.

We already had :-)  (Before you joined the list, I guess.)

Freek

[Adam Naumowicz]

On Wed, 4 Apr 2007, Freek Wiedijk wrote:

> 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.

Apparently we've already discussed this problem (typical ;-)) - please see
the following archival thread and its follow-ups:

http://mizar.uwb.edu.pl/forum/archive/0609/msg00001.html

But I'm affraid no satisfying solution was offered then, and the library
and the system haven't changed yet to support the proposed "future"
solutions...

Best,
Adam Naumowicz

======================================================================
Department of Applied Logic            fax. [phone]
Institute of Computer Science          tel. [phone] (office)
University of Bialystok                e-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================

[Josef Urban]

On Wed, 4 Apr 2007, Jesse Alama wrote:

> What environment are you using?  (I can't count how many hours I've
> been blocked by mystifying errors that are just due to something being
> wrong or missing in my environment.  There has got to be a way to make
> getting the environment right not so unpleasant!  Perhaps we can have
> a separate discussion about that.)

that thread seems
to start at http://mizar.uwb.edu.pl/forum/archive/0609/msg00022.html

Josef

[trybulec]

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

[trybulec]

Dear Freek,

Few seconds after sending the letter I recognized that you need the set
of all positive real numbers and the definitions that I mentioned deals
with the set of all non negative real numbers. Sorry.

Stiil, I do not think that it is worth to introduce such functions.
The attributes are easier to manipulate.

Happy Eastern,
Andrzej