Library Algebra.Monoid.Monoid_sub
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.
Support for submonoids.
Let G : AbelianMonoid.
Let PG : G → Prop.
Lemmas about predicate compatible_m have "cm" in their names, usually as
prefix "cm_", sometimes as suffix "_cm".
Let gen : G → Prop.
Let G1 G2 : AbelianMonoid.
Let PG1 : G1 → Prop.
Let f : G1 → G2.
Let G : AbelianMonoid.
Let PG : G → Prop.
Let HPG : compatible_m PG.
Let G1 G2 : AbelianMonoid.
Let PG1 : G1 → Prop and PG2 : G2 → Prop.
Let HPG1 : compatible_m PG1 and HPG2 : compatible_m PG2.
Let f : G1 → G2.
Let Hf : funS PG1 PG2 f.
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- plus_closed PG states that PG is closed under the monoid law plus;
- zero_closed PG states that PG contains the identity element zero;
- sum_closed PG states that PG is closed under the iterated monoid law sum;
- compatible_m PG states that PG is closed under plus and contains zero, ie is compatible with the AbelianMonoid structure.
- zero_sub_struct G is the singleton with only element zero.
- span_m gen is the specialization span compatible_m gen (see Algebra.Sub_struct), ie it is the intersection of all subsets (= the smallest) compatible with the AbelianMonoid structure that also contain gen.
- Ker f is the preimage by f of zero_sub_struct, aka the kernel of f;
- KerS PG1 f is the intersection inter PG1 (Ker f);
- KerS0 PG1 f is the low-level version of the predicate KerS PG1 f = zero_sub_struct;
- f_plus_compat_sub PG1 f states that f preserves the monoid law plus on PG1;
- f_pzero_compat_sub PG1 f states that f preserves the identity element zero if it belongs to PG1;
- mm_sub PG1 f states that f transports the AbelianMonoid structure from PG1;
- f_sum_compat_sub PG1 f states that f preserves iterations of the monoid law sum on PG1.
- sub_AbelianMonoid HPG is the type sub PG endowed with the AbelianMonoid structure (see Subsets.Sub_type).
- fct_sub_m HPG1 HPG2 Hf is the function fct_sub Hf with type sub_AbelianMonoid HPG1 → sub_AbelianMonoid HPG2 (see Subsets.Sub_type).
Used logic axioms
- classic, the weak form of excluded middle.
Usage
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 Sub_struct.
From Algebra Require Import Monoid_compl Monoid_morphism Monoid_sum.
Local Open Scope Monoid_scope.
Section Compatible_Monoid_Def.
Context {G : AbelianMonoid}.
Definition plus_closed (PG : G → Prop) : Prop :=
∀ x y, PG x → PG y → PG (x + y).
Definition zero_closed (PG : G → Prop) : Prop := PG 0.
Definition sum_closed (PG : G → Prop) : Prop :=
∀ n (u : 'G^n), inclF u PG → PG (sum u).
Definition compatible_m (PG : G → Prop) : Prop :=
plus_closed PG ∧ zero_closed PG.
End Compatible_Monoid_Def.
Section Compatible_Monoid_Facts.
Context {G : AbelianMonoid}.
Lemma plus_zero_sum_closed :
∀ {PG : G → Prop}, plus_closed PG → zero_closed PG → sum_closed PG.
Proof.
intros PG HPG1 HPG2 n u Hu; induction n as [| n Hn].
rewrite sum_nil; easy.
rewrite sum_ind_l; apply HPG1; try easy; apply Hn; intro; apply Hu.
Qed.
Lemma sum_plus_zero_closed :
∀ {PG : G → Prop}, sum_closed PG → plus_closed PG ∧ zero_closed PG.
Proof.
intros PG HPG; split.
intros u v Hu Hv; replace (u + v) with (sum (coupleF u v)).
apply HPG; intros i; destruct (ord2_dec i);
[rewrite coupleF_l | rewrite coupleF_r]; easy.
rewrite sum_coupleF; easy.
unfold zero_closed; rewrite -(sum_nil 0); apply HPG; intros [i Hi]; easy.
Qed.
Lemma sum_plus_zero_closed_equiv :
∀ {PG : G → Prop}, sum_closed PG ↔ plus_closed PG ∧ zero_closed PG.
Proof.
intros; split.
apply sum_plus_zero_closed.
intros; apply plus_zero_sum_closed; easy.
Qed.
Lemma sum_closed_cm :
∀ {PG : G → Prop}, sum_closed PG → compatible_m PG.
Proof. move=>> /sum_plus_zero_closed_equiv //. Qed.
Lemma cm_nonempty : ∀ {PG : G → Prop}, compatible_m PG → nonempty PG.
Proof. move=>> H; ∃ 0; apply H. Qed.
Lemma cm_zero : ∀ {PG : G → Prop}, compatible_m PG → zero_closed PG.
Proof. move=>> H; apply H. Qed.
Lemma cm_plus : ∀ {PG : G → Prop}, compatible_m PG → plus_closed PG.
Proof. move=>> H; apply H. Qed.
Lemma cm_sum : ∀ {PG : G → Prop}, compatible_m PG → sum_closed PG.
Proof. intros PG H; apply plus_zero_sum_closed; apply H. Qed.
Lemma cm_sum_equiv :
∀ {PG : G → Prop}, compatible_m PG ↔ sum_closed PG.
Proof. intros; apply iff_sym, sum_plus_zero_closed_equiv. Qed.
Definition zero_sub_struct : G → Prop := singleton 0.
Lemma zero_sub_struct_correct :
∀ {PG : G → Prop}, PG = zero_sub_struct → ∀ x, PG x → x = 0.
Proof. move=>> → //. Qed.
Lemma nonzero_sub_struct_ex :
∀ {PG : G → Prop},
nonempty PG → PG ≠ zero_sub_struct ↔ ∃ x, PG x ∧ x ≠ 0.
Proof.
intros PG [x0 H0]; rewrite -iff_not_r_equiv not_ex_all_not_equiv; split.
intros H x; rewrite H; easy.
intros H; apply subset_ext; intros x; split; intros Hx.
specialize (H x); rewrite -imp_and_equiv in H; apply H; easy.
specialize (H x0); rewrite -imp_and_equiv in H; rewrite Hx -(H H0); easy.
Qed.
Lemma cm_zero_sub_struct : compatible_m zero_sub_struct.
Proof. split; try easy; intros x y Hx Hy; rewrite Hx Hy plus_zero_r; easy. Qed.
Lemma cm_full : ∀ {PG : G → Prop}, full PG → compatible_m PG.
Proof. intros; split; try unfold zero_closed; easy. Qed.
Lemma cm_fullset : compatible_m (@fullset G).
Proof. easy. Qed.
Lemma plus_closed_inter :
∀ {PG QG : G → Prop},
plus_closed PG → plus_closed QG → plus_closed (inter PG QG).
Proof.
move=>> HPG HQG x y [HxP HxQ] [HyP HyQ]; split; [apply HPG | apply HQG]; easy.
Qed.
Lemma zero_closed_inter :
∀ {PG QG : G → Prop},
zero_closed PG → zero_closed QG → zero_closed (inter PG QG).
Proof. easy. Qed.
Lemma cm_inter :
∀ {PG QG : G → Prop},
compatible_m PG → compatible_m QG → compatible_m (inter PG QG).
Proof.
move=>> [HPG1 HPG2] [HQG1 HQG2]; split;
[apply plus_closed_inter | apply zero_closed_inter]; easy.
Qed.
Lemma plus_closed_inter_any :
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, plus_closed (PG i)) → plus_closed (inter_any PG).
Proof. move=>> HPG; move=>> Hx Hy i; apply HPG; easy. Qed.
Lemma zero_closed_inter_any :
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, zero_closed (PG i)) → zero_closed (inter_any PG).
Proof. move=>> HPG i; apply HPG. Qed.
Lemma cm_inter_any :
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, compatible_m (PG i)) → compatible_m (inter_any PG).
Proof.
move=>> HPG; split.
apply plus_closed_inter_any; intro; apply HPG.
apply zero_closed_inter_any; intro; apply HPG.
Qed.
Definition span_m (gen : G → Prop) := span compatible_m gen.
Lemma span_m_cm : ∀ gen, compatible_m (span_m gen).
Proof. apply span_compatible; move=>>; apply cm_inter_any. Qed.
Lemma span_m_nonempty : ∀ gen, nonempty (span_m gen).
Proof. intros; apply cm_nonempty, span_m_cm. Qed.
Lemma span_m_zero : ∀ gen, zero_closed (span_m gen).
Proof. intros; apply cm_zero, span_m_cm. Qed.
Lemma span_m_plus : ∀ gen, plus_closed (span_m gen).
Proof. intros; apply cm_plus, span_m_cm. Qed.
Lemma span_m_sum : ∀ gen, sum_closed (span_m gen).
Proof. intros; apply cm_sum, span_m_cm. Qed.
Lemma span_m_incl : ∀ gen, incl gen (span_m gen).
Proof. apply span_incl. Qed.
Lemma span_m_lub :
∀ {gen PG}, compatible_m PG → incl gen PG → incl (span_m gen) PG.
Proof. apply span_lub. Qed.
Lemma span_m_full : ∀ {PG}, compatible_m PG → span_m PG = PG.
Proof. apply span_full. Qed.
End Compatible_Monoid_Facts.
Section Compatible_Monoid_Morphism_Facts0.
Context {G1 G2 : AbelianMonoid}.
Lemma cm_mm : compatible_m (@morphism_m G1 G2).
Proof. split; [move=>>; apply: mm_fct_plus | apply mm_fct_zero]. Qed.
End Compatible_Monoid_Morphism_Facts0.
Section Compatible_Monoid_Morphism_Facts1.
Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_m f.
Lemma cm_image : compatible_m PG1 → compatible_m (image f PG1).
Proof.
destruct Hf as [Hfa Hfb]; intros [HPG1a HPG1b]; split.
intros _ _ [x1 Hx1] [y1 Hy1]; rewrite -Hfa; apply Im; auto.
unfold zero_closed; rewrite -Hfb; apply Im; easy.
Qed.
Lemma cm_preimage : compatible_m PG2 → compatible_m (preimage f PG2).
Proof.
destruct Hf as [Hfa Hfb]; intros [HPG2a HPG2b]; split; unfold preimage.
do 2 intro; rewrite Hfa; auto.
unfold zero_closed; rewrite Hfb; easy.
Qed.
End Compatible_Monoid_Morphism_Facts1.
Section Compatible_Monoid_Morphism_Def.
Context {G1 G2 : AbelianMonoid}.
Variable PG1 : G1 → Prop.
Variable f : G1 → G2.
Definition Ker : G1 → Prop := preimage f zero_sub_struct.
Definition KerS : G1 → Prop := inter PG1 Ker.
Definition KerS0 : Prop := ∀ x, PG1 x → f x = 0 → x = 0.
Definition f_plus_compat_sub : Prop :=
∀ x1 y1, PG1 x1 → PG1 y1 → f (x1 + y1) = f x1 + f y1.
Definition f_zero_compat_sub : Prop := PG1 0 → f 0 = 0.
Definition f_sum_compat_sub : Prop :=
∀ n (u1 : 'G1^n), inclF u1 PG1 → f (sum u1) = sum (mapF f u1).
Definition mm_sub : Prop := f_plus_compat_sub ∧ f_zero_compat_sub.
End Compatible_Monoid_Morphism_Def.
Section KerS0_gather.
Context {G1 G2 : AbelianMonoid}.
Variable PG1 : G1 → Prop.
Context {n : nat}.
Variable f : '(G1 → G2)^n.
Lemma KerS0_gather_equiv :
KerS0 PG1 (gather f) ↔
(∀ x : G1, PG1 x → (∀ i, f i x = 0) → x = 0).
Proof.
split; intros H; intros x H1 H2; apply H; try easy.
apply extF; intros i; apply H2.
intros i; apply (fun_ext_rev H2 i).
Qed.
Lemma KerS0_gather_imp : ∀ {n} (f:'(G1 → G2)^n), (0 < n)%coq_nat →
(∀ i, KerS0 PG1 (f i)) → KerS0 PG1 (gather f).
Proof.
clear n f; intros n f Hn H x Hx1 Hx2.
destruct n; try easy.
apply (H ord0); try easy.
apply (fun_ext_rev Hx2 ord0).
Qed.
End KerS0_gather.
Section Compatible_Monoid_Morphism_Facts2.
Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {f : G1 → G2}.
Lemma Ker_correct : ∀ {x1}, f x1 = 0 → Ker f x1.
Proof. easy. Qed.
Lemma Ker_equiv : ∀ {x1}, Ker f x1 ↔ f x1 = 0.
Proof. easy. Qed.
Lemma KerS_correct : ∀ {x1}, PG1 x1 → f x1 = 0 → KerS PG1 f x1.
Proof. easy. Qed.
Lemma KerS_equiv : ∀ {x1}, KerS PG1 f x1 ↔ PG1 x1 ∧ f x1 = 0.
Proof. easy. Qed.
Lemma KerS_incl :
∀ (PG1 : G1 → Prop) (f : G1 → G2), incl (KerS PG1 f) PG1.
Proof. move=>> [Hx _]; easy. Qed.
Lemma KerS_full : KerS fullset f = Ker f.
Proof. apply inter_full_l. Qed.
Lemma KerS0_correct :
zero_closed PG1 → f_zero_compat f →
KerS0 PG1 f ↔ KerS PG1 f = zero_sub_struct.
Proof.
intros HPG1 Hf1; split; intros Hf2.
apply fun_ext; intros x; apply prop_ext; split; intros Hx;
[apply Hf2; apply Hx | rewrite Hx; split; easy].
intros x Hx1 Hx2; apply (zero_sub_struct_correct Hf2 x); easy.
Qed.
End Compatible_Monoid_Morphism_Facts2.
Section Compatible_Monoid_Morphism_Facts3a.
Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Hypothesis HPG1 : compatible_m PG1.
Context {PG2 : G2 → Prop}.
Hypothesis HPG2 : compatible_m PG2.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_m f.
Lemma KerS_cm : compatible_m (KerS PG1 f).
Proof. apply cm_inter, cm_preimage, cm_zero_sub_struct; easy. Qed.
Lemma RgS_gen_cm : compatible_m (RgS_gen PG1 PG2 f).
Proof. apply cm_inter, cm_image; easy. Qed.
Lemma RgS_cm : compatible_m (RgS PG1 f).
Proof. apply cm_image; easy. Qed.
Lemma KerS_m_zero_equiv :
KerS PG1 f = zero_sub_struct ↔ incl (KerS PG1 f) zero_sub_struct.
Proof.
split; intros Hf1; [rewrite Hf1 | apply incl_antisym]; try easy.
move=>> ->; split; [apply cm_zero | apply mm_zero]; easy.
Qed.
Lemma mmS_injS_rev : injS PG1 f → KerS PG1 f = zero_sub_struct.
Proof.
rewrite KerS_m_zero_equiv//; intros Hf1 x1 [Hx1a Hx1b]; apply Hf1;
[| apply cm_zero | rewrite mm_zero]; easy.
Qed.
Lemma mmS_bijS_gen_rev :
bijS PG1 PG2 f →
funS PG1 PG2 f ∧ KerS PG1 f = zero_sub_struct ∧ RgS_gen PG1 PG2 f = PG2.
Proof.
rewrite bijS_equiv; [| apply inhabited_m].
assert (H0 : ∀ P Q1 Q2 R1 R2 : Prop,
(Q1 → R1) → (Q2 → R2) → P ∧ Q1 ∧ Q2 → P ∧ R1 ∧ R2) by tauto.
apply H0; [apply mmS_injS_rev | apply surjS_rev].
Qed.
Lemma mmS_bijS_rev : bijS PG1 (RgS PG1 f) f → KerS PG1 f = zero_sub_struct.
Proof.
rewrite bijS_equiv; [intros; apply mmS_injS_rev; easy | apply inhabited_m].
Qed.
Lemma mmS_bijS_injS_equiv : bijS PG1 (RgS PG1 f) f ↔ injS PG1 f.
Proof. apply bijS_RgS_equiv, inhabited_m. Qed.
End Compatible_Monoid_Morphism_Facts3a.
Section Compatible_Monoid_Morphism_Facts3b.
Context {G1 G2 : AbelianMonoid}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_m f.
Lemma Ker_cm : compatible_m (Ker f).
Proof. rewrite -KerS_full; apply (KerS_cm cm_fullset Hf). Qed.
Lemma Rg_cm : compatible_m (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cm cm_fullset Hf). Qed.
Lemma Ker_m_zero_equiv :
Ker f = zero_sub_struct ↔ incl (Ker f) zero_sub_struct.
Proof. rewrite -KerS_full; apply (KerS_m_zero_equiv cm_fullset Hf). Qed.
Lemma mm_inj_rev : injective f → Ker f = zero_sub_struct.
Proof. rewrite -KerS_full inj_S_equiv; apply (mmS_injS_rev cm_fullset Hf). Qed.
Lemma mm_bij_rev : bijective f → Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof.
rewrite -KerS_full -RgS_gen_full bij_S_equiv; [| apply inhabited_m].
apply (mmS_bijS_gen_rev cm_fullset Hf).
Qed.
End Compatible_Monoid_Morphism_Facts3b.
Section Compatible_Monoid_Morphism_Facts4a.
Context {E1 E2 E3 : AbelianMonoid}.
Context {PE2 : E2 → Prop}.
Context {f : E1 → E2}.
Context {g : E2 → E3}.
Lemma KerS_comp : KerS (preimage f PE2) (g \o f) = preimage f (KerS PE2 g).
Proof. easy. Qed.
End Compatible_Monoid_Morphism_Facts4a.
Section Compatible_Monoid_Morphism_Facts4b.
Context {E1 E2 E3 : AbelianMonoid}.
Context {f : E1 → E2}.
Context {g : E2 → E3}.
Lemma Ker_comp : Ker (g \o f) = preimage f (Ker g).
Proof. easy. Qed.
Lemma Ker_comp_l : surjective f → RgS (Ker (g \o f)) f = Ker g.
Proof.
intros; rewrite Ker_comp RgS_preimage; apply inter_left.
rewrite surj_rev; easy.
Qed.
Lemma Ker_comp_l_alt :
∀ h x2, surjective f → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. move=>> Hf1 ->; rewrite -RgS_ex Ker_comp_l; easy. Qed.
Hypothesis Hf : morphism_m f.
Hypothesis Hg : morphism_m g.
Lemma Ker_m_comp_r : injective g → RgS (Ker (g \o f)) f = Ker g.
Proof.
intros; rewrite Ker_comp RgS_preimage; apply inter_left.
rewrite mm_inj_rev//; move=>> ->; rewrite -(mm_zero Hf); easy.
Qed.
Lemma Ker_m_comp_r_alt :
∀ h x2, injective g → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. move=>> Hg1 ->; rewrite -RgS_ex Ker_m_comp_r; easy. Qed.
End Compatible_Monoid_Morphism_Facts4b.
Section Compatible_Monoid_Morphism_Facts5a.
Context {G1 G2 : AbelianMonoid}.
Variable PG1 : G1 → Prop.
Lemma f_plus_compat_sub_id : f_plus_compat_sub PG1 ssrfun.id.
Proof. easy. Qed.
Lemma f_zero_compat_sub_id : f_zero_compat_sub PG1 ssrfun.id.
Proof. easy. Qed.
Lemma mmS_id : mm_sub PG1 ssrfun.id.
Proof. easy. Qed.
Variable f g : G1 → G2.
Lemma f_plus_compat_is_sub : f_plus_compat f → f_plus_compat_sub PG1 f.
Proof. easy. Qed.
Lemma f_zero_compat_is_sub : f_zero_compat f → f_zero_compat_sub PG1 f.
Proof. easy. Qed.
Lemma mm_is_sub : morphism_m f → mm_sub PG1 f.
Proof. intros [Hfa Hfb]; easy. Qed.
Lemma mmS_plus : mm_sub PG1 f → f_plus_compat_sub PG1 f.
Proof. intros H; apply H. Qed.
Lemma mmS_zero : mm_sub PG1 f → f_zero_compat_sub PG1 f.
Proof. intros H; apply H. Qed.
Lemma mmS_fct_plus : mm_sub PG1 f → mm_sub PG1 g → mm_sub PG1 (f + g).
Proof.
intros [Hfa Hfb] [Hga Hgb]; split.
move=>> Hx1 Hy1. rewrite 3!fct_plus_eq Hfa// Hga// 2!plus_assoc; f_equal;
rewrite -2!plus_assoc; f_equal; apply plus_comm.
intros H0; rewrite fct_plus_eq Hfb// Hgb// plus_zero_r; easy.
Qed.
Lemma mmS_fct_zero : mm_sub PG1 (0 : G1 → G2).
Proof.
split; try easy; intros x1 y1; rewrite 2!fct_zero_eq plus_zero_l; easy.
Qed.
Lemma mmS_ext :
plus_closed PG1 → same_funS PG1 f g → mm_sub PG1 f → mm_sub PG1 g.
Proof.
intros H1 H [Hfa Hfb]; split.
move=>> Hx1 Hy1; rewrite -!H//; [rewrite Hfa// | apply H1; easy].
intros H0; rewrite -H// Hfb; easy.
Qed.
Lemma sum_mmS : f_sum_compat_sub PG1 f → mm_sub PG1 f.
Proof.
intros Hf; split.
move=>> Hx1 Hy1; rewrite -!sum_coupleF -mapF_coupleF; apply Hf.
intros i; destruct (ord2_dec i) as [-> | ->];
[rewrite coupleF_0 | rewrite coupleF_1]; easy.
intros H0; rewrite -(sum_nil (fun _ ⇒ 0)) Hf;
[rewrite mapF_constF sum_nil// |].
intros [i Hi]; easy.
Qed.
Lemma mmS_sum :
zero_closed PG1 → sum_closed PG1 → mm_sub PG1 f → f_sum_compat_sub PG1 f.
Proof.
move=>> H0 Hs [Hfa Hfb] n; induction n as [| n Hn].
intros; rewrite 2!sum_nil; auto.
intros u1 Hu1; rewrite 2!sum_ind_l Hfa//;
[rewrite Hn// | apply Hs]; intro; apply Hu1.
Qed.
Lemma mmS_sum_equiv :
zero_closed PG1 → sum_closed PG1 → mm_sub PG1 f ↔ f_sum_compat_sub PG1 f.
Proof. intros; split; [apply mmS_sum; easy | apply sum_mmS]. Qed.
End Compatible_Monoid_Morphism_Facts5a.
Section Compatible_Monoid_Morphism_Facts5b.
Context {G1 G2 : AbelianMonoid}.
Variable PG1 : G1 → Prop.
Context {n : nat}.
Context {f : '(G1 → G2)^n}.
Lemma mmS_fct_sum : (∀ i, mm_sub PG1 (f i)) → mm_sub PG1 (sum f).
Proof.
intros Hf; induction n as [|m Hm].
rewrite sum_nil; apply mmS_fct_zero.
rewrite sum_ind_l; apply mmS_fct_plus; auto.
apply Hm; intro; apply Hf.
Qed.
Lemma sum_funS_sum :
∀ {p} (u : 'G1^p),
zero_closed PG1 → sum_closed PG1 → inclF u PG1 →
(∀ i, mm_sub PG1 (f i)) → sum f (sum u) = sum (mapF (sum f) u).
Proof. intros; rewrite (mmS_sum PG1)//; apply mmS_fct_sum; easy. Qed.
End Compatible_Monoid_Morphism_Facts5b.
Section Compatible_Monoid_Morphism_Facts5c.
Context {G1 G2 G3 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Variable PG2 : G2 → Prop.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Variable g : G2 → G3.
Lemma f_plus_compat_comp_sub :
f_plus_compat_sub PG1 f → f_plus_compat_sub PG2 g →
f_plus_compat_sub PG1 (g \o f).
Proof.
intros Hf1 Hg1 x1 y1 Hx1 Hy1;
rewrite !comp_correct Hf1// Hg1//; apply Hf; easy.
Qed.
Lemma f_zero_compat_comp_sub :
f_zero_compat_sub PG1 f → f_zero_compat_sub PG2 g →
f_zero_compat_sub PG1 (g \o f).
Proof.
intros Hf1 Hg1 H0;
rewrite comp_correct Hf1// Hg1// -Hf1//; apply Hf; easy.
Qed.
Lemma mm_comp_sub : mm_sub PG1 f → mm_sub PG2 g → mm_sub PG1 (g \o f).
Proof.
intros [Hfa Hfb] [Hga Hgb]; split;
[apply f_plus_compat_comp_sub | apply f_zero_compat_comp_sub]; easy.
Qed.
End Compatible_Monoid_Morphism_Facts5c.
Section Sub_Monoid_Def.
Context {G : AbelianMonoid}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_m PG.
Definition sub_plus (x y : sub PG) : sub PG :=
mk_sub (cm_plus HPG _ _ (in_sub x) (in_sub y)).
Definition sub_zero : sub PG := mk_sub_ PG _ (cm_zero HPG).
Lemma sub_plus_comm : ∀ x y, sub_plus x y = sub_plus y x.
Proof. intros; apply val_inj, plus_comm. Qed.
Lemma sub_plus_assoc:
∀ x y z, sub_plus x (sub_plus y z) = sub_plus (sub_plus x y) z.
Proof. intros; apply val_inj, plus_assoc. Qed.
Lemma sub_plus_zero_r : ∀ x, sub_plus x sub_zero = x.
Proof. intros; apply val_inj, plus_zero_r. Qed.
Definition sub_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ sub_plus_comm sub_plus_assoc sub_plus_zero_r.
Canonical Structure sub_AbelianMonoid :=
AbelianMonoid.Pack _ sub_AbelianMonoid_mixin (sub PG).
Lemma val_zero : f_zero_compat val.
Proof. easy. Qed.
Lemma val_zero_equiv : ∀ (x : sub PG), val x = 0 ↔ x = 0.
Proof.
intros; split; [rewrite -val_zero; apply val_inj | intros; subst; easy].
Qed.
Lemma val_plus : f_plus_compat val.
Proof. easy. Qed.
Lemma val_sum : f_sum_compat val.
Proof.
intros n; induction n as [| n Hn].
intros; rewrite 2!sum_nil; easy.
intros; rewrite 2!sum_ind_l; simpl; f_equal; apply Hn.
Qed.
Lemma val_mm : morphism_m val.
Proof. easy. Qed.
Lemma mk_sub_zero : sub_zero = (0 : sub PG).
Proof. easy. Qed.
Lemma mk_sub_zero_equiv : ∀ {x} (Hx : PG x), mk_sub Hx = 0 ↔ x = 0.
Proof. intros; split; [move⇒ /val_eq | intros; apply val_inj]; easy. Qed.
Lemma mk_sub_plus :
∀ (x y : G) (Hx : PG x) (Hy : PG y),
mk_sub Hx + mk_sub Hy = mk_sub (cm_plus HPG _ _ Hx Hy).
Proof. easy. Qed.
Lemma mk_sub_sum :
∀ {n} (u : 'G^n) (Hu : inclF u PG),
sum (fun i ⇒ mk_sub (Hu i)) = mk_sub (cm_sum HPG _ _ Hu).
Proof. intros; apply val_inj, val_sum. Qed.
Lemma sub_zero_eq : (0 : sub PG) = mk_sub (cm_zero HPG : PG 0).
Proof. easy. Qed.
Lemma sub_plus_eq :
∀ (x y : sub PG),
x + y = mk_sub (cm_plus HPG _ _ (in_sub x) (in_sub y)).
Proof. intros; apply val_inj; easy. Qed.
Lemma sub_sum_eq :
∀ {n} (u : '(sub PG)^n),
sum u = mk_sub (cm_sum HPG _ _ (fun i ⇒ in_sub (u i))).
Proof. intros; apply val_inj, val_sum. Qed.
End Sub_Monoid_Def.
Section Sub_Monoid_Facts1.
Context {G : AbelianMonoid}.
Context {PGa PG : G → Prop}.
Hypothesis HPGa : incl PGa PG.
Hypothesis HPG : compatible_m PG.
Let PG_m := sub_AbelianMonoid HPG.
Let PGa' : PG_m → Prop := preimage val PGa.
Lemma RgS_val_m_eq : RgS PGa' val = PGa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cm : compatible_m PGa → compatible_m PGa'.
Proof. intros; apply cm_preimage; easy. Qed.
Lemma preimage_val_cm_rev : compatible_m PGa' → compatible_m PGa.
Proof. intros; rewrite -RgS_val_m_eq; apply RgS_cm; easy. Qed.
Lemma preimage_val_cm_equiv : compatible_m PGa' ↔ compatible_m PGa.
Proof. split; [apply preimage_val_cm_rev | apply preimage_val_cm]. Qed.
End Sub_Monoid_Facts1.
Section Sub_Monoid_Facts2.
Context {G : AbelianMonoid}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_m PG.
Let PG_m := sub_AbelianMonoid HPG.
Variable PGa : PG_m → Prop.
Let PGa' := RgS PGa val.
Lemma preimage_val_m_eq : preimage val PGa' = PGa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cm : compatible_m PGa → compatible_m PGa'.
Proof. intros; apply RgS_cm; easy. Qed.
Lemma RgS_val_cm_rev : compatible_m PGa' → compatible_m PGa.
Proof. intros; rewrite -preimage_val_m_eq; apply cm_preimage; easy. Qed.
Lemma RgS_val_cm_equiv : compatible_m PGa' ↔ compatible_m PGa.
Proof. split; [apply RgS_val_cm_rev | apply RgS_val_cm]. Qed.
End Sub_Monoid_Facts2.
Section Sub_Monoid_Morphism_Facts1.
Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {HPG1 : compatible_m PG1}.
Context {HPG2 : compatible_m PG2}.
Let PG1_m := sub_AbelianMonoid HPG1.
Let PG2_m := sub_AbelianMonoid HPG2.
Context {f : G1 → G2}.
Context {fS : PG1_m → PG2_m}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_m_f_plus_compat : f_plus_compat f → f_plus_compat fS.
Proof. intros Hf x1 y1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
Lemma sub_m_f_zero_compat : f_zero_compat f → f_zero_compat fS.
Proof. intros Hf; apply val_inj; rewrite HfS Hf; easy. Qed.
Lemma sub_m_f_sum_compat : f_sum_compat f → f_sum_compat fS.
Proof.
intros Hf n u1; apply val_inj; rewrite HfS !val_sum Hf; f_equal.
apply extF; intros i; rewrite !mapF_correct; easy.
Qed.
Lemma sub_m_morphism : morphism_m f → morphism_m fS.
Proof.
intros [Hf1 Hf2]; split;
[apply (sub_m_f_plus_compat Hf1) | apply (sub_m_f_zero_compat Hf2)].
Qed.
Lemma Ker_sub_KerS_equiv :
∀ (x1 : sub PG1), Ker fS x1 ↔ KerS PG1 f (val x1).
Proof.
intros. rewrite Ker_equiv KerS_equiv -HfS. split; intros Hx1.
split; [apply in_sub | rewrite Hx1 val_zero_equiv; easy].
apply val_inj; easy.
Qed.
Lemma KerS_Ker_sub_equiv :
∀ {x1} (Hx1 : PG1 x1), KerS PG1 f x1 ↔ Ker fS (mk_sub Hx1).
Proof. intros; rewrite Ker_sub_KerS_equiv; easy. Qed.
Lemma Ker_sub_zero_equiv :
morphism_m f →
Ker fS = zero_sub_struct ↔ KerS PG1 f = zero_sub_struct.
Proof.
intros Hf; split; intros H; apply subset_ext_equiv; split.
intros x1; destruct (classic (PG1 x1)) as [Hx1 | Hx1].
move⇒ /(KerS_Ker_sub_equiv Hx1); rewrite H; move⇒ /mk_sub_zero_equiv; easy.
intros [Hx1a _]; easy.
move⇒ x1 ->; apply cm_zero, KerS_cm; easy.
move⇒ x1 /Ker_sub_KerS_equiv Hx1; rewrite H in Hx1; apply val_inj; easy.
move⇒ x1 ->; apply (cm_zero (Ker_cm (sub_m_morphism Hf))).
Qed.
Lemma Rg_sub_RgS_equiv :
∀ (x2 : sub PG2), Rg fS x2 ↔ RgS PG1 f (val x2).
Proof.
intros x2; split; [intros [x1 Hx1]; rewrite HfS; apply Im, in_sub |].
intros Hx2; inversion Hx2 as [x1 Hx1a Hx1b].
apply Rg_ex; ∃ (mk_sub Hx1a); apply val_inj; rewrite HfS; easy.
Qed.
Lemma RgS_Rg_sub_equiv :
∀ {x2} (Hx2 : PG2 x2), RgS PG1 f x2 ↔ Rg fS (mk_sub Hx2).
Proof. intros; rewrite Rg_sub_RgS_equiv; easy. Qed.
End Sub_Monoid_Morphism_Facts1.
Section Sub_Monoid_Morphism_Facts2.
Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Hypothesis HPG1 : compatible_m PG1.
Hypothesis HPG2 : compatible_m PG2.
Let PG1_m := sub_AbelianMonoid HPG1.
Let PG2_m := sub_AbelianMonoid HPG2.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Definition fct_sub_m : PG1_m → PG2_m := fct_sub Hf.
Lemma fct_sub_m_inj : injS PG1 f → injective fct_sub_m.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_m_inj_rev : injective fct_sub_m → injS PG1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_m_inj_equiv : injective fct_sub_m ↔ injS PG1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_m_surj : surjS PG1 PG2 f → surjective fct_sub_m.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_m_surj_rev : surjective fct_sub_m → surjS PG1 PG2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_m_surj_equiv : surjective fct_sub_m ↔ surjS PG1 PG2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_m_bij : bijS PG1 PG2 f → bijective fct_sub_m.
Proof. apply fct_sub_bij, inhabited_m. Qed.
Lemma fct_sub_m_bij_rev : bijective fct_sub_m → bijS PG1 PG2 f.
Proof. apply fct_sub_bij_rev, inhabited_m. Qed.
Lemma fct_sub_m_bij_equiv : bijective fct_sub_m ↔ bijS PG1 PG2 f.
Proof. apply fct_sub_bij_equiv, inhabited_m. Qed.
Lemma fct_sub_m_f_plus_compat : f_plus_compat f → f_plus_compat fct_sub_m.
Proof. apply sub_m_f_plus_compat, fct_sub_correct. Qed.
Lemma fct_sub_m_f_zero_compat : f_zero_compat f → f_zero_compat fct_sub_m.
Proof. apply sub_m_f_zero_compat, fct_sub_correct. Qed.
Lemma fct_sub_m_f_sum_compat : f_sum_compat f → f_sum_compat fct_sub_m.
Proof. apply sub_m_f_sum_compat, fct_sub_correct. Qed.
Lemma fct_sub_m_mm : morphism_m f → morphism_m fct_sub_m.
Proof. apply sub_m_morphism, fct_sub_correct. Qed.
Lemma fct_sub_m_f_inv_mm :
∀ (Hfb : bijS PG1 PG2 f),
morphism_m f → morphism_m (f_inv (fct_sub_m_bij Hfb)).
Proof. intros; apply mm_bij_compat, fct_sub_m_mm; easy. Qed.
End Sub_Monoid_Morphism_Facts2.