Re: [mizar] quite some questions about functions

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear Adem,

On Mon, 12 May 2008, Ozyavas, Adem wrote:

> *********
> Question: Is it because there is no scheme available to prove existence of
> FibMoreNatural in the MML so that Fib has to be written in a less natural way and its
> existence be proved with NAT_1:shc 12?
>
>
> scheme :: NAT_1:sch 12
> LambdaRecExD{D() -> non empty set, A() -> Element of D(),
>  G(set,set) -> Element of D()}: ex f being Function of NAT,D() st
>  f.0 = A() & for n being Nat holds f.(n+1) = G(n,f.n);

It's true that at the time when the original definition of Fib was 
written, the scheme:

:: RECDEF_2:sch 4
 LambdaRec2Ex { A,B() -> set, F(set,set,set) -> set }:
  ex f being Function st dom f = NAT & f.0 = A() & f.1 = B() &
  for n being Element of NAT holds f.(n+2) = F(n,f.n,f.(n+1));

had not yet been in the MML. I think, however, that there might have been
other reasons for such a definition: to me it looks very much like an 
iterative algorithm for calculating the Fibonacci numbers, and so from 
such a point of view it seems to look a bit more natural. Maybe the authors would 
like to comment on that?

> *********
> Question: In FUNCT_2:sch 4 (given below), C, in its first use, is without parantheses
> and has left and right paranthesis in definition. Can you briefly explain why?
>
> scheme :: FUNCT_2:sch 4
> LambdaD{C, D() -> non empty set, F(Element of C()) -> Element of D()}:
>  ex f being Function of C(),D() st
>  for x being Element of C() holds f.x = F(x);

The empty parentheses () are used here to distinguish scheme arguments 
from other (simple) variables in its proof. If there are more than one 
variable, each of them should actually have its (), but to have the list 
easier to write, the parentheses are only required (and also allowed) 
for the last item in such a coma separated list as above.

> *********
> Question: In function (or functor) definitions what is the difference between using
> "means" or "equals"?

The definitions with "means" define a functor by means of a relevant 
formula (definiens) rather than just a specially constructed term, which 
is the case with "equals". Recently the "equals" definitions are processed
in such a way, that whenever a relevant 'definitions' directive is present 
in one's environment, the term from the definition is automatically known 
by the checker to be equal to the new functor. Then one does not to refer 
to the new functor's definition to make the checker accept such an 
equality.

> *********
> Question: Going back to the Fib and FibMoreNatural definitions, can Fib be defined as
> below?
>
>  ...
>  func Fib -> Function of NAT, NAT means
>  ...

Of course it can, just like FIB_NUM2:def 2 that you mentioned before.

> *********
> Question: When do we choose between
>
> ...
> func someFunction -> Function of NAT,NAT ...
> ...
>
> and
>
> ...
> let n be Nat;
> func someFunction (n) -> Element of NAT ...
> ...
>
> ?

It depends whether you want to prove some facts about the function as 
such, e.g. that 'someFunction is increasing'. Otherwise, when you're 
iterested only in the function's values, you rather use the latter 
approach - in that case the function's application 'someFunction(n)' is a 
part of Mizar itself rather than an instance of a set theoretical 
application operation 'someFunction.n', i.e. FUNCT_1:def 4.

> Also when I use the first version (func Fib -> Function of ...), the system does not
>
> let me use "let..." before (func Fib -> Function of...)?

That's because there are no formal parameters of the Fib functor
to be introduced with 'let'.

> *********
> Question: I defined a function like the one below:
>
>  ...
>  func someFunction -> Function of [:NAT,NAT:], NAT ...
>  ...
>
>  I could not find a scheme to prove its correctness in the MML? What am I doing wrong?

That very much depends on your definition, but there is no reason why
you shouldn't substitute [:NAT,NAT:] for some C() and NAT for some D()
in one of the available schemes.

> **********
> Questions: An excerpt from MML (SIN_COS.MIZ, Def18) is given below and needed for these
>
> questions.
>
> 1) Is thesis in the proof "existence"? If so, can you expand and spell out what
> "existence" stand for here (and in others possibly)?

The thesis of "existence" is a statement that there exists some f of the 
appropriate type (here 'Function of COMPLEX,COMPLEX') which fulfills the
definiens (here 'for z being Element of COMPLEX holds f.z=Sum(z ExpSeq)', 
please note the 'it' is now instantiated by our f).

> 2) I have seen in a paper I was studying that "take" instantiates the exitentially
> quantified variable in the "current" thesis. What is the current thesis after "take f"?

The thesis is created by droping the existential quantifier and 
instantiating the bound variable with f.

> 3) Is there any method/tool to know what the current thesis is at any point of proof?
>
> definition
>  func exp -> Function of COMPLEX, COMPLEX means
>  :Def18:
>  for z being Element of COMPLEX holds it.z=Sum(z ExpSeq);
>  existence
>  proof
>    deffunc U(Element of COMPLEX) = Sum($1 ExpSeq);
>    consider f being Function of COMPLEX, COMPLEX such that
> A1: for x being Element of COMPLEX holds f.x = U(x) from FUNCT_2:sch 4;
>    take f;
>    thus thesis by A1;
>  end;
>  uniqueness
>  proof
>  ...

Fortunately Josef has added such functionality to his XML rendering of 
Mizar articles. Just run Mizar on an article and then view the *.xml 
file created in an XML-supporting web browser - you should be able to 
click on some items to see the thesis at certain proof steps.

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================