Re: [mizar] Proposal for binders in Mizar

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

> >I was just interested in the semantics, I have no problem
> >with "\" instead of "lambda", or even more syntactic sugar
> >like the "at" construct.
> 
> But then I wonder how you'd write the definition.  For
> instance, can you give an approximation of what the
> definition of the "... at ... of ..." syntax for a "sum"
> binder would look like if it were defined in your style (so
> as a function "sum" applied to a lambda)?

I meant really just syntactic sugar:

definition 
  let seq be Complex_Sequence;
  let n be natural number;
  func sum seq at n -> complex number equals (Partial_Sums seq).n;
  coherence proof ... end;
end;

definition 
  let seq be Complex_Sequence;
  let k,n be natural number;
  func sum seq at k,n -> complex number equals 
       (sum seq at n) - (sum seq at k);
  coherence;
end;

sum (\x of 2*x) at n = n*(n+1);

> >I just do not like the current lack of typing for the
> >Fraenkel terms,
> 
> I agree with that.  Although it's not clear to me what the
> "better" typing rules should be.  (If the type of the
> parameter is Element of A, I probably would like the Fraenkel
> term to have type Subset of A.  But apart from that I don't
> know how it should work.)

The type detection is nothing unusual for Mizar, types of other terms are 
now detected in analyzer. 
Detecting that [x,F(x)] (in T={ [x,F(x)] where x is Element of A: P[X]} ) 
is Element of [: A,B :] (where F(x) widens to Element of B) is not enough 
to know that T defines a function, so the analysis would have to be finer 
for that. Either by searching the ordered pair there, or by using the 
"lambda" (or "\") construct, which could have separate type analysis. Both 
is quite feasible.

Josef