Library Vector

Require Import EnsembleFacts.
Require Import types.
Require Import Array.
Require Import Recdef.
Require Import Omega.
Require Import Range.

Open Local Scope array_scope.
Section Vector.
Variable U:Type.

Defined.
Implicit Arguments ScalarProduct [x].
Lemma ScalarProduct_nil: forall (add prod:Operation U) (zero:U),
ScalarProduct add prod zero (nil U) (nil U)=zero.

Lemma ScalarProduct_single: forall (add prod:Operation U) (zero:U)
(x y:U) (Z:forall t:U, add t zero=t),
ScalarProduct add prod zero (x::nil U) (y::nil U)=prod x y.

Lemma ScalarProduct_commutative: forall (n:nat)
(add prod:Operation U) (zero:U) (a b:array U n),
Commutativity U prod->
ScalarProduct add prod zero a b=
ScalarProduct add prod zero b a.

Definition VectorAdd_d (n:nat) (add:Operation U) (default:U)
(a b:array U n): array U n:=
array_from_func n
 (fun i:nat=>add (nth default i a) (nth default i b)).
Implicit Arguments VectorAdd_d [n].

Lemma VectorAdd_d_nil: forall (add:Operation U) (default:U),
VectorAdd_d add default (nil U) (nil U)=nil U.

Lemma VectorAdd_d_single: forall (add:Operation U)
(default:U) (x y:U),
VectorAdd_d add default (x::nil U) (y::nil U)=(add x y)::nil U.

Lemma VectorAdd_d_commutativity: forall (n:nat) (add:Operation U)
(default:U), Commutativity U add ->
Commutativity (array U n) (VectorAdd_d add default).

Lemma VectorAdd_d_associativity: forall (n:nat) (add:Operation U)
(default:U), Associativity U add ->
Associativity (array U n) (VectorAdd_d add default).

Lemma VectorAdd_d_app: forall (m n:nat) (add:Operation U) (d:U)
(l1 l2:array U m) (r1 r2:array U n),
VectorAdd_d add d (l1++r1) (l2++r2)=
(VectorAdd_d add d l1 l2)++(VectorAdd_d add d r1 r2).

Defined.
Implicit Arguments VectorAdd [x].
Ltac VectorAdd:=
repeat (rewrite VectorAdd_equation;
simpl;repeat rewrite maptype_selfany;simpl).

Lemma VectorAdd_nil: forall (add:Operation U),
VectorAdd add (nil U) (nil U)=nil U.

Lemma VectorAdd_single: forall (add:Operation U) (x y:U),
VectorAdd add (x::nil U) (y::nil U)=(add x y)::nil U.

Lemma VectorAdd_commutativity: forall (n:nat) (add:Operation U),
Commutativity U add ->
Commutativity (array U n) (VectorAdd add).

Lemma VectorAdd_associativity: forall (n:nat) (add:Operation U),
Associativity U add ->
Associativity (array U n) (VectorAdd add).

Theorem VectorAdd_nth: forall (n:nat) (add:Operation U)
(d:U) (a b:array U n) (i:nat), i<n->
nth d i (VectorAdd add a b)=
add (nth d i a) (nth d i b).

Theorem VectorAdd_d_eq: forall (n:nat) (add:Operation U)
(default:U) (a b:array U n),
VectorAdd_d add default a b=VectorAdd add a b.

Lemma VectorAdd_app: forall (m n:nat) (add:Operation U)
(l1 l2:array U m) (r1 r2:array U n),
VectorAdd add (l1++r1) (l2++r2)=
(VectorAdd add l1 l2)++(VectorAdd add r1 r2).

Definition VectorAdd_R (n:nat) (add:Operation U)
(a b:array U n): array U n:=
array_from_funcrange n
 (fun I:lowrangt n=>add (nth_range I a) (nth_range I b)).
Implicit Arguments VectorAdd_R [n].

Lemma VectorAdd_R_nil: forall (add:Operation U) (default:U),
VectorAdd_R add (nil U) (nil U)=nil U.

Theorem VectorAdd_Rd_eq: forall (n:nat) (add:Operation U)
(default:U) (a b:array U n),
VectorAdd_d add default a b=VectorAdd_R add a b.

Theorem VectorAdd_R_eq: forall (n:nat) (add:Operation U)
(a b:array U n),
VectorAdd_R add a b=VectorAdd add a b.

Lemma VectorAdd_R_single: forall (add:Operation U) (x y:U),
VectorAdd_R add (x::nil U) (y::nil U)=(add x y)::nil U.

Lemma VectorAdd_nth_range: forall (n:nat) (add:Operation U)
(a b:array U n) (I:{i|i<n}),
nth_range I (VectorAdd add a b)=
add (nth_range I a) (nth_range I b).

Definition Kronecker_delta (z v:U) (i j:nat):U:=
match eq_nat_dec i j with
|left _ =>v
|right _ =>z
end.

Lemma Kronecker_delta_sym: forall (z v:U) (i j:nat),
Kronecker_delta z v i j=Kronecker_delta z v j i.

Lemma Kronecker_delta_refl: forall (z v:U) (i:nat),
Kronecker_delta z v i i=v.

Lemma Kronecker_delta_diff: forall (z v:U) (i j:nat),i<>j->
Kronecker_delta z v i j=z.

Definition UnitVector (n:nat) (z v:U) (i:nat):array U n:=
array_from_func n (Kronecker_delta z v i).

Lemma UnitVector_as_app_construct: forall (n:nat) (z v:U) (i:nat),
UnitVector (i+S n) z v i=
array_homogeneous U i z ++
v::array_homogeneous U n z.

Lemma UnitVector_as_app: forall (n:nat) (z v:U) (i:nat), i<n->
{p:nat|n=i+S p &
UnitVector (i+S p) z v i=
array_homogeneous U i z ++
v::array_homogeneous U p z}.

Definition VectorProdScalar (n:nat) (prod:Operation U)
(a:array U n) (s:U):=
VectorAdd prod a (array_homogeneous U n s).

Definition ScalarProdVector (n:nat) (prod:Operation U)
(a:array U n) (s:U):=
VectorAdd prod (array_homogeneous U n s) a.

End Vector.

Implicit Arguments ScalarProduct [U x]. Implicit Arguments VectorAdd [U x].
Implicit Arguments Kronecker_delta [U].
Implicit Arguments UnitVector [U].
Implicit Arguments VectorProdScalar[U n].
Implicit Arguments ScalarProdVector[U n].

Section Fold_Left_Recursor.
Variable A B:Type.
Variable f:B->A->B.
Fixpoint fold_left (n:nat) (a:array A n) (s:B) : B :=
match a with
| nil => s
| cons m h t => fold_left m t (f s h)
end.

Lemma fold_left_app: forall (m n:nat) (a:array A m)
(b:array A n) (s:B),
fold_left _ (a++b) s = fold_left _ b (fold_left _ a s).

End Fold_Left_Recursor.
Implicit Arguments fold_left [A B n].

Section Fold_Right_Recursor.
Variable A B:Type.
Variable f:A->B->B.
Fixpoint fold_right (n:nat) (a:array A n) (s:B) : B :=
match a with
| nil => s
| cons m h t => f h (fold_right m t s)
end.

Lemma fold_right_app: forall (m n:nat) (a:array A m)
(b:array A n) (s:B),
fold_right _ (a++b) s = fold_right _ a (fold_right _ b s).

Lemma fold_right_array_from_func_back: forall (n:nat)
(s:B) (g:nat->A),
fold_right _ (array_from_func (S n) g) s=
fold_right _ (array_from_func n g) (f (g n) s).

Lemma fold_right_array_from_funcrange_back: forall (n:nat)
(s:B) (g:{i|i<S n}->A),
fold_right _ (array_from_funcrange (S n) g) s=
fold_right _ (array_from_funcrange n (lowrangt_prevfunc g))
 (f (g (exist _ n (lt_n_Sn n))) s).

End Fold_Right_Recursor.
Implicit Arguments fold_right [A B n].

Theorem ScalarProduct_as_fold: forall (U:Type) (n:nat)
(add prod:Operation U) (zero:U)
(a b:array U n),
ScalarProduct add prod zero a b=
fold_right add (VectorAdd prod a b) zero.

Section Arith.
Variable U:Type.
Variable add prod:Operation U.
Variable zero one:U.

Infix "+" := add.
Infix "*" := prod.
Hypothesis add_comm: Commutativity U add.
Hypothesis add_ass: Associativity U add.
Hypothesis prod_comm: Commutativity U prod.
Hypothesis prod_ass: Associativity U prod.
Hypothesis distributive_left: forall (a b c:U),
a * (b + c)=(a * b) +(a* c).
Hypothesis distributive_right: forall (a b c:U),
(a + b)*c=(a * c) +(b* c).

Hypothesis zeroL: forall (x:U), zero+x=x.
Hypothesis zeroR: forall (x:U), x+zero=x.
Hypothesis oneL: forall (x:U), one*x=x.
Hypothesis oneR: forall (x:U), x*one=x.

Let zerovector (n:nat):=array_homogeneous U n zero.
Let unitvector (n i:nat):=UnitVector n zero one i.
Let dotproduct (n:nat) (a b:array U n):=
 ScalarProduct add prod zero a b.
Implicit Arguments dotproduct [n].
Infix "\u00b7" := dotproduct (at level 45).

Let summatory (n:nat) (f:{k|k<n}->U):=
 fold_right add (array_from_funcrange n f) zero.
Implicit Arguments summatory [n].

Hypothesis prod_zero_l: forall (x:U), zero*x=zero.
Hypothesis prod_zero_r: forall (x:U), x*zero=zero.

Lemma fold_right_add_zero: forall (n:nat) (s:U),
fold_right add (zerovector n) s=s.

Lemma fold_right_add_UnitVector: forall (n i:nat) (v:U), i<n->
fold_right add (UnitVector n zero v i) zero=v.

Lemma fold_right_shift: forall (n:nat) (a:array U n) (s:U),
fold_right add a s=(fold_right add a zero) + s.

Lemma fold_right_add_unit: forall (n i:nat), i<n->
fold_right add (unitvector n i) zero=one.

Lemma VectorAdd_zerovector_l: forall (n:nat) (a:array U n),
VectorAdd add (zerovector n) a=a.

Lemma VectorAdd_zerovector_r: forall (n:nat) (a:array U n),
VectorAdd add a (zerovector n)=a.

Lemma ElementProduct_zero_l: forall (n:nat) (a:array U n),
VectorAdd prod (zerovector n) a=(zerovector n).

Lemma ElementProduct_zero_r: forall (n:nat) (a:array U n),
VectorAdd prod a (zerovector n)=(zerovector n).

Lemma ElementProduct_unit_same: forall (n i:nat), i<n->
VectorAdd prod (unitvector n i) (unitvector n i)=(unitvector n i).

Lemma ElementProduct_unit_diff: forall (n i j:nat)
(Hi:i<n) (Hj:j<n) (Hij:i<>j),
VectorAdd prod (unitvector n i) (unitvector n j)=zerovector n.

Lemma ElementProduct_unit_l: forall (n i:nat)
(a:array U n), i<n->
VectorAdd prod (unitvector n i) a=
UnitVector n zero (nth zero i a) i.

Lemma ElementProduct_unit_r: forall (n i:nat)
(a:array U n), i<n->
VectorAdd prod a (unitvector n i)=
UnitVector n zero (nth zero i a) i.

Lemma ScalarProduct_zero_l: forall (n:nat) (a:array U n),
ScalarProduct add prod zero (zerovector n) a=zero.

Lemma ScalarProduct_zero_r: forall (n:nat) (a:array U n),
ScalarProduct add prod zero a (zerovector n)=zero.

Lemma ScalarProduct_unit_same: forall (n i:nat), i<n->
ScalarProduct add prod zero (unitvector n i) (unitvector n i)=one.

Lemma ScalarProduct_unit_diff: forall (n i j:nat)
(Hi:i<n) (Hj:j<n) (Hij:i<>j),
ScalarProduct add prod zero (unitvector n i) (unitvector n j)=zero.

Lemma ScalarProduct_unit_l: forall (n i:nat) (a:array U n),
i<n->
ScalarProduct add prod zero (unitvector n i) a=
nth zero i a.

Lemma ScalarProduct_unit_r: forall (n i:nat) (a:array U n),
i<n->
ScalarProduct add prod zero a (unitvector n i)=
nth zero i a.

Lemma ScalarProduct_cons: forall (n:nat)
(a b:array U n) (ha hb:U),
(ha::a) \u00b7 (hb::b) = (ha*hb)+(a\u00b7b).

Lemma ScalarProduct_app: forall (m n:nat)
(l1 l2:array U m) (r1 r2:array U n),
(l1++r1)\u00b7(l2++r2)=(l1\u00b7l2)+(r1\u00b7r2).

Theorem summatory_extensionality: forall (n:nat)
(f g:{k|k<n}->U) (EXT:forall m, f m= g m),
summatory f=summatory g.

Lemma summatory0: forall (f:{k|k<0}->U),
summatory f=zero.

Lemma summatoryS: forall (n:nat) (f:{k|k<S n}->U),
summatory f=summatory (lowrangt_prevfunc f)
+ f (exist _ n (lt_n_Sn n)).

Lemma summatory_prod_r: forall (n:nat) (f:{k|k<n}->U) (c:U),
(summatory f)*c=summatory (fun K:{k|k<n}=>f K * c).

Lemma summatory_prod_l: forall (n:nat) (f:{k|k<n}->U) (c:U),
c*(summatory f)=summatory (fun K:{k|k<n}=>c*(f K)).

Lemma summatory_add: forall (n:nat) (f g:{k|k<n}->U),
summatory (fun K:{k|k<n} => f K + g K)=
summatory f + summatory g.

Theorem summatory_swap: forall (m n:nat) (f:{i|i<m}->{j|j<n}->U),
summatory (fun I:{i|i<m}=>summatory (fun J:{j|j<n}=>f I J))=
summatory (fun J:{j|j<n}=>summatory (fun I:{i|i<m}=>f I J)).

Lemma fold_right_VectorProdScalar: forall (n:nat)
(a:array U n) (s:U),
fold_right add (VectorProdScalar prod a s) zero=
(fold_right add a zero)*s.

Lemma fold_right_ScalarProdVector: forall (n:nat)
(a:array U n) (s:U),
fold_right add (ScalarProdVector prod a s) zero=
s*(fold_right add a zero).

Lemma VectorProdScalar_nth_range: forall (n:nat)
(a:array U n) (s:U) (I:{i|i<n}),
nth_range I (VectorProdScalar prod a s)=
nth_range I a* s.

Lemma ScalarProdVector_nth_range: forall (n:nat)
(a:array U n) (s:U) (I:{i|i<n}),
nth_range I (ScalarProdVector prod a s)=
s*nth_range I a.

Lemma summatory_Kronecker_delta_out: forall (n i:nat)
(Hi:i>=n),
summatory (fun J:{j|j<n}=>
let (j,Hj):=J in (Kronecker_delta zero one i j))
=zero.

Lemma summatory_Kronecker_delta: forall (n i:nat)
(Hi:i<n),
summatory (fun J:{j|j<n}=>
let (j,Hj):=J in (Kronecker_delta zero one i j))
=one.

Lemma summatory_fR_Kronecker_delta: forall (n i:nat)
(Hi:i<n) (f:{j|j<n}->U),
summatory (fun J:{j|j<n}=> f J *
let (j,Hj):=J in (Kronecker_delta zero one i j))
=f (exist _ i Hi).

Lemma ScalarProduct_as_summatory: forall (n:nat)
(a b:array U n),
ScalarProduct add prod zero a b=
summatory (fun K:{k|k<n}=>
 (nth_range K a) * (nth_range K b)).

Lemma ScalarProduct_ScalarProdVector_l: forall (n:nat)
(a b:array U n) (s:U),
(ScalarProdVector prod a s)\u00b7b=s*(a\u00b7b).

Lemma ScalarProduct_VectorProdScalar_r: forall (n:nat)
(a b:array U n) (s:U),
a\u00b7(VectorProdScalar prod b s)=(a\u00b7b)*s.

End Arith.

Check VectorAdd_d.
Example ej1: VectorAdd_d nat 2 plus 0 (1::2::nil nat)
 (3::1::nil nat)=4::3::nil nat.

Ltac arraycompute:=
unfold VectorAdd_d;unfold array_from_func;
simpl;repeat rewrite maptype_selfany;simpl.

Example ej2: VectorAdd_d nat 3 plus 0 (1::5::2::nil nat)
 (3::1::22::nil nat)=4::6::24::nil nat.

Example ej3: VectorAdd plus (1::2::nil nat) (3::1::nil nat)
=4::3::nil nat.