Library Algebra.Monoid.MonoidMult
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for multiplicative commutative monoid.
The AbelianMonoid algebraic structure defined in the Coquelicot library is
fully abstract, but in everybody's mind, plus and zero stand for an
additive structure, hence the provided notations + and 0, and the iterated
law called sum.
Nonetheless, multiplicative monoids are also useful, and it may look strange
to use +, 0 and sum when we mean ×, 1 and prod. Hence the present
specialization.
These notations are local to avoid any confusion outside the module.
Let G : AbelianMonoid and x0 : G.
Let u : 'nat_mul^n.
Let alpha : 'nat^n.
Let u : 'R_mul^n.
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Beware that multiplicative notations for the generic plus and zero are
local to the present module. Outside, results appear with 0 and + instead
of 1 and ×.
Brief description
Description
Additional definition and notation
Some multiplicative commutative monoids
- nat_mul is an alias for nat;
- to_nat_mul and of_nat_mul are coercions between nat and nat_mul;
- nat_MultiplicativeAbelianMonoid is nat_mul endowed with the (multiplicative) AbelianMonoid structure;
- R_mul is an alias for R;
- to_R_mul and of_R_mul are coercions between R and R_mul;
- R_MultiplicativeAbelianMonoid is R_mul endowed with the (multiplicative) AbelianMonoid structure;
Support for product of natural numbers
Support for product of real numbers
Usage
From Requisite Require Import stdlib_wR 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 Monoid_sum.
Declare Scope MonoidMult_scope.
Delimit Scope MonoidMult_scope with Mmult.
Local Notation "x * y" := (plus x y) : MonoidMult_scope.
Local Notation "1" := (zero) : MonoidMult_scope.
Local Open Scope MonoidMult_scope.
Section Multiplicative_Monoid_Defs.
Context {G : AbelianMonoid}.
Definition absorbing (x0 : G) : Prop := ∀ x, x0 × x = x0.
End Multiplicative_Monoid_Defs.
Section Multiplicative_Monoid_Facts.
Context {G : AbelianMonoid}.
Lemma sum_absorbing :
∀ x0 {n} (u : 'G^n), absorbing x0 → inF x0 u → sum u = x0.
Proof.
intros x0 [| n] u Hx0 [i0 Hu]; [now destruct i0 |].
rewrite (sum_skipF _ i0) -Hu; easy.
Qed.
End Multiplicative_Monoid_Facts.
Section Some_Multiplicative_Monoids.
Definition nat_MultiplicativeAbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Nat.mul_comm Nat.mul_assoc Nat.mul_1_r.
Definition nat_mul := nat.
Coercion to_nat_mul (x : nat) : nat_mul := x.
Coercion of_nat_mul (x : nat_mul) : nat := x.
Canonical Structure nat_MultiplicativeAbelianMonoid :=
AbelianMonoid.Pack nat_mul nat_MultiplicativeAbelianMonoid_mixin nat_mul.
Definition R_MultiplicativeAbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Rmult_comm (SYM3 Rmult_assoc) Rmult_1_r.
Definition R_mul := R.
Coercion to_R_mul (x : R) : R_mul := x.
Coercion of_R_mul (x : R_mul) : R := x.
Canonical Structure R_MultiplicativeAbelianMonoid :=
AbelianMonoid.Pack R_mul R_MultiplicativeAbelianMonoid_mixin R_mul.
End Some_Multiplicative_Monoids.
Section Prod_nat_Facts.
Definition prod_nat {n} (u : 'nat_mul^n) : nat_mul := sum u.
Lemma prod_nat_ext :
∀ {n} (u v : 'nat^n), (∀ i, u i = v i) → prod_nat u = prod_nat v.
Proof. intros; apply sum_ext; easy. Qed.
Lemma prod_nat_nil : ∀ (u : 'nat_mul^0), prod_nat u = 1.
Proof. apply sum_nil. Qed.
Lemma prod_nat_ind_l :
∀ {n} (u : 'nat_mul^n.+1), prod_nat u = u ord0 × prod_nat (liftF_S u).
Proof. intros; apply sum_ind_l. Qed.
Lemma prod_nat_ind_r :
∀ {n} (u : 'nat_mul^n.+1), prod_nat u = prod_nat (widenF_S u) × u ord_max.
Proof. intros; apply sum_ind_r. Qed.
Lemma prod_nat_one : ∀ {n}, prod_nat (1 : 'nat_mul^n) = 1.
Proof. intros; apply sum_zero. Qed.
Lemma prod_nat_one_compat : ∀ {n} (u : 'nat_mul^n), u = 1 → prod_nat u = 1.
Proof. move=>>; apply sum_zero_compat. Qed.
Lemma prod_nat_singl :
∀ {n} (u : 'nat_mul^n.+1) i0, skipF u i0 = 1 → prod_nat u = u i0.
Proof. move=>>; apply sum_one. Qed.
Lemma prod_nat_castF :
∀ {n1 n2} (H : n1 = n2) (u : 'nat_mul^n1),
prod_nat (castF H u) = prod_nat u.
Proof. intros; apply sum_castF. Qed.
Lemma prod_nat_singleF : ∀ (u0 : nat_mul), prod_nat (singleF u0) = u0.
Proof. move=>>; apply sum_singleF. Qed.
Lemma prod_nat_singleF_alt :
∀ {n} (u : 'nat_mul^n) (H : n = 1%nat), prod_nat u = castF H u ord0.
Proof. intros; subst; rewrite castF_id; apply sum_1. Qed.
Lemma prod_nat_concatF :
∀ {n1 n2} (u1 : 'nat_mul^n1) (u2 : 'nat_mul^n2),
prod_nat (concatF u1 u2) = prod_nat u1 × prod_nat u2.
Proof. intros; apply sum_concatF. Qed.
Lemma prod_nat_replaceF :
∀ {n} (u : 'nat_mul^n.+1) x0 i0,
u i0 × prod_nat (replaceF u x0 i0) = x0 × prod_nat u.
Proof. intros; apply sum_replaceF. Qed.
Lemma prod_nat_zero : ∀ {n} (u : 'nat_mul^n), inF 0 u → prod_nat u = 0.
Proof. intros; apply sum_absorbing; easy. Qed.
Lemma prod_nat_zero_rev :
∀ {n} (u : 'nat_mul^n), prod_nat u = 0 → inF 0 u.
Proof.
intros n u; induction n as [| n Hn].
rewrite prod_nat_nil; easy.
rewrite prod_nat_ind_l; move⇒ /Nat.mul_eq_0 [Hu | Hu].
∃ ord0; easy.
destruct (Hn _ Hu) as [i Hi]; ∃ (lift_S i); easy.
Qed.
Lemma prod_nat_zero_equiv :
∀ {n} (u : 'nat_mul^n), prod_nat u = 0 ↔ inF 0 u.
Proof. intros; split. apply prod_nat_zero_rev. apply prod_nat_zero. Qed.
Lemma prod_nat_nonzero :
∀ {n} (u : 'nat_mul^n), ¬ inF 0 u → prod_nat u ≠ 0.
Proof. move=>>; rewrite -contra_equiv; apply prod_nat_zero_rev. Qed.
Lemma prod_nat_nonzero_rev :
∀ {n} (u : 'nat_mul^n), prod_nat u ≠ 0 → ¬ inF 0 u.
Proof. move=>>; rewrite -contra_equiv; apply prod_nat_zero. Qed.
Lemma prod_nat_nonzero_equiv :
∀ {n} (u : 'nat_mul^n), prod_nat u ≠ 0 ↔ ¬ inF 0 u.
Proof. intros; split. apply prod_nat_nonzero_rev. apply prod_nat_nonzero. Qed.
End Prod_nat_Facts.
Section Multi_Factorial.
Definition multi_fact {n : nat} (alpha : 'nat^n) : nat :=
prod_nat (mapF fact alpha).
End Multi_Factorial.
Section Prod_R_Facts.
Definition prod_R {n} (u : 'R_mul^n) : R_mul := sum u.
Lemma prod_R_ext :
∀ {n} (u v : 'R^n), (∀ i, u i = v i) → prod_R u = prod_R v.
Proof. intros; apply sum_ext; easy. Qed.
Lemma prod_R_nil : ∀ (u : 'R_mul^0), prod_R u = 1.
Proof. apply sum_nil. Qed.
Lemma prod_R_ind_l :
∀ {n} (u : 'R_mul^n.+1), prod_R u = u ord0 × prod_R (liftF_S u).
Proof. intros; apply sum_ind_l. Qed.
Lemma prod_R_ind_r :
∀ {n} (u : 'R_mul^n.+1), prod_R u = prod_R (widenF_S u) × u ord_max.
Proof. intros; apply sum_ind_r. Qed.
Lemma prod_R_one : ∀ {n}, prod_R (1 : 'R_mul^n) = 1.
Proof. intros; apply sum_zero. Qed.
Lemma prod_R_one_compat : ∀ {n} (u : 'R_mul^n), u = 1 → prod_R u = 1.
Proof. move=>>; apply sum_zero_compat. Qed.
Lemma prod_R_singl :
∀ {n} (u : 'R_mul^n.+1) i0, skipF u i0 = 1 → prod_R u = u i0.
Proof. move=>>; apply sum_one. Qed.
Lemma prod_R_castF :
∀ {n1 n2} (H : n1 = n2) (u : 'R_mul^n1), prod_R (castF H u) = prod_R u.
Proof. intros; apply sum_castF. Qed.
Lemma prod_R_singleF : ∀ (x0 : R_mul), prod_R (singleF x0) = x0.
Proof. move=>>; apply sum_singleF. Qed.
Lemma prod_R_singleF_alt :
∀ {n} (u : 'R_mul^n) (H : n = 1%nat), prod_R u = castF H u ord0.
Proof. intros; subst; rewrite castF_id; apply sum_1. Qed.
Lemma prod_R_concatF :
∀ {n1 n2} (u1 : 'R_mul^n1) (u2 : 'R_mul^n2),
prod_R (concatF u1 u2) = prod_R u1 × prod_R u2.
Proof. intros; apply sum_concatF. Qed.
Lemma prod_R_replaceF :
∀ {n} (u : 'R_mul^n.+1) x0 i0,
u i0 × prod_R (replaceF u x0 i0) = x0 × prod_R u.
Proof. intros; apply sum_replaceF. Qed.
Lemma prod_R_zero : ∀ {n} (u : 'R_mul^n), inF 0%R u → prod_R u = 0%R.
Proof. intros; apply sum_absorbing; [intro; apply Rmult_0_l | easy]. Qed.
Lemma prod_R_zero_rev : ∀ {n} (u : 'R_mul^n), prod_R u = 0%R → inF 0%R u.
Proof.
intros n u; induction n as [| n Hn].
rewrite prod_R_nil; intros Hu; contradict Hu; apply R1_neq_R0.
rewrite prod_R_ind_l; move⇒ /Rmult_integral [Hu | Hu].
∃ ord0; easy.
destruct (Hn _ Hu) as [i Hi]; ∃ (lift_S i); easy.
Qed.
Lemma prod_R_zero_equiv :
∀ {n} (u : 'R_mul^n), prod_R u = 0%R ↔ inF 0%R u.
Proof. intros; split. apply prod_R_zero_rev. apply prod_R_zero. Qed.
Lemma prod_R_nonzero :
∀ {n} (u : 'R_mul^n), ¬ inF 0%R u → prod_R u ≠ 0%R.
Proof. move=>>; rewrite -contra_equiv; apply prod_R_zero_rev. Qed.
Lemma prod_R_nonzero_rev :
∀ {n} (u : 'R_mul^n), prod_R u ≠ 0%R → ¬ inF 0%R u.
Proof. move=>>; rewrite -contra_equiv; apply prod_R_zero. Qed.
Lemma prod_R_nonzero_equiv :
∀ {n} (u : 'R_mul^n), prod_R u ≠ 0%R ↔ ¬ inF 0%R u.
Proof. intros; split. apply prod_R_nonzero_rev. apply prod_R_nonzero. Qed.
Lemma prod_R_div :
∀ {n} (u v : 'R_mul^n),
¬ inF 0%R v → (prod_R u / prod_R v)%R = prod_R (fun i ⇒ (u i / v i)%R).
Proof.
move⇒ n u v /inF_not Hv; induction n as [| n Hn].
rewrite !prod_R_nil; apply Rdiv_1_r.
rewrite 3!prod_R_ind_l; rewrite -Hn; try easy; unfold plus; simpl.
replace (prod_R (fun i ⇒ u (lift_S i))) with (prod_R (liftF_S u)); try easy.
replace (prod_R (fun i ⇒ v (lift_S i))) with (prod_R (liftF_S v)); try easy.
field; split; try now apply not_eq_sym.
apply prod_R_nonzero; rewrite inF_not; intros i; apply (Hv (lift_S i)).
Qed.
End Prod_R_Facts.