SSL nvectors.pvs
Sprache: unbekannt
|
|
rahmenlose Ansicht.pvs DruckansichtUnknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
nvectors: THEORY
%----------------------------------------------------------------------------
% N-dimensional vectors of reals and operations (zero-based)
%----------------------------------------------------------------------------
BEGIN
% reals: LIBRARY = "../reals"
IMPORTING reals@sigma_nat, reals@sqrt
IMPORTING structures@fseqs_def[real,0]
n: VAR posnat
Vector : TYPE = {s: fseq | s`length > 0}
Vect(n): TYPE = {v: Vector | v`length = n}
a,b,c : VAR real
nza : VAR nzreal
u,v,w,z : VAR Vector
% ----------- Vector Operations -------------------------------------------
-(v): Vect(v`length) =
(# length := v`length,
seq := LAMBDA (i: nat): -v(i)
#) ;
+(u: Vector, v: Vect(u`length)): Vect(u`length) =
(# length := u`length,
seq := (LAMBDA (i: nat): u`seq(i) + v`seq(i))
#) ;
-(u: Vector, v: Vect(u`length)): Vect(u`length) = u + -v ;
*(u: Vector, v: Vect(u`length)): real =
sigma(0, u`length-1, LAMBDA (i: nat):u(i)*v(i)); % Dot Product
*(a,v): Vect(v`length) =
(# length := v`length,
seq := LAMBDA (i: nat): a*v(i)
#)
% ^(nzv): Normalized = (1/norm(nzv))*nzv % defined ahead
% ----------- Vector Functions -------------------------------------------
sqv(v): nnreal = v*v
sq(v): nnreal = sigma(0,v`length-1,LAMBDA (i: nat): sq(v(i)))
norm(v): nnreal = sqrt(sqv(v))
zero_vector?(v) : MACRO bool = (norm(v) = 0)
nz_vector?(v) : MACRO bool = (norm(v) /= 0)
normalized?(v) : MACRO bool = (norm(v) = 1)
zero_vect?(n)(v: Vect(n)) : MACRO bool = (norm(v) = 0)
nz_vect?(n)(v: Vect(n)) : MACRO bool = (norm(v) /= 0)
normalized_vect?(n)(v: Vect(n)) : MACRO bool = (norm(v) = 1)
Zero_vector : TYPE = (zero_vector?)
Nz_vector : TYPE = (nz_vector?)
Normalized : TYPE = (normalized?)
Zero_vect(n) : TYPE = (zero_vect?(n))
Nz_vect(n) : TYPE = (nz_vect?(n))
Normalized_vect(n) : TYPE = (normalized_vect?(n))
nzu,nzv : VAR Nz_vector
% normalize(nzv) : Normalized = (1/norm(nzv))*nzv
% ----------- Special vectors ---------------------------------------------
zero(n) : Zero_vect(n) = (# length := n, seq := LAMBDA (i: nat): 0 #)
unity(n)(i: below(n)): Normalized_vect(n) =
zero(n) WITH [`seq(i) := 1]
const_vec(n)(a): Vect(n) = const_seq(n,a)
% ----------- Vector Component Lemmas -------------------------------------
comp_distr_add : LEMMA
FORALL (v: Vector, w: Vect(v`length), i: nat): i < v`length IMPLIES
(v + w)`seq(i) = v`seq(i) + w`seq(i)
comp_distr_sub : LEMMA
FORALL (v: Vector, w: Vect(v`length), i: nat): i < v`length IMPLIES
(v - w)`seq(i) = v`seq(i) - w`seq(i)
comp_distr_scal : LEMMA
FORALL (v: Vector, i: nat): i < v`length IMPLIES
(a*v)`seq(i) = a*(v`seq(i)) %% NEW %%
comp_zero : LEMMA FORALL (i: below(n)): zero(n)`seq(i) = 0
comp_eq : LEMMA
FORALL (u, (w: Vect(u`length))):
u = w IFF FORALL (i: below(u`length)): u(i) = w(i) %%%% NEW %%%%
% ----------- Vector Operation Lemmas -------------------------------------
add_zero_left : LEMMA FORALL (v: Vect(n)): zero(n) + v = v
add_zero_right : LEMMA FORALL (v: Vect(n)): v + zero(n) = v
add_comm : LEMMA FORALL (u: Vector, v: Vect(u`length)): u+v = v+u
add_assoc : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): u+(v+w) = (u+v)+w
add_move_right : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): u + w = v IFF u = v - w
add_move_both : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): v = u + w IFF u = v - w
add_neg_sub : LEMMA
FORALL (u: Vector, v: Vect(u`length)): v + -u = v - u
add_cancel : LEMMA
FORALL (v: Vector, w: Vect(v`length)): v + w - v = w
add_cancel_neg : LEMMA
FORALL (v: Vector, w: Vect(v`length)): -v + w + v = w
add_cancel2 : LEMMA
FORALL (v: Vector, w: Vect(v`length)): w - v + v = w
add_cancel_neg2 : LEMMA
FORALL (v: Vector, w: Vect(v`length)): w + v - v = w
sub_zero_left : LEMMA FORALL (v: Vect(n)): zero(n) - v = -v
sub_zero_right : LEMMA FORALL (v: Vect(n)): v - zero(n) = v
sub_eq_args : LEMMA FORALL (v: Vect(n)): v - v = zero(n)
sub_eq_zero : LEMMA FORALL (u, v: Vect(n)):
u - v = zero(n) IFF u = v
sub_cancel : LEMMA
FORALL (v: Vector, w: Vect(v`length)): v - w - v = -w
sub_cancel_neg : LEMMA
FORALL (v: Vector, w: Vect(v`length)): -v - w + v = -w
neg_add_left : LEMMA FORALL (v: Vect(n)): -v + v = zero(n)
neg_add_right : LEMMA FORALL (v: Vect(n)): v + -v = zero(n)
neg_distr_sub : LEMMA
FORALL (u: Vector, v: Vect(u`length)): -(v - u) = u - v
neg_neg : LEMMA --v = v
neg_distr_add : LEMMA
FORALL (u: Vector, v: Vect(u`length)): -(u + v) = -u - v
dot_neg_left : LEMMA
FORALL (u: Vector, w: Vect(u`length)): (-u)*w = -(u*w)
dot_neg_right : LEMMA
FORALL (u: Vector, w: Vect(u`length)): u*(-w) = -(u*w)
dot_neg_sq : LEMMA (-v)*(-v) = v*v
dot_zero_left : LEMMA zero(v`length) * v = 0
dot_zero_right : LEMMA v * zero(v`length) = 0
dot_comm : LEMMA
FORALL (u: Vector, v: Vect(u`length)): u*v = v*u
dot_assoc : LEMMA
FORALL (w: Vect(v`length)): a*(v*w) = (a*v)*w
dot_eq_args_ge : LEMMA u*u >= 0
dot_distr_add_left : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): u*(v+w) = u*v + u*w
dot_distr_add_right : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): (v+w)*u = v*u + w*u
dot_distr_sub_left : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): u*(v-w) = u*v - u*w
dot_distr_sub_right : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): (v-w)*u = v*u - w*u
dot_divby : LEMMA
FORALL (u: Vector, v: Vect(u`length)): nza*u = nza*v IMPLIES u = v %%%% NEW %%%%
dot_scal_left : LEMMA
FORALL (u: Vector, v: Vect(u`length)): (a*u)*v = a*(u*v)
dot_scal_right : LEMMA
FORALL (u: Vector, v: Vect(u`length)): u*(a*v) = a*(u*v)
dot_scal_assoc : LEMMA a*(b*u) = (a*b)*u
dot_scal_canon : LEMMA
FORALL (u: Vector, v: Vect(u`length)): (a*u)*(b*v) = (a*b)*(u*v) %% NEW %%x
dot_scal_distr_add : LEMMA (a+b)*u = a*u + b*u
dot_scal_distr_sub : LEMMA (a-b)*u = a*u - b*u
scal_add_distr : LEMMA
FORALL (u: Vector, v: Vect(u`length)): a*(u+v) = a*u + a*v
scal_sub_distr : LEMMA
FORALL (u, (v: Vect(u`length))): a*(u-v) = a*u - a*v
scal_zero : LEMMA a * zero(n) = zero(n)
scal_0 : LEMMA 0 * v = zero(v`length)
scal_1 : LEMMA 1 * v = v
scal_cancel : LEMMA a*nzv = b*nzv IMPLIES a = b %% NEW %%
scal_dot_eq_0 : LEMMA
FORALL (v: Vect(n)): c*v = zero(n) IMPLIES c = 0 OR v = zero(n) %%%% NEW %%%%
dot_ge_dist : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): w*u >= w*v IMPLIES w*(u-v) >= 0
dot_gt_dist : LEMMA
FORALL (u: Vector, v, w: Vect(u`length)): w*u > w*v IMPLIES w*(u-v) > 0
sq_dot_eq : LEMMA
v*v = 0 IFF v = zero(v`length)
sqv_sq : LEMMA sqv(v) = sq(v)
sq_sqv : LEMMA sq(v) = sqv(v)
sq_lem : LEMMA
sq(v) = sigma(0,v`length-1,LAMBDA (i: nat): sq(v(i)))
sqv_lem : LEMMA
sqv(u) = sigma(0,u`length-1,(LAMBDA (i: nat): sq(u(i))))
sqv_zero : LEMMA sqv(zero(n)) = 0
sqv_eq_0 : LEMMA sqv(v) = 0 IFF v = zero(v`length)
sqv_neg : LEMMA sqv(-v) = sqv(v)
sqv_add : LEMMA
FORALL (u: Vector, v: Vect(u`length)): sqv(u+v) = sqv(u) + sqv(v) + 2*u*v
sqv_sub : LEMMA
FORALL (u: Vector, v: Vect(u`length)): sqv(u-v) = sqv(u) + sqv(v) - 2*u*v
sqv_sym : LEMMA
FORALL (u: Vector, v: Vect(u`length)): sqv(u-v) = sqv(v-u)
sqv_scal : LEMMA sqv(a*v) = sq(a)*sqv(v)
sqrt_sqv_sq : LEMMA sqrt(sqv(v)) * sqrt(sqv(v)) = sqv(v)
norm_sym : LEMMA
FORALL (u: Vector, v: Vect(u`length)): norm(u-v) = norm(v-u)
norm_neg : LEMMA norm(-u) = norm(u)
dot_sq_norm : LEMMA u*u = sq(norm(u))
sq_norm : LEMMA sq(norm(u)) = u*u
sqrt_sqv_norm : LEMMA sqrt(sqv(v)) = norm(v)
norm_eq_0 : LEMMA
norm(v) = 0 IFF v = zero(v`length)
norms_eq_sqv : LEMMA
FORALL (u: Vector, v: Vect(u`length)): norm(u) = norm(v) IFF sqv(u) = sqv(v)
norm_scal : LEMMA norm(a*v) = abs(a)*norm(v)
idem_right : LEMMA
a * v = v IFF (a = 1 OR v = zero(v`length)) ;
^(nzv) : Normalized = (1/norm(nzv))*nzv %% NEW %%
normalize(nzv) : MACRO Normalized = ^(nzv)
dot_normalize : LEMMA
FORALL (nzv: Nz_vect(nzu`length)): ^(nzu) * ^(nzv) %% NEW %%
= nzu*nzv/(norm(nzu)*norm(nzv))
normalize_normalize: LEMMA ^(^(nzv)) = ^(nzv) %%%% NEW %%%%%%%
sqv_minus_dot : LEMMA
FORALL (u: Vector, v: Vect(u`length)): sqv(u-a*v) = sqv(u) - 2*a*u*v + sq(a)*sqv(v)
cauchy_schwarz : LEMMA
FORALL (u: Vector, v: Vect(u`length)): sq(u*v) <= sqv(u)*sqv(v)
dot_norm : LEMMA
FORALL (u: Vector, v: Vect(u`length)): -norm(u)*norm(v) <= u*v AND u*v <= norm(u)*norm(v)
norm_add_le : LEMMA
FORALL (u: Vector, v: Vect(u`length)): norm(u+v) <= norm(u) + norm(v)
norm_sub_le : LEMMA
FORALL (u: Vector, v: Vect(u`length)): norm(u-v) <= norm(u) + norm(v)
norm_sub_ge : LEMMA
FORALL (u: Vector, v: Vect(u`length)): norm(u-v) >= norm(u) - norm(v)
norm_ge_comps : LEMMA
FORALL (i: nat): norm(u) >= abs(u`seq(i)) %% NEW %%
v0,v1,v2 : VAR Vector
norm_triangle : LEMMA
FORALL (v0: Vector, v1, v2: Vect(v0`length)):
LET a = v1-v0, b = v1-v2, c = v2-v0 IN %% NEW %%
sq(norm(c)) = sq(norm(a)) + sq(norm(b)) - 2*a*b
nzvec_has_nz : LEMMA (EXISTS (i: below(nzv`length)): nzv`seq(i) /= 0) %% NEW %%
nzvec_neq_zero : LEMMA nzv /= zero(nzv`length) %% NEW %%
v_neq_0 : LEMMA v /= zero(v`length) IFF sigma(0,v`length-1,(LAMBDA (i: nat): sq(v(i)))) > 0
% ---------- Predicates over vectors ---------
parallel?(nzu, (nzv: Nz_vect(nzu`length))): bool =
^(nzu)*^(nzv) = 1 OR ^(nzu)*^(nzv) = -1 %% NEW %%
orthogonal?(u,(v: Vect(u`length))): bool = u * v = 0 ;
% parallel_lem: LEMMA parallel?(nzu,nzv) IFF (EXISTS (k:nzreal): nzu = k*nzv)
% ---------- Auto Rewrites ------------------------------------
AUTO_REWRITE+ add_zero_left
AUTO_REWRITE+ add_zero_right
AUTO_REWRITE+ sub_zero_left
AUTO_REWRITE+ sub_zero_right
AUTO_REWRITE+ sub_eq_zero %% NEW %%
AUTO_REWRITE+ sub_eq_args
AUTO_REWRITE+ neg_add_left
AUTO_REWRITE+ neg_add_right
AUTO_REWRITE+ dot_zero_left
AUTO_REWRITE+ dot_zero_right
AUTO_REWRITE+ scal_zero
AUTO_REWRITE+ scal_0
AUTO_REWRITE+ sqv_zero
AUTO_REWRITE+ add_neg_sub
AUTO_REWRITE+ neg_neg
AUTO_REWRITE+ dot_scal_left
AUTO_REWRITE+ dot_scal_right
AUTO_REWRITE+ dot_scal_assoc
AUTO_REWRITE+ dot_scal_canon %% NEW %%
AUTO_REWRITE+ sqv_neg
AUTO_REWRITE+ sqrt_sqv_sq
AUTO_REWRITE+ norm_neg
AUTO_REWRITE+ comp_zero
AUTO_REWRITE+ add_cancel
AUTO_REWRITE+ sub_cancel
AUTO_REWRITE+ add_cancel_neg
AUTO_REWRITE+ sub_cancel_neg
AUTO_REWRITE+ add_cancel2
AUTO_REWRITE+ add_cancel_neg2
% ---- Turn off dangerous and unhelpful rewrites for auto-rewrite-theory --
AUTO_REWRITE- add_comm % LEMMA u+v = v+u
AUTO_REWRITE- dot_comm % LEMMA u*v = v*u
AUTO_REWRITE- dot_assoc % LEMMA a*(v*w) = (a*v)*w
AUTO_REWRITE- sqv_lem % LEMMA sqv(u) = u*u
AUTO_REWRITE- sqv_sym % LEMMA sqv(u-v) = sqv(v-u)
AUTO_REWRITE- norm_sym % LEMMA norm(u-v) = norm(v-u)
AUTO_REWRITE- dot_sq_norm % LEMMA u*u = sq(norm(u))
END nvectors
[ Verzeichnis aufwärts0.117unsichere Verbindung
]
|
2026-03-28
|
