:: Logical Correctness of Vector Calculation Programs
:: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2017 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,
MEMBERED, FINSEQ_1, AFINSQ_1, VALUED_0, FINSEQ_2, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities CARD_1, 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 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 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 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;
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).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) 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=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 i0;
thus for i being Nat st i0 implies for i being Nat st i0 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 i0 implies for i being Nat st i0 implies for i being Nat st i0 implies for i being Nat st i0 implies for i being Nat st i 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) 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 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 i0;
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;