quite some questions about functions

[Ozyavas, Adem]

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

[Adam Naumowicz]

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

Hi Ad[ae]m :-),

On Mon, 12 May 2008, Adam Naumowicz wrote:

> On Mon, 12 May 2008, Ozyavas, Adem wrote:
>
>> 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.

Or, if it is an existing MML article like in this case, just go to:
http://mmlquery.mizar.org/mml/current/sin_cos.html#D18 . Clicking on the
'existence' keyword will show you the existence condition, and clicking on
the followng 'proof' keyword will expand the proof, where the ':: thesis:'
after each natural deduction step can again be clicked on.

If it is a new article (not yet in MML), either use the method Adam
described, or you can also paste the article into
http://octopi.mizar.org/~mptp/MizAR.html and press the Send button.

Josef

[Jesse Alama]

Josef Urban <urban@...> writes:

> Hi Ad[ae]m :-),
>
> On Mon, 12 May 2008, Adam Naumowicz wrote:
>
>> On Mon, 12 May 2008, Ozyavas, Adem wrote:
>>
>>> 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.
>
> Or, if it is an existing MML article like in this case, just go to:
> http://mmlquery.mizar.org/mml/current/sin_cos.html#D18 . Clicking on
> the 'existence' keyword will show you the existence condition, and
> clicking on the followng 'proof' keyword will expand the proof, where
> the ':: thesis:' after each natural deduction step can again be
> clicked on.
>
> If it is a new article (not yet in MML), either use the method Adam
> described, or you can also paste the article into
> http://octopi.mizar.org/~mptp/MizAR.html and press the Send button.

What's going on at octopi.mizar.org?

Jesse

--
Jesse Alama (alama@...)

[Josef Urban]

On Tue, 13 May 2008, Jesse Alama wrote:

> Josef Urban <urban@...> writes:
>>
>> If it is a new article (not yet in MML), either use the method Adam
>> described, or you can also paste the article into
>> http://octopi.mizar.org/~mptp/MizAR.html and press the Send button.
>
> What's going on at octopi.mizar.org?

It is a fairly experimental service for explaining Mizar atomic
inferences (and doing more) using automated provers. As a byproduct, it
also html-izes articles. More at
http://mizar.uwb.edu.pl/forum/archive/0804/msg00004.html .

Josef