:: Partial correctness of GCD algorithm
::  by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NOMIN_1, NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1,
      XXREAL_0, NAT_1, ARYTM_3, PARTFUN1, MARGREL1, XBOOLEAN, TARSKI, FUNCOP_1,
      ZFMISC_1, ARYTM_1, NOMIN_3, NOMIN_4, XCMPLX_0, INT_2, NOMIN_2, ORDERS_5,
      PARTPR_1, COMPLEX1, PARTPR_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, MARGREL1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1,
      BINOP_1, XXREAL_0, XCMPLX_0, FUNCT_3, INT_2, NOMIN_1, PARTPR_1, PARTPR_2,
      NOMIN_2, NOMIN_3;
 constructors RELSET_1, NOMIN_3, INT_2, NOMIN_2;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, RELSET_1, INT_1,
      NOMIN_3, NOMIN_1, MARGREL1, XCMPLX_0, NEWTON02, NUMBERS, NOMIN_2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve v for object;
reserve V,A for set;
reserve f for SCBinominativeFunction of V,A;

definition
  let A;
  attr A is complex-containing means
:: NOMIN_4:def 1
COMPLEX c= A;
end;

registration
  cluster complex-containing for set;
  cluster complex-containing -> non empty for set;
end;

scheme :: NOMIN_4:sch 1
BinPredToFunEx{ X, Y() -> set, P[object,object] }:
  ex f being Function of [:X(),Y():],BOOLEAN st
  for x,y being object st x in X() & y in Y() holds
    (P[x,y] implies f.(x,y) = TRUE) & (not P[x,y] implies f.(x,y) = FALSE);

scheme :: NOMIN_4:sch 2
BinPredToFunUnique{ X, Y() -> set, P[object,object] }:
  for f,g being Function of [:X(),Y():],BOOLEAN st
    (for x,y being object st x in X() & y in Y() holds
    (P[x,y] implies f.(x,y) = TRUE) & (not P[x,y] implies f.(x,y) = FALSE)) &
    (for x,y being object st x in X() & y in Y() holds
    (P[x,y] implies g.(x,y) = TRUE) & (not P[x,y] implies g.(x,y) = FALSE))
  holds f = g;

scheme :: NOMIN_4:sch 3
Lambda2Unique{X, Y, Z() -> set, F(object,object)->object}:
  for f,g being Function of [:X(),Y():],Z() st
    (for x,y being object st x in X() & y in Y() holds f.(x,y) = F(x,y)) &
    (for x,y being object st x in X() & y in Y() holds g.(x,y) = F(x,y))
  holds f = g;

definition
  let V,A;
  func nonatomicsND(V,A) -> set equals
:: NOMIN_4:def 2
  the set of all d where d is NonatomicND of V,A;
end;

theorem :: NOMIN_4:1
  for d being object st d in nonatomicsND(V,A) holds d is NonatomicND of V,A;

theorem :: NOMIN_4:2
  {} in nonatomicsND(V,A);

registration
  let V,A;
  cluster nonatomicsND(V,A) -> non empty functional;
end;

definition
  let V,A;
  pred A is_without_nonatomicND_wrt V means
:: NOMIN_4:def 3
  A misses nonatomicsND(V,A);
end;

theorem :: NOMIN_4:3
  A is_without_nonatomicND_wrt V implies
  for d being NonatomicND of V,A holds not d in A;

theorem :: NOMIN_4:4
  A is_without_nonatomicND_wrt V & v in V implies
  for d1 being NonatomicND of V,A
    for d2 being TypeSCNominativeData of V,A
  holds dom local_overlapping(V,A,d1,d2,v) = {v} \/ dom d1;

theorem :: NOMIN_4:5
  A is_without_nonatomicND_wrt V implies
  for d being NonatomicND of V,A holds
    v in V & d in dom f implies
  dom (SC_assignment(f,v).d) = dom d \/ {v};

reserve d for TypeSCNominativeData of V,A;
reserve d1 for NonatomicND of V,A;

theorem :: NOMIN_4:6
  for d1 being NonatomicND of V,A holds
   v in V & A is_without_nonatomicND_wrt V implies
  local_overlapping(V,A,d1,d,v) in dom denaming(V,A,v);

reserve a,b,c,z for Element of V;
reserve x,y for object;
reserve p,q,r,s for SCPartialNominativePredicate of V,A;

definition
  let V,A,d,a;
  pred a is_ext_real_on d means
:: NOMIN_4:def 4
  denaming(V,A,a).d is ext-real;
  pred a is_complex_on d means
:: NOMIN_4:def 5
  denaming(V,A,a).d is complex;
  pred a is_a_value_on d means
:: NOMIN_4:def 6
  denaming(V,A,a).d in A;
end;

theorem :: NOMIN_4:7
  A is complex-containing & (for d holds a is_complex_on d)
  implies for d holds a is_a_value_on d;

theorem :: NOMIN_4:8
  (for d holds a is_a_value_on d) implies rng denaming(V,A,a) c= A;

theorem :: NOMIN_4:9
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) implies
  rng <:denaming(V,A,a), denaming(V,A,b):> c= [:A,A:];

definition
  let V,A;
  let a,b be Element of V;
  let p be Function of [:A,A:],BOOLEAN;
  func lift_binary_pred(p,a,b) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_4:def 7
    p * <:denaming(V,A,a), denaming(V,A,b):>;
end;

definition
  let V,A;
  let a,b be Element of V;
  let op be Function of [:A,A:],A;
  func lift_binary_op(op,a,b) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 8
    op * <:denaming(V,A,a), denaming(V,A,b):>;
end;

definition
  let A;
  func Equality(A) -> Function of [:A,A:],BOOLEAN means
:: NOMIN_4:def 9
    for a,b being object st a in A & b in A holds
     (a = b implies it.(a,b) = TRUE) & (a <> b implies it.(a,b) = FALSE);
end;

definition
  let V,A;
  let x,y be Element of V;
  func Equality(A,x,y) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_4:def 10
    lift_binary_pred(Equality(A),x,y);
end;

definition
  let x,y be object;
  pred x less_pred y means
:: NOMIN_4:def 11
    ex x1,y1 being ExtReal st x1 = x & y1 = y & x1 < y1;
  irreflexivity;
  asymmetry;
end;

theorem :: NOMIN_4:10
  for x,y being ExtReal holds
   not x less_pred y implies y less_pred x or x = y;

definition
  let A;
  func less(A) -> Function of [:A,A:],BOOLEAN means
:: NOMIN_4:def 12
    for x,y being object st x in A & y in A holds
      (x less_pred y implies it.(x,y) = TRUE) &
      (not x less_pred y implies it.(x,y) = FALSE);
end;

definition
  let V,A;
  let x,y be Element of V;
  func less(A,x,y) -> SCPartialNominativePredicate of V,A equals
:: NOMIN_4:def 13
    lift_binary_pred(less(A),x,y);
end;

theorem :: NOMIN_4:11
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) implies
  dom Equality(A,a,b) = dom denaming(V,A,a) /\ dom denaming(V,A,b);

theorem :: NOMIN_4:12
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) implies
  dom less(A,a,b) = dom denaming(V,A,a) /\ dom denaming(V,A,b);

theorem :: NOMIN_4:13
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) &
  (for d holds a is_ext_real_on d) & (for d holds b is_ext_real_on d)
  implies
  PP_not(Equality(A,a,b)) = PP_or(less(A,a,b),less(A,b,a));

theorem :: NOMIN_4:14
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) &
  a is_ext_real_on d & b is_ext_real_on d &
  d in dom(PP_not Equality(A,a,b)) & (PP_not Equality(A,a,b)).d = TRUE implies
  d in dom less(A,a,b) & less(A,a,b).d = TRUE or
  d in dom less(A,b,a) & less(A,b,a).d = TRUE;

definition
  let x,y be object;
  assume
 x is Complex & y is Complex;
  func subtraction(x,y) -> Complex means
:: NOMIN_4:def 14
    ex x1,y1 being Complex st x1 = x & y1 = y & it = x1 - y1;
end;

definition
  let A;
  assume
 A is complex-containing;
  func subtraction(A) -> Function of [:A,A:],A means
:: NOMIN_4:def 15
    for x,y being object st x in A & y in A holds it.(x,y) = subtraction(x,y);
end;

definition
  let V,A;
  let x,y be Element of V;
  func subtraction(A,x,y) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 16
    lift_binary_op(subtraction(A),x,y);
end;

theorem :: NOMIN_4:15
  A is complex-containing & a in dom d1 & b in dom d1 &
  d1 in dom subtraction(A,a,b) implies
  for x,y being Complex st x = d1.a & y = d1.b holds
  subtraction(A,a,b).d1 = x - y;

:: Definition of a program over type SC nominative data which implements the GCD computation algorithm
:: Atomic data are assumed to be natural numbers
:: Basic operations and relations on atomic data include difference operation (subtraction) and comparisons (less, Equality)

:: Pseudo code of the algorithm

:: Input: nonnegative integers x and y
:: Output: nonnegative integer z = gcd(x,y)
:: a := x;
:: b := y;
:: while not (a=b) do
::  if b<a then a := a-b;
::  if a<b then b := b-a;
:: end;
:: z := a;

definition
  let V,A,a,b;
  func gcd_conditional_step(V,A,a,b) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 17
    PP_IF(less(A,b,a),
          SC_assignment(subtraction(A,a,b),a),
          PPid(ND(V,A)));
end;

definition
  let V,A,a,b;
  func gcd_loop_body(V,A,a,b) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 18
    PP_composition(
      gcd_conditional_step(V,A,a,b),
      gcd_conditional_step(V,A,b,a)
    );
end;

definition
   let V,A,a,b;
   func gcd_main_loop(V,A,a,b) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 19
     PP_while(PP_not(Equality(A,a,b)),
              gcd_loop_body(V,A,a,b));
end;

definition
  let V,A,a,b,x,y;
  func gcd_var_init(V,A,a,b,x,y) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 20
    PP_composition(
      SC_assignment(denaming(V,A,x), a),
      SC_assignment(denaming(V,A,y), b)
    );
end;

definition
  let V,A,a,b,x,y;
  func gcd_main_part(V,A,a,b,x,y) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 21
    PP_composition(
       gcd_var_init(V,A,a,b,x,y),
       gcd_main_loop(V,A,a,b)
    );
end;

definition
  let V,A,a,b,x,y,z;
  func gcd_program(V,A,a,b,x,y,z) -> SCBinominativeFunction of V,A equals
:: NOMIN_4:def 22
    PP_composition(
      gcd_main_part(V,A,a,b,x,y),
      SC_assignment(denaming(V,A,a),z)
    );
end;

reserve x0,y0 for Nat;

definition
  let V,A,x,y,x0,y0;
  let d be object;
  pred valid_gcd_input_pred V,A,x,y,x0,y0,d means
:: NOMIN_4:def 23
    ex d1 being NonatomicND of V,A st d = d1 & x in dom d1 & y in dom d1 &
     d1.x = x0 & d1.y = y0;
end;

definition
  let V,A,x,y,x0,y0;
  func valid_gcd_input(V,A,x,y,x0,y0) -> SCPartialNominativePredicate of V,A
  means
:: NOMIN_4:def 24
    dom it = ND(V,A) &
    for d being object st d in dom it holds
    (valid_gcd_input_pred V,A,x,y,x0,y0,d implies it.d = TRUE) &
    (not valid_gcd_input_pred V,A,x,y,x0,y0,d implies it.d = FALSE);
end;

registration
  let V,A,x,y,x0,y0;
  cluster valid_gcd_input(V,A,x,y,x0,y0) -> total;
end;

definition
  let V,A,z,x0,y0;
  let d be object;
  pred valid_gcd_output_pred V,A,z,x0,y0,d means
:: NOMIN_4:def 25
   ex d1 being NonatomicND of V,A st d = d1 & z in dom d1 & d1.z = x0 gcd y0;
end;

definition
  let V,A,z,x0,y0;
  func valid_gcd_output(V,A,z,x0,y0) -> SCPartialNominativePredicate of V,A
  means
:: NOMIN_4:def 26
    dom it = {d where d is TypeSCNominativeData of V,A:
        d in dom denaming(V,A,z)} &
    for d being object st d in dom it holds
    (valid_gcd_output_pred V,A,z,x0,y0,d implies it.d = TRUE) &
    (not valid_gcd_output_pred V,A,z,x0,y0,d implies it.d = FALSE);
end;

definition
  let V,A,a,b,x0,y0;
  let d be object;
  pred gcd_inv_pred V,A,a,b,x0,y0,d means
:: NOMIN_4:def 27
    ex d1 being NonatomicND of V,A st d = d1 & a in dom d1 & b in dom d1 &
     ex x,y being Nat st x = d1.a & y = d1.b & x gcd y = x0 gcd y0;
end;

definition
  let V,A,a,b,x0,y0;
  func gcd_inv(V,A,a,b,x0,y0) -> SCPartialNominativePredicate of V,A means
:: NOMIN_4:def 28

    dom it = ND(V,A) &
    for d being object st d in dom it holds
    (gcd_inv_pred V,A,a,b,x0,y0,d implies it.d = TRUE) &
    (not gcd_inv_pred V,A,a,b,x0,y0,d implies it.d = FALSE);
end;

registration
  let V,A,a,b,x0,y0;
  cluster gcd_inv(V,A,a,b,x0,y0) -> total;
end;

theorem :: NOMIN_4:16
  <*PP_inversion(SC_Psuperpos(p,denaming(V,A,x),a)),
    SC_assignment(denaming(V,A,x),a),
    p*>
  is SFHT of ND(V,A);

theorem :: NOMIN_4:17
  V is non empty & A is_without_nonatomicND_wrt V &
  a <> b & a <> y implies
  <* valid_gcd_input(V,A,x,y,x0,y0), gcd_var_init(V,A,a,b,x,y),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:18
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
  A is complex-containing &
  (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* PP_and(less(A,b,a),gcd_inv(V,A,a,b,x0,y0)),
     SC_assignment(subtraction(A,a,b),a),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:19
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
  A is complex-containing &
  (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* PP_and(less(A,a,b),gcd_inv(V,A,a,b,x0,y0)),
     SC_assignment(subtraction(A,b,a),b),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:20
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
  A is complex-containing &
  (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* gcd_inv(V,A,a,b,x0,y0),
     gcd_conditional_step(V,A,a,b),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:21
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
  A is complex-containing &
  (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* gcd_inv(V,A,a,b,x0,y0),
     gcd_conditional_step(V,A,b,a),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:22
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
  A is complex-containing &
  (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* gcd_inv(V,A,a,b,x0,y0),
     gcd_loop_body(V,A,a,b),
     gcd_inv(V,A,a,b,x0,y0) *> is SFHT of ND(V,A);

::$CT

theorem :: NOMIN_4:24
  V is non empty & A is_without_nonatomicND_wrt V & a <> b &
   A is complex-containing &
   (for d holds a is_complex_on d) & (for d holds b is_complex_on d) implies
  <*gcd_inv(V,A,a,b,x0,y0),
    gcd_main_loop(V,A,a,b),
    PP_and(Equality(A,a,b),gcd_inv(V,A,a,b,x0,y0))*> is SFHT of ND(V,A);

theorem :: NOMIN_4:25
  V is non empty & A is_without_nonatomicND_wrt V & a <> b & a <> y &
   A is complex-containing &
   (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <*valid_gcd_input(V,A,x,y,x0,y0), gcd_main_part(V,A,a,b,x,y),
    PP_and(Equality(A,a,b),gcd_inv(V,A,a,b,x0,y0)) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:26
  V is non empty & A is_without_nonatomicND_wrt V &
  (for d holds a is_a_value_on d) & (for d holds b is_a_value_on d) implies
  <* PP_and(Equality(A,a,b),gcd_inv(V,A,a,b,x0,y0)),
     SC_assignment(denaming(V,A,a),z),
     valid_gcd_output(V,A,z,x0,y0) *> is SFHT of ND(V,A);

theorem :: NOMIN_4:27
  A is complex-containing & (for d holds a is_complex_on d) &
  (for d holds b is_complex_on d) implies
  <* PP_inversion(PP_and(Equality(A,a,b),gcd_inv(V,A,a,b,x0,y0))),
     SC_assignment(denaming(V,A,a),z),
     valid_gcd_output(V,A,z,x0,y0) *> is SFHT of ND(V,A);

::$N Partial correctness of GCD algorithm
theorem :: NOMIN_4:28
  V is non empty & A is_without_nonatomicND_wrt V & a <> b & a <> y &
   A is complex-containing &
   (for d holds a is_complex_on d) & (for d holds b is_complex_on d)
  implies
  <* valid_gcd_input(V,A,x,y,x0,y0), gcd_program(V,A,a,b,x,y,z),
     valid_gcd_output(V,A,z,x0,y0) *> is SFHT of ND(V,A);