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.

Brief description

Support for submonoids.

Description

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.

Used logic axioms

  • classic, the weak form of excluded middle.

Usage

This module may be used through the import of Algebra.Monoid.Monoid, 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 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 imk_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 iin_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.
movex1 ->; apply cm_zero, KerS_cm; easy.
movex1 /Ker_sub_KerS_equiv Hx1; rewrite H in Hx1; apply val_inj; easy.
movex1 ->; 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.