LAProof.accuracy_proofs.mv_mathcomp
From LAProof.accuracy_proofs Require Import preamble common
dotprod_model sum_model dot_acc float_acc_lems.
From mathcomp.algebra_tactics Require Import ring.
Open Scope ring_scope.
Open Scope order_scope.
Definition sum_abs {m n} (A: 'M[R]_(m,n)) i : R:= \sum_j (Rabs (A i j)).
Definition normv {m} (v: 'cV[R]_m) : R:= \big[maxr/0]_(i < m) Rabs (v i 0%Ri).
Definition normM {m n} (A: 'M[R]_(m,n)) : R:= \big[maxr/0]_i (sum_abs A i).
Definition seq_of_rV {T}[n] (x: 'rV[T]_n) := map (x ord0) (ord_enum n).
Ltac case_splitP j :=
first [is_var j | fail 1 "case_splitP requires a variable, but got" j];
match type of j with 'I_(addn ?a ?b) ⇒
let i := fresh "j" in let H := fresh in
destruct (splitP j) as [i H | i H];
[replace j with (@lshift a b i); [ | apply ord_inj; simpl; lia]
|replace j with (@rshift a b i); [ | apply ord_inj; simpl; lia]];
clear j H; rename i into j
end.
Example of how to use case_splitP
Local Remark mul_mx_row' [R : GRing.SemiRing.type] m n p1 p2
(A: 'M[R]_(m,n)) (Bl: 'M[R]_(n,p1)) (Br: 'M[R]_(n,p2)):
A ×m row_mx Bl Br = row_mx (A ×m Bl) (A ×m Br).
(A: 'M[R]_(m,n)) (Bl: 'M[R]_(n,p1)) (Br: 'M[R]_(n,p2)):
A ×m row_mx Bl Br = row_mx (A ×m Bl) (A ×m Br).
Example of how the mathcomp experts do this another way, from mathcomp.algebra.matrix
Local Remark mul_mx_row'' [R : GRing.SemiRing.type] m n p1 p2 (A : 'M[R]_(m, n)) (Bl : 'M_(n, p1)) (Br : 'M_(n, p2)) :
A ×m row_mx Bl Br = row_mx (A ×m Bl) (A ×m Br).
Lemma nth_List_nth: ∀ {A: Type} (d: A) (l: seq.seq A) (n: nat),
seq.nth d l n = List.nth n l d.
Lemma pred_lt: ∀ [n: nat], (0 < n → n.-1 < n)%nat.
Definition pred_ord [n: nat] (Hn: (0 < n)%nat) : 'I_n := Ordinal (pred_lt Hn).
Lemma ordinal_enum_size: ∀ n: nat,
size (Finite.enum (ordinal n)) = n.
Lemma size_ord_enum: ∀ n, size (ord_enum n) = n.
Lemma nth_index_enum: ∀ {n: nat} (x: 'I_n) y,
seq.nth y (index_enum (ordinal n)) x = x.
Lemma nth_ord_enum': ∀ n (i: 'I_n) x, seq.nth x (ord_enum n) i = i.
Lemma index_ord_enum: ∀ (n: nat), (index_enum (ordinal n)) = ord_enum n.
Lemma size_seq_of_rV : ∀ {T} [n] x, size (@seq_of_rV T n x) = n.
Lemma nth_seq_of_rV: ∀ {T}[n](d: T)(x: 'rV[T]_n) (i: 'I_n), nth d (seq_of_rV x) i = x ord0 i.
Lemma maxrC : @commutative R R maxr.
Lemma maxrA : @associative R maxr.
Lemma big_mul {n:nat} (F : ordinal n → R) op a:
(∀ i b, op (F i) b × a = op (F i × a) (b × a)) →
R0 ≤ a → \big[op/0]_(i0 < n) (F i0) × a = \big[op/0]_(i0 < n) (F i0 × a).
Lemma big_max_mul {n:nat} (F : ordinal n → R) a:
R0 ≤ a → \big[maxr/0]_(i0 < n) (F i0) × a = \big[maxr/0]_(i0 < n) (F i0 × a).
Lemma normv_pos {m} (v: 'cV[R]_m) : R0 ≤ normv v.
Lemma normM_pos [m n] (A: 'M[R]_(m,n)) : R0 ≤ normM A.
Lemma Rabs_sum (n:nat) : ∀ (F : ordinal n → R),
Rabs (\sum_j F j) ≤ \sum_j Rabs (F j).
Lemma subMultNorm m n (A: 'M[R]_(m,n)) (u : 'cV_n) :
normv ( A ×m u ) ≤ normM A × normv u.
Lemma normv_triang m (u v: 'cV_m) :
normv ( u + v ) ≤ normv u + normv v.
Local Definition crazy (T: Type): 'I_0 → T.
Defined.
Lemma exists_mx: ∀ {T} [m n] (F: 'I_m → 'I_n → T → Prop),
(∀ i j, ∃ x, F i j x) →
∃ A: 'M[T]_(m,n), ∀ i j, F i j (A i j).
Lemma rev_ord_enum: ∀ n, rev (ord_enum n) = map (@rev_ord n) (ord_enum n).
Lemma nth_ord_enum_lemma:
∀ [T] (d: T) (u: seq T),
u = map (nth d u \o @nat_of_ord (size u)) (ord_enum (size u)).
Lemma sumR_sum: ∀ (x: seq R), sumR x = \sum_(i in 'I_(size x)) nth R0 x (nat_of_ord i).
Module F.
Section WithNAN.
Context {NAN: FPCore.Nans} {t : type}.
Definition sum [n: nat] (x: 'I_n → ftype t) : ftype t :=
\big[BPLUS / neg_zero]_i x (rev_ord i).
Definition dotprod [n: nat] (x: 'rV[ftype t]_n) (y: 'cV[ftype t]_n) : ftype t :=
\big[BPLUS / pos_zero]_i (BMULT (x ord0 (rev_ord i)) (y (rev_ord i) ord0)).
Definition mulmx [m n p] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,p)) :=
\matrix_(i,k) dotprod (row i A) (col k B).
Definition scalemx [m n] (a: ftype t) (M: 'M[ftype t]_(m,n)) :=
map_mx (BMULT a) M.
Definition addmx [m n] (A B: 'M[ftype t]_(m,n)) : 'M[ftype t]_(m,n) :=
\matrix_(i,j) BPLUS (A i j) (B i j).
Lemma mulmx_row:
∀ m n p1 p2 (A: 'M[ftype t]_(m,n)) (Bl: 'M_(n,p1)) (Br: 'M_(n,p2)),
mulmx A (row_mx Bl Br) = row_mx (mulmx A Bl) (mulmx A Br).
Lemma sum_sumF: ∀ [n] (x: 'I_n → ftype t), sum x = sumF (map x (ord_enum n)).
Lemma dotprod_dotprodF:
∀ [n] (x: 'rV[ftype t]_n) (y: 'cV[ftype t]_n),
dotprod x y = dotprodF (seq_of_rV x) (seq_of_rV (trmx y)).
Lemma mulmx_dotprodF:
∀ [n] (A: 'M[ftype t]_(1,n)) (B: 'M[ftype t]_(n,1)),
mulmx A B = const_mx (dotprodF (seq_of_rV A) (seq_of_rV (trmx B))).
Definition finitemx [m n] (A: 'M[ftype t]_(m,n)) : Prop :=
(∀ i j, Binary.is_finite (A i j)).
Lemma finitemx_addmx_e: ∀ [m n] (A B: 'M[ftype t]_(m,n)),
finitemx (addmx A B) → finitemx A ∧ finitemx B.
Lemma finitemx_scalemx_e: ∀ [m n] (c: ftype t) (A: 'M[ftype t]_(m,n)),
finitemx (scalemx c A) → finitemx A.
End WithNAN.
End F.
A ×m row_mx Bl Br = row_mx (A ×m Bl) (A ×m Br).
Lemma nth_List_nth: ∀ {A: Type} (d: A) (l: seq.seq A) (n: nat),
seq.nth d l n = List.nth n l d.
Lemma pred_lt: ∀ [n: nat], (0 < n → n.-1 < n)%nat.
Definition pred_ord [n: nat] (Hn: (0 < n)%nat) : 'I_n := Ordinal (pred_lt Hn).
Lemma ordinal_enum_size: ∀ n: nat,
size (Finite.enum (ordinal n)) = n.
Lemma size_ord_enum: ∀ n, size (ord_enum n) = n.
Lemma nth_index_enum: ∀ {n: nat} (x: 'I_n) y,
seq.nth y (index_enum (ordinal n)) x = x.
Lemma nth_ord_enum': ∀ n (i: 'I_n) x, seq.nth x (ord_enum n) i = i.
Lemma index_ord_enum: ∀ (n: nat), (index_enum (ordinal n)) = ord_enum n.
Lemma size_seq_of_rV : ∀ {T} [n] x, size (@seq_of_rV T n x) = n.
Lemma nth_seq_of_rV: ∀ {T}[n](d: T)(x: 'rV[T]_n) (i: 'I_n), nth d (seq_of_rV x) i = x ord0 i.
Lemma maxrC : @commutative R R maxr.
Lemma maxrA : @associative R maxr.
Lemma big_mul {n:nat} (F : ordinal n → R) op a:
(∀ i b, op (F i) b × a = op (F i × a) (b × a)) →
R0 ≤ a → \big[op/0]_(i0 < n) (F i0) × a = \big[op/0]_(i0 < n) (F i0 × a).
Lemma big_max_mul {n:nat} (F : ordinal n → R) a:
R0 ≤ a → \big[maxr/0]_(i0 < n) (F i0) × a = \big[maxr/0]_(i0 < n) (F i0 × a).
Lemma normv_pos {m} (v: 'cV[R]_m) : R0 ≤ normv v.
Lemma normM_pos [m n] (A: 'M[R]_(m,n)) : R0 ≤ normM A.
Lemma Rabs_sum (n:nat) : ∀ (F : ordinal n → R),
Rabs (\sum_j F j) ≤ \sum_j Rabs (F j).
Lemma subMultNorm m n (A: 'M[R]_(m,n)) (u : 'cV_n) :
normv ( A ×m u ) ≤ normM A × normv u.
Lemma normv_triang m (u v: 'cV_m) :
normv ( u + v ) ≤ normv u + normv v.
Local Definition crazy (T: Type): 'I_0 → T.
Defined.
Lemma exists_mx: ∀ {T} [m n] (F: 'I_m → 'I_n → T → Prop),
(∀ i j, ∃ x, F i j x) →
∃ A: 'M[T]_(m,n), ∀ i j, F i j (A i j).
Lemma rev_ord_enum: ∀ n, rev (ord_enum n) = map (@rev_ord n) (ord_enum n).
Lemma nth_ord_enum_lemma:
∀ [T] (d: T) (u: seq T),
u = map (nth d u \o @nat_of_ord (size u)) (ord_enum (size u)).
Lemma sumR_sum: ∀ (x: seq R), sumR x = \sum_(i in 'I_(size x)) nth R0 x (nat_of_ord i).
Module F.
Section WithNAN.
Context {NAN: FPCore.Nans} {t : type}.
Definition sum [n: nat] (x: 'I_n → ftype t) : ftype t :=
\big[BPLUS / neg_zero]_i x (rev_ord i).
Definition dotprod [n: nat] (x: 'rV[ftype t]_n) (y: 'cV[ftype t]_n) : ftype t :=
\big[BPLUS / pos_zero]_i (BMULT (x ord0 (rev_ord i)) (y (rev_ord i) ord0)).
Definition mulmx [m n p] (A: 'M[ftype t]_(m,n)) (B: 'M[ftype t]_(n,p)) :=
\matrix_(i,k) dotprod (row i A) (col k B).
Definition scalemx [m n] (a: ftype t) (M: 'M[ftype t]_(m,n)) :=
map_mx (BMULT a) M.
Definition addmx [m n] (A B: 'M[ftype t]_(m,n)) : 'M[ftype t]_(m,n) :=
\matrix_(i,j) BPLUS (A i j) (B i j).
Lemma mulmx_row:
∀ m n p1 p2 (A: 'M[ftype t]_(m,n)) (Bl: 'M_(n,p1)) (Br: 'M_(n,p2)),
mulmx A (row_mx Bl Br) = row_mx (mulmx A Bl) (mulmx A Br).
Lemma sum_sumF: ∀ [n] (x: 'I_n → ftype t), sum x = sumF (map x (ord_enum n)).
Lemma dotprod_dotprodF:
∀ [n] (x: 'rV[ftype t]_n) (y: 'cV[ftype t]_n),
dotprod x y = dotprodF (seq_of_rV x) (seq_of_rV (trmx y)).
Lemma mulmx_dotprodF:
∀ [n] (A: 'M[ftype t]_(1,n)) (B: 'M[ftype t]_(n,1)),
mulmx A B = const_mx (dotprodF (seq_of_rV A) (seq_of_rV (trmx B))).
Definition finitemx [m n] (A: 'M[ftype t]_(m,n)) : Prop :=
(∀ i j, Binary.is_finite (A i j)).
Lemma finitemx_addmx_e: ∀ [m n] (A B: 'M[ftype t]_(m,n)),
finitemx (addmx A B) → finitemx A ∧ finitemx B.
Lemma finitemx_scalemx_e: ∀ [m n] (c: ftype t) (A: 'M[ftype t]_(m,n)),
finitemx (scalemx c A) → finitemx A.
End WithNAN.
End F.