Finite_dim_MS_lin_indep.v

(**
This file is part of the Coq Numerical Analysis library

Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(**

 * Brief description

 Support for linear independent finite families in module spaces.

 * Description

 For results that are only valid when the ring of scalars is commutative, or
 being ordered, see [Algebra.Finite_dim.Finite_dim_MS_lin_indep_R] where they
 are only stated in the case of the ring of real numbers [R_Ring].

 * Bibliography

 #<DIV><A NAME="GostiauxT1"></A></DIV>#
 [[GostiauxT1]]
 Bernard Gostiaux,
 Cours de mathématiques spéciales - 1. Algèbre,
 Mathématiques, Presses Universitaires de France, Paris, 1993,
 #<A HREF="https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre">#
 https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre#</A>#.

 * Usage

 This module may be used through the import of
 [Algebra.Finite_dim.Finite_dim_MS], [Algebra.Finite_dim.Finite_dim],
 [Algebra.Algebra], or [Algebra.Algebra_wDep], where it is exported.
*)

From Requisite Require Import stdlib ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring ModuleSpace.
From Algebra Require Import Finite_dim_MS_def.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.


Section Linear_independent_Facts.

(** Properties of lin_dep/lin_indep. *)

Context {K : Ring}.
Hypothesis HK : nonzero_struct K.
Context {E : ModuleSpace K}.

Lemma lin_dep_ex :
  forall {n} {B : 'E^n}, lin_dep B <-> exists L, lin_comb L B = 0 /\ L <> 0.
Proof.
intros n B; split; intros HB.
destruct (not_all_ex_not _ _ HB) as [L HL]; exists L; apply imply_to_and; easy.
destruct HB as [L [HL1 HL2]]; apply ex_not_not_all; exists L; intros; auto.
Qed.

(** Establish first the property on lin_dep. *)

Lemma lin_dep_with_zero : forall {n} {B : 'E^n}, inF 0 B -> lin_dep B.
Proof.
intros n B [i Hi]; apply lin_dep_ex; exists (kron i); split.
rewrite lc_l_kron_r; easy.
apply nextF; exists i; rewrite kron_is_1; try easy.
apply one_not_zero; easy.
Qed.

Lemma lin_dep_S_zero : forall {n}, lin_dep (0 : 'E^n.+1).
Proof. intros; apply lin_dep_with_zero; exists ord0; easy.  Qed.

Lemma lin_dep_zero_rev : forall {n}, lin_dep (0 : 'E^n) -> (0 < n)%coq_nat.
Proof.
move=>> /lin_dep_ex [L [_ /nextF_rev [i _]]].
apply Nat.neq_0_lt_0; contradict i; rewrite i; intros [j Hj]; easy.
Qed.

Lemma lin_dep_zero_equiv : forall {n}, lin_dep (0 : 'E^n) <-> (0 < n)%coq_nat.
Proof.
intros n; split; [apply lin_dep_zero_rev |].
destruct n as [| n]; try easy; intros _; apply lin_dep_S_zero.
Qed.

Lemma lin_dep_not_injF : forall {n} {B : 'E^n}, ~ injective B -> lin_dep B.
Proof.
move=> n B /not_all_ex_not [i0 /not_all_ex_not [i1 H]].
destruct n; try now destruct i0.
apply imply_to_and in H; destruct H as [HB Hi]; apply not_eq_sym in Hi.
destruct n; try now rewrite 2!ord_one in Hi.
rewrite lin_dep_ex; exists (kron i0 - kron i1); split.
(* *)
rewrite lc_plus_l lc_opp_l 2!lc_l_kron_r -HB.
apply: minus_eq_zero.
(* *)
apply nextF; exists i0.
rewrite -> fct_minus_eq, kron_is_1, kron_is_0; try easy.
rewrite minus_zero_r; apply one_not_zero; easy.
apply ord_neq_compat; easy.
Qed.

Lemma lin_dep_castF_compat :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep B1 -> lin_dep (castF H B1).
Proof.
intros n1 n2 H B1; rewrite 2!lin_dep_ex.
intros [L [HL HL0]]; exists (castF H L); split; try now rewrite lc_castF.
contradict HL0; apply (castF_zero_reg H); easy.
Qed.

Lemma lin_dep_castF_reg :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep (castF H B1) -> lin_dep B1.
Proof.
intros n1 n2 H B1 HB; rewrite -(castF_can _ (eq_sym H) B1).
apply lin_dep_castF_compat; easy.
Qed.

Lemma lin_dep_castF_equiv :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_dep (castF H B1) <-> lin_dep B1.
Proof.
intros; split. apply lin_dep_castF_reg. apply lin_dep_castF_compat.
Qed.

Lemma lin_dep_concatF_compat_l :
  forall {n1 n2} {B1 : 'E^n1} (B2 : 'E^n2),
    lin_dep B1 -> lin_dep (concatF B1 B2).
Proof.
move=>>; rewrite 2!lin_dep_ex; intros [L HL]; exists (concatF L 0); split.
rewrite lc_concatF_zero_lr; easy.
apply concatF_zero_nextF_compat_l; easy.
Qed.

Lemma lin_dep_concatF_compat_r :
  forall {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    lin_dep B2 -> lin_dep (concatF B1 B2).
Proof.
move=>>; rewrite 2!lin_dep_ex; intros [L HL]; exists (concatF 0 L); split.
rewrite lc_concatF_zero_ll; easy.
apply concatF_zero_nextF_compat_r; easy.
Qed.

Lemma lin_dep_concatF_not_disjF :
  forall {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2} x,
    inF x B1 -> inF x B2 -> lin_dep (concatF B1 B2).
Proof.
intros n1 n2 B1 B2 x [i1 Hx1] [i2 Hx2]; apply lin_dep_not_injF.
assert (Hf : (first_ord n2 i1 < n1)%coq_nat) by now apply /ltP; simpl.
assert (Hl : ~ (last_ord n1 i2 < n1)%coq_nat)
    by (apply Nat.nlt_ge; apply /leP; apply leq_addr).
apply ex_not_not_all; exists (first_ord n2 i1).
apply ex_not_not_all; exists (last_ord n1 i2).
rewrite not_imp_and_equiv; split; try apply ord_neq; auto with zarith.
rewrite concatF_correct_l concat_l_first
    concatF_correct_r concat_r_last -Hx1; easy.
Qed.

Lemma lin_dep_insertF_compat :
  forall {n} i0 x0 {B : 'E^n}, lin_dep B -> lin_dep (insertF i0 x0 B).
Proof.
intros n i0 x0 B; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]].
exists (insertF i0 0 L); split.
rewrite lc_insertF scal_zero_l HL plus_zero_l; easy.
apply nextF; exists (skip_ord i0 i); rewrite insertF_correct; easy.
Qed.

Lemma lin_dep_skipF_reg :
  forall {n} i0 {B : 'E^n.+1}, lin_dep (skipF i0 B) -> lin_dep B.
Proof.
intros n i0 B; rewrite -{2}(insertF_skipF i0 B).
apply lin_dep_insertF_compat.
Qed.

Lemma lin_dep_line :
  forall {n} {B : 'E^n} {i j}, i <> j -> line (B i) (B j) -> lin_dep B.
Proof.
move=> n B i j Hi /lin_span_EX [Lj HLj]; apply lin_dep_ex;
    exists (kron j - scal (Lj ord0) (kron i)); split.
(* *)
rewrite lc_minus_l lc_scal_l 2!lc_l_kron_r HLj.
rewrite lc_1; apply: minus_eq_zero.
(* *)
apply nextF; exists j.
rewrite -> fct_minus_eq, fct_scal_r_eq, kron_is_1, kron_is_0; try easy.
rewrite scal_zero_r minus_zero_r; apply one_not_zero; easy.
intros; contradict Hi; apply ord_inj; easy.
Qed.

Lemma lin_dep_plane :
  forall {n} {B : 'E^n} {i j k},
    i <> k -> j <> k -> plane (B i) (B j) (B k) -> lin_dep B.
Proof.
move=> n B i j k Hi Hj /lin_span_EX [Lk HLk]; apply lin_dep_ex;
  exists (kron k
      - scal (Lk ord0) (kron i) - scal (Lk ord_max) (kron j)); split.
(* *)
rewrite 2!lc_minus_l 2!lc_scal_l 3!lc_l_kron_r HLk.
rewrite lc_2 coupleF_0 coupleF_1; apply: minus2_eq_zero.
(* *)
apply nextF; exists k.
rewrite -> 2!fct_minus_eq, 2!fct_scal_r_eq,
    kron_is_1, 2!kron_is_0; try apply ord_neq_compat; try easy.
rewrite 2!scal_zero_r 2!minus_zero_r; apply one_not_zero; easy.
Qed.

Lemma lin_indep_without_zero : forall {n} {B : 'E^n}, lin_indep B -> ~ inF 0 B.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_with_zero. Qed.

Lemma lin_indep_zero_rev : forall {n}, lin_indep (0 : 'E^n) -> n = O.
Proof.
intros n; rewrite -Nat.le_0_r -Nat.nlt_ge contra_not_r_equiv.
destruct n as [| n]; try easy; intros _; apply lin_dep_S_zero.
Qed.

Lemma lin_indep_zero_equiv : forall {n}, lin_indep (0 : 'E^n) <-> n = O.
Proof.
move=>>; rewrite -Nat.le_0_r -Nat.nlt_ge iff_not_r_equiv.
apply lin_dep_zero_equiv.
Qed.

Lemma lin_indep_nil_or_nonzero :
  forall {n} (B : 'E^n), lin_indep B -> n = O \/ B <> 0.
Proof.
intros [| n]; [intros; left; easy |].
move=>> HB; right; contradict HB; rewrite HB; apply lin_dep_S_zero.
Qed.

Lemma lin_indep_S_nonzero : forall {n} {B : 'E^n.+1}, lin_indep B -> B <> 0.
Proof. move=>> /lin_indep_nil_or_nonzero [H | H]; easy. Qed.

Lemma lin_indep_nonnil_or_zero :
  forall {n} (B : 'E^n), lin_indep B -> (0 < n)%coq_nat \/ B = 0.
Proof.
intros [| n]; [intros; right; apply hat0F_eq; easy |].
move=>>; left; auto with arith.
Qed.

Lemma lin_indep_nonnil :
  forall {n} (B : 'E^n), lin_indep B -> B <> 0 -> (0 < n)%coq_nat.
Proof. move=>> /lin_indep_nonnil_or_zero [H | H]; easy. Qed.

Lemma lin_indep_nonnil_nonzero_equiv :
  forall {n} (B : 'E^n), lin_indep B -> (0 < n)%coq_nat <-> B <> 0.
Proof.
intros n B HB; apply iff_sym; split; [apply lin_indep_nonnil; easy |].
destruct n as [| n]; try easy; intros _; apply lin_indep_S_nonzero; easy.
Qed.

Lemma lin_indep_nil_zero_equiv :
  forall {n} (B : 'E^n), lin_indep B -> n = O <-> B = 0.
Proof.
intros; rewrite -Nat.le_0_r iff_not_equiv Nat.nle_gt.
apply lin_indep_nonnil_nonzero_equiv; easy.
Qed.

Lemma lin_indep_injF : forall {n} {B : 'E^n}, lin_indep B -> injective B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_not_injF. Qed.

Lemma lin_indep_castF_compat :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep B1 -> lin_indep (castF H B1).
Proof. move=>>; apply contra_equiv, lin_dep_castF_reg. Qed.

Lemma lin_indep_castF_reg :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep (castF H B1) -> lin_indep B1.
Proof. move=>>; apply contra_equiv, lin_dep_castF_compat. Qed.

Lemma lin_indep_castF_equiv :
  forall {n1 n2} (H : n1 = n2) {B1 : 'E^n1},
    lin_indep (castF H B1) <-> lin_indep B1.
Proof. move=>>; apply iff_not_equiv, lin_dep_castF_equiv. Qed.

Lemma lin_indep_concatF_reg_l :
  forall {n1 n2} {B1 : 'E^n1} (B2 : 'E^n2),
    lin_indep (concatF B1 B2) -> lin_indep B1.
Proof. move=>>; apply contra_equiv; apply lin_dep_concatF_compat_l. Qed.

Lemma lin_indep_concatF_reg_r :
  forall {n1 n2} (B1 : 'E^n1) {B2 : 'E^n2},
    lin_indep (concatF B1 B2) -> lin_indep B2.
Proof. move=>>; apply contra_equiv; apply lin_dep_concatF_compat_r. Qed.

Lemma lin_indep_concatF_disjF :
  forall {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2} x,
    lin_indep (concatF B1 B2) -> ~ inF x B1 \/ ~ inF x B2.
Proof.
move=>>; rewrite -not_and_equiv contra_not_r_equiv.
intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy].
Qed.

Lemma lin_indep_insertF_reg :
  forall {n} i0 x0 {B : 'E^n}, lin_indep (insertF i0 x0 B) -> lin_indep B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed.

Lemma lin_indep_skipF_compat :
  forall {n} i0 {B : 'E^n.+1}, lin_indep B -> lin_indep (skipF i0 B).
Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed.

Lemma lin_indep_not_line :
  forall {n} {B : 'E^n},
    lin_indep B -> forall i j, i <> j -> ~ line (B i) (B j).
Proof.
move=>> HB; move=>> Hi H; contradict HB;
    eapply lin_dep_line; [apply Hi | apply H].
Qed.

Lemma lin_indep_not_plane :
  forall {n} {B : 'E^n},
    lin_indep B -> forall i j k, i <> k -> j <> k -> ~ plane (B i) (B j) (B k).
Proof.
move=>> HB; move=>> Hi Hj H; contradict HB;
    eapply lin_dep_plane; [apply Hi | apply Hj | apply H].
Qed.

(** Establish first the property on lin_indep. *)

Lemma lin_indep_coupleF_sym :
  forall (x0 x1 : E), lin_indep (coupleF x0 x1) -> lin_indep (coupleF x1 x0).
Proof.
move=>> H L; rewrite (coupleF_correct L) lc_coupleF; intros HL.
apply coupleF_zero_compat. apply (coupleF_zero_reg_r (L ord_max)).
2: apply (coupleF_zero_reg_l _ (L ord0)).
all: apply H; rewrite lc_coupleF plus_comm; easy.
Qed.

Lemma lin_indep_concatF_sym :
  forall {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
    lin_indep (concatF B1 B2) -> lin_indep (concatF B2 B1).
Proof.
move=>> H L; specialize (H (concatF (lastF L) (firstF L))); revert H.
rewrite lc_concatF lc_splitF_l plus_comm; intros H HL.
specialize (H HL); apply concatF_zero_reg in H; apply splitF_zero_reg; easy.
Qed.

Lemma lin_indep_decomp_uniq : forall {n} {B : 'E^n}, lin_indep B -> lc_injL B.
Proof.
move=>> HB =>> /minus_zero_compat HL.
apply minus_zero_reg, HB; rewrite lc_minus_l; easy.
Qed.

Lemma lin_indep_decomp_uniq_rev :
  forall {n} {B : 'E^n}, lc_injL B -> lin_indep B.
Proof. intros n B HB L HL; apply HB; rewrite (lc_zero_compat_l 0); easy. Qed.

Lemma lin_indep_decomp_uniq_equiv :
  forall {n} {B : 'E^n}, lin_indep B <-> lc_injL B.
Proof.
intros; split; [apply lin_indep_decomp_uniq | apply lin_indep_decomp_uniq_rev].
Qed.

Lemma lin_indep_nil : forall (B : 'E^0), lin_indep B.
Proof. intros B L HL; extF i; destruct i; easy. Qed.

Lemma lin_indep_permutF :
  forall {n} {p} {B : 'E^n},
    bijective p -> lin_indep B -> lin_indep (permutF p B).
Proof.
intros n p B Hp HB L; rewrite {1}(permutF_f_inv_r Hp L) lc_permutF;
    try now apply bij_inj.
move=> /HB /extF_rev HL; extF i.
specialize (HL (p i)); rewrite zeroF in HL; rewrite zeroF -HL.
unfold permutF; rewrite f_inv_can_l; easy.
Qed.

Lemma lin_indep_permutF_equiv :
  forall {n} {p} {B : 'E^n},
    bijective p -> lin_indep (permutF p B) <-> lin_indep B.
Proof.
intros n p B Hp; split; [| apply lin_indep_permutF; easy].
inversion Hp as [q Hq1 Hq2]; rewrite -{2}(permutF_can Hq2 B).
apply lin_indep_permutF, (Bijective Hq2 Hq1).
Qed.

Lemma lin_dep_coupleF_sym :
  forall (x0 x1 : E), lin_dep (coupleF x0 x1) -> lin_dep (coupleF x1 x0).
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed.

Lemma lin_dep_concatF_sym :
  forall {n1 n2} {B1 : 'E^n1} {B2 : 'E^n2},
    lin_dep (concatF B1 B2) -> lin_dep (concatF B2 B1).
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_concatF_sym. Qed.

Lemma lin_dep_not_uniq_decomp :
  forall {n} {B : 'E^n}, lin_dep B -> ~ lc_injL B.
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_decomp_uniq_rev. Qed.

Lemma lin_dep_not_uniq_decomp_rev :
  forall {n} {B : 'E^n}, ~ lc_injL B -> lin_dep B.
Proof. move=>>; rewrite -contra_equiv; apply lin_indep_decomp_uniq. Qed.

Lemma lin_dep_not_uniq_decomp_equiv :
  forall {n} {B : 'E^n}, lin_dep B <-> ~ lc_injL B.
Proof. move=>>; apply not_iff_compat, lin_indep_decomp_uniq_equiv. Qed.

Lemma lin_dep_nonnil : forall {n} (B : 'E^n), lin_dep B -> (0 < n)%coq_nat.
Proof.
move=>>; rewrite contra_not_l_equiv Nat.nlt_ge Nat.le_0_r.
intros; subst; apply lin_indep_nil.
Qed.

(** Mixed properties of lin_dep/lin_indep. *)

(**
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (=>) *)
Lemma lin_dep_insertF :
  forall {n} i0 {x0} {B : 'E^n}, lin_span B x0 -> lin_dep (insertF i0 x0 B).
Proof.
intros n i0 x0 B [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split.
rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l.
rewrite -(insertF_zero i0); apply insertF_nextF_compat_l.
apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy.
Qed.

Lemma lin_indep_insertF_rev :
  forall {n} i0 {x0} {B : 'E^n},
    lin_indep (insertF i0 x0 B) -> ~ lin_span B x0.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed.

End Linear_independent_Facts.


Section Linear_independent_Euclidean_space_Facts.

Context {K : Ring}.
Context {d : nat}.
Hypothesis Hd : d = 0.

Lemma FT0_lin_indep : lin_indep (singleF ((fun=> 1) : FTd K d)).
Proof.
intros L; rewrite lc_1 singleF_0 scal_const; intros HL; extF.
move: HL => /fun_ext_rev; apply (spec_hyp 0);
    rewrite scal_eq_K mult_one_r ord_one; easy.
Qed.

Lemma FT0_dual_lin_indep : lin_indep (singleF (fun f : FTd K d => f 0)).
Proof.
move=> L; rewrite lc_1 singleF_0; intros HL; extF.
move: HL => /fun_ext_rev; apply (spec_hyp 1);
    rewrite fct_scal_eq scal_eq_K mult_one_r ord_one; easy.
Qed.

End Linear_independent_Euclidean_space_Facts.


Section Linear_independent_sub_Facts1a.

(** Properties of lin_indep on sub-module spaces. *)

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E -> Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.

Context {n : nat}.
Context {B : 'E^n}.
Hypothesis HB : inclF B PE.
Let B_ms : 'PE_ms^n := fun i => mk_sub (HB i).

Lemma lin_indep_sub : lin_indep B -> lin_indep B_ms.
Proof.
intros HB1 L HL; apply HB1;
    rewrite mk_sub_lc in HL; apply mk_sub_inj in HL; easy.
Qed.

Lemma lin_indep_sub_rev : lin_indep B_ms -> lin_indep B.
Proof. intros HB1 L HL; apply HB1; apply val_inj; rewrite val_lc; easy. Qed.

Lemma lin_indep_sub_equiv : lin_indep B_ms <-> lin_indep B.
Proof. split; [apply lin_indep_sub_rev | apply lin_indep_sub]. Qed.

End Linear_independent_sub_Facts1a.


Section Linear_independent_sub_Facts1c.

(** More properties of lin_indep on sub-module spaces. *)

Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {PE : E -> Prop}.
Hypothesis HPE : compatible_ms PE.
Let PE_ms := sub_ModuleSpace HPE.

Context {n : nat}.
Context {B_ms : 'PE_ms^n}.
Let B := mapF val B_ms.

Lemma lin_indep_val : lin_indep B_ms -> lin_indep B.
Proof.
rewrite -(lin_indep_sub_equiv HPE (in_subF B_ms)) -(mk_subF_eq B_ms); easy.
Qed.

Lemma lin_indep_val_rev : lin_indep B -> lin_indep B_ms.
Proof. rewrite (mk_subF_eq B_ms) (lin_indep_sub_equiv HPE); easy. Qed.

Lemma lin_indep_val_equiv : lin_indep B <-> lin_indep B_ms.
Proof. rewrite (mk_subF_eq B_ms) (lin_indep_sub_equiv HPE); easy. Qed.

End Linear_independent_sub_Facts1c.