Add LoadPath "./interval".

Require Import Fourier Rdefinitions Raxioms RIneq Rbasic_fun.
Require Import  ssreflect ssrbool ssrnat eqtype ssrfun seq fintype finfun matrix
   bigops ssralg.
Require Import Rstruct min_max topology interval_R 
  real_matrix.

Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Open Scope R_scope.
Delimit Scope R_scope with Re.

Open Scope ring_scope.
Delimit Scope ring_scope with Ri.


Section ClassicLogic.

Lemma iff_not:
forall (p q: Prop), (p <-> q) <-> (~ p <-> ~ q).
Proof.
move=> p q; split; [intuition|].
have H1:  (~ p <-> ~ q) -> (~ (~ p) <-> ~(~q)).
 by intuition.
have H2 :forall p, ~ ~ p <-> p.
move=> r; split; [apply NNPP|intuition].
by move: H1; rewrite !H2 => H1.
Qed.

End ClassicLogic.
 

Section MatIntDef.

Variable m n p: nat.

Definition minf (A: 'M_(m,n)) := map_mx inf A.

Definition msup (A : 'M_(m,n)):= map_mx sup A.

Definition mmid (A : 'M_(m,n)) := map_mx mid A.

Definition mrad (A : 'M_(m,n)):= map_mx rad A.

Definition mmag (A : 'M_(m,n)):= map_mx mag A.

Definition madd_i (A B: matrix closedInt m n):=
  \matrix_(i < m, j < n) add_i (A i j) (B i j).

Definition mopp_i (A: matrix closedInt m n) := map_mx opp_i A.


Definition mmul_i (A: 'M_(m, n)) (B: 'M_(n, p)):=
   \matrix_(i, k) \big[add_i/R0:closedInt]_j mul_i (A i j) (B j k). 

(*Definition mvmul_i (A : matrix closedInt m n) (x: vec closedInt n):= 
  \vec_(i < m)  \big[add_i/ R0:closedInt]_j mul_i (A i j) (x j).*)

Definition mmuls_i (A : matrix closedInt m n) (r: 'M_(n,p)):= 
  \matrix_(i, k)  \big[add_i/ R0:closedInt]_j muls_i  (r j k) (A i j).

(* interval matrix view as a set of real matrices *)
Definition inSetmb (A: matrix closedInt m n) (vA: matrix R m n) :=
  forallb i, forallb j, vA i j \in A i j.

Definition inSetm p q (A: matrix closedInt p q) (vA: matrix R p q) :=
  forall i j, vA i j \in A i j.

Definition sigma_sol (A: 'M_(m, n)) (b: 'cV_m) :=
  fun  x => 
    exists vA: 'M_(m, n), inSetm A vA /\ 
    exists vb: 'cV_m, inSetm b vb /\  vA *m x = vb.


(* we need to talk about the set of solutions of an interval equation (system) *)

End MatIntDef.


Section MatIntProp.

Variable m n p: nat.

Lemma madd_i_correct:
   forall (A: 'M_(m, n)) B a b, inSetm A a-> inSetm B b -> inSetm (madd_i A B) (a+b ) .
by move=> A B a b Ha Hb i j; rewrite !mxE; apply add_i_correct. Qed.

Lemma big_add_i_correct:
  forall V v, @inSetm n 1 V v ->  
  (\big[+%R/R0]_i v i ord0) \in (\big[add_i/R0:closedInt]_i V i ord0).
Proof.
move=> V v Hv.
elim: index_enum.
by rewrite !big_nil in_int /=; split; right.
move => x s IH.
rewrite !big_cons.
apply add_i_correct; first by done.
case S:(Nil _ !=s); first by apply: IH.
by move/eqP:S => S; rewrite -S !big_nil; rewrite in_int /=; split; right.
Qed.

Lemma big_add_i_fun_correct:
  forall (V: 'I_n -> closedInt) v, (forall i: 'I_n, v i \in V i) ->  
  (\big[+%R/R0]_i v i) \in (\big[add_i/R0:closedInt]_i V i).
Proof.
move=> V v Hv.
elim: index_enum.
by rewrite !big_nil in_int /=; split; right.
move => x s IH.
rewrite !big_cons.
apply add_i_correct; first by done.
case S:(Nil _ !=s); first by apply: IH.
by move/eqP:S => S; rewrite -S !big_nil; rewrite in_int /=; split; right.
Qed.


Lemma mopp_i_correct:
  forall (V: 'M_(m, n)) v, inSetm V v -> inSetm (mopp_i V) (- v ) .
by move=> V v Hv i j; rewrite !mxE; apply opp_i_correct. Qed.

Lemma mmul_i_correct:
  forall (A: 'M_(m, n)) (V: 'cV_n) a v, 
  inSetm A a -> inSetm V v -> inSetm (mmul_i A V) (a *m v).
move=> A V a v Ha Hv i j;  rewrite !mxE.
by apply:  big_add_i_fun_correct=> k; apply: mul_i_correct.
Qed.


Lemma mmuls_i_correct:
  forall (A: 'M_(m, n)) a (v: 'cV_n), inSetm A a ->  inSetm (mmuls_i A v) (a *m v).
move=> A a v Ha i k; rewrite !mxE.
apply:  big_add_i_fun_correct=> j.
by rewrite /GRing.mul /= Rmult_comm; apply muls_i_correct.
Qed.

Lemma madd_i_compl:
    forall  (V1 V2: 'M_(m, n)) v, inSetm (madd_i V1 V2 ) v -> 
   {av | inSetm V1 av.1 /\ inSetm V2 av.2 /\ v =  av.1 + av.2}.
Proof.
move=> U V w Hw.
  have Hi: forall i j, {ar| ar.1 \in U i j /\ ar.2 \in V i j /\ w i j = ar.1 + ar.2}.
  move=> i j; apply add_i_compl. 
  have Hwi := Hw i j.
  by rewrite /inSetm /mmuls_i mxE /= in Hwi.
  have Hf: { f: 'I_m -> 'I_n -> R*R | 
      forall i j, (f i j).1 \in U i j /\ (f i j).2 \in V i j/\ w i j = (f i j).1 + (f i j).2}.
  exists (fun i j => proj1_sig (Hi i j)); move=> i j; case (Hi i j) =>* //=.
elim Hf=> f Hf1; exists (\matrix_(i, j) (f i j).1 , \matrix_(i, j) (f i j).2); split.
  by move=> i j; rewrite mxE; elim (Hf1 i j).
  split.
     move=> i j; rewrite mxE; elim (Hf1 i j); intuition.
  by apply/matrixP => i j; rewrite !mxE; elim (Hf1 i j); intuition.
Qed.
  

Lemma big_add_i_fun_compl:
  forall  (V: 'I_n -> closedInt) vr, vr \in (\big[add_i/R0:closedInt]_i V i)->
  { f | (forall i: 'I_n, f i \in V i) /\ vr =  \big[+%R/R0]_i f i}.
Proof.
elim: n.
move=> //=  V vr.
rewrite big_ord0 => hvr.
exists (fun x => 0); split.
by move=> i; elim: i => *.
rewrite big_ord0.
move: hvr; rewrite in_int /=; move => [H1 H2].
by apply Rle_antisym.
move=>   n' Rn'  V vr.
rewrite big_ord_recr //==> Hvr.
case: (ltnP 0 n') => H.
elim (add_i_compl Hvr) => /= x [ /= Hx1 [Hx2 Hxs]].
  elim (Rn' ( fun i: 'I_n' => V (widen_ord (m:=n'.+1) (leqnSn n') i)) _ Hx1) =>
    f [Hf1 Hfs].
set g:= fun i => match insub i with
                          | Some (exist _ Px) =>
                              f (Ordinal (n:=n') (m:=i) Px)
                          | None => x.2
                          end.
exists g.
have Hn' : g n' = x.2.
rewrite /g.
case: (insubP)=> [[] /= _ Hi _ _| _]; last by done .
have Hi2:= Hi.
by rewrite ltnn in Hi2.
have Hii: forall i: 'I_n', g i = f i.
move=> i ; rewrite /g.
case: (insubP)=> [[] /= _ Hi _ _|].
by f_equal; apply: val_inj.
by move/negP=> H3; elim H3.
split.
move=> i; rewrite /g.
case: (insubP)=> [[] /= _ Hi _ _|]. 
have H2: (widen_ord (m:=n'.+1) (leqnSn n') (Ordinal (n:=n') (m:=i) Hi)) = i.
apply: val_inj; rewrite //=.
by rewrite -{2}H2.
rewrite -leqNgt.
move/leP=> H3.
have h:= leP (ltn_ord i). 
have h4: i = ord_max.
apply: val_inj ; rewrite /=.
omega.
by rewrite h4. 
rewrite Hxs  big_ord_recr //= Hfs Hn' .
by rewrite (@eq_bigr _ _ _ _ _ (fun _ => true)  f g  ).
(*n'=0*)
rewrite leqn0 in H; move/eqP : H => H.
have hbig0: forall   T (idx:T) (op : Monoid.com_law idx) p f , p = 0%Dn -> 
  \big[op/idx]_(i<p) f i = idx.
move=> T idx op p' f Hp.
move: f.
rewrite Hp.
apply big_ord0.
rewrite hbig0  in Hvr; last by done.
rewrite left_id_add_i in Hvr.
set g:= fun i: 'I_n'.+1 => match insub i with
                          | Some (exist _ Px) => INR (Ordinal (n:=n') (m:=i) Px)
                          | None => vr
                          end.
exists g.
have Hn' : g ord_max  = vr.
rewrite /g.
case: (insubP)=> [[] /= _ Hi _ _| _]; last by done .
by rewrite ltnn in Hi.
split.
have Heq: forall i: 'I_n'.+1, i = ord_max.
rewrite H=> i; rewrite /ord_max //=.
case: i => i Hi.
have Hi2 := Hi.
move/ltP: Hi2 => Hi2.
have Hi0: (i=0)%nat.
omega.
apply: ord_inj; rewrite //=.
by move=> i; rewrite (Heq i) Hn'.
rewrite big_ord_recr //= hbig0; last by done.
by rewrite Hn'  ; rewrite ->Rplus_0_l.
Qed.


Lemma mvmuls_i_compl:
   forall  (M: 'M_(m, n)) (r: 'cV_n) v, inSetm (mmuls_i M r ) v -> 
   {m0| inSetm M m0 /\ v =  m0 *m r}.
Proof.
move=> M r x Hm.
rewrite /mmuls_i in Hm.
have Hij: forall i , 
 {v | inSetm (\col_j M i j) v  /\ x i ord0 = \big[Rplus/0]_j (v j ord0  * r j ord0)}.
move=> i .
have Hmi := Hm i ord0; rewrite mxE in Hmi.
have H1 := @big_add_i_fun_compl _ (x i ord0) (Hmi).
elim: H1 => f [Hset Heq].
have H2 : forall j, {t| t \in M i j /\ f j =( r j ord0 * t) }.
by move=> j; apply: muls_i_compl.
exists (\col_j proj1_sig (H2 j)).
split.
move=> j k; rewrite !mxE; elim: (H2 j)=> t [Ht Ht2] ; rewrite //=.
rewrite Heq.
apply eq_bigr =>j _;  rewrite  mxE; elim: (H2 j)=> t [Ht Ht2] /=. 
rewrite Ht2; toR; ring.
exists (\matrix_(i, j)  (proj1_sig (Hij i) j ord0)).
split.
move=> i j; rewrite !mxE; elim: (Hij i)=> t [Ht Ht2] /=.
by have Htj:= (Ht j ord0); rewrite mxE in Htj.
apply/matrixP => i k; rewrite mxE.
have kord0: k=ord0.
case: k => i0 Hi0.
apply: ord_inj; rewrite /=.
move/leP: Hi0 => Hi0; omega.
transitivity (\sum_j ( sval (Hij i) j ord0) * r j ord0). 
elim: (Hij i)=> t [Ht Ht2] /=.
rewrite kord0 Ht2.
by apply eq_bigr =>*.
by apply eq_bigr =>*; rewrite kord0 mxE /=.
Qed.


Lemma mid_big_add:
  forall V: 'I_n -> closedInt, 
  mid (\big[add_i/R0:closedInt]_i V i) = \big[Rplus/R0]_i mid (V i).
Proof.
move=> V.
elim: index_enum.
rewrite !big_nil /mid /=; field .
move => x s IH.
rewrite !big_cons mid_add.
apply Rplus_eq_compat_l.
case S:(Nil _ !=s); first by apply: IH.
move/eqP:S => S; rewrite -S !big_nil.
rewrite /mid /=; field.
Qed.  
 
Lemma rad_big_add:
  forall V: 'I_n -> closedInt, 
  rad (\big[add_i/R0:closedInt]_i V i) = \big[Rplus/R0]_i rad (V i).
Proof.
move=> V.
elim: index_enum.
rewrite !big_nil /rad /=; field.
move => x s IH.
rewrite !big_cons rad_add. 
apply Rplus_eq_compat_l.
case S:(Nil _ !=s); first by apply: IH.
move/eqP:S => S; rewrite -S !big_nil.
rewrite /rad /=; field.
Qed.




End MatIntProp.

Implicit Arguments mmid[m n].
Implicit Arguments minf[m n].
Implicit Arguments msup[m n].
Implicit Arguments mrad[m n].
Implicit Arguments mmag[m n].
Implicit Arguments madd_i[m n].
Implicit Arguments mopp_i[m n].
Implicit Arguments mmul_i[m n p].
Implicit Arguments mmuls_i[m n p].
Implicit Arguments sigma_sol[m n].
Implicit Arguments inSetm[p q].
Implicit Arguments inSetmb[m n].


Section SqrMatIntDef.

Variable n: nat.

Definition regular (A: 'M_(n)) :=
forall vA, inSetm A vA -> \det vA != 0.

Definition singular (A : 'M_(n)) := 
exists vA, inSetm A vA /\ \det vA = 0.

Lemma reg_nsing:
forall A, regular A -> ~ singular A.
Proof.
move=> A Hra [x [Hsx Hsx2]].
by move/eqP: (Hra x Hsx) => H; elim H.
Qed.


Lemma nsing_reg:
forall A, ~ singular A -> regular A.
Proof.
move=> A Hns.
red in Hns |-*.
apply: Classical_Pred_Type.not_ex_not_all.
move=> H; apply Hns.
elim H => x J.
exists x.
elim (imply_to_and _ _ J) => J1 J2.
split; first by done.
by move/negP: J2; rewrite negbK; move/eqP=> J2.
Qed.
(* a bit of classical reasoning to allow proof by contradiction
  for proving regularity *)

Lemma reg_nsing_eq:
forall A, regular A <-> ~ singular A.
split; [apply reg_nsing| apply nsing_reg]. Qed.
  

Lemma sing_nreg_eq:
forall A, singular A <-> ~ regular  A.
Proof.
move=> A.
have Ha:= reg_nsing_eq A.
rewrite iff_not -Ha; split; [intuition|apply NNPP].
Qed.


End SqrMatIntDef.