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.