[mizar] factorial function

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

Dear All,

I wanted to present a comment about a question I asked over the weekend so that hopefully it is a bit more clearer. I am giving a factorial function I wrote
a day ago with its correctness together with a theorem about this function:



::FIRST DEFINITION and ITS CORRECTNESS
definition
  let n be Nat;
  func mfac(n) -> Element of NAT means
  :Defmfac:
  ex fac being Function of NAT, NAT st
  it = fac.n & fac.0 = 1 & for n being Nat
  holds fac.(n+1) = (fac.n) * (n+1);
  existence
  proof
    deffunc F(Nat, Element of NAT) = $2 * ($1+1);
    consider fac being Function of NAT, NAT such that
A1: fac.0 = 1 and
A2: for n being Nat holds fac.(n+1) = F(n,fac.n) from NAT_1:sch 12;
    take fac.n, fac;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof

    let it1, it2 be Element of NAT;
    deffunc F(Nat,Element of NAT) = $2 * ($1 + 1);
    given fac1 being Function of NAT, NAT such that
A3: it1 = fac1.n and
A4: fac1.0 = 1 and
B4: for n being Nat holds
    fac1.(n+1) = F(n,fac1.n);
    given fac2 being Function of NAT, NAT such that
A5: it2 = fac2.n and
A6: fac2.0 = 1 and
B6: for n being Nat holds
    fac2.(n+1) = F(n,fac2.n);
    fac1 = fac2 from NAT_1:sch 16(A4,B4,A6,B6);
    hence thesis by A3,A5;
  end;
end;


::THE THEOREM
theorem for n being Nat holds mfac(n) > 0
  proof
    ::let n be Nat;
    defpred P[Nat] means mfac($1) > 0;
    deffunc F(Nat, Element of NAT) = $2 * ($1 + 1);
    consider fac being Function of NAT, NAT such that
  A1:fac.0 = 1 and
  A2:for n being Nat
    holds fac.(n+1) = F(n,fac.n) from NAT_1:sch 12;
  A3:mfac(0) = 1 by A1, A2, Defmfac;
    then
  P0:P[0];

  PN: for n being Nat holds P[n] implies P[n+1]
    proof
      let n be Nat;
      assume B0:P[n];
    B3:mfac(n+1) = fac.(n+1) by A1, A2, Defmfac
                .= (fac.n) * (n + 1) by A2
                .= mfac(n) * (n + 1) by A1,A2,Defmfac;
    B4:(n+1) > 0 by NAT_1:5;
    B5:mfac(n) * (n + 1) > 0 * (n + 1) by B0, B4, XREAL_1:70;
       mfac(n) * (n + 1) > 0 by B5;
       hence P[n+1] by B3;
    end;
    thus for n being Nat holds P[n] from NAT_1:sch 2(P0,PN);
  end;


My comment:
Statements I want to prove about functions are going to be similar to the theorem given, that is, factorial
function applied to a natural number always is a positive integer or the greatest common divisor function,
called egcd in my earlier email, is really the greatest common divisor of its two arguments, that is,
egcd(m,n) = m hcf n where m and n are natural numbers. As can be seen from the theorem proven above
I basically manipulate the definition of functions and derive some conclusions so that I am not really interested in
actual values of functions or properties of functions in my  proofs. Functors are better suited than functions for my
goals but functions are the only way when translating recursive math functions to Mizar.
Any comments on these are truly appreciated.


Also, I would prefer the Mizar factorial function, mfac  here, to be written as close to its SequenceL function
as possible, such as,

definition
  func mfac -> Function of NAT, NAT means
  :Def1:
  for n being Nat holds it.n = 1 if n = 0 otherwise it.n = it.(n-1) * n;
  existence;
  uniqueness;
end;

which may not be syntactically correct  and which I am working on or something which compiles


definition
  func megcd -> Function of [:NAT, NAT:], NAT means
  :Def2:
  for m,n being Element of NAT holds
   it.[m,n] = IFEQ(m,0,n,it.[n mod m, m]);
  existence;
::>       *4
  uniqueness;
::>        *4
end;

Def1 and Def2 looks similar to their SequenceL counterpart which is given below:

seqL_fac(n) = 1 when n = 0 else seqL_fac(n-1) * n

I prefer Def1 and Def2 to the Defmfac given in the function definition at the top becuase they are closer
to the SequenceL definition of factorial function.  I could not find any
schemes so far in the MML to prove correctness of Def1 or Def2 so that I did the way in Defmfac...
I am searching for schemes because they make proofs much easier and semi-automate them.
 I appreciate any help or comment on this.

I tried to give you a sample of what I am trying and thanks for your patience again. Have a good semester all..

Adem Ozyavas
Graduate Student
Texas Tech University