:: Logical Correctness of Vector Calculation Programs
:: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2026 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, NAT_1, XBOOLE_0, AFINSQ_1, SUBSET_1, TARSKI, CARD_1,
FUNCT_1, RELAT_1, ORDINAL1, FINSEQ_1, XXREAL_0, ARYTM_3, ARYTM_1,
FUNCOP_1, ORDINAL4, REAL_1, INT_1, CARD_3, PARTFUN1, RVSUM_1, FINSEQ_2,
PRGCOR_2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
CARD_1, ORDINAL4, XREAL_0, REAL_1, VALUED_0, XCMPLX_0, NAT_1, PARTFUN1,
FINSEQ_1, FUNCOP_1, AFINSQ_1, INT_1, RVSUM_1, NAT_D, FINSEQ_2, XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, PARTFUN1, NAT_D, AFINSQ_1, BINOP_2,
INT_1, VALUED_1, RVSUM_1, RELSET_1, ORDINAL4, FUNCOP_1, FUNCT_7, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
FINSEQ_1, AFINSQ_1, VALUED_0, FINSEQ_2, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities ORDINAL1;
expansions TARSKI;
theorems FUNCT_1, NAT_1, RELAT_1, ORDINAL1, FINSEQ_1, FUNCOP_1, AFINSQ_1,
RVSUM_1, FINSEQ_4, FINSEQ_2, XREAL_1, XXREAL_0, PARTFUN1, VALUED_1,
XREAL_0, FINSEQ_5, CARD_1, NUMBERS, TARSKI;
schemes NAT_1, AFINSQ_1;
begin
reserve k,i for Nat;
reserve D for non empty set;
definition let D;
let p be XFinSequence of D, q be FinSequence of D;
pred p is_an_xrep_of q means
NAT c= D & (p.0)=len q & len q < len p &
for i st 1<=i & i<=len q holds p.i=q.i;
end;
theorem
for p being XFinSequence of D st NAT c= D &
(p.0) is Nat & (p.0) in dom p holds p is_an_xrep_of (XFS2FS*(p))
proof
let p be XFinSequence of D;
assume that
A1: NAT c= D and
A2: (p.0) is Nat and
A3: (p.0) in dom p;
reconsider m0=(p.0) as Nat by A2;
A4: m0<len p by A3,AFINSQ_1:86;
(p.0) in len p by A3;
then len (XFS2FS*(p)) =m0 & for i st 1<=i & i<= m0 holds (XFS2FS*(p)).i=p.i
by AFINSQ_1:def 11;
hence thesis by A1,A4;
end;
definition
let x be object, y be set, a,b,c be object;
func IFLGT(x,y,a,b,c) -> object equals :Def2:
a if x in y, b if x = y otherwise c;
correctness
proof
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence thesis;
end;
end;
theorem Th2:
for q being FinSequence of D, n being Nat st NAT c= D & n>len q
ex p being XFinSequence of D st len p=n & p is_an_xrep_of q
proof
let q be FinSequence of D, n be Nat;
assume that
A1: NAT c= D and
A2: n>len q;
reconsider n as Element of NAT by ORDINAL1:def 12;
consider d2 being set such that
A3: d2 in D and
A4: d2=len q by A1;
reconsider d=d2 as Element of D by A3;
deffunc F(object)= IFEQ($1,0,d,IFLGT($1,len q,q.$1,q.$1,d));
ex p being XFinSequence st len p = n & for k be Nat st k
in n holds p.k=F(k) from AFINSQ_1:sch 2;
then consider p being XFinSequence such that
A5: len p = n and
A6: for k be Nat st k in n holds p.k=F(k);
rng p c= D
proof
let y be object;
assume y in rng p;
then consider x being object such that
A7: x in dom p and
A8: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Ordinal by A7;
reconsider kx=nx as Element of NAT by A7;
A9: p.kx=F(kx) by A5,A6,A7;
now
per cases;
case
x=0;
then F(x)=d by FUNCOP_1:def 8;
hence p.x in D by A9;
end;
case
A10: x<>0;
then
A11: F(x)=IFLGT(x,len q,q.x,q.x,d) by FUNCOP_1:def 8;
now
per cases;
case
A12: x in Segm len q;
then
A13: kx<len q by NAT_1:44;
0+1<=kx by A10,NAT_1:13;
then kx in Seg len q by A13,FINSEQ_1:1;
then x in dom q by FINSEQ_1:def 3; then
A14: q.x in rng q by FUNCT_1:def 3;
A15: rng q c= D by FINSEQ_1:def 4;
F(x)=q.x by A11,A12,Def2;
hence p.x in D by A9,A14,A15;
end;
case
A16: x=len q;
0+1<=kx by A10,NAT_1:13;
then kx in Seg len q by A16,FINSEQ_1:1;
then x in dom q by FINSEQ_1:def 3;
then
A17: q.x in rng q by FUNCT_1:def 3;
A18: rng q c= D by FINSEQ_1:def 4;
F(x)=q.x by A11,A16,Def2;
hence p.x in D by A9,A17,A18;
end;
case
not (x in len q or x=len q);
then F(x)=d by A11,Def2;
hence p.x in D by A9;
end;
end;
hence p.x in D;
end;
end;
hence thesis by A8;
end;
then reconsider p as XFinSequence of D by RELAT_1:def 19;
reconsider p2=Replace(p,0,d) as XFinSequence of D;
A19: for i st 1<=i & i<=len q holds p2.i=q.i
proof
let i;
assume that
A20: 1<=i and
A21: i<=len q;
i<len q or i=len q by A21,XXREAL_0:1;
then
A22: i in Segm len q or i=len q by NAT_1:44;
i<n by A2,A21,XXREAL_0:2;
then
A23: i in Segm n by NAT_1:44;
i in NAT by ORDINAL1:def 12;
hence p2.i=p.i by A20,AFINSQ_1:44
.=F(i) by A6,A23
.=IFLGT(i,len q,q.i,q.i,d) by A20,FUNCOP_1:def 8
.=q.i by A22,Def2;
end;
A24: len p2=len p by AFINSQ_1:44;
p2.0 =len q by A2,A4,A5,AFINSQ_1:44;
then p2 is_an_xrep_of q by A1,A2,A5,A24,A19;
hence thesis by A5,A24;
end;
:: Non-overwriting program calculating inner product of vectors
::#define V_SIZE 1024
:: float inner_prd_prg(float a[V_SIZE],float b[V_SIZE]){
:: int n,i; float s[V_SIZE];
:: s[0]=0;
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=0;i<n;i++)s[i+1]=s[i]+a[i+1]*b[i+1];
:: }
:: return s[n];
:: }
definition
let a,b be XFinSequence of REAL;
assume that
A1: b.0 is Nat and
A2: b.0 < len a;
func inner_prd_prg(a,b) -> Real means
:Def3:
ex s being XFinSequence of REAL
, n being Integer st len s=len a & s.0=0 & n= b.0 & (n<>0 implies for i being
Nat st i<n holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & it=s.n;
existence
proof
reconsider q0=<%In(0,REAL)%> as XFinSequence of REAL;
set n2=len a;
reconsider nn2=b.0 as Nat by A1;
reconsider nn=nn2 as Integer;
defpred P[Nat] means ex q being XFinSequence of REAL st (len q=
$1+1 & q.0=0 & (for k st k<$1 & k<nn2 holds q.(k+1)=q.k+(a.(k+1))*(b.(k+1))));
A3: for k st k< 0 & k<nn2 holds q0.(k+1)=q0.k+(a.(k+1))*(b.(k+1));
A4: for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
reconsider k0=k as Nat;
assume P[k];
then consider q2 being XFinSequence of REAL such that
A5: len q2= k+1 and
A6: q2.0=0 and
A7: for k2 being Nat st k2<k & k2<nn2 holds q2.(k2+1) =q2.k2+(a.(k2
+1)) *(b.(k2+1));
reconsider qab=q2.k0+(a.(k0+1))*(b.(k0+1)) as Element of REAL
by XREAL_0:def 1;
set q3=q2^<% qab %>;
0 in len q2 by A5,AFINSQ_1:86;
then
A8: q3.0 =0 by A6,AFINSQ_1:def 3;
A9: for k2 being Nat st k2<k+1 & k2<nn2 holds q3.(k2+1) =q3.k2+(a.(k2+1
))*(b.(k2+1))
proof
let k2 be Nat;
assume that
A10: k2<k+1 and
A11: k2<nn2;
A12: k2<=k by A10,NAT_1:13;
now
per cases by A12,XXREAL_0:1;
case
A13: k2<k;
then k2< len q2 by A5,NAT_1:13;
then k2 in dom q2 by AFINSQ_1:86;
then
A14: q3.(k2)=q2.(k2) by AFINSQ_1:def 3;
k2+1<k+1 by A13,XREAL_1:6;
then k2+1 in len q2 by A5,AFINSQ_1:86;
then q3.(k2+1)=q2.(k2+1) by AFINSQ_1:def 3;
hence thesis by A7,A11,A13,A14;
end;
case
A15: k2=k;
0 in Segm 1 by NAT_1:44;
then
(<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>).0 = q2.k0+(a.(k0+1))*(b.(
k0+1)) & 0 in dom (<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>) by AFINSQ_1:def 4;
then
A16: q3.(k2+1+0) =q2.(k0)+(a.(k0+1))*(b.(k0+1)) by A5,A15,AFINSQ_1:def 3
;
k2<k2+1 by NAT_1:13;
then k2 in dom q2 by A5,A15,AFINSQ_1:86;
hence thesis by A15,A16,AFINSQ_1:def 3;
end;
end;
hence thesis;
end;
len q3=len q2+len (<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>) by AFINSQ_1:17
.=k+1+1 by A5,AFINSQ_1:33;
hence thesis by A8,A9;
end;
len q0=1 & q0.0=In(0,REAL) by AFINSQ_1:def 4;
then
A17: P[0] by A3;
for k being Nat holds P[k] from NAT_1:sch 2(A17,A4);
then consider q being XFinSequence of REAL such that
A18: len q=n2-'1+1 & q.0=0 and
A19: for k3 being Nat st k3<n2-'1 & k3<nn2 holds q.(k3+1)=q.k3+(a.(k3+
1 ))*(b.(k3+1));
reconsider ss2=q.nn2 as Real;
n2>=0+1 by A1,A2,NAT_1:13;
then n2-1>=0 by XREAL_1:48;
then
A20: n2-'1=n2-1 by XREAL_0:def 2;
nn<>0 implies for i being Nat st i<nn holds q.(i+1)=q.i + (a.(i+1))*(
b.(i+1))
proof
assume nn<>0;
thus for i being Nat st i<nn holds q.(i+1)=q.i + (a.(i+1))*(b.(i+1))
proof
let i be Nat;
assume
A21: i<nn;
nn+1<=n2 by A2,NAT_1:13;
then nn+1-1<=n2-1 by XREAL_1:9;
then i<n2-'1 by A20,A21,XXREAL_0:2;
hence thesis by A19,A21;
end;
end;
then
ex s being XFinSequence of REAL, n being Integer st len s=len a & s.0
=0 & n=b.0 & (n<>0 implies for i being Nat st i<n holds s.(i+1)=s.i + (a.(i+1))
*(b.(i+1)) ) & ss2=s.n by A18,A20;
hence thesis;
end;
uniqueness
proof
thus for w1,w2 being Real
st (ex s being XFinSequence of REAL, n1 being
Integer st len s=len a & s.0=0 & n1=b.0 & (n1<>0 implies for i being Nat st i<
n1 holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & w1=s.n1) & ( ex s being
XFinSequence of REAL, n2 being Integer st len s=len a & s.0=0 & n2=b.0 & (n2<>0
implies for i being Nat st i<n2 holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & w2=
s.n2) holds w1=w2
proof
let w1,w2 be Real ;
assume that
A22: ex s being XFinSequence of REAL, n1 being Integer st len s=len
a & s.0 =0 & n1=b.0 & (n1<>0 implies for i being Nat st i<n1 holds s.(i+1)=s.i
+ (a.(i+ 1))*(b.(i+1)) ) & w1=s.n1 and
A23: ex s being XFinSequence of REAL, n2 being Integer st len s=len
a & s.0=0 & n2=b.0 & (n2<>0 implies for i being Nat st i<n2 holds s.(i+1)=s.i +
( a.(i+1))*(b.(i+1))) & w2=s.n2;
consider s1 being XFinSequence of REAL, n1 being Integer such that
len s1=len a and
A24: s1.0=0 and
A25: n1=b.0 and
A26: n1<>0 implies for i being Nat st i<n1 holds s1.(i+1)=s1.i + (a.
(i+ 1))*(b.(i+1)) and
A27: w1=s1.n1 by A22;
consider s2 being XFinSequence of REAL, n2 being Integer such that
len s2 =len a and
A28: s2.0=0 and
A29: n2=b.0 and
A30: n2<>0 implies for i being Nat st i<n2 holds s2.(i+1)=s2.i + (a.
(i+ 1))*(b.(i+1)) and
A31: w2=s2.n2 by A23;
reconsider n=n1 as Nat by A1,A25;
defpred P2[Nat] means $1<=n implies s1.$1=s2.$1;
A32: for k being Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume
A33: P2[k];
now
assume k+1<=n; then
A34: k<n by NAT_1:13;
then s1.(k+1)=s1.k + (a.(k+1))*(b.(k+1)) by A26;
hence s1.(k+1)=s2.(k+1) by A25,A29,A30,A33,A34;
end;
hence thesis;
end;
A35: P2[0] by A24,A28;
for k being Nat holds P2[k] from NAT_1:sch 2(A35,A32);
hence thesis by A25,A27,A29,A31;
end;
end;
end;
theorem Th3:
for a being FinSequence of REAL, s being XFinSequence of REAL st
s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) holds Sum a =s.(len a)
proof
let a be FinSequence of REAL, s be XFinSequence of REAL;
assume that
A1: s.0=0 and
A2: for i st i<len a holds s.(i+1)=s.i+a.(i+1);
defpred P[Nat] means $1<=len a implies Sum (a|$1)=s.($1);
A3: for k st P[k] holds P[k+1]
proof
let k;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
reconsider m=k1+1 as Nat;
assume
A4: P[k];
k+1<=len a implies Sum (a|m)=s.(k+1)
proof
reconsider x0=<*a/.m*> as FinSequence of REAL;
reconsider rx=a/.m as Element of REAL;
reconsider q0=a|k as FinSequence of REAL;
assume
A5: k+1<=len a;
then
A6: a|m = (a|k)^<*a/.m*> by FINSEQ_5:82;
A7: 1<=k+1 by NAT_1:11;
then m in Seg len a by A5,FINSEQ_1:1;
then
A8: m in dom a by FINSEQ_1:def 3;
m in Seg m by A7,FINSEQ_1:1;
then m in Seg (len (a|m)) by A5,FINSEQ_1:59;
then
A9: m in dom (a|m) by FINSEQ_1:def 3;
Sum x0=rx by RVSUM_1:73;
then
A10: Sum (a|m) =s.(k)+rx by A4,A5,A6,NAT_1:13,RVSUM_1:75;
A11: len (a|m)=m by A5,FINSEQ_1:59;
A12: k<len a by A5,NAT_1:13;
len (a|m) =len q0 + len (<*rx*>) by A6,FINSEQ_1:22
.=len q0 +1 by FINSEQ_1:40;
then rx=(a|m).m by A6,A11,FINSEQ_1:42
.=(a|m)/.m by A9,PARTFUN1:def 6
.=a/.m by A9,FINSEQ_4:70
.=a.m by A8,PARTFUN1:def 6;
hence thesis by A2,A12,A10;
end;
hence thesis;
end;
A13: P[0] by A1,RVSUM_1:72;
for k holds P[k] from NAT_1:sch 2(A13,A3);
then P[len a];
hence thesis by FINSEQ_1:58;
end;
theorem
for a being FinSequence of REAL holds ex s being XFinSequence of REAL
st len s=len a +1 & s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) & Sum
a =s.(len a)
proof
let a be FinSequence of REAL;
deffunc F(Nat) = Sum (a|$1);
ex p being XFinSequence st len p = len a +1 & for k be Nat
st k in len a+1 holds p.k=F(k) from AFINSQ_1:sch 2;
then consider p being XFinSequence such that
A1: len p = len a +1 and
A2: for k be Nat st k in len a+1 holds p.k=F(k);
rng p c= REAL
proof
let y be object;
assume y in rng p;
then consider x being object such that
A3: x in dom p and
A4: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A3;
p.nx =Sum(a|nx) by A1,A2,A3;
hence thesis by A4, XREAL_0:def 1;
end;
then reconsider p as XFinSequence of REAL by RELAT_1:def 19;
A5: for i st i<len a holds p.(i+1)=p.i+a.(i+1)
proof
let i;
assume
A6: i<len a;
reconsider i as Element of NAT by ORDINAL1:def 12;
reconsider ii=i+1 as Nat;
A7: i+1<=len a by A6,NAT_1:13;
1<=1+i by NAT_1:11;
then i+1 in Seg len a by A7,FINSEQ_1:1;
then
A8: i+1 in dom a by FINSEQ_1:def 3;
i<len a+1 by A6,NAT_1:13;
then i in Segm(len a+1) by NAT_1:44;
then
A9: p.i=Sum (a|i) by A2;
i+1<len a+1 by A6,XREAL_1:6;
then
A10: i+1 in Segm(len a +1) by NAT_1:44;
a|ii=(a|i)^<*a/.ii*> by A7,FINSEQ_5:82;
then Sum(a|ii)=Sum(a|i)+Sum(<*a/.ii*>) by RVSUM_1:75
.=p.i +a/.ii by A9,RVSUM_1:73
.=p.i +a.ii by A8,PARTFUN1:def 6;
hence thesis by A2,A10;
end;
0 in Segm(len a +1) by NAT_1:44;
then
A11: p.0=F(0) by A2
.=0 by RVSUM_1:72;
then Sum a=p.(len a) by A5,Th3;
hence thesis by A1,A11,A5;
end;
theorem
for a,b being FinSequence of REAL, n being Nat st len a=len b & n>len
a holds |(a,b)| = inner_prd_prg(FS2XFS*(a,n),FS2XFS*(b,n))
proof
let a,b be FinSequence of REAL, n2 be Nat;
assume that
A1: len a=len b and
A2: n2>len a;
reconsider rb=b as Element of (len a)-tuples_on REAL by A1,FINSEQ_2:92;
reconsider ra=a as Element of (len a)-tuples_on REAL by FINSEQ_2:92;
set ri= inner_prd_prg(FS2XFS*(a,n2),FS2XFS*(b,n2));
set pa= FS2XFS*(a,n2);
set pb= FS2XFS*(b,n2);
A3: len b = (pb.0) by A1,A2,AFINSQ_1:def 10,NUMBERS:19;
len pa=n2 by A2,AFINSQ_1:def 10,NUMBERS:19;
then consider s being XFinSequence of REAL, n being Integer such that
len s=len pa and
A4: s.0=0 and
A5: n=pb.0 and
A6: n<>0 implies for i being Nat st i<n holds s.(i+1)=s.i + (pa.(i+1))*
(pb.(i+1)) and
A7: ri=s.n by A1,A2,A3,Def3;
A8: len mlt(ra,rb)=len a by CARD_1:def 7;
for i st i<len mlt(a,b) holds s.(i+1)=s.i+(mlt(a,b)).(i+1)
proof
let i;
assume
A9: i<len mlt(a,b);
then
1<=i+1 & i+1<=len a by A8,NAT_1:11,13;
then A10: pa.(i+1)=a.(i+1) & pb.(i+1)=b.(i+1)
by A1,A2,AFINSQ_1:def 10,NUMBERS:19;
A11: i<n by A1,A2,A5,A8,A9,AFINSQ_1:def 10,NUMBERS:19;
now
per cases;
case n<>0;
s.(i+1)=s.i + (pa.(i+1))*(pb.(i+1)) by A6,A11
.=s.i+(mlt(a,b)).(i+1) by A10,RVSUM_1:59;
hence thesis;
end;
case n=0;
hence contradiction by A1,A2,A5,A8,A9,AFINSQ_1:def 10,NUMBERS:19;
end;
end;
hence thesis;
end;
then Sum mlt(a,b) =s.n by A1,A3,A4,A5,A8,Th3;
hence thesis by A7,RVSUM_1:def 16;
end;
:: Vector Calculation Program: Scalar Product of Vector
::
:: The following C program is correct if it is used under some limited
::conditions, which are shown in the theorem following the definition
::after this program.
:: But it still remains a possibility of overflow.
:: The following program does not take an explicit function form.
::It means the value of the function does not have a sense.
::The result of the calculation is
::given in a variable c. Precisely speaking, the result is not unique,
::because of the difference of initial value of c.
:: For a model of such a program, we propose the logical predicate form
::(we call such a model, Logical-Model of a program) in the following
::definition.
::
::#define V_SIZE 1024
::void scalar_prd_prg(float c[V_SIZE], float a, float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a*b[i];
:: }
:: return;
::}
::The following definition is Logical-Model of the above program.
definition
let b,c be XFinSequence of REAL,a be Real,m be Integer;
pred m scalar_prd_prg c,a,b means
len c =m & len b =m & ex n being
Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n holds
c.i=a*(b.i));
end;
theorem
for b being non empty XFinSequence of REAL, a being Real,m being Nat
st b.0 is Nat & len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m
scalar_prd_prg c,a,b)& for c being non empty XFinSequence of REAL st m
scalar_prd_prg c,a,b holds (XFS2FS*(c))=a*(XFS2FS*(b))
proof
let b be non empty XFinSequence of REAL,a be Real,m be Nat;
assume that
A1: b.0 is Nat and
A2: len b=m and
A3: b.0 < m;
reconsider k= b.0 as Nat by A1;
reconsider c2= a*(XFS2FS*(b)) as FinSequence of REAL;
dom(a*(XFS2FS*(b))) = dom (XFS2FS*(b)) by VALUED_1:def 5;
then
A4: Seg len (a*(XFS2FS*(b)))= dom (XFS2FS*(b)) by FINSEQ_1:def 3;
A5: b.0 in Segm m by A1,A3,NAT_1:44;
then len (XFS2FS*(b)) = b.0 by A2,AFINSQ_1:def 11;
then
A6: len c2 =k by A4,FINSEQ_1:def 3;
then consider p being XFinSequence of REAL such that
A7: len p=m and
A8: p is_an_xrep_of c2 by A3,Th2,NUMBERS:19;
reconsider b0 = b.0 as Element of REAL by XREAL_0:def 1;
reconsider p2 = Replace(p,0,b0) as XFinSequence of REAL;
A9: now
assume k<>0;
thus for i being Nat st 1<=i & i<=k holds p2.i=a*(b.i)
proof
let i be Nat;
assume that
A10: 1<=i and
A11: i<=k;
(XFS2FS*(b)).i= b.i by A2,A5,A10,A11,AFINSQ_1:def 11;
then
A12: (a*(XFS2FS*(b))).i = a*(b.i) by RVSUM_1:44;
i in NAT & p.i=c2.i by A6,A8,A10,A11,ORDINAL1:def 12;
hence thesis by A10,A12,AFINSQ_1:44;
end;
end;
len p=len p2 & p2.0=b.0 by A1,A3,A7,AFINSQ_1:44;
then m scalar_prd_prg p2,a,b by A2,A7,A9;
hence ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b;
A13: 0 < len b;
thus for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b
holds (XFS2FS*(c))=a*(XFS2FS*(b))
proof
let c be non empty XFinSequence of REAL;
assume
A14: m scalar_prd_prg c,a,b;
then consider n being Integer such that
A15: c.0=b.0 and
A16: n=b.0 and
A17: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=a*(b.i);
A18: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
i being Nat st 1<=i & i<=n holds c.i=a*(b.i)) by A14;
then
A19: len (XFS2FS*(c)) = c.0 by A5,AFINSQ_1:def 11;
now
per cases;
case
n=0;
then
(XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A13,A18,A16,AFINSQ_1:64;
hence thesis by RVSUM_1:46;
end;
case
n<>0;
set p3=(XFS2FS*(c));
for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
proof
let k3 be Nat;
assume that
A20: 1 <=k3 and
A21: k3 <= len p3;
A22: (c.0) in len c by A1,A3,A18,AFINSQ_1:86;
then
A23: k3 <= n by A15,A16,A21,AFINSQ_1:def 11,A1;
then
A24: b.k3 = (XFS2FS*(b)).k3 by A2,A5,A16,A20,AFINSQ_1:def 11;
len p3=n by A15,A16,A22,AFINSQ_1:def 11,A1;
then p3.k3=c.k3 by A15,A16,A20,A21,A22,AFINSQ_1:def 11
.=a*(b.k3) by A17,A20,A23;
hence thesis by A24,RVSUM_1:44;
end;
hence thesis by A6,A15,A19,FINSEQ_1:14;
end;
end;
hence thesis;
end;
end;
:: Vector Calculation Program: Minus Vector
::#define V_SIZE 1024
::void vector_minus_prg(float c[V_SIZE], float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]= -b[i];
:: }
:: return;
::}
::The following definition is Logical-Model of the above program.
definition
let b,c be XFinSequence of REAL,m be Integer;
pred m vector_minus_prg c,b means
len c =m & len b =m & ex n being
Integer st c.0=b.0 & n= b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n
holds c.i= -(b.i));
end;
theorem
for b being non empty XFinSequence of REAL,m being Nat st b.0 is Nat &
len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m vector_minus_prg
c,b)& for c being non empty XFinSequence of REAL st m vector_minus_prg c,b
holds (XFS2FS*(c))= -(XFS2FS*(b))
proof
let b be non empty XFinSequence of REAL,m be Nat;
assume that
A1: b.0 is Nat and
A2: len b=m and
A3: b.0 < m;
reconsider k= b.0 as Nat by A1;
reconsider c2= -(XFS2FS*(b)) as FinSequence of REAL;
dom( -(XFS2FS*(b))) = dom (XFS2FS*(b)) by VALUED_1:8;
then
A4: Seg len ( -(XFS2FS*(b)))= dom (XFS2FS*(b)) by FINSEQ_1:def 3;
A5: b.0 in Segm m by A1,A3,NAT_1:44;
then len (XFS2FS*(b)) = b.0 by A2,AFINSQ_1:def 11;
then
A6: len c2 =k by A4,FINSEQ_1:def 3;
then consider p being XFinSequence of REAL such that
A7: len p=m and
A8: p is_an_xrep_of c2 by A3,Th2,NUMBERS:19;
reconsider b0 = b.0 as Element of REAL by XREAL_0:def 1;
reconsider p2=Replace(p,0,b0) as XFinSequence of REAL;
A9: k<>0 implies for i being Nat st 1<=i & i<=k holds p2.i= -(b.i)
proof
assume k<>0;
let i be Nat;
assume that
A10: 1<=i and
A11: i<=k;
(XFS2FS*(b)).i= b.i by A2,A5,A10,A11,AFINSQ_1:def 11;
then
A12: ( -(XFS2FS*(b))).i = -(b.i) by RVSUM_1:17;
i in NAT & p.i=c2.i by A6,A8,A10,A11,ORDINAL1:def 12;
hence thesis by A10,A12,AFINSQ_1:44;
end;
len p=len p2 & p2.0=b.0 by A1,A3,A7,AFINSQ_1:44;
then m vector_minus_prg p2,b by A2,A7,A9;
hence ex c being XFinSequence of REAL st m vector_minus_prg c,b;
A13: 0 < len b;
thus for c being non empty XFinSequence of REAL st m vector_minus_prg c,b
holds (XFS2FS*(c))= -(XFS2FS*(b))
proof
let c be non empty XFinSequence of REAL;
assume
A14: m vector_minus_prg c,b;
then consider n being Integer such that
A15: c.0=b.0 and
A16: n=b.0 and
A17: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i= -(b.i);
A18: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
i being Nat st 1<=i & i<=n holds c.i= -(b.i)) by A14;
then
A19: len (XFS2FS*(c)) = (c.0) by A5,AFINSQ_1:def 11;
now
per cases;
case
A20: n=0;
then (XFS2FS*(b))=<*>REAL by A13,A16,AFINSQ_1:64;
hence thesis by A18,A16,A20,AFINSQ_1:64,RVSUM_1:19;
end;
case
n<>0;
set p3=(XFS2FS*(c));
for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
proof
let k3 be Nat;
A21: (c.0) in len c by A1,A3,A18,AFINSQ_1:86;
then
A22: len p3=n by A15,A16,AFINSQ_1:def 11,A1;
assume
A23: 1 <=k3 & k3 <= len p3;
then
A24: b.k3 = (XFS2FS*b).k3 by A2,A5,A16,A22,AFINSQ_1:def 11;
p3.k3=c.k3 by A15,A16,A23,A21,A22,AFINSQ_1:def 11
.= -(b.k3) by A17,A23,A22;
hence thesis by A24,RVSUM_1:17;
end;
hence thesis by A6,A15,A19,FINSEQ_1:14;
end;
end;
hence thesis;
end;
end;
:: Vector Calculation Program: Sum of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a+b in a variable c.
::
::#define V_SIZE 1024
::void vector_add_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a[i]+b[i];
:: }
:: return;
::}
definition
let a,b,c be XFinSequence of REAL,m be Integer;
pred m vector_add_prg c,a,b means
len c =m & len a=m & len b =m & ex
n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i
<=n holds c.i=(a.i)+(b.i) );
end;
theorem
for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_add_prg c,a,b)& for c being non empty XFinSequence of REAL st
m vector_add_prg c,a,b holds (XFS2FS*(c))=(XFS2FS*(a))+(XFS2FS*(b))
proof
let a,b be non empty XFinSequence of REAL,m be Nat;
assume that
A1: b.0 is Nat and
A2: len a=m and
A3: len b=m and
A4: (a.0)=b.0 and
A5: b.0 < m;
reconsider k= b.0 as Nat by A1;
reconsider Fb=(XFS2FS*(b)) as FinSequence of REAL;
reconsider Fa=(XFS2FS*(a)) as FinSequence of REAL;
reconsider c2= Fa + Fb as FinSequence of REAL;
A6: b.0 in Segm m by A1,A5,NAT_1:44;
then
A7: len (XFS2FS*(a)) = b.0 by A2,A4,AFINSQ_1:def 11;
A8: len (XFS2FS*(b)) = b.0 by A3,A6,AFINSQ_1:def 11;
then
A9: len c2=len (XFS2FS*(a)) by A7,RVSUM_1:115;
then dom c2= Seg len (XFS2FS*(b)) by A8,A7,FINSEQ_1:def 3;
then dom((XFS2FS*(a))+(XFS2FS*(b))) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
then Seg len (c2) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
then
A10: len c2 =k by A8,FINSEQ_1:def 3;
then consider p being XFinSequence of REAL such that
A11: len p=m and
A12: p is_an_xrep_of c2 by A5,Th2,NUMBERS:19;
reconsider b0 = b.0 as Element of REAL by XREAL_0:def 1;
reconsider p2=Replace(p,0,b0) as XFinSequence of REAL;
A13: now
assume k<>0;
thus for i being Nat st 1<=i & i<=k holds p2.i=(a.i)+(b.i)
proof
let i be Nat;
assume that
A14: 1<=i and
A15: i<=k;
i in Seg len c2 by A7,A9,A14,A15,FINSEQ_1:1;
then
A16: i in dom c2 by FINSEQ_1:def 3;
(XFS2FS*(a)).i= a.i & (XFS2FS*(b)).i= b.i
by A2,A3,A4,A6,A14,A15,AFINSQ_1:def 11;
then
A17: ((XFS2FS*(a))+(XFS2FS*(b))).i = (a.i)+(b.i) by A16,VALUED_1:def 1;
i in NAT & p.i=c2.i by A10,A12,A14,A15,ORDINAL1:def 12;
hence thesis by A14,A17,AFINSQ_1:44;
end;
end;
len p=len p2 & p2.0=b.0 by A1,A5,A11,AFINSQ_1:44;
then m vector_add_prg p2,a,b by A2,A3,A11,A13;
hence ex c being XFinSequence of REAL st m vector_add_prg c,a,b;
A18: 0 < len b;
thus for c being non empty XFinSequence of REAL st m vector_add_prg c,a,b
holds (XFS2FS*(c))=(XFS2FS*(a))+(XFS2FS*(b))
proof
let c be non empty XFinSequence of REAL;
assume
A19: m vector_add_prg c,a,b;
then consider n being Integer such that
A20: c.0=b.0 and
A21: n=b.0 and
A22: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=(a.i)+(b.i);
A23: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
i being Nat st 1<=i & i<=n holds c.i=(a.i)+(b.i)) by A19;
then
A24: len (XFS2FS*(c)) = (c.0) by A6,AFINSQ_1:def 11;
now
per cases;
case
n=0;
then
(XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A18,A23,A21,AFINSQ_1:64;
hence thesis by RVSUM_1:12;
end;
case
n<>0;
set p3=(XFS2FS*(c));
for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
proof
let k3 be Nat;
assume that
A25: 1 <=k3 and
A26: k3 <= len p3;
A27: (c.0) in len c by A1,A5,A23,AFINSQ_1:86;
then
A28: k3 <= n by A20,A21,A26,AFINSQ_1:def 11,A1;
then
A29: a.k3 = (XFS2FS*(a)).k3 & b.k3 = (XFS2FS*(b)).k3 by A2,A3,A4,A6,A21
,A25,AFINSQ_1:def 11;
k3 in Seg len c2 by A10,A21,A25,A28,FINSEQ_1:1;
then
A30: k3 in dom c2 by FINSEQ_1:def 3;
len p3=n by A20,A21,A27,AFINSQ_1:def 11,A1;
then p3.k3=c.k3 by A20,A21,A25,A26,A27,AFINSQ_1:def 11
.=(a.k3)+(b.k3) by A22,A25,A28;
hence thesis by A30,A29,VALUED_1:def 1;
end;
hence thesis by A10,A20,A24,FINSEQ_1:14;
end;
end;
hence thesis;
end;
end;
:: Vector Calculation Program: Subtraction of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a-b in a variable c.
::
::#define V_SIZE 1024
::void vector_sub_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{ int n,i;
:: c[0]=b[0];
:: n=(int)(b[0]);
:: if (n != 0)
:: { for(i=1;i<=n;i++)c[i]=a[i]-b[i];
:: }
:: return;
::}
definition
let a,b,c be XFinSequence of REAL,m be Integer;
pred m vector_sub_prg c,a,b means
len c =m & len a=m & len b =m & ex n being Integer st c.0=b.0 & n=b.0 &
(n<>0 implies for i being Nat st 1<=i & i <=n holds c.i=(a.i)-(b.i) );
end;
theorem
for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_sub_prg c,a,b) & for c being non empty XFinSequence of REAL st
m vector_sub_prg c,a,b holds XFS2FS*(c)=XFS2FS*(a)-XFS2FS*(b)
proof
let a,b be non empty XFinSequence of REAL,m be Nat;
assume that
A1: b.0 is Nat and
A2: len a=m and
A3: len b=m and
A4: a.0=b.0 and
A5: b.0 < m;
reconsider k= b.0 as Nat by A1;
reconsider Fb=(XFS2FS*(b)) as FinSequence of REAL;
reconsider Fa=(XFS2FS*(a)) as FinSequence of REAL;
reconsider c2= Fa - Fb as FinSequence of REAL;
A6: b.0 in Segm m by A1,A5,NAT_1:44;
then
A7: len (XFS2FS*(a)) = b.0 by A2,A4,AFINSQ_1:def 11;
A8: len (XFS2FS*(b)) = b.0 by A3,A6,AFINSQ_1:def 11;
then
A9: len c2=len (XFS2FS*(a)) by A7,RVSUM_1:116;
then dom c2= Seg len (XFS2FS*(b)) by A8,A7,FINSEQ_1:def 3;
then dom((XFS2FS*(a))-(XFS2FS*(b))) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
then Seg len (c2) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
then
A10: len c2 =k by A8,FINSEQ_1:def 3;
then consider p being XFinSequence of REAL such that
A11: len p=m and
A12: p is_an_xrep_of c2 by A5,Th2,NUMBERS:19;
reconsider b0 = b.0 as Element of REAL by XREAL_0:def 1;
reconsider p2=Replace(p,0,b0) as XFinSequence of REAL;
A13: now
assume k<>0;
thus for i being Nat st 1<=i & i<=k holds p2.i=(a.i)-(b.i)
proof
let i be Nat;
assume that
A14: 1<=i and
A15: i<=k;
i in Seg len c2 by A7,A9,A14,A15,FINSEQ_1:1; then
A16: i in dom c2 by FINSEQ_1:def 3;
(XFS2FS*(a)).i= a.i & (XFS2FS*(b)).i= b.i
by A2,A3,A4,A6,A14,A15,AFINSQ_1:def 11; then
A17: ((XFS2FS*(a))-(XFS2FS*(b))).i = (a.i)-(b.i) by A16,VALUED_1:13;
i in NAT & p.i=c2.i by A10,A12,A14,A15,ORDINAL1:def 12;
hence thesis by A14,A17,AFINSQ_1:44;
end;
end;
len p=len p2 & p2.0=b.0 by A1,A5,A11,AFINSQ_1:44;
then m vector_sub_prg p2,a,b by A2,A3,A11,A13;
hence ex c being XFinSequence of REAL st m vector_sub_prg c,a,b;
A18: 0 < len b;
thus for c being non empty XFinSequence of REAL st m vector_sub_prg c,a,b
holds (XFS2FS*(c))=(XFS2FS*(a))-(XFS2FS*(b))
proof
let c be non empty XFinSequence of REAL;
assume
A19: m vector_sub_prg c,a,b;
then consider n being Integer such that
A20: c.0=b.0 and
A21: n=b.0 and
A22: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=(a.i)-(b.i);
A23: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
i being Nat st 1<=i & i<=n holds c.i=(a.i)-(b.i)) by A19;
then
A24: len (XFS2FS*(c)) = (c.0) by A6,AFINSQ_1:def 11;
now
per cases;
case n=0;
then
(XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A18,A23,A21,AFINSQ_1:64;
hence thesis by RVSUM_1:28;
end;
case n<>0;
set p3=(XFS2FS*(c));
for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
proof
let k3 be Nat;
assume that
A25: 1 <=k3 and
A26: k3 <= len p3;
A27: (c.0) in len c by A1,A5,A23,AFINSQ_1:86;
then
A28: k3 <= n by A20,A21,A26,AFINSQ_1:def 11,A1;
then
A29: a.k3 = (XFS2FS*(a)).k3 & b.k3 = (XFS2FS*(b)).k3 by A2,A3,A4,A6,A21
,A25,AFINSQ_1:def 11;
k3 in Seg len c2 by A10,A21,A25,A28,FINSEQ_1:1;
then
A30: k3 in dom c2 by FINSEQ_1:def 3;
A31: len p3=n by A20,A21,A27,AFINSQ_1:def 11,A1;
then p3.k3=c.k3 by A20,A21,A25,A26,A27,AFINSQ_1:def 11
.=(a.k3)-(b.k3) by A22,A25,A26,A31;
hence thesis by A30,A29,VALUED_1:13;
end;
hence thesis by A10,A20,A24,FINSEQ_1:14;
end;
end;
hence thesis;
end;
end;