Library Algebra.Monoid.Monoid_FF

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 families on commutative monoids.

Description

Let G be an AbelianMonoid, and T be any type.

Constructor

Let x be in G.
  • itemF n x i0 is the n-family with i0-th item equal to x, and others set to 0.

Operators

Let u1 and u2 respectively be an n1-family and an n2-family in G. Let f : 'I_n1 'I_n2.
  • unfun0F f u1 is the n2-family with values of u1 on f 'I_n1, in the same order, and zero elsewhere.
Let P be a predicate on 'I_n.
  • maskPF0 P A x is the n-family with values of A when P holds and 0 otherwise, in the same order.
Let u be an n-family in G. Let v an n-family of any type T.
  • filter0F u keeps the zero items of u, in the same order;
  • filter0F_gen u v keeps the items of v with zero value of u, in the same order;
  • filter_n0F u keeps the nonzero items of u, in the same order;
  • filter_n0F_gen u v keeps the items of v with nonzero value of u, in the same order.
Let u be an n.+1-family in G.
  • squeezeF u i0 i1 is the n-family where i1-th item is added to i0_th item and skipped.

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

Local Open Scope Monoid_scope.

Section Monoid_FF_Def.

Context {G : AbelianMonoid}.

Definition itemF n x i0 : 'G^n := replaceF 0 x i0.

Definition unfun0F {n1 n2} (f : 'I_{n1,n2}) (u1 : 'G^n1) : 'G^n2 :=
  unfunF f u1 0.

Definition maskPF0 {n} (P : 'Prop^n) (u : 'G^n) : 'G^n := maskPF P u 0.

Definition filter0F_gen {T : Type} {n} (u : 'G^n) (v : 'T^n) :=
  filter_eqF_gen u 0 v.

Definition filter0F {n} (u : 'G^n) := filter_eqF u 0.

Definition filter_n0F_gen {T : Type} {n} (u : 'G^n) (v : 'T^n) :=
  filter_neqF_gen u 0 v.

Definition filter_n0F {n} (u : 'G^n) := filter_neqF u 0.

Definition split0F_gen {T : Type} {n} (u : 'G^n) (v : 'T^n) :=
  split_eqF_gen u 0 v.

Definition split0F {n} (u : 'G^n) := split_eqF u 0.

Definition squeezeF {n} (u : 'G^n.+1) (i0 i1 : 'I_n.+1) : 'G^n :=
  skipF (replaceF u (u i0 + u i1) i0) i1.

End Monoid_FF_Def.

Section Monoid_FF_Facts0.

Correctness lemmas.

Context {G : AbelianMonoid}.

Lemma itemF_correct_l :
   n (x : G) {i0 i}, i = i0 itemF n x i0 i = x.
Proof. move=>>; unfold itemF; apply replaceF_correct_l. Qed.

Lemma itemF_correct_r :
   n (x : G) {i0 i}, i i0 itemF n x i0 i = 0.
Proof. intros; unfold itemF; rewrite replaceF_correct_r; easy. Qed.

Lemma unfun0F_correct_l :
   {n1 n2} (f : 'I_{n1,n2}) (u1 : 'G^n1) i1 i2,
    injective f f i1 = i2 unfun0F f u1 i2 = u1 i1.
Proof. move=>>; apply unfunF_correct_l. Qed.

Lemma unfun0F_correct_r :
   {n1 n2} (f : 'I_{n1,n2}) (u1 : 'G^n1) i2,
    ( i1, f i1 i2) unfun0F f u1 i2 = 0.
Proof. move=>>; apply unfunF_correct_r. Qed.

Lemma unfun0F_correct :
   {n1 n2} {f : 'I_{n1,n2}} (u1 : 'G^n1) i2,
    injective f
    ( i1, f i1 = i2 unfun0F f u1 i2 = u1 i1)
    ( i1, f i1 i2) unfun0F f u1 i2 = 0.
Proof. move=>>; apply unfunF_correct. Qed.

Lemma funF_unfun0F :
   {n1 n2} (f : 'I_{n1,n2}),
    injective f cancel (unfun0F f) (@funF G _ _ f).
Proof. move=>>; apply funF_unfunF. Qed.

Lemma unfun0F_funF :
   {n1 n2} (f : 'I_{n1,n2}) (u2 : 'G^n2),
    injective f unfun0F f (funF f u2) = maskPF0 (image f fullset) u2.
Proof. move=>>; apply unfunF_funF. Qed.

Lemma maskPF0_correct_l :
   {n} {P : 'Prop^n} {u : 'G^n} i, P i maskPF0 P u i = u i.
Proof. move=>>; apply maskPF_correct_l. Qed.

Lemma maskPF0_correct_r :
   {n} {P : 'Prop^n} {u : 'G^n} i, ¬ P i maskPF0 P u i = 0.
Proof. move=>>; apply maskPF_correct_r. Qed.

Lemma filter0F_correct : {n} (u : 'G^n), filter0F u = 0.
Proof.
intros n u; apply extF; intro; unfold filter0F, filter0F_gen.
apply (filterP_ord_correct (fun iu i = 0)).
Qed.

Lemma filter_n0F_correct : {n} (u : 'G^n) i, filter_n0F u i 0.
Proof.
intros n u i; unfold filter0F, filter0F_gen.
apply (filterP_ord_correct (fun iu i 0)).
Qed.

Lemma split0F_gen_correct :
   {T : Type} {n} (u : 'G^n) (v : 'T^n),
    split0F_gen u v = concatF (filter0F_gen u v) (filter_n0F_gen u v).
Proof. easy. Qed.

Lemma split0F_correct :
   {n} (u : 'G^n), split0F u = concatF (filter0F u) (filter_n0F u).
Proof. easy. Qed.

Lemma squeezeF_correct_l :
   {n} (u : 'G^n.+1) {i0 i1} (Hi : i0 i1),
    squeezeF u i0 i1 (insert_ord Hi) = u i0 + u i1.
Proof.
move=>>; unfold squeezeF; rewrite skipF_correct replaceF_correct_l; easy.
Qed.

Lemma squeezeF_correct_l_alt :
   {n} (u : 'G^n.+1) {i0 i1} j,
    i1 i0 skip_ord i1 j = i0 squeezeF u i0 i1 j = u i0 + u i1.
Proof.
move=>> Hi Hj; rewrite (skip_insert_ord_eq (not_eq_sym Hi)) in Hj; rewrite Hj.
apply squeezeF_correct_l.
Qed.

Lemma squeezeF_correct_r :
   {n} (u : 'G^n.+1) {i0 i1} j,
    i1 i0 skip_ord i1 j i0 squeezeF u i0 i1 j = skipF u i1 j.
Proof. intros; unfold squeezeF, skipF; rewrite replaceF_correct_r; easy. Qed.

Lemma squeezeF_correct_eq :
   {n} (u : 'G^n.+1) {i0 i1}, i1 = i0 squeezeF u i0 i1 = skipF u i0.
Proof. move=>> ->; apply skipF_replaceF. Qed.

End Monoid_FF_Facts0.

Section Monoid_FF_Facts1.

Context {G G1 G2 G3 : AbelianMonoid}.

Properties of constructor itemF.

Lemma itemF_diag : n (x : G) i0, itemF n x i0 i0 = x.
Proof. intros; apply itemF_correct_l; easy. Qed.

Lemma itemF_eq_gen :
   n (x y : G) i0 j0, x = y i0 = j0 itemF n x i0 = itemF n y j0.
Proof. intros; f_equal; easy. Qed.

Lemma itemF_eq :
   n (x y : G) i0, x = y itemF n x i0 = itemF n y i0.
Proof. intros; f_equal; easy. Qed.

Lemma itemF_inj :
   n (x y : G) i0, itemF n x i0 = itemF n y i0 x = y.
Proof. intros n x y i0 H; rewrite -(itemF_diag n x i0) H itemF_diag; easy. Qed.

Lemma itemF_sym :
   m {n} (A : 'G^n) i0 i j, itemF m A i0 j i = itemF m (A i) i0 j.
Proof.
intros m n A i0 i j; destruct (ord_eq_dec j i0).
rewrite → 2!itemF_correct_l; easy.
rewrite → 2!itemF_correct_r; easy.
Qed.

Lemma skipF_itemF_diag :
   n (x : G) i0, skipF (itemF n.+1 x i0) i0 = 0.
Proof. intros; rewrite skipF_replaceF; easy. Qed.

Lemma skipF_itemF_0:
   (n : nat) (x : G) (i0 : 'I_n.+1) (H:i0 ord0),
   skipF (itemF n.+1 x i0) ord0 = itemF n x (lower_S H).
Proof.
intros n x i0 H.
rewrite skipF_first; unfold liftF_S.
apply extF; intros j.
case (ord_eq_dec (lift_S j) i0); intros H1.
rewrite itemF_correct_l; try easy.
rewrite itemF_correct_l; try easy.
apply ord_inj; rewrite lower_S_correct -H1; easy.
rewrite itemF_correct_r; try easy.
rewrite itemF_correct_r; try easy.
intros H2; apply H1.
rewrite H2; apply lift_lower_S.
Qed.

Lemma mapF_itemF :
   n (f : G1 G2) (x1 : G1) i0,
    mapF f (itemF n x1 i0) = replaceF (mapF f 0) (f x1) i0.
Proof.
intros n f x1 i0; apply extF; intros i;
    rewrite mapF_correct; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewritereplaceF_correct_l, itemF_correct_l; easy.
rewritereplaceF_correct_r, itemF_correct_r; easy.
Qed.

Lemma mapF_itemF_0 :
   n (f : G1 G2) (x1 : G1) i0,
    f 0 = 0 mapF f (itemF n x1 i0) = itemF n (f x1) i0.
Proof.
intros; rewrite mapF_itemF; unfold itemF; f_equal; apply fun_ext; easy.
Qed.

Lemma map2F_itemF_l :
   n (f : G1 G2 G3) (x1 : G1) i0 (A2 : 'G2^n),
    map2F f (itemF n x1 i0) A2 = replaceF (map2F f 0 A2) (f x1 (A2 i0)) i0.
Proof.
intros n f x1 i0 A2; apply extF; intros i;
    unfold map2F at 1; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewritereplaceF_correct_l, itemF_correct_l, Hi; easy.
rewritereplaceF_correct_r, itemF_correct_r; easy.
Qed.

Lemma map2F_itemF_r :
   n (f : G1 G2 G3) (A1 : 'G1^n) (x2 : G2) i0,
    map2F f A1 (itemF n x2 i0) = replaceF (map2F f A1 0) (f (A1 i0) x2) i0.
Proof.
intros n f A1 x2 i0; apply extF; intros i;
    unfold map2F at 1; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewritereplaceF_correct_l, itemF_correct_l, Hi; easy.
rewritereplaceF_correct_r, itemF_correct_r; easy.
Qed.

Lemma itemF_ind_l : d (x:G),
   itemF d.+1 x = concatF
                     (singleF (itemF d.+1 x ord0))
                     (mapF (concatF (singleF 0)) (itemF d x)).
Proof.
intros d x; apply extF; intros i; unfold itemF.
case (ord_eq_dec i ord0); intros Hi.
rewrite Hi concatF_correct_l; try easy.
assert (nat_of_ord i O)%coq_nat; auto with arith.
intros T; apply Hi; apply ord_inj; easy.
assert (0 < nat_of_ord i)%coq_nat; auto with zarith arith.
rewrite concatF_correct_r; try easy.
apply Nat.le_ngt; auto with zarith arith.
intros K; rewrite mapF_correct.
apply extF; intros j.
case (ord_eq_dec j ord0); intros Hj1.
rewrite Hj1.
rewrite replaceF_correct_r; auto.
case (ord_eq_dec i j); intros Hj2.
rewrite replaceF_correct_l; try easy.
rewrite concatF_correct_r; try easy.
rewrite -Hj2; simpl; auto with arith.
intros K'.
rewrite replaceF_correct_l; try easy.
apply ord_inj; simpl; rewrite Hj2; easy.
rewrite replaceF_correct_r; try auto.
assert (O < nat_of_ord j)%coq_nat; auto with zarith.
assert (O nat_of_ord j)%coq_nat; auto with zarith.
intros T; apply Hj1; apply ord_inj; easy.
rewrite concatF_correct_r; try easy.
apply Nat.le_ngt; auto with zarith arith.
intros K'.
rewrite replaceF_correct_r; try easy.
apply ord_neq; simpl; rewrite -minusE.
destruct i as (n,Hn).
destruct j as (m,Hm); simpl in ×.
assert (m n)%coq_nat; auto with zarith arith.
intros T; apply Hj2; apply ord_inj; easy.
Qed.

End Monoid_FF_Facts1.

Section Monoid_FF_Facts2.

Context {G : AbelianMonoid}.

Properties of operators unfun0F/maskPF0.

Lemma unfun0F_nil :
   {n} (f : '('I_n)^0) (u : 'G^0), unfun0F f u = 0.
Proof. intros; apply: unfunF_nil. Qed.

Lemma unfun0F_ub :
   {n1 n2} (f : 'I_{n1,n2}) (u1 : 'G^n1),
    injective f invalF u1 (unfun0F f u1).
Proof. move=>>; apply unfunF_ub. Qed.

Lemma unfun0F_castF :
   {n1 p1 n2} (H1 : n1 = p1) (f : 'I_{n1,n2}) (u1 : 'G^n1),
    injective f unfun0F (castF H1 f) (castF H1 u1) = unfun0F f u1.
Proof. move=>>; apply unfunF_castF. Qed.

Lemma unfun0F_eq :
   {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f),
     p, injective p (u1 : 'G^n1),
      unfun0F f u1 =
        permutF p (castF (injF_plus_minus_r Hf) (concatF u1 0)).
Proof.
intros n1 n2 f Hf; destruct (@unfunF_eq G _ _ _ Hf) as [p Hp].
p; split; [easy | intro; apply Hp].
Qed.

End Monoid_FF_Facts2.

Section Monoid_FF_Facts3.

Context {G : AbelianMonoid}.

Properties of operators filter0F/filter_n0F/split0F.

Lemma filter0F_eq_gen_funF :
   {H : Type} {n} (u : 'G^n) (v : 'H^n),
    filter0F_gen u v = funF filterP_ord v.
Proof. easy. Qed.

Lemma filter0F_eq_funF :
   {n} (u : 'G^n), filter0F u = funF filterP_ord u.
Proof. easy. Qed.

Lemma filter_n0F_gen_eq_funF :
   {H : Type} {n} (u : 'G^n) (v : 'H^n),
    filter_n0F_gen u v = funF filterP_ord v.
Proof. easy. Qed.

Lemma filter_n0F_eq_funF :
   {n} (u : 'G^n), filter_n0F u = funF filterP_ord u.
Proof. easy. Qed.


Lemma len_n0F_unfun0F :
   {n1 n2} {f : 'I_{n1,n2}} {u1 : 'G^n1},
    injective f
    lenPF (fun i1u1 i1 0) = lenPF (fun i2unfun0F f u1 i2 0).
Proof. move=>>; apply len_neqF_unfunF. Qed.

Lemma filter_n0F_gen_unfun0F :
   {H : AbelianMonoid} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
      (u1 : 'G^n1) (v1 : 'H^n1),
    let q1 := proj1_sig (injF_restr_bij_EX Hf) in
    let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
    let Hq1b := bij_inj Hq1a in
    filter_n0F_gen (unfun0F f u1) (unfun0F f v1) =
      castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
        (filter_n0F_gen (permutF q1 u1) (permutF q1 v1))).
Proof.
intros; unfold filter_n0F_gen;
    rewrite filter_neqF_gen_unfunF; apply castF_eq_l.
Qed.

Lemma filter_n0F_gen_unfun0F_l :
   {H : AbelianMonoid} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
      (u1 : 'G^n1) (u2 : 'H^n2),
    let q1 := proj1_sig (injF_restr_bij_EX Hf) in
    let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
    let Hq1b := bij_inj Hq1a in
    filter_n0F_gen (unfun0F f u1) u2 =
      castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
        (filter_n0F_gen (permutF q1 u1) (permutF q1 (funF f u2)))).
Proof.
intros; unfold filter_n0F_gen; rewrite filter_neqF_gen_unfunF_l;
    [apply castF_eq_l | apply inhabited_m].
Qed.

Lemma filter_n0F_unfun0F :
   {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f) (u1 : 'G^n1),
    let q1 := proj1_sig (injF_restr_bij_EX Hf) in
    let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
    let Hq1b := bij_inj Hq1a in
    filter_n0F (unfun0F f u1) =
      castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
        (filter_n0F (permutF q1 u1))).
Proof.
intros; unfold filter_n0F; rewrite filter_neqF_unfunF; apply castF_eq_l.
Qed.

End Monoid_FF_Facts3.

Section Monoid_FF_Facts4.

Properties with the identity element of monoids (zero).

Context {T : Type}.
Context {G G1 G2 : AbelianMonoid}.

Lemma nil_is_zero : A : 'G^0, A = 0.
Proof. intros; apply hat0F_unit. Qed.

Lemma nonzero_is_nonnil : {n} (A : 'G^n), A 0 (0 < n)%coq_nat.
Proof.
move=>>; rewrite contra_not_l_equiv Nat.nlt_ge Nat.le_0_r.
intros; subst; apply nil_is_zero.
Qed.

Lemma zeroF : {n} (i : 'I_n), 0 i = (0 : G).
Proof. easy. Qed.

Lemma constF_zero : {n}, constF n (0 : G) = 0.
Proof. easy. Qed.

Lemma singleF_zero : singleF (0 : G) = 0.
Proof. easy. Qed.

Lemma coupleF_zero : coupleF (0 : G) 0 = 0.
Proof. apply extF; intro; unfold coupleF; destruct (ord2_dec _); easy. Qed.

Lemma tripleF_zero : tripleF (0 : G) 0 0 = 0.
Proof.
apply extF; intro; unfold tripleF;
    destruct (ord3_dec _) as [[H | H] | H]; easy.
Qed.

Lemma itemF_zero : n i0, itemF n (0 : G) i0 = 0.
Proof.
intros n i0; apply extF; intros i; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite itemF_correct_l; easy.
rewrite itemF_correct_r; easy.
Qed.

Lemma inF_zero : {n}, inF 0 (0 : 'G^n.+1).
Proof. intros n; apply inF_constF. Qed.

Lemma castF_zero : {n1 n2} (H : n1 = n2), castF H (0 : 'G^n1) = 0.
Proof. easy. Qed.

Lemma firstF_zero : {n1 n2}, firstF (0 : 'G^(n1 + n2)) = 0.
Proof. easy. Qed.

Lemma lastF_zero : {n1 n2}, lastF (0 : 'G^(n1 + n2)) = 0.
Proof. easy. Qed.

Lemma concatF_zero : {n1 n2}, concatF (0 : 'G^n1) (0 : 'G^n2) = 0.
Proof. intros; rewrite (concatF_splitF 0); easy. Qed.

Lemma insertF_zero : {n} i0, insertF (0 : 'G^n) 0 i0 = 0.
Proof.
intros; apply extF; intro; unfold insertF; destruct (ord_eq_dec _ _); easy.
Qed.

Lemma insert2F_zero :
   {n} {i0 i1} (H : i1 i0), insert2F (0 : 'G^n) 0 0 H = 0.
Proof. intros; rewrite insert2F_correct; rewrite 2!insertF_zero; easy. Qed.

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

Lemma skip2F_zero :
   {n} {i0 i1} (H : i1 i0), skip2F (0 : 'G^n.+2) H = 0.
Proof. easy. Qed.

Lemma replaceF_zero : {n} i0, replaceF (0 : 'G^n) 0 i0 = 0.
Proof.
intros; rewrite replaceF_equiv_def_skipF; rewrite insertF_zero skipF_zero; easy.
Qed.

Lemma replace2F_zero :
   {n} i0 i1, replace2F (0 : 'G^n) 0 0 i0 i1 = 0.
Proof. intros; unfold replace2F; rewrite 2!replaceF_zero; easy. Qed.

Lemma mapF_zero : {n} (f : G1 G2), f 0 = 0 mapF f (0 : 'G1^n) = 0.
Proof. intros; apply extF; intro; easy. Qed.

Lemma mapF_zero_f : {n} (A : 'T^n), mapF (0 : T G) A = 0.
Proof. easy. Qed.

Lemma constF_zero_compat : {n} (x : G), x = 0 constF n x = 0.
Proof. move=>> H; rewrite H; apply constF_zero. Qed.

Lemma singleF_zero_compat : (x0 : G), x0 = 0 singleF x0 = 0.
Proof. move=>> H0; rewrite H0; apply singleF_zero. Qed.

Lemma coupleF_zero_compat :
   (x0 x1 : G), x0 = 0 x1 = 0 coupleF x0 x1 = 0.
Proof. move=>> H0 H1; rewrite H0 H1; apply coupleF_zero. Qed.

Lemma tripleF_zero_compat :
   (x0 x1 x2 : G), x0 = 0 x1 = 0 x2 = 0 tripleF x0 x1 x2 = 0.
Proof. move=>> H0 H1 H2; rewrite H0 H1 H2; apply tripleF_zero. Qed.

Lemma itemF_zero_compat : n (x : G) i0, x = 0 itemF n x i0 = 0.
Proof. move=>> H; rewrite H; apply itemF_zero. Qed.

Lemma castF_zero_compat :
   {n1 n2} (H : n1 = n2) (A : 'G^n1), A = 0 castF H A = 0.
Proof. move=>> H; rewrite H; apply castF_zero. Qed.

Lemma firstF_zero_compat :
   {n1 n2} (A : 'G^(n1 + n2)),
    ( i : 'I_(n1 + n2), (i < n1)%coq_nat A i = 0) firstF A = 0.
Proof. move=>>; erewrite <- firstF_zero. apply firstF_compat. Qed.

Lemma lastF_zero_compat :
   {n1 n2} (A : 'G^(n1 + n2)),
    ( i : 'I_(n1 + n2), (n1 i)%coq_nat A i = 0) lastF A = 0.
Proof. move=>>; erewrite <- lastF_zero; apply lastF_compat. Qed.

Lemma splitF_zero_compat:
   {n1 n2} (A : 'G^(n1 + n2)), A = 0 firstF A = 0 lastF A = 0.
Proof. move=>>; apply splitF_compat. Qed.

Lemma concatF_zero_compat :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2),
    A1 = 0 A2 = 0 concatF A1 A2 = 0.
Proof. move=>> H1 H2; rewrite H1 H2; apply concatF_zero. Qed.

Lemma concatF_zero_nextF_compat_l :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2), A1 0 concatF A1 A2 0.
Proof. move=>>; rewrite -concatF_zero; apply concatF_nextF_compat_l. Qed.

Lemma concatF_zero_nextF_compat_r :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2), A2 0 concatF A1 A2 0.
Proof. move=>>; rewrite -concatF_zero; apply concatF_nextF_compat_r. Qed.

Lemma insertF_zero_compat :
   {n} (A : 'G^n) x0 i0, A = 0 x0 = 0 insertF A x0 i0 = 0.
Proof. move=>> HA H0; rewrite HA H0; apply insertF_zero. Qed.

Lemma insert2F_zero_compat :
   {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 i0),
    A = 0 x0 = 0 x1 = 0 insert2F A x0 x1 H = 0.
Proof. move=>> HA H0 H1; rewrite HA H0 H1; apply insert2F_zero. Qed.

Lemma skipF_zero_compat :
   {n} (A : 'G^n.+1) i0, eqxF A 0 i0 skipF A i0 = 0.
Proof.
move=>> H; erewrite <- skipF_zero; apply skipF_compat; try apply H; easy.
Qed.

Lemma skip2F_zero_compat :
   {n} (A : 'G^n.+2) {i0 i1 : 'I_n.+2} (H : i1 i0),
    eqx2F A 0 i0 i1 skip2F A H = 0.
Proof.
intros n A i0 i1 H HA; rewrite -(skip2F_zero H); apply skip2F_compat; easy.
Qed.

Lemma replaceF_zero_compat :
   {n} (A : 'G^n) x0 i0, eqxF A 0 i0 x0 = 0 replaceF A x0 i0 = 0.
Proof. intros; erewrite <- replaceF_zero; apply replaceF_compat; easy. Qed.

Lemma replace2F_zero_compat :
   {n} (A : 'G^n) x0 x1 i0 i1,
    eqx2F A 0 i0 i1 x0 = 0 x1 = 0 replace2F A x0 x1 i0 i1 = 0.
Proof. intros; erewrite <- replace2F_zero; apply replace2F_compat; easy. Qed.

Lemma mapF_zero_compat :
   {n} (f : G1 G2) (A : 'G1^n), f 0 = 0 A = 0 mapF f A = 0.
Proof. move=>> Hf HA; rewrite HA; apply (mapF_zero _ Hf). Qed.

Lemma mapF_zero_compat_f :
   {n} (f : T G) (A : 'T^n), f = 0 mapF f A = 0.
Proof. move=>> Hf; rewrite Hf; easy. Qed.

Lemma constF_zero_reg : {n} (x : G), constF n.+1 x = 0 x = 0.
Proof. intros; apply (constF_inj n); easy. Qed.

Lemma singleF_zero_reg : (x0 : G), singleF x0 = 0 x0 = 0.
Proof. intros; apply singleF_inj; easy. Qed.

Lemma coupleF_zero_reg :
   (x0 x1 : G), coupleF x0 x1 = 0 x0 = 0 x1 = 0.
Proof. intros; apply coupleF_inj; rewrite coupleF_zero; easy. Qed.

Lemma coupleF_zero_reg_l : (x0 x1 : G), coupleF x0 x1 = 0 x0 = 0.
Proof. move=>>; apply coupleF_zero_reg. Qed.

Lemma coupleF_zero_reg_r : (x0 x1 : G), coupleF x0 x1 = 0 x1 = 0.
Proof. move=>>; apply coupleF_zero_reg. Qed.

Lemma tripleF_zero_reg :
   (x0 x1 x2 : G), tripleF x0 x1 x2 = 0 x0 = 0 x1 = 0 x2 = 0.
Proof. intros; apply tripleF_inj; rewrite tripleF_zero; easy. Qed.

Lemma tripleF_zero_reg_l : (x0 x1 x2 : G), tripleF x0 x1 x2 = 0 x0 = 0.
Proof. move=>>; apply tripleF_zero_reg. Qed.

Lemma tripleF_zero_reg_m : (x0 x1 x2 : G), tripleF x0 x1 x2 = 0 x1 = 0.
Proof. move=>>; apply tripleF_zero_reg. Qed.

Lemma tripleF_zero_reg_r : (x0 x1 x2 : G), tripleF x0 x1 x2 = 0 x2 = 0.
Proof. move=>>; apply tripleF_zero_reg. Qed.

Lemma itemF_zero_reg : n (x : G) i0, itemF n x i0 = 0 x = 0.
Proof. intros n x i0; rewrite -(itemF_zero _ i0); apply itemF_inj. Qed.

Lemma castF_zero_reg :
   {n1 n2} (H : n1 = n2) (A : 'G^n1), castF H A = 0 A = 0.
Proof. move=>> H; eapply castF_inj; apply H. Qed.

Lemma splitF_zero_reg :
   {n1 n2} (A : 'G^(n1 + n2)), firstF A = 0 lastF A = 0 A = 0.
Proof. intros; apply splitF_reg; easy. Qed.

Lemma concatF_zero_reg :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2),
    concatF A1 A2 = 0 A1 = 0 A2 = 0.
Proof. intros; apply concatF_inj; rewrite concatF_zero; easy. Qed.

Lemma concatF_zero_reg_l :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2), concatF A1 A2 = 0 A1 = 0.
Proof. move=>>; apply concatF_zero_reg. Qed.

Lemma concatF_zero_reg_r :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2), concatF A1 A2 = 0 A2 = 0.
Proof. move=>>; apply concatF_zero_reg. Qed.

Lemma concatF_zero_nextF_reg :
   {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2),
    concatF A1 A2 0 A1 0 A2 0.
Proof. move=>>; rewrite -concatF_zero; apply concatF_nextF_reg. Qed.

Lemma insertF_zero_reg_l :
   {n} (A : 'G^n) x0 i0, insertF A x0 i0 = 0 A = 0.
Proof. move=>>; erewrite <- insertF_zero; apply insertF_inj_l. Qed.

Lemma insertF_zero_reg_r :
   {n} (A : 'G^n) x0 i0, insertF A x0 i0 = 0 x0 = 0.
Proof. move=>>; erewrite <- insertF_zero; apply insertF_inj_r. Qed.

Lemma insert2F_zero_reg_l :
   {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 i0),
    insert2F A x0 x1 H = 0 A = 0.
Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_l. Qed.

Lemma insert2F_zero_reg_r0 :
   {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 i0),
    insert2F A x0 x1 H = 0 x0 = 0.
Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_r0. Qed.

Lemma insert2F_zero_reg_r1 :
   {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 i0),
    insert2F A x0 x1 H = 0 x1 = 0.
Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_r1. Qed.

Lemma skipF_zero_reg :
   {n} (A : 'G^n.+1) i0, skipF A i0 = 0 eqxF A 0 i0.
Proof. move=>>; erewrite <- skipF_zero; apply skipF_reg. Qed.

Lemma skip2F_zero_reg :
   {n} (A : 'G^n.+2) {i0 i1} (H : i1 i0),
    skip2F A H = 0 eqx2F A 0 i0 i1.
Proof. move=>>; erewrite <- skip2F_zero; apply skip2F_reg. Qed.

Lemma replaceF_zero_reg_l :
   {n} (A : 'G^n) x0 i0, replaceF A x0 i0 = 0 eqxF A 0 i0.
Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg_l. Qed.

Lemma replaceF_zero_reg_r :
   {n} (A : 'G^n) x0 i0, replaceF A x0 i0 = 0 x0 = 0.
Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg_r. Qed.

Lemma replaceF_zero_reg :
   {n} (A : 'G^n) x0 i0, replaceF A x0 i0 = 0 eqxF A 0 i0 x0 = 0.
Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg. Qed.

Lemma replace2F_zero_reg_l :
   {n} (A : 'G^n) x0 x1 i0 i1,
    replace2F A x0 x1 i0 i1 = 0 eqx2F A 0 i0 i1.
Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_l. Qed.

Lemma replace2F_zero_reg_r0 :
   {n} (A : 'G^n) x0 x1 {i0 i1},
    i1 i0 replace2F A x0 x1 i0 i1 = 0 x0 = 0.
Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_r0. Qed.

Lemma replace2F_zero_reg_r1 :
   {n} (A : 'G^n) x0 x1 i0 i1, replace2F A x0 x1 i0 i1 = 0 x1 = 0.
Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_r1. Qed.

Lemma replace2F_zero_reg :
   {n} (A : 'G^n) x0 x1 {i0 i1},
    i1 i0 replace2F A x0 x1 i0 i1 = 0
    eqx2F A 0 i0 i1 x0 = 0 x1 = 0.
Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg. Qed.

Lemma mapF_zero_reg :
   {n} (f : G1 G2) (A : 'G1^n),
    ( x, f x = 0 x = 0) mapF f A = 0 A = 0.
Proof. moven f A Hf /extF_rev HA; apply extF; intro; apply Hf, HA. Qed.

Lemma mapF_zero_reg_f :
   {n} (f : T G), ( (A : 'T^n.+1), mapF f A = 0) f = 0.
Proof. move=>> H; eapply mapF_inj_f; intros; apply H. Qed.

Lemma eqxF_zero_equiv :
   {n} (A : 'G^n.+1) i0, eqxF A 0 i0 skipF A i0 = 0.
Proof. intros n A i0; rewrite -(skipF_zero i0); apply eqxF_equiv. Qed.

Lemma eqx2F_zero_equiv :
   {n} (A : 'G^n.+2) {i0 i1} (H : i1 i0),
    eqx2F A 0 i0 i1 skip2F A H = 0.
Proof. intros n A i0 i1 H; rewrite -(skip2F_zero H); apply eqx2F_equiv. Qed.

Lemma neqxF_zero_equiv :
   {n} (A : 'G^n.+1) i0, neqxF A 0 i0 skipF A i0 0.
Proof. intros n A i0; rewrite -(skipF_zero i0); apply neqxF_equiv. Qed.

Lemma neqx2F_zero_equiv :
   {n} (A : 'G^n.+2) {i0 i1} (H : i1 i0),
    neqx2F A 0 i0 i1 skip2F A H 0.
Proof. intros n A i0 i1 H; rewrite -(skip2F_zero H); apply neqx2F_equiv. Qed.

Lemma extF_zero_splitF :
   {n n1 n2} (H : n = (n1 + n2)%nat) (A : 'G^n),
    firstF (castF H A) = 0 lastF (castF H A) = 0 A = 0.
Proof. move=>> Hf Hl; eapply extF_splitF. apply Hf. apply Hl. Qed.

Lemma extF_zero_ind_l :
   {n} (A : 'G^n.+1), A ord0 = 0 liftF_S A = 0 A = 0.
Proof. intros; apply extF_ind_l; easy. Qed.

Lemma extF_zero_ind_r :
   {n} (A : 'G^n.+1), widenF_S A = 0 A ord_max = 0 A = 0.
Proof. intros; apply extF_ind_r; easy. Qed.

Lemma extF_zero_skipF :
   {n} (A : 'G^n.+1) i0, A i0 = 0 skipF A i0 = 0 A = 0.
Proof. intros n A i0; rewrite -(skipF_zero i0); apply: extF_skipF. Qed.

Lemma skipF_nextF_zero_reg :
   {n} (A : 'G^n.+1) i0, skipF A i0 0 neqxF A 0 i0.
Proof. move=>>; erewrite <- skipF_zero; apply skipF_neqxF_reg. Qed.

Lemma mapF_zero_nat :
   {n} (f : nat G2), f 0%nat = 0 mapF f (constF n 0%nat) = 0.
Proof. intros; apply extF; intro; easy. Qed.

Lemma mapF_zero_compat_nat :
   {n} (f : nat G2) A,
    f 0%nat = 0 A = constF n 0%nat mapF f A = 0.
Proof. move=>> Hf HA; rewrite HA; apply (mapF_zero_nat _ Hf). Qed.

Lemma mapF_zero_reg_nat :
   {n} (f : nat G2) (A : 'nat^n),
    ( x, f x = 0 x = 0%nat) mapF f A = 0 A = constF n 0%nat.
Proof. moven f A Hf /extF_rev HA; apply extF; intro; apply Hf, HA. Qed.

End Monoid_FF_Facts4.

Section Monoid_FF_Facts5.

Properties with the law of monoids (plus).

Context {G : AbelianMonoid}.

Lemma constF_plus :
   n (x y : G), constF n (x + y) = constF n x + constF n y.
Proof. easy. Qed.

Lemma castF_plus :
   {n1 n2} (H : n1 = n2) (A1 B1 : 'G^n1),
    castF H (A1 + B1) = castF H A1 + castF H B1.
Proof. easy. Qed.

Lemma widenF_S_plus :
   {n} (A B : 'G^n.+1), widenF_S (A + B) = widenF_S A + widenF_S B.
Proof. easy. Qed.

Lemma liftF_S_plus :
   {n} (A B : 'G^n.+1), liftF_S (A + B) = liftF_S A + liftF_S B.
Proof. easy. Qed.

Lemma widenF_plus :
   {n1 n2} (H : n1 n2) (A2 B2 : 'G^n2),
    widenF H (A2 + B2) = widenF H A2 + widenF H B2.
Proof. easy. Qed.

Lemma firstF_plus :
   {n1 n2} (A B : 'G^(n1 + n2)), firstF (A + B) = firstF A + firstF B.
Proof. easy. Qed.

Lemma lastF_plus :
   {n1 n2} (A B : 'G^(n1 + n2)), lastF (A + B) = lastF A + lastF B.
Proof. easy. Qed.

Lemma concatF_plus :
   {n1 n2} (A1 B1 : 'G^n1) (A2 B2 : 'G^n2),
    concatF (A1 + B1) (A2 + B2) = concatF A1 A2 + concatF B1 B2.
Proof.
intros n1 n2 A1 B1 A2 B2; apply extF; intros i; rewrite fct_plus_eq;
    destruct (lt_dec i n1) as [Hi | Hi];
    [rewrite !concatF_correct_l | rewrite !concatF_correct_r]; easy.
Qed.

Lemma insertF_plus :
   {n} (A B : 'G^n) a0 b0 i0,
    insertF (A + B) (a0 + b0) i0 = insertF A a0 i0 + insertF B b0 i0.
Proof.
intros n A B a0 b0 i0; apply extF; intros i; rewrite fct_plus_eq;
    destruct (ord_eq_dec i i0) as [Hi | Hi];
    [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed.

Lemma skipF_plus :
   {n} (A B : 'G^n.+1) i0, skipF (A + B) i0 = skipF A i0 + skipF B i0.
Proof. easy. Qed.

Lemma replaceF_plus :
   {n} (A B : 'G^n.+1) a0 b0 i0,
    replaceF (A + B) (a0 + b0) i0 = replaceF A a0 i0 + replaceF B b0 i0.
Proof.
intros n A B a0 b0 i0; apply extF; intros i; rewrite fct_plus_eq;
    destruct (ord_eq_dec i i0) as [Hi | Hi];
    [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed.

Lemma permutF_plus :
   {n} (p : 'I_[n]) (A B : 'G^n),
    permutF p (A + B) = permutF p A + permutF p B.
Proof. easy. Qed.


End Monoid_FF_Facts5.