[mizar] Question about functions' correctness

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

Dear All,

I posted a question on August 19th about how to prove correctness (existence and uniqueness) of a binary recursive function. Professor Trybulec and Grabowski asked me to attach the mizar article for more specificity. I am pasting the article here and my comments and questions follow the article.

environ
 vocabularies MCART_1,   ::` operator
              FUNCT_1,   ::nothing imported from SEQ_1
              ARYTM_3,
              NAT_1,     ::mod
              PRE_FF,
              ARYTM,     ::required for numeral zero(0)
              MARGREL1,  ::for BOOLEAN,TRUE
              MY_MIZAR;  ::egcd, if_then_else

 notations SUBSET_1,
           NUMBERS,    ::required for zero
           NAT_1,
           NAT_D,      ::mod format
           MCART_1,    ::requried for [ and ] (cart.prod.)
           SEQ_1,      ::.operator(?)
           FUNCT_2,    ::Function of
           DOMAIN_1,   ::unknown functor format ]
           MARGREL1,   ::BOOLEAN, TRUE, FALSE
           XXREAL_0;   ::>=, <

 constructors NAT_1,
              NAT_D,
              SEQ_1,
              DOMAIN_1,
              MARGREL1,
              XXREAL_0;

 registrations SUBSET_1,
               ORDINAL1,
               XXREAL_0; ::>=, < (with Element of NAT)
                         ::cluster natural -> ext-real num.

 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems ORDINAL1,MCART_1;
 schemes NAT_1;

begin

 definition
 let D be set; let x be Element of BOOLEAN;
 let y,z be Element of D;
 func if_then_else(x,y,z) -> Element of D equals
 :Def2:y if (x = TRUE) otherwise z;
 correctness;
 end;

 definition
 let D be set; let x be Element of D;
 func saeq0(x) -> Element of BOOLEAN equals
 :Def3:TRUE if (x = 0) otherwise FALSE;
 correctness;
 end;

 definition
 let m,n be Element of NAT;
 func modmn(m,n) -> Element of NAT equals
 :Def4: m mod n;
 correctness;
 end;

 definition
 func egcd -> Function of [:NAT,NAT:],NAT means
  for m,n being Element of NAT holds
   (m >= n & n > 0) implies
     (it.([m,n])=if_then_else(saeq0(n),m,it.([n,modmn(m,n)])));
 existence;
::>      *4
 uniqueness;
::>       *4
 end;


My comments first:
1) Please ignore some of the directive items (they were required for some proofs I removed and left only those required my questions).
2) I am interested in translating quite some functions from a functional language to Mizar and prove properties of them. That is why
   I want to have a much better understanding of writing Mizar functions, functors and use them in my proofs. To this end, I constantly
   search the MML for functors and functions as examples, read Mizar tutorials and articles that I find on the Internet.
  I realized that I need much more insight and understanding.
3)egcd is a recursive Euclidean greatest common divisor function which is the more or less translation of
   egcd(m,n) = if (n = 0) then m else egcd(n,m mod n) with the assumption of m >= n > 0.
4) I got help from Professor Yatsuka Nakamura's paper called "Proving the Correctness of Functional Programs using Mizar" both in writing the
   if_then_else functor and getting ideas on how to write the rest.

QUESTIONS:
1) What scheme I can/should use from the MML to prove the existence and uniqueness of egcd? (I could not find one in the MML)
2) I tried to write egcd like the following with arguments but could not complete the parts with question marks.

       definition
       let m,n be Element of NAT;
       func egcd(m,n) -> Element of NAT means
       for m,n be Element of NAT holds (m >= n & n > 0) implies
           ?????=if_then_else(saeq0(n),m, ?????);
       existence;
       uniqueness;
       end;


I will stop with these questions and comments for now. I truly appreciate your help. Thank you and have a good semester...

Adem Ozyavas