:: Quick Sort on SCMPDS :: by JingChao Chen :: :: Received June 14, 2000 :: Copyright (c) 2000-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 NUMBERS, SCMPDS_2, SUBSET_1, FSM_1, SCMPDS_4, AMI_1, TURING_1, SCMFSA8A, SCMFSA_7, AMI_3, INT_1, SCMFSA8B, CARD_1, ARYTM_3, FUNCT_1, XXREAL_0, UNIALG_2, SCMFSA7B, SCMFSA6B, RELAT_1, FUNCT_4, AMI_2, SCMFSA_9, ARYTM_1, VALUED_1, TARSKI, GRAPHSP, CIRCUIT2, MSUALG_1, NAT_1, FUNCOP_1, CARD_3, FINSEQ_1, GRAPH_2, SCPISORT, SCMP_GCD, CLASSES1, SCPQSORT, EXTPRO_1, SCMFSA6C, COMPOS_1, MEMSTR_0; notations TARSKI, XBOOLE_0, FUNCT_2, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, PBOOLE, VALUED_1, XCMPLX_0, RECDEF_1, INT_1, NAT_1, STRUCT_0, COMPOS_1, MEMSTR_0, EXTPRO_1, AMI_2, FUNCT_7, SCMPDS_2, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, CARD_3, FINSEQ_1, SCMPDS_8, GRAPH_2, CLASSES1, SCPISORT, FINSEQ_6; constructors REAL_1, RECDEF_1, NEWTON, MESFUNC1, SCM_1, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMP_GCD, SCMPDS_8, SCPISORT, CLASSES1, GRAPH_2, VALUED_1, AMI_2, SCMPDS_1, PRE_POLY, AMISTD_1, AMISTD_2, SCMPDS_7, PBOOLE, AMISTD_5, MEMSTR_0, FINSEQ_6; registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMPDS_2, SCMPDS_4, SCMPDS_5, SCMPDS_6, SCMPDS_8, ORDINAL1, VALUED_0, COMPOS_1, AFINSQ_1, MEMSTR_0, EXTPRO_1, FUNCT_4, FUNCT_7, PRE_POLY, AMI_3, COMPOS_0; requirements NUMERALS, REAL, SUBSET, ARITHM; begin :: The Several Properties of "while" Program and Finite Sequence reserve x for Int_position, n,p0 for Nat; registration let I,J be shiftable Program of SCMPDS, a be Int_position,k1 be Integer; cluster if>0(a,k1,I,J) -> shiftable; end; reserve P,Q,V for Instruction-Sequence of SCMPDS; theorem :: SCPQSORT:1 :: see SCMPDS_6:87 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, J being shiftable Program of SCMPDS,a,b be Int_position,k1 being Integer st s.DataLoc(s.a,k1) > 0 & I is_closed_on s,P & I is_halting_on s,P holds IExec(if>0(a,k1,I,J),P,s).b = IExec(I,P,s).b; theorem :: SCPQSORT:2 for s,sm be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be Int_position,i be Integer, m be Nat st I is_closed_on s,P & I is_halting_on s,P & s.DataLoc(s.a,i) > 0 & m=LifeSpan(P +* stop I,Initialize s)+2 & sm=Comput(P +* stop while>0(a,i,I),Initialize s,m) holds DataPart sm = DataPart IExec(I,P,Initialize s) & Initialize sm=sm; theorem :: SCPQSORT:3 for s be State of SCMPDS,I be Program of SCMPDS st for t be 0-started State of SCMPDS, Q st DataPart t = DataPart s holds I is_halting_on t,Q holds I is_closed_on s,P; theorem :: SCPQSORT:4 for i1,i2,i3,i4 be Instruction of SCMPDS holds card (i1 ';' i2 ';' i3 ';' i4) = 4; theorem :: SCPQSORT:5 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,x,y be Int_position, i,c be Integer st s.x >= c+s. DataLoc(s.a,i) & (for t be 0-started State of SCMPDS,Q st t.x >= c+t.DataLoc(s.a,i) & t.y=s .y & t.a=s.a & t.DataLoc(s.a,i) > 0 holds IExec(I,Q,t).a=t.a & I is_closed_on t,Q & I is_halting_on t,Q & IExec(I,Q,t).DataLoc(s.a,i) < t.DataLoc(s.a,i) & IExec(I,Q,t).x >= c+IExec(I,Q,t).DataLoc(s.a,i) & IExec(I,Q,t).y=t.y) holds while>0(a,i,I) is_closed_on s,P & while>0(a,i,I) is_halting_on s,P & (s.DataLoc(s.a,i) > 0 implies IExec(while>0(a,i,I),P,s) =IExec(while>0(a,i,I),P,Initialize IExec(I,P,s))); theorem :: SCPQSORT:6 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,x,y be Int_position, i,c be Integer st s.x >= c & ( for t be 0-started State of SCMPDS,Q st t.x >= c & t.y=s.y & t.a=s.a & t.DataLoc(s.a,i) > 0 holds IExec(I,Q,t).a=t.a & I is_closed_on t,Q & I is_halting_on t,Q & IExec(I,Q,t). DataLoc(s.a,i) < t.DataLoc(s.a,i) & IExec(I,Q,t).x >= c & IExec(I,Q,t).y=t.y) holds while>0(a,i,I) is_closed_on s,P & while>0(a,i,I) is_halting_on s,P & ( s.DataLoc(s.a,i) > 0 implies IExec(while>0(a,i,I),P,s) =IExec(while>0(a,i,I),P,Initialize IExec(I,P,s))); theorem :: SCPQSORT:7 for s being 0-started State of SCMPDS,I being halt-free shiftable Program of SCMPDS, a,x1,x2,x3,x4 be Int_position, i,c,md be Integer st s. x4=s.x3-c+s.x1 & md <= s.x3-c & (for t be 0-started State of SCMPDS,Q st t.x4=t.x3-c+t.x1 & md <= t.x3-c & t.x2=s.x2 & t.a=s.a & t.DataLoc(s.a,i) > 0 holds IExec(I,Q,t).a=t. a & I is_closed_on t,Q & I is_halting_on t,Q & IExec(I,Q,t).DataLoc(s.a,i) < t. DataLoc(s.a,i) & IExec(I,Q,t).x4= IExec(I,Q,t).x3-c+IExec(I,Q,t).x1 & md <= IExec(I,Q,t) .x3-c & IExec(I,Q,t).x2=t.x2) holds while>0(a,i,I) is_closed_on s,P & while>0(a,i,I) is_halting_on s,P & ( s.DataLoc(s.a,i) > 0 implies IExec(while>0(a,i,I),P,s) = IExec(while>0(a,i,I),P,Initialize IExec(I,P,s)) ); theorem :: SCPQSORT:8 for f being FinSequence of INT,m,k1,k,n be Nat st k1=k -1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k+1,n & (for i be Nat st m <= i & i < k holds f.i <= f.k) & (for i be Nat st k < i & i <= n holds f.k <= f.i) holds f is_non_decreasing_on m,n; begin :: Program Partition is to split a sequence into a "smaller" and :: a "larger" subsequence :: a5=a7=length a2=mid(x[1]), a3=x[2], a4=x[n], a6=save definition func Partition -> Program of SCMPDS equals :: SCPQSORT:def 1 ((GBP,5):=(GBP,4) ';' SubFrom(GBP ,5,GBP,2) ';' (GBP,3):=(GBP,2) ';' AddTo(GBP,3,1)) ';' while>0(GBP,5, while>0( GBP,5, (GBP,7):=(GBP,5) ';' AddTo(GBP,5,-1) ';' (GBP,6):=(intpos 4,0) ';' SubFrom(GBP,6,intpos 2,0) ';' if>0(GBP,6, AddTo(GBP,4,-1) ';' AddTo(GBP,7,-1), Load (GBP,5):=0 ) ) ';' while>0(GBP,7, (GBP,5):=(GBP,7) ';' AddTo(GBP,7,-1) ';' (GBP,6):=(intpos 2,0) ';' SubFrom(GBP,6,intpos 3,0) ';' if>0(GBP,6, AddTo(GBP,3 ,1) ';' AddTo(GBP,5,-1), Load (GBP,7):=0 ) ) ';' if>0(GBP,5,((GBP,6):=(intpos 4 ,0) ';' (intpos 4,0):=(intpos 3,0) ';' (intpos 3,0):=(GBP,6) ';' AddTo(GBP,5,-2 ) ';' AddTo(GBP,3,1)) ';' AddTo(GBP,4,-1) ) ) ';' (GBP,6):=(intpos 4,0) ';' ( intpos 4,0):=(intpos 2,0) ';' (intpos 2,0):=(GBP,6); end; begin :: The Construction of Quick Sort :: a0=global, a1=stack, a2=stack depth definition let n,p0 be Nat; func QuickSort(n,p0) -> Program of SCMPDS equals :: SCPQSORT:def 2 ((GBP:=0) ';' (SBP:=1) ';' (SBP,p0+n):=(p0+1) ';' (SBP,p0+n+1):=(p0+n)) ';' while>0(GBP,1, (GBP,2):=(SBP, p0+n+1) ';' SubFrom(GBP,2,SBP,p0+n) ';' if>0(GBP,2, (GBP,2):=(SBP,p0+n) ';' ( GBP,4):=(SBP,p0+n+1) ';' Partition ';' (((SBP,p0+n+3):=(SBP,p0+n+1) ';' (SBP,p0 +n+1):=(GBP,4) ';' (SBP,p0+n+2):=(GBP,4) ';' AddTo(SBP,p0+n+1,-1)) ';' AddTo( SBP,p0+n+2,1) ';' AddTo(GBP,1,2)), Load AddTo(GBP,1,-2) ) ); end; begin :: The Basic Property of Partition Program theorem :: SCPQSORT:9 card Partition=38; theorem :: SCPQSORT:10 for s be 0-started State of SCMPDS, md,p0 be Nat st s.GBP=0 & s. intpos 2=md & md >= p0+1 & p0 >= 7 holds Partition is_closed_on s,P & Partition is_halting_on s,P; theorem :: SCPQSORT:11 for s be 0-started State of SCMPDS, md,p0,n be Nat,f,f1 be FinSequence of INT st s.GBP=0 & s.intpos 4-s.intpos 2 > 0 & s.intpos 2=md & md >= p0+1 & s.intpos 4 <= p0+n & p0 >= 7 & f is_FinSequence_on s,p0 & len f=n & f1 is_FinSequence_on IExec(Partition,P,s),p0 & len f1=n holds IExec(Partition,P,s).GBP=0 & IExec(Partition,P,s).intpos 1=s.intpos 1 & f,f1 are_fiberwise_equipotent & ex m4 be Nat st m4=IExec(Partition,P,s).intpos 4 & md <= m4 & m4 <= s.intpos 4 & (for i be Nat st md<=i & i < m4 holds IExec(Partition,P,s).intpos m4 >= IExec(Partition,P,s).intpos i) & (for i be Nat st m4 < i & i <= s.intpos 4 holds IExec(Partition,P,s).intpos m4 <= IExec(Partition,P,s).intpos i) & for i be Nat st i >= p0+1 & (i < s.intpos 2 or i > s. intpos 4) holds IExec(Partition,P,s).intpos i = s.intpos i; theorem :: SCPQSORT:12 Partition is halt-free shiftable; begin :: The Basic Property of Quick Sort and Its Correctness theorem :: SCPQSORT:13 card QuickSort(n,p0)=57; theorem :: SCPQSORT:14 for p0,n being Nat st p0 >= 7 holds QuickSort(n,p0) is parahalting; theorem :: SCPQSORT:15 for s being 0-started State of SCMPDS,p0,n being Nat st p0 >= 7 ex f,g be FinSequence of INT st len f=n & f is_FinSequence_on s,p0 & len g = n & g is_FinSequence_on IExec(QuickSort(n,p0),P,s),p0 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n;