FinMatrix.CoqExt.LinearSpace

Require Export Hierarchy.

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable Variables A Aadd Azero Aopp Amul Aone Ainv Adiv Alt Ale
  V Vadd Vzero Vopp Vcmul
  W Wadd Wzero Wopp Wcmul.
Generalizable Variables B Badd Bzero.
Generalizable Variables C Cadd Czero.

Declare Scope VectorSpace_scope.
Delimit Scope VectorSpace_scope with VS.

Open Scope A_scope.
Open Scope VectorSpace_scope.

Section vsum.


  Context {C : Type}.
  Context `{CMonoid : Monoid C Cadd Czero}.


End vsum.

Class VectorSpace `{F : Field} {V : Type} (Vadd : V -> V -> V) (Vzero : V)
  (Vopp : V -> V) (Vcmul : A -> V -> V) := {
    vs_vaddC :: Commutative Vadd;
    vs_vaddA :: Associative Vadd;
    vs_vaddIdR :: IdentityRight Vadd Vzero;
    vs_vaddInvR :: InverseRight Vadd Vzero Vopp;
    vs_vcmul_1_l : forall v : V, Vcmul Aone v = v;
    vs_vcmul_assoc : forall a b v, Vcmul (Amul a b) v = Vcmul a (Vcmul b v);
    vs_vcmul_aadd : forall a b v, Vcmul (Aadd a b) v = Vadd (Vcmul a v) (Vcmul b v);
    vs_vcmul_vadd : forall a u v, Vcmul a (Vadd u v) = Vadd (Vcmul a u) (Vcmul a v);
  }.

Section field_VectorSpace.
  Context `{HField : Field}.
  Add Field field_inst : (make_field_theory HField).

  #[export] Instance field_VectorSpace : VectorSpace Aadd Azero Aopp Amul.
  Proof. split_intro; try field. Qed.
End field_VectorSpace.

Section props.
  Context `{HVectorSpace : VectorSpace}.
  Add Field field_inst : (make_field_theory F).
  Infix "+" := Aadd : A_scope.
  Notation "0" := Azero : A_scope.
  Notation "- a" := (Aopp a) : A_scope.
  Notation Asub a b := (a + -b).
  Infix "-" := Asub : A_scope.
  Infix "*" := Amul : A_scope.
  Notation "1" := Aone : A_scope.
  Notation "/ a" := (Ainv a) : A_scope.
  Notation Adiv := (fun a b => a * (/b)).
  Infix "/" := Adiv : A_scope.

  Infix "+" := Vadd : VectorSpace_scope.
  Notation "0" := Vzero : VectorSpace_scope.
  Notation "- v" := (Vopp v) : VectorSpace_scope.
  Notation Vsub u v := (u + -v).
  Infix "-" := Vsub : VectorSpace_scope.
  Infix "\.*" := Vcmul : VectorSpace_scope.

  #[export] Instance vs_vaddIdL : IdentityLeft Vadd 0.
  Proof. constructor; intros. rewrite commutative, identityRight; auto. Qed.

  #[export] Instance vs_vaddInvL : InverseLeft Vadd 0 Vopp.
  Proof. constructor; intros. rewrite commutative, inverseRight; auto. Qed.

  Lemma vs_vadd_0_l : forall v : V, 0 + v = v.
  Proof. intros. apply identityLeft. Qed.

  Lemma vs_vadd_0_r : forall v : V, v + 0 = v.
  Proof. intros. apply identityRight. Qed.

  Lemma vs_vadd_vopp_l : forall v : V, - v + v = 0.
  Proof. intros. apply inverseLeft. Qed.

  Lemma vs_vadd_vopp_r : forall v : V, v + - v = 0.
  Proof. intros. apply inverseRight. Qed.

  #[export] Instance vs_vadd_AGroup : AGroup Vadd 0 Vopp.
  Proof.
    repeat constructor; intros;
      try apply vs_vaddA;
      try apply vs_vadd_0_l;
      try apply vs_vadd_0_r;
      try apply vs_vadd_vopp_l;
      try apply vs_vadd_vopp_r;
      try apply vs_vaddC.
  Qed.

  Theorem vs_cancel_l : forall u v w, u + v = u + w -> v = w.
  Proof. intros. apply group_cancel_l in H; auto. Qed.

  Theorem vs_cancel_r : forall u v w, v + u = w + u -> v = w.
  Proof. intros. apply group_cancel_r in H; auto. Qed.

  Theorem vs_add_eqR_imply0 : forall u v, u + v = v -> u = 0.
  Proof.
    intros. apply vs_cancel_r with (u:=v). rewrite H.
    pose proof vs_vadd_AGroup. agroup.
  Qed.

  Theorem vs_add_eqL_imply0 : forall u v, u + v = u -> v = 0.
  Proof.
    intros. apply vs_cancel_l with (u:=u). rewrite H.
    pose proof vs_vadd_AGroup. agroup.
  Qed.

  Theorem vs_vzero_uniq_l : forall v0, (forall v, v0 + v = v) -> v0 = 0.
  Proof. intros. apply group_id_uniq_l; auto. Qed.

  Theorem vs_vzero_uniq_r : forall v0, (forall v, v + v0 = v) -> v0 = 0.
  Proof. intros. apply group_id_uniq_r; auto. Qed.

  Theorem vs_vopp_uniq_l : forall v v', v + v' = 0 -> -v = v'.
  Proof. intros. eapply group_opp_uniq_l; auto. Qed.

  Theorem vs_vopp_uniq_r : forall v v', v' + v = 0 -> -v = v'.
  Proof. intros. eapply group_opp_uniq_r; auto. Qed.

  Theorem vs_vcmul_0_l : forall v : V, 0%A \.* v = 0.
  Proof.
    intros. pose proof vs_vadd_AGroup as HAGroup_vadd.
    assert (0%A \.* v + 0%A \.* v = 0%A \.* v + 0).
    - rewrite <- vs_vcmul_aadd. agroup. f_equal. field.
    - apply vs_cancel_l in H. auto.
  Qed.

  Theorem vs_vcmul_0_r : forall a : A, a \.* 0 = 0.
  Proof.
    intros. pose proof vs_vadd_AGroup as HAGroup_vadd.
    assert (a \.* 0 = a \.* 0 + a \.* 0).
    { rewrite <- vs_vcmul_vadd. f_equal. agroup. }
    assert (a \.* 0 = a \.* 0 + 0). agroup.
    rewrite H in H0 at 1. apply vs_cancel_l in H0. auto.
  Qed.

  Theorem vs_sol_l : forall u v w, u + v = w -> u = w + - v.
  Proof. intros. apply group_sol_l; auto. Qed.

  Theorem vs_sol_r : forall u v w, u + v = w -> v = - u + w.
  Proof. intros. apply group_sol_r; auto. Qed.

  Theorem vs_vcmul_opp : forall c v, (- c)%A \.* v = - (c \.* v).
  Proof.
    intros. symmetry. apply vs_vopp_uniq_l; auto.
    rewrite <- vs_vcmul_aadd. rewrite inverseRight, vs_vcmul_0_l; auto.
  Qed.

  Theorem vs_vcmul_vopp : forall c v, c \.* (- v) = - (c \.* v).
  Proof.
    intros. symmetry. apply vs_vopp_uniq_l; auto.
    rewrite <- vs_vcmul_vadd. rewrite inverseRight, vs_vcmul_0_r; auto.
  Qed.

  Theorem vs_vcmul_opp1 : forall v : V, (-(1))%A \.* v = -v.
  Proof. intros. rewrite vs_vcmul_opp, vs_vcmul_1_l; auto. Qed.

  Theorem vs_vsub_self : forall v : V, v - v = 0.
  Proof. intros. pose proof vs_vadd_AGroup as HAGroup_vadd. agroup. Qed.

  Section AeqDec.
    Context {AeqDec : Dec (@eq A)}.

    Theorem vs_vcmul_eq0_imply_k0_or_v0 : forall a v, a \.* v = 0 -> a = 0%A \/ v = 0.
    Proof.
      intros. destruct (Aeqdec a 0%A); auto. right.
      assert (/a \.* (a \.* v) = /a \.* 0) by (rewrite H; auto).
      rewrite <- vs_vcmul_assoc in H0.
      rewrite field_mulInvL in H0; auto.
      rewrite vs_vcmul_1_l, vs_vcmul_0_r in H0. auto.
    Qed.

    Corollary vs_vcmul_neq0_if_neq0_neq0 : forall a v, a <> 0%A -> v <> 0 -> a \.* v <> 0.
    Proof.
      intros. intro. apply vs_vcmul_eq0_imply_k0_or_v0 in H1. destruct H1; auto.
    Qed.
  End AeqDec.

End props.

Class SubSpaceStruct `{HVectorSpace : VectorSpace} (P : V -> Prop) := {
    ss_zero_keep : P Vzero;
    ss_add_closed : forall {u v : sig P}, P (Vadd u.val v.val);
    ss_cmul_closed : forall {a : A} {v : sig P}, P (Vcmul a v.val);
  }.

Definition Hbelong `{ss: SubSpaceStruct} (v : V) : Prop := P v.

Section makeSubSpace.
  Context `{ss : SubSpaceStruct}.

  Notation H := (sig P).

  Definition Hadd (u v : H) : H := exist _ (Vadd u.val v.val) ss_add_closed.
  Definition Hzero : H := exist _ Vzero ss_zero_keep.
  Definition Hopp (v : H) : H.
    refine (exist _ (Vopp v.val) _). rewrite <- vs_vcmul_opp1.
    apply ss_cmul_closed.
  Defined.
  Definition Hcmul (a : A) (v : H) : H := exist _ (Vcmul a v.val) ss_cmul_closed.

  Lemma makeSubSpace : VectorSpace Hadd Hzero Hopp Hcmul.
  Proof.
    repeat constructor; unfold Hadd, Hcmul; intros.
    - apply sig_eq_iff. apply commutative.
    - apply sig_eq_iff. simpl. apply associative.
    - destruct a. apply sig_eq_iff. simpl. apply identityRight.
    - destruct a. apply sig_eq_iff. simpl. apply vs_vadd_vopp_r.
    - destruct v. apply sig_eq_iff. simpl. apply vs_vcmul_1_l.
    - destruct v. apply sig_eq_iff. simpl. apply vs_vcmul_assoc.
    - destruct v. apply sig_eq_iff. simpl. apply vs_vcmul_aadd.
    - destruct v. apply sig_eq_iff. simpl. apply vs_vcmul_vadd.
  Qed.
End makeSubSpace.
Arguments makeSubSpace {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} ss.

Section zero_SubSpace.
  Context `{HVectorSpace : VectorSpace}.

  Instance zero_SubSpaceStruct : SubSpaceStruct (fun v => v = Vzero).
  Proof.
    constructor; auto.
    - intros. rewrite u.prf, v.prf. apply vs_vadd_0_l.
    - intros. rewrite v.prf. apply vs_vcmul_0_r.
  Qed.

  #[export] Instance zero_SubSpace : VectorSpace Hadd Hzero Hopp Hcmul :=
    makeSubSpace zero_SubSpaceStruct.
End zero_SubSpace.

Section self_SubSpace.
  Context `{HVectorSpace : VectorSpace}.

  Instance self_SubSpaceStruct : SubSpaceStruct (fun v => True).
  Proof. constructor; auto. Qed.

  #[export] Instance self_SubSpace : VectorSpace Hadd Hzero Hopp Hcmul :=
    makeSubSpace self_SubSpaceStruct.

End self_SubSpace.