[mizar] I need help with Mizar functions...

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

Dear All,

I have been a mizar user for around two months. I started in April
and I had to take a break from Mizar this last summer. I would like
to tell about my overall goal before I ask my questions. I would ask
for your patience for this long email.

My research is to use Mizar to help programmers of a purely
functional language, called SequenceL, prove correctness of
properties of functions in it. I will give an example of theorem
that I want to prove shortly. Hopefully, this research is going to
be my thesis. I know I am just a consumer but I would like to
contribute to the Mizar group. I am also planning to teach classes
with mizar (discrete math and logic) after I graduate.


The Mizar version I am using is 7.8.10. Let me first state the proof
I have been working on. Please, keep in mind the following
explanation for the rest of the discussion and questions. Let m and
n be natural numbers. The egcd (Euclidean gcd) function in SequenceL
is

    egcd(m,n) = n when m = 0 else egcd(n%m, m)

where % is the modulus operator, mod, in Mizar.
What I want to prove about the egcd function is the following:
          egcd(m,n) = m hcf n            (1)
I sent an email around mid August about how to write egcd(m,n) in
accordance with my needs, that is, whether to write it is a function
or functor, and how to prove its correctness.
First I would like to give the outline of my proof and ask my
questions of how to translate them to Mizar. Some general questions
will follow these specific questions. First my proof of (1):

I used "complete induction" for the proof of (1). The induction is
on m and n is any arbitrary number. The proof is a mixture of mizar
syntax and informal math.

Base case:          egcd(0,n) = n............def of egcd
                                           .= 0 hcf n......theorem
                                                           ......from Mizar(0 hcf n = n)

Induction step:
                          induction hytpthesis:
                         for i st i < k holds egcd(i,n) = i hcf n

                         prove egcd(k,n) = k hcf n
                         so that
                         for m egcd(m,n) = m hcf n

I do not give the details of the proof. Here are my specific
questions about the proof:

Q1) I wrote different version of mizar version of egcd. The
following is one of them:

definition
  func mizar_egcd -> Function of [:NAT, NAT:], NAT means
  :Defmizar_egcd:
  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;
::>
::> 4: This inference is not accepted


mizar_egcd is written as a function. Is there a scheme in Mizar to
do the "existence" and "uniqueness" proof of megcd?

In case there is no scheme in Mizar for a proof of a function, say
mizar_egcd, does that mean that one has either of the two following
options:

  (i) write megcd in in a new structure that might look different
      from egcd in SequenceL so that one can find a scheme for its proof, or

  (ii) keep megcd as it is  and write your own scheme in Mizar and
       use it for megcd's proof of correctness?


Q2) In my research I need to translate functions from SequenceL to
Mizar and I am "not" insterested in values of these Mizar functions
or properties of them but more of using functions' definiens to
prove theorems with them. Therefore, functors (constructing terms
and manipulating them) is more appropriate but I believe recursive
functions should be written as functions. So does that mean that I
have no option but a function for the above egcd?


Q3) This is another major question that I have. How can we use the
scheme

scheme :: NAT_1:sch 4
 CompInd { P[Nat] } : for k being Nat holds P[k]
provided
 for k being Nat st for n being Nat st n < k holds P[n] holds P[k];

in the proof (1)? (This scheme seems to be designed to be used with
one variable (the induction variable) but in Theorem 1, there are
two variables where m is the induction variable and n is arbitrary.)

I truely appreciate your help and thank you...

Adem Ozyavas
Graduate Student
Computer Science Department
Texas Tech University