[mizar] quite some questions about functions

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Hello all,

I have quite some comments together with my related questions about functions (and 
indirectly about functors) and appreciate your help in advance. My questions are:

1) the Fib function given partly below does not follow naturally from the informal 
definition of Fibonacci series.  As far as I see part of Fib definition is in terms of 
a recursive function fib that takes one argument, say a,  and the value of fib at a is 
a pair. 

definition
  let n be Nat;
  func Fib (n) -> Element of NAT means
  :Def1:
  ex fib being Function of NAT, [:NAT, NAT:] st
  it = (fib.n)`1 & fib.0 = [0,1] & for n being Nat
  holds fib.(n+1) = [ (fib.n)`2, (fib.n)`1 + (fib.n)`2 ];
  ...


A more natural definition of Fibonacci series would be, let me call this 
FibMoreNatural:

definition
   func Fib -> Function of NAT, NAT means
   it.0 = 0 &
   it.1 = 1 &
   for k being Nat holds it.(k+2) = it.(k+1) + it.k;
end;

which was defined by Adam Grabowski and Magdalena Jastrzcebska.

The scheme used to prove Fib's existence requires a function from NAT to D(). I see the 
reason why fib in Fib definition has type from NAT to pair (here pair can be pattern 
matched with D() in the scheme definition, NAT_1:sch 12 given below). 


*********
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);

*********
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);

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

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

*********
Question: When do we choose between
 
 ...
 func someFunction -> Function of NAT,NAT ...
 ... 

 and

 ...
 let n be Nat;
 func someFunction (n) -> Element of NAT ...
 ...

 ?

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

let me use "let..." before (func Fib -> Function of...)?

*********
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?

**********
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)?

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"?

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


I truly appreciate all your help and I know that my best  helper is the MML. But I 
could not help asking these questions and trying to figure out many more myself. Thank 
you all...

Adem Ozyavas