Library Algebra.Monoid.Monoid_FT

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

Additional support for finite tables on commutative monoids.

Description

Constructors

Let G be an AbelianMonoid. Let x be in G. Let A be a p-family of G.
  • rowT m A i is the (m, p)-table with items equal to 0, except i-th row equal to A, in the same order;
  • colT n A j is the (p, n)-table with items equal to 0, except j-th colomn equal to A, in the same order;
  • row1T A is the (1, p)-table with row equal to A;
  • col1T A is the (p, 1)-table with column equal to A;
  • itemT m n x i j is the (m, n)-table with items equal to 0, except item in i-th row and j-th column equal to x;
  • diagT A is the (p, p)-table with items equal to 0, except the diagonal equal to A, in the same order.

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 Monoid_FF.

Local Open Scope Monoid_scope.

Section Monoid_FT_Def.

Context {G : AbelianMonoid}.

Definition rowT m {n} (A : 'G^n) i0 : 'G^{m,n} := itemF m A i0.
Definition colT {m} n (A : 'G^m) j0 : 'G^{m,n} := fun iitemF n (A i) j0.

Definition row1T {n} (A : 'G^n) : 'G^{1,n} := rowT 1 A ord0.
Definition col1T {m} (A : 'G^m) : 'G^{m,1} := colT 1 A ord0.

Definition itemT m n (x : G) i0 j0 : 'G^{m,n} := rowT m (itemF n x j0) i0.

Definition diagT {n} (A : 'G^n) : 'G^[n] :=
  fun i jmatch ord_eq_dec i j with
    | left _A i
    | right _ ⇒ 0
    end.

End Monoid_FT_Def.

Section Monoid_FT_Facts0.

Correctness lemmas.

Context {G : AbelianMonoid}.

Lemma rowT_correct_l :
   m {n} (A : 'G^n) {i0 i}, i = i0 rowT m A i0 i = A.
Proof. move=>>; apply itemF_correct_l. Qed.

Lemma rowT_correct_r :
   m {n} (A : 'G^n) {i0 i}, i i0 rowT m A i0 i = 0.
Proof. move=>>; apply itemF_correct_r. Qed.

Lemma colT_correct_l :
   {m} n (A : 'G^m) {j0} i {j}, j = j0 colT n A j0 i j = A i.
Proof. intros; apply itemF_correct_l; easy. Qed.

Lemma colT_correct_r :
   {m} n (A : 'G^m) {j0} i {j}, j j0 colT n A j0 i j = 0.
Proof. intros; apply itemF_correct_r; easy. Qed.

Lemma itemT_correct_l :
   m n (x : G) {i0 j0 i j},
    i = i0 j = j0 itemT m n x i0 j0 i j = x.
Proof.
intros; unfold itemT; rewrite rowT_correct_l; try apply itemF_correct_l; easy.
Qed.

Lemma itemT_correct_ri :
   m n (x : G) {i0 j0 i}, i i0 itemT m n x i0 j0 i = 0.
Proof. intros; unfold itemT; apply rowT_correct_r; easy. Qed.

Lemma itemT_correct_rj :
   m n (x : G) {i0 j0 i j}, j j0 itemT m n x i0 j0 i j = 0.
Proof.
intros m n x i0 j0 i j H; unfold itemT.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite (rowT_correct_l _ _ Hi) itemF_correct_r; easy.
rewrite rowT_correct_r; easy.
Qed.

Lemma itemT_correct_r :
   m n (x : G) {i0 j0 i j},
    i i0 j j0 itemT m n x i0 j0 i j = 0.
Proof.
move=>> [H | H].
rewrite itemT_correct_ri; easy.
apply itemT_correct_rj; easy.
Qed.

Lemma itemT_equiv_def :
   m n (x : G) i0 j0, itemT m n x i0 j0 = colT n (itemF m x i0) j0.
Proof.
intros m n x i0 j0; apply extF; intros i; unfold itemT, rowT, colT.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite (itemF_correct_l m x Hi) itemF_correct_l; easy.
rewrite (itemF_correct_r m x Hi) (itemF_correct_r _ _ Hi) itemF_zero; easy.
Qed.

Lemma row1T_correct : {n} (A : 'G^n), row1T A ord0 = A.
Proof. intros; apply rowT_correct_l; easy. Qed.

Lemma col1T_correct : {m} (A : 'G^m) i, col1T A i ord0 = A i.
Proof. intros; apply colT_correct_l; easy. Qed.

Lemma diagT_correct_l : {n} (A : 'G^n) {i j}, i = j diagT A i j = A i.
Proof. intros; unfold diagT; destruct (ord_eq_dec _ _); easy. Qed.

Lemma diagT_correct_r : {n} (A : 'G^n) {i j}, i j diagT A i j = 0.
Proof. intros; unfold diagT; destruct (ord_eq_dec _ _); easy. Qed.

End Monoid_FT_Facts0.

Section Monoid_FT_Facts1.

Properties of constructors rowT/colT/itemT/diagT.

Context {G G1 G2 : AbelianMonoid}.

Lemma itemT_diag :
   m n (x : G) i0 j0, itemT m n x i0 j0 i0 j0 = x.
Proof. intros; apply itemT_correct_l; easy. Qed.

Lemma diagT_diag : {n} (A : 'G^n) i, diagT A i i = A i.
Proof. intros; apply diagT_correct_l; easy. Qed.

Lemma rowT_eq_gen :
   m {n} (A B : 'G^n) i0 k0,
    A = B i0 = k0 rowT m A i0 = rowT m B k0.
Proof. intros; f_equal; easy. Qed.

Lemma colT_eq_gen :
   {m} n (A B : 'G^m) j0 l0,
    A = B j0 = l0 colT n A j0 = colT n B l0.
Proof. intros; f_equal; easy. Qed.

Lemma itemT_eq_gen :
   m n (x y : G) i0 j0 k0 l0,
    x = y i0 = k0 j0 = l0 itemT m n x i0 j0 = itemT m n y k0 l0.
Proof. intros; f_equal; easy. Qed.

Lemma rowT_eq :
   m {n} (A B : 'G^n) i0, A = B rowT m A i0 = rowT m B i0.
Proof. intros; f_equal; easy. Qed.

Lemma colT_eq :
   {m} n (A B : 'G^m) j0, A = B colT n A j0 = colT n B j0.
Proof. intros; f_equal; easy. Qed.

Lemma itemT_eq :
   m n (x y : G) i0 j0, x = y itemT m n x i0 j0 = itemT m n y i0 j0.
Proof. intros; f_equal; easy. Qed.

Lemma diagT_eq : {n} (A B : 'G^n), A = B diagT A = diagT B.
Proof. intros; f_equal; easy. Qed.

Lemma rowT_inj :
   m {n} (A B : 'G^n) i0, rowT m A i0 = rowT m B i0 A = B.
Proof. move=>>; apply itemF_inj. Qed.

Lemma colT_inj :
   {m} n (A B : 'G^m) j0, colT n A j0 = colT n B j0 A = B.
Proof.
movem n A B j0 /extF_rev H; apply extF; intro; apply (itemF_inj n _ _ j0), H.
Qed.

Lemma itemT_inj :
   m n (x y : G) i0 j0, itemT m n x i0 j0 = itemT m n y i0 j0 x = y.
Proof. intros; apply (itemF_inj n _ _ j0), (rowT_inj m _ _ i0); easy. Qed.

Lemma diagT_inj : {n} (A B : 'G^n), diagT A = diagT B A = B.
Proof.
moven A B /extT_rev H; apply extF; intros i.
specialize (H i i); rewrite 2!diagT_diag in H; easy.
Qed.

Lemma row_rowT : m {n} (A : 'G^n) i0, row (rowT m A i0) i0 = A.
Proof. intros; apply itemF_diag. Qed.

Lemma rowT_row : {m n} (M : 'G^{m,n}) i0, rowT m (row M i0) i0 i0 = M i0.
Proof. intros; apply row_rowT. Qed.

Lemma col_colT : {m} n (A : 'G^m) j0, col (colT n A j0) j0 = A.
Proof. intros; apply extF; intro; apply itemF_diag. Qed.

Lemma colT_col : {m n} (M : 'G^{m,n}) j0, (colT n (col M j0) j0)^~ j0 = M^~ j0.
Proof. intros; apply col_colT. Qed.

Lemma flipT_rowT : m {n} (A : 'G^n) i0, flipT (rowT m A i0) = colT m A i0.
Proof. intros; apply extT; move=>>; apply itemF_sym. Qed.

Lemma flipT_colT : {m} n (A : 'G^m) j0, flipT (colT n A j0) = rowT n A j0.
Proof. intros; apply extT; move=>>; symmetry; apply itemF_sym. Qed.

Lemma flipT_itemT :
   m n (x : G) i0 j0, flipT (itemT m n x i0 j0) = itemT n m x j0 i0.
Proof.
intros m n x i0 j0; apply extT; intros i j; unfold flipT.
destruct (ord_eq_dec j i0) as [Hj | Hj], (ord_eq_dec i j0) as [Hi | Hi].
rewrite → 2!itemT_correct_l; easy.
rewriteitemT_correct_rj, itemT_correct_ri; easy.
1,2: rewriteitemT_correct_ri, itemT_correct_rj; easy.
Qed.

Lemma flipT_diagT : {n} (A : 'G^n), flipT (diagT A) = diagT A.
Proof.
intros n A; apply extT; intros i j; unfold flipT; destruct (ord_eq_dec i j) as [H | H].
rewrite H; easy.
rewrite (diagT_correct_r _ H) (diagT_correct_r _ (not_eq_sym H)); easy.
Qed.

Lemma mapT_rowT :
   m {n} (f : G1 G2) (A : 'G1^n) i0,
    f 0 = 0 mapT f (rowT m A i0) = rowT m (mapF f A) i0.
Proof. intros; apply mapF_itemF_0, mapF_zero; easy. Qed.

Lemma mapT_colT :
   {m} n (f : G1 G2) (A : 'G1^m) j0,
    f 0 = 0 mapT f (colT n A j0) = colT n (mapF f A) j0.
Proof.
intros; apply extT; move=>>; unfold mapT; rewrite mapF_correct mapF_itemF_0; easy.
Qed.

Lemma mapT_itemT :
   m n (f : G1 G2) (x : G1) i0 j0,
    f 0 = 0 mapT f (itemT m n x i0 j0) = itemT m n (f x) i0 j0.
Proof. intros; rewrite mapT_rowT; try rewrite mapF_itemF_0; easy. Qed.

Lemma mapT_diagT :
   n (f : G1 G2) (A : 'G1^n),
    f 0 = 0 mapT f (diagT A) = diagT (mapF f A).
Proof.
intros n f A Hf; apply extT; intros i j; rewrite mapT_correct.
destruct (ord_eq_dec i j) as [H | H].
rewrite → 2!diagT_correct_l; easy.
rewrite → 2!diagT_correct_r; easy.
Qed.

End Monoid_FT_Facts1.

Section Monoid_FT_Facts2.

Properties with the identity element of monoids (zero).

Context {G G1 G2 : AbelianMonoid}.

Lemma hat0nT_is_zero : {n} (M : 'G^{0,n}), M = 0.
Proof. intros; apply nil_is_zero. Qed.

Lemma hatm0T_is_zero : {m} (M : 'G^{m,0}), M = 0.
Proof. intros; apply extF; intro; apply nil_is_zero. Qed.

Lemma zeroT : {m n} (i : 'I_m) (j : 'I_n), 0 i j = (0 : G).
Proof. easy. Qed.

Lemma constT_zero : {m n}, constT m n (0 : G) = 0.
Proof. easy. Qed.

Lemma blk1T_zero : blk1T (0 : G) = 0.
Proof. easy. Qed.

Lemma blk2T_zero : blk2T (0 : G) (0 : G) (0 : G) (0 : G) = 0.
Proof. unfold blk2T; rewrite 2!coupleF_zero; easy. Qed.

Lemma rowT_zero : m {n} i0, rowT m (0 : 'G^n) i0 = 0.
Proof.
intros m n i0; apply extF; intros i; destruct (ord_eq_dec i i0);
    [apply rowT_correct_l | apply rowT_correct_r]; easy.
Qed.

Lemma colT_zero : {m} n j0, colT n (0 : 'G^m) j0 = 0.
Proof. intros; apply flipT_inj; rewrite flipT_colT rowT_zero; easy. Qed.

Lemma itemT_zero : m n i0 j0, itemT m n (0 : G) i0 j0 = 0.
Proof. intros; unfold itemT; rewrite itemF_zero rowT_zero; easy. Qed.

Lemma diagT_zero : {n}, diagT (0 : 'G^n) = 0.
Proof.
intros n; apply extT; intros i j; destruct (ord_eq_dec i j);
    [rewrite diagT_correct_l | rewrite diagT_correct_r]; easy.
Qed.

Lemma castTr_zero :
   {m1 m2 n} (Hm : m1 = m2), castTr Hm (0 : 'G^{m1,n}) = 0.
Proof. easy. Qed.

Lemma castTc_zero :
   {m n1 n2} (Hn : n1 = n2), castTc Hn (0 : 'G^{m,n1}) = 0.
Proof. easy. Qed.

Lemma castT_zero :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2),
    castT Hm Hn (0 : 'G^{m1,n1}) = 0.
Proof. easy. Qed.

Lemma upT_zero : {m1 m2 n}, upT (0 : 'G^{m1 + m2,n}) = 0.
Proof. easy. Qed.

Lemma downT_zero : {m1 m2 n}, downT (0 : 'G^{m1 + m2,n}) = 0.
Proof. easy. Qed.

Lemma leftT_zero : {m n1 n2}, leftT (0 : 'G^{m,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma rightT_zero : {m n1 n2}, rightT (0 : 'G^{m,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma ulT_zero : {m1 m2 n1 n2}, ulT (0 : 'G^{m1 + m2,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma urT_zero : {m1 m2 n1 n2}, urT (0 : 'G^{m1 + m2,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma dlT_zero : {m1 m2 n1 n2}, dlT (0 : 'G^{m1 + m2,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma drT_zero : {m1 m2 n1 n2}, drT (0 : 'G^{m1 + m2,n1 + n2}) = 0.
Proof. easy. Qed.

Lemma concatTr_zero :
   {m1 m2 n}, concatTr (0 : 'G^{m1,n}) (0 : 'G^{m2,n}) = 0.
Proof. intros; apply concatF_zero. Qed.

Lemma concatTc_zero :
   {m n1 n2}, concatTc (0 : 'G^{m,n1}) (0 : 'G^{m,n2}) = 0.
Proof. intros; apply extF; intro; apply concatF_zero. Qed.

Lemma concatT_zero :
   {m1 m2 n1 n2}, concatT (0 : 'G^{m1,n1}) 0 0 (0 : 'G^{m2,n2}) = 0.
Proof.
intros; unfold concatT; rewrite 2!concatTc_zero concatTr_zero; easy.
Qed.

Lemma insertTr_zero : {m n} i0, insertTr (0 : 'G^{m,n}) 0 i0 = 0.
Proof. intros; apply insertF_zero. Qed.

Lemma insertTc_zero : {m n} j0, insertTc (0 : 'G^{m,n}) 0 j0 = 0.
Proof. intros; apply extF; intro; apply insertF_zero. Qed.

Lemma insertT_zero :
   {m n} i0 j0, insertT (0 : 'G^{m,n}) 0 0 0 i0 j0 = 0.
Proof.
intros; unfold insertT; rewrite insertTc_zero insertF_zero insertTr_zero; easy.
Qed.

Lemma skipTr_zero : {m n} i0, skipTr (0 : 'G^{m.+1,n}) i0 = 0.
Proof. easy. Qed.

Lemma skipTc_zero : {m n} j0, skipTc (0 : 'G^{m,n.+1}) j0 = 0.
Proof. easy. Qed.

Lemma skipT_zero : {m n} i0 j0, skipT (0 : 'G^{m.+1,n.+1}) i0 j0 = 0.
Proof. easy. Qed.

Lemma replaceTr_zero : {m n} i0, replaceTr (0 : 'G^{m,n}) 0 i0 = 0.
Proof. intros; apply replaceF_zero. Qed.

Lemma replaceTc_zero : {m n} j0, replaceTc (0 : 'G^{m,n}) 0 j0 = 0.
Proof. intros; apply extF; intro; apply replaceF_zero. Qed.

Lemma replaceT_zero :
   {m n} i0 j0, replaceT (0 : 'G^{m,n}) 0 0 0 i0 j0 = 0.
Proof.
intros; unfold replaceT;
    rewrite replaceTc_zero replaceF_zero replaceTr_zero; easy.
Qed.

Lemma mapT_zero :
   {m n} (f : G1 G2), f 0 = 0 mapT f (0 : 'G1^{m,n}) = 0.
Proof. intros; do 2 apply mapF_zero; easy. Qed.

Lemma mapT_zero_f :
   {m n} (M : 'G1^{m,n}), mapT (0 : G1 G2) M = 0.
Proof. intros; unfold mapT; rewrite mapF_zero_f; easy. Qed.

Lemma constT_zero_compat : {m n} (x : G), x = 0 constT m n x = 0.
Proof. move=>> H; rewrite H; apply constT_zero. Qed.

Lemma blk1T_zero_compat : (x00 : G), x00 = 0 blk1T x00 = 0.
Proof. move=>> H00; rewrite H00; apply blk1T_zero. Qed.

Lemma blk2T_zero_compat :
   (x00 x01 x10 x11 : G),
    x00 = 0 x01 = 0 x10 = 0 x11 = 0 blk2T x00 x01 x10 x11 = 0.
Proof. move=>> H00 H01 H10 H11; rewrite H00 H01 H10 H11; apply blk2T_zero. Qed.

Lemma rowT_zero_compat : m {n} (A : 'G^n) i0, A = 0 rowT m A i0 = 0.
Proof. move=>> H; rewrite H; apply rowT_zero. Qed.

Lemma colT_zero_compat : {m} n (A : 'G^m) j0, A = 0 colT n A j0 = 0.
Proof. move=>> H; rewrite H; apply colT_zero. Qed.

Lemma itemT_zero_compat :
   m n (x : G) i0 j0, x = 0 itemT m n x i0 j0 = 0.
Proof. move=>> H; rewrite H; apply itemT_zero. Qed.

Lemma diagT_zero_compat : {n} (A : 'G^n), A = 0 diagT A = 0.
Proof. move=>> H; rewrite H; apply diagT_zero. Qed.

Lemma castTr_zero_compat :
   {m1 m2 n} (Hm : m1 = m2) (M : 'G^{m1,n}), M = 0 castTr Hm M = 0.
Proof. move=>>; apply castF_zero_compat. Qed.

Lemma castTc_zero_compat :
   {m n1 n2} (Hn : n1 = n2) (M : 'G^{m,n1}), M = 0 castTc Hn M = 0.
Proof. move=>> Hn; rewrite Hn; apply castTc_zero. Qed.

Lemma castT_zero_compat :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M : 'G^{m1,n1}),
    M = 0 castT Hm Hn M = 0.
Proof. move=>> H; rewrite H; apply castT_zero. Qed.

Lemma upT_zero_compat :
   {m1 m2 n} (M : 'G^{m1 + m2,n}),
    ( i : 'I_(m1 + m2), (i < m1)%coq_nat M i = 0) upT M = 0.
Proof. move=>>; apply firstF_zero_compat. Qed.

Lemma downT_zero_compat :
   {m1 m2 n} (M : 'G^{m1 + m2,n}),
    ( i : 'I_(m1 + m2), (m1 i)%coq_nat M i = 0) downT M = 0.
Proof. move=>>; apply lastF_zero_compat. Qed.

Lemma leftT_zero_compat :
   {m n1 n2} (M : 'G^{m,n1 + n2}),
    ( i (j : 'I_(n1 + n2)), (j < n1)%coq_nat M i j = 0)
    leftT M = 0.
Proof. intros; apply extF; intro; apply firstF_zero_compat; auto. Qed.

Lemma rightT_zero_compat :
   {m n1 n2} (M : 'G^{m,n1 + n2}),
    ( i (j : 'I_(n1 + n2)), (n1 j)%coq_nat M i j = 0)
    rightT M = 0.
Proof. intros; apply extF; intro; apply lastF_zero_compat; auto. Qed.

Lemma ulT_zero_compat :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (i < m1)%coq_nat (j < n1)%coq_nat M i j = 0)
    ulT M = 0.
Proof. move=>> H; erewrite <- ulT_zero; apply ulT_compat, H. Qed.

Lemma urT_zero_compat :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (i < m1)%coq_nat (n1 j)%coq_nat M i j = 0)
    urT M = 0.
Proof. move=>> H; erewrite <- urT_zero; apply urT_compat, H. Qed.

Lemma dlT_zero_compat :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (m1 i)%coq_nat (j < n1)%coq_nat M i j = 0)
    dlT M = 0.
Proof. move=>> H; erewrite <- dlT_zero; apply dlT_compat, H. Qed.

Lemma drT_zero_compat :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    ( (i : 'I_(m1 + m2)) (j : 'I_(n1 + n2)),
      (m1 i)%coq_nat (n1 j)%coq_nat M i j = 0)
    drT M = 0.
Proof. move=>> H; erewrite <- drT_zero; apply drT_compat, H. Qed.

Lemma splitTr_zero_compat :
   {m1 m2 n} (M : 'G^{m1 + m2,n}), M = 0 upT M = 0 downT M = 0.
Proof. move=>>; apply splitF_zero_compat. Qed.

Lemma splitTc_zero_compat :
   {m n1 n2} (M : 'G^{m,n1 + n2}), M = 0 leftT M = 0 rightT M = 0.
Proof. move=>> H; rewrite H leftT_zero rightT_zero; easy. Qed.

Lemma splitT_zero_compat :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    M = 0 ulT M = 0 urT M = 0 dlT M = 0 drT M = 0.
Proof. move=>> H; rewrite H ulT_zero urT_zero dlT_zero drT_zero; easy. Qed.

Lemma concatTr_zero_compat :
   {m1 m2 n} (M1 : 'G^{m1,n}) (M2 : 'G^{m2,n}),
    M1 = 0 M2 = 0 concatTr M1 M2 = 0.
Proof. move=>>; apply concatF_zero_compat. Qed.

Lemma concatTc_zero_compat :
   {m n1 n2} (M1 : 'G^{m,n1}) (M2 : 'G^{m,n2}),
    M1 = 0 M2 = 0 concatTc M1 M2 = 0.
Proof. move=>> H1 H2; rewrite H1 H2; apply concatTc_zero. Qed.

Lemma concatT_zero_compat :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    M11 = 0 M12 = 0 M21 = 0 M22 = 0 concatT M11 M12 M21 M22 = 0.
Proof.
move=>> H11 H12 H21 H22; rewrite H11 H12 H21 H22; apply concatT_zero.
Qed.

Lemma insertTr_zero_compat :
   {m n} (M : 'G^{m,n}) A i0, M = 0 A = 0 insertTr M A i0 = 0.
Proof. move=>>; apply insertF_zero_compat. Qed.

Lemma insertTc_zero_compat :
   {m n} (M : 'G^{m,n}) B j0, M = 0 B = 0 insertTc M B j0 = 0.
Proof. move=>> HM HB; rewrite HM HB; apply insertTc_zero. Qed.

Lemma insertT_zero_compat :
   {m n} (M : 'G^{m,n}) A B x i0 j0,
    M = 0 A = 0 B = 0 x = 0 insertT M A B x i0 j0 = 0.
Proof. move=>> HM HA HB Hx; rewrite HM HA HB Hx; apply insertT_zero. Qed.

Lemma skipTr_zero_compat :
   {m n} (M : 'G^{m.+1,n}) i0, eqxTr M 0 i0 skipTr M i0 = 0.
Proof. move=>>; apply skipF_zero_compat. Qed.

Lemma skipTc_zero_compat :
   {m n} (M : 'G^{m,n.+1}) j0, eqxTc M 0 j0 skipTc M j0 = 0.
Proof. intros; erewrite <- skipTc_zero; apply skipTc_compat; easy. Qed.

Lemma skipT_zero_compat :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0, eqxT M 0 i0 j0 skipT M i0 j0 = 0.
Proof. intros; erewrite <- skipT_zero; apply skipT_compat; easy. Qed.

Lemma replaceTr_zero_compat :
   {m n} (M : 'G^{m,n}) A i0,
    eqxTr M 0 i0 A = 0 replaceTr M A i0 = 0.
Proof. move=>>; apply replaceF_zero_compat. Qed.

Lemma replaceTc_zero_compat :
   {m n} (M : 'G^{m,n}) B j0,
    eqxTc M 0 j0 B = 0 replaceTc M B j0 = 0.
Proof. intros; erewrite <- replaceTc_zero; apply replaceTc_compat; easy. Qed.

Lemma replaceT_zero_compat :
   {m n} (M : 'G^{m,n}) A B x i0 j0,
    eqxT M 0 i0 j0 eqxF A 0 j0 eqxF B 0 i0 x = 0
    replaceT M A B x i0 j0 = 0.
Proof. intros; erewrite <- replaceT_zero; apply replaceT_compat; easy. Qed.

Lemma mapT_zero_compat :
   {m n} (f : G1 G2) (M : 'G1^{m,n}),
    f 0 = 0 M = 0 mapT f M = 0.
Proof. move=>> Hf HM; rewrite HM; apply mapT_zero; easy. Qed.

Lemma mapT_zero_compat_f :
   {m n} (f : G1 G2) (M : 'G1^{m,n}), f = 0 mapT f M = 0.
Proof. move=>> H; rewrite H; apply mapT_zero_f. Qed.

Lemma constT_zero_reg : {m n} (x : G), constT m.+1 n.+1 x = 0 x = 0.
Proof. intros; apply (constT_inj m n); easy. Qed.

Lemma blk1T_zero_reg : (x00 : G), blk1T x00 = 0 x00 = 0.
Proof. intros; apply blk1T_inj; rewrite blk1T_zero; easy. Qed.

Lemma blk2T_zero_reg :
   (x00 x01 x10 x11 : G),
    blk2T x00 x01 x10 x11 = 0 x00 = 0 x01 = 0 x10 = 0 x11 = 0.
Proof. intros; apply blk2T_inj; rewrite blk2T_zero; easy. Qed.

Lemma rowT_zero_reg : m {n} (A : 'G^n) i0, rowT m A i0 = 0 A = 0.
Proof. move=>>; apply itemF_zero_reg. Qed.

Lemma colT_zero_reg : {m} n (A : 'G^m) j0, colT n A j0 = 0 A = 0.
Proof. move=>> H; eapply colT_inj; rewrite colT_zero; apply H. Qed.

Lemma itemT_zero_reg : m n (x : G) i0 j0, itemT m n x i0 j0 = 0 x = 0.
Proof. move=>> H; eapply itemT_inj; rewrite itemT_zero; apply H. Qed.

Lemma diagT_zero_reg : {n} (A : 'G^n), diagT A = 0 A = 0.
Proof. intros; eapply diagT_inj; rewrite diagT_zero; easy. Qed.

Lemma castTr_zero_reg :
   {m1 m2 n} (Hm : m1 = m2) (M : 'G^{m1,n}), castTr Hm M = 0 M = 0.
Proof. move=>>; apply castF_zero_reg. Qed.

Lemma castTc_zero_reg :
   {m n1 n2} (Hn : n1 = n2) (M : 'G^{m,n1}), castTc Hn M = 0 M = 0.
Proof. move=>> H; eapply castTc_inj; apply H. Qed.

Lemma castT_zero_reg :
   {m1 m2 n1 n2} (Hm : m1 = m2) (Hn : n1 = n2) (M : 'G^{m1,n1}),
    castT Hm Hn M = 0 M = 0.
Proof. move=>>H; eapply castT_inj; apply H. Qed.

Lemma splitTr_zero_reg :
   {m1 m2 n} (M : 'G^{m1 + m2,n}), upT M = 0 downT M = 0 M = 0.
Proof. move=>>; apply splitF_zero_reg. Qed.

Lemma splitTc_zero_reg :
   {m n1 n2} (M : 'G^{m,n1 + n2}), leftT M = 0 rightT M = 0 M = 0.
Proof. intros; apply splitTc_reg; easy. Qed.

Lemma splitT_zero_reg :
   {m1 m2 n1 n2} (M : 'G^{m1 + m2,n1 + n2}),
    ulT M = 0 urT M = 0 dlT M = 0 drT M = 0 M = 0.
Proof. intros; apply splitT_reg; easy. Qed.

Lemma concatTr_zero_reg_u :
   {m1 m2 n} (M1 : 'G^{m1,n}) (M2 : 'G^{m2,n}),
    concatTr M1 M2 = 0 M1 = 0.
Proof. move=>>; apply concatF_zero_reg_l. Qed.

Lemma concatTr_zero_reg_d :
   {m1 m2 n} (M1 : 'G^{m1,n}) (M2 : 'G^{m2,n}),
    concatTr M1 M2 = 0 M2 = 0.
Proof. move=>>; apply concatF_zero_reg_r. Qed.

Lemma concatTr_zero_reg :
   {m1 m2 n} (M1 : 'G^{m1,n}) (M2 : 'G^{m2,n}),
    concatTr M1 M2 = 0 M1 = 0 M2 = 0.
Proof. move=>>; apply concatF_zero_reg. Qed.

Lemma concatTc_zero_reg_l :
   {m n1 n2} (M1 : 'G^{m,n1}) (M2 : 'G^{m,n2}),
    concatTc M1 M2 = 0 M1 = 0.
Proof. move=>>; rewrite -concatTc_zero; apply concatTc_inj_l. Qed.

Lemma concatTc_zero_reg_r :
   {m n1 n2} (M1 : 'G^{m,n1}) (M2 : 'G^{m,n2}),
    concatTc M1 M2 = 0 M2 = 0.
Proof. move=>>; rewrite -concatTc_zero; apply concatTc_inj_r. Qed.

Lemma concatTc_zero_reg :
   {m n1 n2} (M1 : 'G^{m,n1}) (M2 : 'G^{m,n2}),
    concatTc M1 M2 = 0 M1 = 0 M2 = 0.
Proof. move=>>; rewrite -concatTc_zero; apply concatTc_inj. Qed.

Lemma concatT_zero_reg_ul :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    concatT M11 M12 M21 M22 = 0 M11 = 0.
Proof. move=>>; rewrite -concatT_zero; apply concatT_inj_ul. Qed.

Lemma concatT_zero_reg_ur :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    concatT M11 M12 M21 M22 = 0 M12 = 0.
Proof. move=>>; rewrite -concatT_zero; apply concatT_inj_ur. Qed.

Lemma concatT_zero_reg_dl :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    concatT M11 M12 M21 M22 = 0 M21 = 0.
Proof. move=>>; rewrite -concatT_zero; apply concatT_inj_dl. Qed.

Lemma concatT_zero_reg_dr :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    concatT M11 M12 M21 M22 = 0 M22 = 0.
Proof. move=>>; rewrite -concatT_zero; apply concatT_inj_dr. Qed.

Lemma concatT_zero_reg :
   {m1 m2 n1 n2} (M11 : 'G^{m1,n1}) (M12 : 'G^{m1,n2})
      (M21 : 'G^{m2,n1}) (M22 : 'G^{m2,n2}),
    concatT M11 M12 M21 M22 = 0 M11 = 0 M12 = 0 M21 = 0 M22 = 0.
Proof. move=>>; rewrite -concatT_zero; apply concatT_inj. Qed.

Lemma insertTr_zero_reg_l :
   {m n} (M : 'G^{m,n}) A i0, insertTr M A i0 = 0 M = 0.
Proof. move=>>; apply insertF_zero_reg_l. Qed.

Lemma insertTr_zero_reg_r :
   {m n} (M : 'G^{m,n}) A i0, insertTr M A i0 = 0 A = 0.
Proof. move=>>; apply insertF_zero_reg_r. Qed.

Lemma insertTc_zero_reg_l :
   {m n} (M : 'G^{m,n}) B j0, insertTc M B j0 = 0 M = 0.
Proof. move=>>; erewrite <- insertTc_zero at 1; apply insertTc_inj_l. Qed.

Lemma insertTc_zero_reg_r :
   {m n} (M : 'G^{m,n}) B j0, insertTc M B j0 = 0 B = 0.
Proof. move=>>; erewrite <- insertTc_zero at 1; apply insertTc_inj_r. Qed.

Lemma insertT_zero_reg_l :
   {m n} (M : 'G^{m,n}) A B x i0 j0, insertT M A B x i0 j0 = 0 M = 0.
Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_l. Qed.

Lemma insertT_zero_reg_ml :
   {m n} (M : 'G^{m,n}) A B x i0 j0, insertT M A B x i0 j0 = 0 A = 0.
Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_ml. Qed.

Lemma insertT_zero_reg_mr :
   {m n} (M : 'G^{m,n}) A B x i0 j0, insertT M A B x i0 j0 = 0 B = 0.
Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_mr. Qed.

Lemma insertT_zero_reg_r :
   {m n} (M : 'G^{m,n}) A B x i0 j0, insertT M A B x i0 j0 = 0 x = 0.
Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_r. Qed.

Lemma skipTr_zero_reg :
   {m n} (M : 'G^{m.+1,n}) i0, skipTr M i0 = 0 eqxTr M 0 i0.
Proof. move=>>; apply skipF_zero_reg. Qed.

Lemma skipTc_zero_reg :
   {m n} (M : 'G^{m,n.+1}) j0, skipTc M j0 = 0 eqxTc M 0 j0.
Proof. move=>>; erewrite <- skipTc_zero; apply skipTc_reg. Qed.

Lemma skipT_zero_reg :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0, skipT M i0 j0 = 0 eqxT M 0 i0 j0.
Proof. move=>>; erewrite <- skipT_zero; apply skipT_reg. Qed.

Lemma replaceTr_zero_reg_l :
   {m n} (M : 'G^{m,n}) A i0, replaceTr M A i0 = 0 eqxTr M 0 i0.
Proof. move=>>; apply replaceF_zero_reg_l. Qed.

Lemma replaceTr_zero_reg_r :
   {m n} (M : 'G^{m,n}) A i0, replaceTr M A i0 = 0 A = 0.
Proof. move=>>; apply replaceF_zero_reg_r. Qed.

Lemma replaceTc_zero_reg_l :
   {m n} (M : 'G^{m,n}) B j0, replaceTc M B j0 = 0 eqxTc M 0 j0.
Proof. move=>>; erewrite <- replaceTc_zero at 1; apply replaceTc_reg_l. Qed.

Lemma replaceTc_zero_reg_r :
   {m n} (M : 'G^{m,n}) B j0, replaceTc M B j0 = 0 B = 0.
Proof. move=>>; erewrite <- replaceTc_zero at 1; apply replaceTc_reg_r. Qed.

Lemma replaceT_zero_reg_l :
   {m n} (M : 'G^{m,n}) A B x i0 j0,
    replaceT M A B x i0 j0 = 0 eqxT M 0 i0 j0.
Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_l. Qed.

Lemma replaceT_zero_reg_ml :
   {m n} (M : 'G^{m,n}) A B x i0 j0,
    replaceT M A B x i0 j0 = 0 eqxF A 0 j0.
Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_ml. Qed.

Lemma replaceT_zero_reg_mr :
   {m n} (M : 'G^{m,n}) A B x i0 j0,
    replaceT M A B x i0 j0 = 0 eqxF B 0 i0.
Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_mr. Qed.

Lemma replaceT_zero_reg_r :
   {m n} (M : 'G^{m,n}) A B x i0 j0, replaceT M A B x i0 j0 = 0 x = 0.
Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_r. Qed.

Lemma mapT_zero_reg :
   {m n} (f : G1 G2) (M : 'G1^{m,n}),
    ( x, f x = 0 x = 0) mapT f M = 0 M = 0.
Proof. move=>> H; apply mapF_zero_reg; intro; apply mapF_zero_reg; easy. Qed.

Lemma mapT_zero_reg_f :
   m n (f : G1 G2),
    ( (M : 'G1^{m.+1,n.+1}), mapT f M = 0) f = 0.
Proof. move=>> H; eapply mapT_inj_f; intros; apply H. Qed.

Lemma eqxTr_zero_equiv :
   {m n} (M : 'G^{m.+1,n}) i0, eqxTr M 0 i0 skipTr M i0 = 0.
Proof. intros; apply eqxF_zero_equiv. Qed.

Lemma eqxTc_zero_equiv :
   {m n} (M : 'G^{m,n.+1}) j0, eqxTc M 0 j0 skipTc M j0 = 0.
Proof. intros m n M j0; rewrite -(skipTc_zero j0); apply eqxTc_equiv. Qed.

Lemma eqxT_zero_equiv :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
    eqxT M 0 i0 j0 skipT M i0 j0 = 0.
Proof. intros m n M i0 j0; rewrite -(skipT_zero i0 j0); apply eqxT_equiv. Qed.

Lemma neqxTr_zero_equiv :
   {m n} (M : 'G^{m.+1,n}) i0, neqxTr M 0 i0 skipTr M i0 0.
Proof. intros; apply neqxF_zero_equiv. Qed.

Lemma neqxTc_zero_equiv :
   {m n} (M : 'G^{m,n.+1}) j0, neqxTc M 0 j0 skipTc M j0 0.
Proof. intros m n M j0; rewrite -(skipTc_zero j0); apply neqxTc_equiv. Qed.

Lemma neqxT_zero_equiv :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
    neqxT M 0 i0 j0 skipT M i0 j0 0.
Proof. intros m n M i0 j0; rewrite -(skipT_zero i0 j0); apply neqxT_equiv. Qed.

Lemma extTr_zero_splitTr :
   {m m1 m2 n} (Hm : m = (m1 + m2)%nat) (M : 'G^{m,n}),
    upT (castTr Hm M) = 0 downT (castTr Hm M) = 0 M = 0.
Proof. move=>>; apply extF_zero_splitF. Qed.

Lemma extTc_zero_splitTc :
   {m n n1 n2} (Hn : n = (n1 + n2)%nat) (M : 'G^{m,n}),
    leftT (castTc Hn M) = 0 rightT (castTc Hn M) = 0 M = 0.
Proof. move=>> Hl Hr; eapply extTc_splitTc. apply Hl. apply Hr. Qed.

Lemma extT_zero_splitT :
   {m m1 m2 n n1 n2}
      (Hm : m = (m1 + m2)%nat) (Hn : n = (n1 + n2)%nat) (M : 'G^{m,n}),
    ulT (castT Hm Hn M) = 0 urT (castT Hm Hn M) = 0
    dlT (castT Hm Hn M) = 0 drT (castT Hm Hn M) = 0
    M = 0.
Proof.
move=>> Hul Hur Hdl Hdr; eapply extT_splitT.
apply Hul. apply Hur. apply Hdl. apply Hdr.
Qed.

Lemma extT_zero_skipTr :
   {m n} (M : 'G^{m.+1,n}) i0, row M i0 = 0 skipTr M i0 = 0 M = 0.
Proof. move=>>; apply extF_zero_skipF. Qed.

Lemma extT_zero_skipTc :
   {m n} (M : 'G^{m,n.+1}) j0, col M j0 = 0 skipTc M j0 = 0 M = 0.
Proof. move=>>; erewrite <- skipTc_zero; apply: extT_skipTc. Qed.

Lemma extT_zero_skipT :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
    row M i0 = 0 col M j0 = 0 skipT M i0 j0 = 0 M = 0.
Proof. move=>>; erewrite <- skipT_zero; apply: extT_skipT. Qed.

Lemma skipTr_nextT_zero_reg :
   {m n} (M : 'G^{m.+1,n}) i0, skipTr M i0 0 neqxTr M 0 i0.
Proof. move=>>; apply skipF_nextF_zero_reg. Qed.

Lemma skipTc_nextT_zero_reg :
   {m n} (M : 'G^{m,n.+1}) j0, skipTc M j0 0 neqxTc M 0 j0.
Proof. move=>>; erewrite <- skipTc_zero; apply skipTc_neqxTc_reg. Qed.

Lemma skipT_nextT_zero_reg :
   {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
    skipT M i0 j0 0 neqxT M 0 i0 j0.
Proof. move=>>; erewrite <- skipT_zero; apply skipT_neqxT_reg. Qed.

End Monoid_FT_Facts2.