Library LM.direct_sum

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
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.

From Coq Require Import Reals ssreflect.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Algebra Require Import Algebra_wDep.

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

Sums and direct sums

Section Compat_m.

Context {K : Ring}.
Context {E : ModuleSpace K}.

Inductive sum_sub (PE QE : E Prop) : E Prop :=
  | Sum_sub : xPE xQE, PE xPE QE xQE sum_sub PE QE (xPE + xQE).

Definition m_plus (PE QE : E Prop) :=
  fun x xPE xQE, PE xPE QE xQE x = xPE + xQE.

Lemma m_plus_equiv : PE QE, sum_sub PE QE = m_plus PE QE.
Proof.
intros; apply subset_ext_equiv; split; intros x.
intros [xPE xQE HxPE HxQE]; xPE, xQE; easy.
intros [xPE [xQE [HxPE [HxQE ->]]]]; easy.
Qed.

Variable PE QE : E Prop.

Hypothesis HPE: compatible_ms PE.
Hypothesis HQE: compatible_ms QE.

Lemma cms_plus2: compatible_ms (m_plus PE QE).
Proof.
split; try split; try split.
intros x y (x1,(x2,(Hx1,(Hx2,Hx3)))) (y1,(y2,(Hy1,(Hy2,Hy3)))).
(x1+y1); (x2+y2); split; try split.
now apply HPE.
now apply HQE.
rewrite Hx3 Hy3; repeat rewrite -plus_assoc; f_equal.
rewrite plus_comm -plus_assoc; f_equal; apply plus_comm.
zero; zero; repeat split; try apply HPE; try apply HQE.
now rewrite plus_zero_l.
intros x (x1,(x2,(Hx1,(Hx2,Hx3)))).
(-x1); (-x2); repeat split.
now apply HPE.
now apply HQE.
now rewrite Hx3 opp_plus.
intros l x (x1,(x2,(Hx1,(Hx2,Hx3)))).
(scal l x1); (scal l x2); repeat split.
now apply HPE.
now apply HQE.
now rewrite Hx3 scal_distr_l.
Qed.

Definition direct_sumable := x, PE x QE x x = zero.

Lemma direct_sum_eq1:
   direct_sumable
    ( u u' , PE u QE u' plus u u' = zero u=zero u'=zero).
Proof.
intros. split.
unfold compatible_ms in ×.
unfold compatible_g in ×.
assert (u = opp u').
rewrite -(plus_opp_r u') in H2.
rewrite plus_comm in H2.
apply: plus_reg_l H2.
assert (QE u).
rewrite H3 in H2.
rewrite H3.
rewrite <- scal_opp_one.
apply (proj2 HQE). trivial.
apply H; trivial.
assert (u' = opp u).
rewrite -(plus_opp_r u) in H2.
apply: plus_reg_l H2.
assert (PE u').
rewrite H3 in H2.
rewrite H3.
rewrite <- scal_opp_one.
apply (proj2 HPE). trivial.
apply H; trivial.
Qed.

Lemma plus_u_opp_v : (u v : E), u = v (plus u (opp v) = zero).
Proof.
intros; split.
+ intros. rewrite H. rewrite plus_opp_r. reflexivity.
+ intros. apply plus_reg_r with (opp v). rewrite plus_opp_r; trivial.
Qed.

Lemma direct_sum_eq2:
  ( u u' , PE u QE u' plus u u' = zero u=zero u'=zero)
   ( u v u' v', PE u PE v QE u' QE v' plus u u' = plus v v' u=v u'=v').
Proof.
intros H u v u' v' Hu Hv Hu' Hv' H1.
assert (H0: u-v=0 u'-v'=0).
apply H.
apply HPE; try easy; apply HPE; easy.
apply HQE; try easy; apply HQE; easy.
now rewrite plus_comm4_m H1 -opp_plus plus_opp_r.
split; apply plus_u_opp_v, H0.
Qed.

Lemma direct_sum_eq3:
   ( u v u' v', PE u PE v QE u' QE v' plus u u' = plus v v' u=v u'=v')
      direct_sumable.
Proof.
intros H x Hx1 Hx2.
assert (H0: (x = zero) (-x = zero));[idtac|easy].
apply H; try easy; try apply HPE; try apply HQE; try easy.
now rewrite plus_zero_l plus_opp_r.
Qed.

End Compat_m.