Re: [mizar] Binders?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Mon, Oct 14, 2002 at 10:13:14PM +0200, Freek Wiedijk wrote:
> Dear Piotr,
> 
> >Interesting, I always thought that "sum(i=1,n,i^2)" was
> >clumsy in comparison to "sum f".
> 
> So I feel the other way around.  The first notation becomes
> even nicer when you nest binders.  To write a lemma
> "sum(i=1,n,sum(j=1,m,a[i,j])) = sum(j=1,m,sum(i=1,n,a[i,j]))"
> the second way will be a _lot_ less transparent, I think.
> Just tell me how you would write this scheme in the "sum f"
> style, and we'll see.

I wrote interesting, it does not mean I will defend it forever.

Without operators introducing bound variables I would have to define
a sequence f of len n whose elements are sequences of len m and
a sequence g of len m whose elements are sequences of len n and
then  I would have 

	sum flatten f = sum flatten g

Indeed it is far from common practice but still it can go a long way.
Hwoever, the crux of the matter is rather to have convenient notation 
for introducing object "a" above, as pan Urban noticed in his note.

Cheers,

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr