Library Kn

Require Import Aux List Setoid Field VectorSpace.

Section Kn.

Variable p : params.
Hypothesis Hp : fparamsProp p.

We recover the usual mathematical notation

Notation "'K'" := (K p).

Delimit Scope kn_scope with k.
Open Scope vector_scope.
Open Scope kn_scope.

A vector is a list of length n

We first build the functions of the vector space

Equality of two vectors as list

Generate the constant k for the dimension n

Notation " [ k ] " := (genk _ k) (at level 10): kn_scope.

Adding two vectors as list

Multiplication by a scalar

Canonical Structure vn_eparams (n: nat) :=
  Build_eparams (kn n) K (genk n 0%f) (eq n) (add n) (scal n).

Definition fn n : vparamsProp (vn_eparams n).
Qed.

Hint Resolve fn.

Ltac Kfold n :=
     change (add n) with (addE (vn_eparams n));
     change (scal n) with (scalE (vn_eparams n));
     change (genk n 0%f) with (E0 (vn_eparams n)).

scal is integral

Lemma scal_integral n k (x: kn n) : k .* x = 0 -> k = 0%f \/ x = 0.

Lemma genk_inj n k1 k2 : [k1] = [k2] :> kn n.+1 -> k1 = k2.

Lemma genk0_dec n (x: kn n) : x = 0 \/ x <> 0.

Conversion from list to kn

Fixpoint kn2l (n : nat) : kn n -> list K :=
  match n return (kn n -> list K) with
  | 0 => fun x => nil
  | S n1 => fun v => let (a, v1) := v in a :: kn2l n1 v1
  end.

Lemma kn2ll2knE n x : l2kn n (kn2l n x) = x.

Lemma genk_id0 n i : In i (kn2l n (genk n 0%f)) -> i = 0%f.

Inductive eql_t0 : list K -> list K -> Prop :=
  eql_t0N: eql_t0 nil nil
| eql_t0Nl: forall l, eql_t0 l nil -> eql_t0 (0%f :: l) nil
| eql_t0Nr: forall l, eql_t0 nil l -> eql_t0 nil (0%f :: l)
| eql_t0R: forall a l1 l2, eql_t0 l1 l2 -> eql_t0 (a :: l1) (a :: l2).

Hint Constructors eql_t0.

Lemma eql_refl l : eql_t0 l l.

Lemma eql_sym l1 l2 : eql_t0 l1 l2 -> eql_t0 l2 l1.

Lemma eql_trans l2 l1 l3 : eql_t0 l1 l2 -> eql_t0 l2 l3 -> eql_t0 l1 l3.

Lemma dmap2_eql a l1 l2 l3 :
  eql_t0 l2 l3 ->
  eql_t0 (dmap2 (multK K) a l1 l2) (dmap2 (multK K) a l1 l3).

Lemma kn2l_0 n : eql_t0 (kn2l n 0) nil.

Generate the p element of the base in dimension n

Notation " 'e_ p" := (gen _ p) (at level 70): kn_scope.

Lemma gen_inj n p1 p2 : p1 < n -> p2 < n ->
'e_p1 = ('e_p2 : kn n) -> p1 = p2.

Lemma kn2l_e0 n : eql_t0 (kn2l n.+1 ('e_0)) (1%f :: nil).

Lemma kn2l_ei n i :
eql_t0 (kn2l n.+1 ('e_i .+1)) (0%f :: kn2l n ('e_i)).

Definition lift (n: nat) (v: kn n) : (kn (S n)) := (0%f, v).

Lemma lift0 n : lift n 0 = 0.

Lift of generator of the base

Lemma lift_e : forall n i, 'e_(S i) = lift n ('e_i).

Lift on add

Lemma lift_add n x y : lift n (x + y) = lift n x + lift n y.

Lift on scalar multiplication

Lemma lift_scal n k x : lift n (k .* x) = scalE (vn_eparams (S n)) k (lift n x).

Lift on the multiple product

Lemma lift_mprod (n: nat) ks vs : ks *X * map (lift n) vs =
lift n (mprod (vn_eparams n) ks vs).

The base as the list of all the generators

Each generator is in the base

Lemma e_in_base n i : i < n -> In ('e_i) (base n).

An element of the base is a generator

Lemma e_in_base_ex n v :
In v (base n) -> exists p1, p1 < n /\ v = 'e_p1.

The length of the base is n

Lemma base_length n : length (base n) = n.

The base is free

Lemma base_free n : free _ (base n).

Lemma k2l_mprod n (v: kn n) : kn2l n v *X * base n = v.

Every vector is a linear combination of the base

Lemma cbl_base n v : cbl _ (base n) v.

Lemma kn_induct n (P: kn n -> Prop) :
     P 0 ->
     (forall p, p < n -> P ('e_p)) ->
     (forall v1 v2, P v1 -> P v2 -> P (v1 + v2)) ->
     (forall k v, P v -> P (k .* v)) ->
     (forall x, P x).

Coordinates for k vector

Fixpoint proj (n: nat) k : (kn n) -> K :=
  match n return kn n -> K with
  | O => fun _ => 0%f
  | S n1 => fun l => let (a,l1) := l in
          match k with | O => a | S k1 =>
           proj n1 k1 l1
          end
  end.

Lemma proj0 n i : proj n i 0 = 0%f.

Lemma proj_e n i j : j < n ->
  proj n i ('e_j) = if (i ?= j)%nat then 1%f else 0%f.

Lemma proj_scal n i k x : proj n i (k .* x) = (k * proj n i x)%f.

Lemma proj_add n i x y :
proj n i (x + y) = (proj n i x + proj n i y)%f.

Fixpoint pscal (n: nat): (kn n) -> (kn n) -> K :=
  match n return kn n -> kn n -> K with
  | O => fun a b => 0%f
  | S n1 => fun l1 l2 => let (a,l3) := l1 in let (b,l4) := l2 in
                         (a * b + pscal n1 l3 l4)%f
  end.

Notation "a [.] b" := (pscal _ a b) (at level 40): kn_scope.

Lemma pscal0l n (x: kn n) : 0 [.] x = 0%f.

Lemma pscal0r n (x: kn n) : x [.] 0 = 0%f.

Lemma pscal_com n (x y: kn n) : x [.] y = y [.] x.

Lemma pscal_e n (i j: nat) : i < n -> j < n ->
  ('e_i: kn n) [.] ('e_j ) = if (i ?= j)%nat then 1%f else 0%f.

Lemma pscal_scall n k (x y: kn n) :
  (k .* x) [.] y = (k * (x [.] y))%f.

Lemma pscal_scalr n k (x y: kn n) :
  x [.] (k .* y) = (k * (x [.] y))%f.

Lemma pscal_addl n (x y z: kn n) :
  (x + y) [.] z = (x [.] z + (y [.] z))%f.

Lemma pscal_addr n (x y z: kn n) :
  z [.] (x + y) = (z [.] x + (z [.] y))%f.

Our final vector

Definition Kn := kn p.
Definition K0 := genk p 0%f.
Definition Keq: Kn -> Kn -> bool := eq p.
Definition Kadd: Kn -> Kn -> Kn := add p.
Definition Kscal: K -> Kn -> Kn := scal p.
Definition Kproj: nat -> Kn -> K := proj p.
Definition Ksprod: Kn -> Kn -> K := pscal p.
Definition Kgen := gen p.

Canonical Structure v_eparams :=
Build_eparams Kn K K0 Keq Kadd Kscal.
Definition f : vparamsProp v_eparams := fn p.

Prod of two vectors as list

Fixpoint kprod (n : nat) : kn n -> kn n -> kn n :=
  match n with
  | 0%nat => fun a b => tt
  | S n1 =>
      fun l1 l2 =>
      let (v1, l3) := l1 in
      let (v2, l4) := l2 in ((v1 * v2)%f, kprod n1 l3 l4)
  end.

Local Notation "a [*] b" := (kprod _ a b) (at level 40).

Lemma kprod0l n a : 0 [*] a = 0 :> kn n.

Lemma kprod0r n a : a [*] 0 = 0 :> kn n.

Lemma kprodkl n k a : [k] [*] a = k .* a :> kn n.

Lemma kprodkr n k a : a [*] [k] = k .* a :> kn n.

Lemma kprod1l n a : [1%f] [*] a = a :> kn n.

Lemma kprod1r n a : a [*] [1%f] = a :> kn n.

Lemma kprod_addl n a b c :
  (a + b) [*] c = a [*] c + b [*] c :> kn n.

Lemma kprod_addr n a b c :
  a [*] (b + c) = a [*] b + a [*] c :> kn n.

Lemma kprod_scall n k a b :
  (k .* a) [*] b = k .* (a [*] b) :> kn n.

Lemma kprod_scalr n k a b :
  a [*] (k .* b) = k .* (a [*] b) :> kn n.

Lemma kprod_assoc n a b c :
  (a [*] b) [*] c = a [*] (b [*] c) :> kn n.

End Kn.

Notation " 'e_ p" := (gen _ _ p) (at level 8) : Kn_scope.
Notation " [ k ] " := (genk _ _ k) (at level 9) : Kn_scope.
Notation "a [.] b" := (pscal _ _ a b) (at level 40): Kn_scope.
Notation "a [*] b" := (kprod _ _ a b) (at level 40): Kn_scope.

Delimit Scope Kn_scope with Kn.

Hint Constructors eql_t0.