:: Partial correctness of an algorithm computing Lucas sequences
::  by Adrian Jaszczak
:: 
:: Received October 25, 2020
:: Copyright (c) 2020-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, ZFMISC_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1,
      FINSEQ_1, NAT_1, ARYTM_3, PARTFUN1, XBOOLEAN, TARSKI, NOMIN_3, NOMIN_4,
      XCMPLX_0, NOMIN_2, PARTPR_1, PARTPR_2, NOMIN_5, CARD_1, PRE_FF, NOMIN_7,
      XXREAL_0, ARYTM_1, INT_1, MCART_1, NOMIN_8, FIB_NUM3, ORDINAL4, NOMIN_9;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS,
      DOMAIN_1, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, CARD_1,
      FINSEQ_1, BINOP_1, XXREAL_0, XCMPLX_0, INT_1, NAT_1, FUNCT_3, AOFA_A00,
      PRE_FF, NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5,
      NOMIN_7, FIB_NUM3, NOMIN_8;
 constructors RELSET_1, NOMIN_2, NOMIN_3, NOMIN_4, NOMIN_5, NOMIN_6, NOMIN_7,
      PRE_FF, DOMAIN_1, FIB_NUM3, AOFA_A00, FINSEQ_4, NOMIN_8;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, INT_1, NOMIN_1, NUMBERS,
      NAT_1, XXREAL_0, XREAL_0, CARD_1, FINSEQ_1, FINSEQ_4, NEWTON04, NOMIN_4,
      NOMIN_7, AOFA_A00, SUBSET_1, PARTPR_2, XTUPLE_0, NOMIN_8;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Introduction about finite sequences

registration
  let n be Nat;
  let f be n-element FinSequence;
  reduce f | Seg n to f;
end;

registration
  let A,B be set;
  let f1,f2,f3,f4,f5,f6 be PartFunc of A,B;
  cluster <*f1,f2,f3,f4,f5,f6*> -> PFuncs(A,B)-valued;
end;

registration
  let V,A be set;
  let f1,f2,f3,f4,f5,f6 be SCBinominativeFunction of V,A;
  cluster <*f1,f2,f3,f4,f5,f6*> -> FPrg(ND(V,A))-valued;
end;

registration
  let a1,a2,a3,a4,a5,a6 be object;
  reduce <*a1,a2,a3,a4,a5,a6*>.1 to a1;
  reduce <*a1,a2,a3,a4,a5,a6*>.2 to a2;
  reduce <*a1,a2,a3,a4,a5,a6*>.3 to a3;
  reduce <*a1,a2,a3,a4,a5,a6*>.4 to a4;
  reduce <*a1,a2,a3,a4,a5,a6*>.5 to a5;
  reduce <*a1,a2,a3,a4,a5,a6*>.6 to a6;
end;

definition
  let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
  func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence equals
:: NOMIN_9:def 1
  <*a1,a2,a3,a4,a5,a6,a7,a8*>^<*a9*>;
end;

theorem :: NOMIN_9:1
  for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object
  for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> iff
  len f = 9 &
  f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7 &
  f.8 = a8 & f.9 = a9;

registration
  let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
  cluster <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> 9-element;
end;

registration
  let a1,a2,a3,a4,a5,a6,a7,a8,a9 be object;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.1 to a1;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.2 to a2;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.3 to a3;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.4 to a4;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.5 to a5;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.6 to a6;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.7 to a7;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.8 to a8;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>.9 to a9;
end;

theorem :: NOMIN_9:2
  for a1,a2,a3,a4,a5,a6,a7,a8,a9 being object holds
  rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = {a1,a2,a3,a4,a5,a6,a7,a8,a9};

definition
  let X be non empty set;
  let a1,a2,a3,a4,a5,a6,a7,a8,a9 be Element of X;
  redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> -> FinSequence of X;
end;

definition
  let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
  func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence equals
:: NOMIN_9:def 2
  <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>^<*a10*>;
end;

theorem :: NOMIN_9:3
  for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object
  for f being FinSequence holds f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> iff
  len f = 10 &
  f.1 = a1 & f.2 = a2 & f.3 = a3 & f.4 = a4 & f.5 = a5 & f.6 = a6 & f.7 = a7 &
  f.8 = a8 & f.9 = a9 & f.10 = a10;

registration
  let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
  cluster <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> 10-element;
end;

registration
  let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be object;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.1 to a1;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.2 to a2;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.3 to a3;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.4 to a4;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.5 to a5;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.6 to a6;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.7 to a7;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.8 to a8;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.9 to a9;
  reduce <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>.10 to a10;
end;

theorem :: NOMIN_9:4
  for a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 being object holds
  rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10};

definition
  let X be non empty set;
  let a1,a2,a3,a4,a5,a6,a7,a8,a9,a10 be Element of X;
  redefine func <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> -> FinSequence of X;
end;

begin :: Lucas Sequences

definition
  let i,j be Integer;
  redefine func [i,j] -> Element of [:INT,INT:];
end;

reserve x,y,P,Q for Integer;
reserve a,b,n for Nat;
reserve V,A for set;
reserve val for Function;
reserve loc for V-valued Function;
reserve d1 for NonatomicND of V,A;
reserve p for SCPartialNominativePredicate of V,A;
reserve d for object;
reserve z for Element of V;
reserve T for TypeSCNominativeData of V,A;
reserve size for non zero Nat;
reserve x0, y0, p0, q0 for Integer;
reserve n0 for Nat;

definition
  let x,y,P,Q;
  func Lucas_Sequence(x,y,P,Q) -> sequence of [:INT,INT:] means
:: NOMIN_9:def 3
  it.0 = [x,y] &
  for n being Nat holds it.(n+1) = [ (it.n)`2, P*(it.n)`2 - Q*(it.n)`1 ];
end;

definition
  let x,y,P,Q,n;
  func Lucas(x,y,P,Q,n) -> Element of INT equals
:: NOMIN_9:def 4
  (Lucas_Sequence(x,y,P,Q).n)`1;
end;

theorem :: NOMIN_9:5
  Lucas(x,y,P,Q,0) = x & Lucas(x,y,P,Q,1) = y &
  for n holds Lucas(x,y,P,Q,n+2) = P*Lucas(x,y,P,Q,n+1)-Q*Lucas(x,y,P,Q,n);

theorem :: NOMIN_9:6
  Lucas_Sequence(0,1,1,-1) = Fib;

theorem :: NOMIN_9:7
  Lucas(0,1,1,-1,n) = Fib(n);

theorem :: NOMIN_9:8
  Lucas_Sequence(a,b,1,-1) = GenFib(a,b);

theorem :: NOMIN_9:9
  Lucas(a,b,1,-1,n) = GenFib(a,b,n);

theorem :: NOMIN_9:10
  Lucas_Sequence(2,1,1,-1) = Lucas;

theorem :: NOMIN_9:11
  Lucas(2,1,1,-1,n) = Lucas(n);

begin :: Main algorithm

:: Pseudocode of Lucas(x,y,p,q,n)
::
:: i  := val.1  :: counter
:: j  := val.2  :: constant 1
:: n  := val.3  :: index of searched element
:: s  := val.4  :: result
:: b  := val.5
:: c  := val.6
:: p  := val.7  :: constant P
:: q  := val.8  :: constant Q
:: ps := val.9
:: qc := val.10
::
::   { s == Lucas(i) && b == Lucas(i+1) &&
::	   p == p0 && q == q0	}
:: while ( i <> n )
::  c  := s
::  s  := b
::  ps := p*s
::  qc := q*c
::  b  := ps - qc
::  i  := i + j
:: return s
::   { n == i && s == Lucas(i) && b == Lucas(i+1) &&
::	   p == p0 && q == q0    }
::
:: where
::   val.1 = 0,
::   val.2 = 1,
::   val.3 - the number n the Lucas of which we compute,
::   val.4 = x
::   val.5 = y
::   val.6 = x
::   val.7 = p
::   val.8 = q
::   val.9 = 0
::   val.10 = 0
:: are input data from the environment,
:: and loc/.1 = i, loc/.2 = j, loc/.3 = n, loc/.4 = s, loc/.5 = b, loc/.6 = c,
:: loc/.7 = p, loc/.8 = q, loc/.9 = ps, loc/.10 = qc

theorem :: NOMIN_9:12
  Seg 10 c= dom loc & loc is_valid_wrt d1 implies
  { loc/.1, loc/.2, loc/.3, loc/.4, loc/.5,
    loc/.6, loc/.7, loc/.8, loc/.9, loc/.10 } c= dom d1;

definition
  let V,A,loc;
  func Lucas_loop_body(A,loc) -> SCBinominativeFunction of V,A equals
:: NOMIN_9:def 5
    PP_composition(
      SC_assignment(denaming(V,A,loc/.4),loc/.6),
      SC_assignment(denaming(V,A,loc/.5),loc/.4),
      SC_assignment(multiplication(A,loc/.7,loc/.4),loc/.9),
      SC_assignment(multiplication(A,loc/.8,loc/.6),loc/.10),
      SC_assignment(subtraction(A,loc/.9,loc/.10),loc/.5),
      SC_assignment(addition(A,loc/.1,loc/.2),loc/.1)
    );
end;

definition
  let V,A,loc;
  func Lucas_main_loop(A,loc) -> SCBinominativeFunction of V,A equals
:: NOMIN_9:def 6
  PP_while(PP_not(Equality(A,loc/.1,loc/.3)),Lucas_loop_body(A,loc));
end;

definition
  let V,A,loc,val;
  func Lucas_main_part(A,loc,val)
       -> SCBinominativeFunction of V,A equals
:: NOMIN_9:def 7
    PP_composition(
       initial_assignments(A,loc,val,10),
       Lucas_main_loop(A,loc)
    );
end;

definition
  let V,A,loc,val,z;
  func Lucas_program(A,loc,val,z)
       -> SCBinominativeFunction of V,A equals
:: NOMIN_9:def 8
    PP_composition(
      Lucas_main_part(A,loc,val),
      SC_assignment(denaming(V,A,loc/.4),z)
    );
end;

definition
  let x0,y0,p0,q0,n0;
  func Lucas_input(x0,y0,p0,q0,n0) -> FinSequence equals
:: NOMIN_9:def 9
  <*0,1,n0,x0,y0,x0,p0,q0,0,0*>;
end;

registration
  let x0,y0,p0,q0,n0;
  cluster Lucas_input(x0,y0,p0,q0,n0) -> 10-element;
end;

definition
  let V,A,x0,y0,p0,q0,n0,d;
  let val be FinSequence;
  pred valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d means
:: NOMIN_9:def 10
  Lucas_input(x0,y0,p0,q0,n0) is_valid_input V,A,val,d;
end;

definition
  let V,A,x0,y0,p0,q0,n0;
  let val be FinSequence;
  func valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0)
       -> SCPartialNominativePredicate of V,A equals
:: NOMIN_9:def 11
  valid_input(V,A,val,Lucas_input(x0,y0,p0,q0,n0));
end;

registration
  let V,A,x0,y0,p0,q0,n0;
  let val be FinSequence;
  cluster valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0) -> total;
end;

definition
  let V,A,z,x0,y0,p0,q0,n0,d;
  pred valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d means
:: NOMIN_9:def 12
  <*Lucas(x0,y0,p0,q0,n0)*> is_valid_output V,A,<*z*>,d;
end;

definition
  let V,A,z,x0,y0,p0,q0,n0;
  func valid_Lucas_output(A,z,x0,y0,p0,q0,n0) ->
       SCPartialNominativePredicate of V,A equals
:: NOMIN_9:def 13
  valid_output(V,A,z,Lucas(x0,y0,p0,q0,n0));
end;

definition
  let V,A,loc,x0,y0,p0,q0,n0,d;
  pred Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d means
:: NOMIN_9:def 14
  ex d1 being NonatomicND of V,A st
   d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4, loc/.5,
   loc/.6, loc/.7, loc/.8, loc/.9, loc/.10 } c= dom d1 &
   d1.(loc/.2) = 1 & d1.(loc/.3) = n0 &
   d1.(loc/.7) = p0 & d1.(loc/.8) = q0 &
    ex I being Nat st I = d1.(loc/.1) &
     d1.(loc/.4) = Lucas(x0,y0,p0,q0,I) &
     d1.(loc/.5) = Lucas(x0,y0,p0,q0,I+1);
end;

definition
  let V,A,loc,x0,y0,p0,q0,n0;
  func Lucas_inv(A,loc,x0,y0,p0,q0,n0) -> SCPartialNominativePredicate of V,A
  means
:: NOMIN_9:def 15

  dom it = ND(V,A) &
  for d being object st d in dom it holds
   (Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies it.d = TRUE) &
   (not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies it.d = FALSE);
end;

registration
  let V,A,loc,x0,y0,p0,q0,n0;
  cluster Lucas_inv(A,loc,x0,y0,p0,q0,n0) -> total;
end;

theorem :: NOMIN_9:13
  for val being 10-element FinSequence holds
  V is non empty & A is_without_nonatomicND_wrt V &
  Seg 10 c= dom loc & loc|Seg 10 is one-to-one & loc,val are_different_wrt 10
  implies
  valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0) ||=
  SC_Psuperpos_Seq(loc,val,Lucas_inv(A,loc,x0,y0,p0,q0,n0)).
    len SC_Psuperpos_Seq(loc,val,Lucas_inv(A,loc,x0,y0,p0,q0,n0));

theorem :: NOMIN_9:14
  for val being 10-element FinSequence holds
  V is non empty & A is_without_nonatomicND_wrt V &
  Seg 10 c= dom loc & loc|Seg 10 is one-to-one & loc,val are_different_wrt 10
  implies
  <* valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0),
     initial_assignments(A,loc,val,10),
     Lucas_inv(A,loc,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A);

theorem :: NOMIN_9:15
  V is non empty & A is complex-containing & A is_without_nonatomicND_wrt V &
  d1 in dom Lucas_loop_body(A,loc) & loc is_valid_wrt d1 & Seg 10 c= dom loc &
  (for T holds loc/.1 is_a_value_on T & loc/.2 is_a_value_on T &
    loc/.4 is_a_value_on T & loc/.6 is_a_value_on T &
    loc/.7 is_a_value_on T & loc/.8 is_a_value_on T &
    loc/.9 is_a_value_on T & loc/.10 is_a_value_on T)
  implies
  prg_doms_of loc,d1,
   <*denaming(V,A,loc/.4),denaming(V,A,loc/.5),multiplication(A,loc/.7,loc/.4),
    multiplication(A,loc/.8,loc/.6),subtraction(A,loc/.9,loc/.10),
    addition(A,loc/.1,loc/.2)*>,
   <*6,4,9,10,5,1*>;

theorem :: NOMIN_9:16
  for V being non empty set
  for loc being V-valued 10-element FinSequence holds
   A is complex-containing & A is_without_nonatomicND_wrt V &
  (for T being TypeSCNominativeData of V,A
    holds loc/.1 is_a_value_on T & loc/.2 is_a_value_on T &
    loc/.4 is_a_value_on T & loc/.6 is_a_value_on T &
    loc/.7 is_a_value_on T & loc/.8 is_a_value_on T &
    loc/.9 is_a_value_on T & loc/.10 is_a_value_on T) &
    loc is one-to-one
  implies
  <* Lucas_inv(A,loc,x0,y0,p0,q0,n0),
     Lucas_loop_body(A,loc),
     Lucas_inv(A,loc,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A);

theorem :: NOMIN_9:17
  for V being non empty set
  for loc being V-valued 10-element FinSequence holds
  A is complex-containing & A is_without_nonatomicND_wrt V &
  (for T being TypeSCNominativeData of V,A
    holds loc/.1 is_a_value_on T & loc/.2 is_a_value_on T &
    loc/.4 is_a_value_on T & loc/.6 is_a_value_on T &
    loc/.7 is_a_value_on T & loc/.8 is_a_value_on T &
    loc/.9 is_a_value_on T & loc/.10 is_a_value_on T) &
  loc is one-to-one
  implies
  <* Lucas_inv(A,loc,x0,y0,p0,q0,n0),
     Lucas_main_loop(A,loc),
     PP_and(Equality(A,loc/.1,loc/.3),Lucas_inv(A,loc,x0,y0,p0,q0,n0)) *>
  is SFHT of ND(V,A);

theorem :: NOMIN_9:18
  for V being non empty set
  for loc being V-valued 10-element FinSequence holds
  for val being 10-element FinSequence holds
  A is complex-containing & A is_without_nonatomicND_wrt V &
   (for T being TypeSCNominativeData of V,A
     holds loc/.1 is_a_value_on T & loc/.2 is_a_value_on T &
    loc/.4 is_a_value_on T & loc/.6 is_a_value_on T &
    loc/.7 is_a_value_on T & loc/.8 is_a_value_on T &
    loc/.9 is_a_value_on T & loc/.10 is_a_value_on T) &
   loc is one-to-one & loc,val are_different_wrt 10
  implies
  <* valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0),
     Lucas_main_part(A,loc,val),
     PP_and(Equality(A,loc/.1,loc/.3),Lucas_inv(A,loc,x0,y0,p0,q0,n0)) *>
  is SFHT of ND(V,A);

theorem :: NOMIN_9:19
  V is non empty & A is_without_nonatomicND_wrt V &
  (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
  implies
  PP_and(Equality(A,loc/.1,loc/.3),Lucas_inv(A,loc,x0,y0,p0,q0,n0))
  ||=
  SC_Psuperpos(valid_Lucas_output(A,z,x0,y0,p0,q0,n0),denaming(V,A,loc/.4),z);

theorem :: NOMIN_9:20
  V is non empty & A is_without_nonatomicND_wrt V &
  (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
  implies
  <* PP_and(Equality(A,loc/.1,loc/.3),Lucas_inv(A,loc,x0,y0,p0,q0,n0)),
     SC_assignment(denaming(V,A,loc/.4),z),
     valid_Lucas_output(A,z,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A);

theorem :: NOMIN_9:21
  (for T holds loc/.1 is_a_value_on T & loc/.3 is_a_value_on T)
  implies
  <* PP_inversion(PP_and(Equality(A,loc/.1,loc/.3),
     Lucas_inv(A,loc,x0,y0,p0,q0,n0))),
     SC_assignment(denaming(V,A,loc/.4),z),
     valid_Lucas_output(A,z,x0,y0,p0,q0,n0) *> is SFHT of ND(V,A);

::$N Partial correctness of a Lucas algorithm
theorem :: NOMIN_9:22
  for V being non empty set
  for loc being V-valued 10-element FinSequence
  for val being 10-element FinSequence
  for z being Element of V holds
  A is complex-containing & A is_without_nonatomicND_wrt V &
   (for T being TypeSCNominativeData of V,A holds loc/.1 is_a_value_on T &
   loc/.2 is_a_value_on T & loc/.3 is_a_value_on T &
   loc/.4 is_a_value_on T & loc/.6 is_a_value_on T &
   loc/.7 is_a_value_on T & loc/.8 is_a_value_on T &
   loc/.9 is_a_value_on T & loc/.10 is_a_value_on T) &
   loc is one-to-one & loc,val are_different_wrt 10
  implies
  <* valid_Lucas_input(V,A,val,x0,y0,p0,q0,n0),
     Lucas_program(A,loc,val,z),
     valid_Lucas_output(A,z,x0,y0,p0,q0,n0) *>
  is SFHT of ND(V,A);