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.
Additional support for finite families on commutative monoids.
Let G be an AbelianMonoid, and T be any type.
Let x be in G.
Let u1 and u2 respectively be an n1-family and an n2-family in G.
Let f : 'I_n1 → 'I_n2.
Let P be a predicate on 'I_n.
Let u be an n-family in G.
Let v an n-family of any type T.
Let u be an n.+1-family in G.
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
Constructor
Operators
- 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.
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 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 i ⇒ u 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 i ⇒ u 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].
rewrite → replaceF_correct_l, itemF_correct_l; easy.
rewrite → replaceF_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].
rewrite → replaceF_correct_l, itemF_correct_l, Hi; easy.
rewrite → replaceF_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].
rewrite → replaceF_correct_l, itemF_correct_l, Hi; easy.
rewrite → replaceF_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}.
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}.
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 i1 ⇒ u1 i1 ≠ 0) = lenPF (fun i2 ⇒ unfun0F 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. move⇒ n 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. move⇒ n 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.