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
