Re: [mizar] A general question on writing recursive functions in mizar

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

Dear Adem,

On Wed, 30 Apr 2008, Ozyavas, Adem wrote:

> I want to write recursive functions in mizar and prove properties of 
> them. I have found a paper by Yatsuka Nakamura which helped but not 
> enough for me.  For the time being I am searching the MML for examples. 
> Can anyone refer me to a tutorial, paper, notes, etc which provides info 
> on
> 1) the distinction between mizar functors and functions,
> 2) how to write mizar recursive functions and prove their correctness.
I'm not sure if there are any printed papers addressing these particular 
questions, so let me try to explain it here:
> 1) the distinction between mizar functors and functions,
You define functors when you're interested in constructing terms 
easily rather than proving some set-theoretical properties of 
corresponding functions. E.g. we have:
definition
  func sin -> Function of REAL, REAL means
:: SIN_COS:def 20
  for d being Element of REAL holds
  it.d = Im(Sum([*0,d*] ExpSeq));
end;

definition
  let th be real number;
  func sin th equals
:: SIN_COS:def 21
  sin.th;
end;

To prove that the sine function is bounded, you would use the first 
definition, but in case you want to show some properties of its values for 
certain angles, the other is better (the application of arguments is 
then part of the Mizar language with type control, etc.)
> 2) how to write mizar recursive functions and prove their correctness.
For example, please take a look at

definition
  let n be Nat;
  func Fib (n) -> Element of NAT means
:: PRE_FF:def 1
  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 ];
end;

and the schemes used in the correctness proof are:

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

and

scheme :: NAT_1:sch 16
 LambdaRecUnD{D() -> non empty set,A() -> Element of D(),
  RecFun(set,set) -> Element of D(), F, G() -> Function of NAT,D()}: F() = G()
provided
 F().0 = A() and
 for n holds F().(n+1) = RecFun(n,F().n) and
 G().0 = A() and
 for n holds G().(n+1) = RecFun(n,G().n);

I hope the above may be of some help.

Best regards,

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/
======================================================================