Re: [mizar] Question about functions' correctness

[trybulec <trybulec@math.uwb.edu.pl>]

Dear Adem,

Ozyavas, Adem wrote:

First, some technical remarks.

> 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)])));
>
>
>  
It is a definition of a partial function, so it should be written as

func egcd -> PartFunc of [:NAT,NAT:],NAT means
 dom it = .... &
 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)])));

>       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, ?????);
>  
believe closer to what you want is a permissive definition.

      let m,n be Element of NAT such that
        m >= n & n > 0 ;
      func egcd(m,n) -> Element of NAT means
      ex b being BinOp of NAT st it = b.(m,n) &
      for m,n be Element of NAT st m >= n & n > 0
       holds b.(m,n) =if_then_else(saeq0(n),m, b.(n, m mod n));


BTW Why you assume m >= n, it seems that it works pretty well without it.

Have you looked to
let x,y,a,b be set;
func IFEQ(x,y,a,b) -> set equals
: FUNCOP_1:def 8
a if x = y otherwise b;

You may write IFEQ(n,0,m,b.(n,m mod n)) instead of
       if_then_else(saeq0(n),m, b.(n, m mod n));


I have not found a scheme that can be used to justify the correctness 
(existence; uniqueness does not need a scheme).
Give me a couple of days to think about it.

Regards,
Andrzej Trybulec