Library Algebra.Hierarchy_compl
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.
Complements for the Hierarchy module of the Coquelicot library.
The Hierarchy of the Coquelicot library provides a series of algebraic
structures, including support for the cartesian product of two instances of
the same algebraic structure. This includes, but is not limited to:
The present module adds:
Monoid scope Monoid_scope (delimitor = 'M')
See also Algebra.Monoid.MonoidMult.
Group scope Group_scope (delimitor = 'G')
Ring scope Ring_scope (delimitor = 'R')
Let T be any type.
Let f g : T → G.
Let T be any type.
Let G : AbelianGroup.
Let f g : T → G.
Let T be any type.
Let f g : T → K.
Let K : Ring and E : ModuleSpace K.
Let T : Type and f : T → E.
This module may be used through the import of Algebra.Algebra, or
Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- AbelianMonoid for commutative monoids,
- AbelianGroup for commutative groups,
- Ring for (not necessarily commutative) rings,
- ModuleSpace for modules over a ring.
- notations,
- some instances of AbelianMonoid,
- support for functions to types equipped with one of the algebraic structure listed above.
Additional notations
Some commutative monoids
- nat_AbelianMonoid is nat endowed with the (additive) AbelianMonoid structure;
- Rbp is the type of nonnegative extended real numbers;
- Rbp_AbelianMonoid is Rbp endowed with the (additive) AbelianMonoid structure.
Support for functions to an AbelianMonoid
- fct_plus f g is the function that "adds" outputs of f and g;
- fct_zero is the constant function of value 0;
- fct_AbelianMonoid is the type T → G endowed with the AbelianMonoid structure.
Support for functions to an AbelianGroup
- fct_opp f is the function that takes the "opposite" of the output of f;
- fct_minus f g is the function that takes the "difference" of the outputs of f and g;
- fct_AbelianGroup is the type T → G endowed with the AbelianGroup structure.
Support for functions to a Ring
- fct_mult f g is the function that takes the product of the outputs of f and g;
- fct_one is the constant function of value 1;
- fct_Ring is the type T → K endowed with the Ring structure.
Support for functions to a ModuleSpace
- fct_scal_l f u t is equal to scal (f t) u.
- fct_ModuleSpace is the type T → K endowed with the ModuleSpace structure.
Used logic axioms
- proof_irrel, an alias for proof_irrelevance.
Usage
From Requisite Require Import stdlib_wR ssr.
From Coquelicot Require Import Hierarchy Rbar.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
Declare Scope Monoid_scope.
Delimit Scope Monoid_scope with M.
Notation "x + y" := (plus x y) : Monoid_scope.
Notation "0" := (zero) : Monoid_scope.
Declare Scope Group_scope.
Delimit Scope Group_scope with G.
Notation "- x" := (opp x) : Group_scope.
Notation "x - y" := (minus x y) : Group_scope.
Section Ring_Def.
Context {K : Ring}.
Definition two : K := plus one one.
End Ring_Def.
Declare Scope Ring_scope.
Delimit Scope Ring_scope with K.
Notation "x * y" := (mult x y) : Ring_scope.
Notation "1" := (one) : Ring_scope.
Notation "2" := (two) : Ring_scope.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Some_Monoids.
Definition nat_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Nat.add_comm Nat.add_assoc Nat.add_0_r.
Canonical Structure nat_AbelianMonoid :=
AbelianMonoid.Pack _ nat_AbelianMonoid_mixin nat.
Lemma Rbar_plus_nonneg :
∀ {x y}, Rbar_le 0%R x → Rbar_le 0%R y → Rbar_le 0%R (Rbar_plus x y).
Proof.
move=>>; rewrite -{3}(Rbar_plus_0_l 0%R); apply Rbar_plus_le_compat.
Qed.
Lemma Rbar_plus_assoc_bounded_l :
∀ {x y z} (lb : R),
Rbar_le lb x → Rbar_le lb y → Rbar_le lb z →
Rbar_plus x (Rbar_plus y z) = Rbar_plus (Rbar_plus x y) z.
Proof.
intros x y z lb Hx Hy Hz; destruct x, y, z; try easy; simpl.
rewrite Rplus_assoc; easy.
Qed.
Lemma Rbar_plus_assoc_bounded_r :
∀ {x y z} (rb : R),
Rbar_le x rb → Rbar_le y rb → Rbar_le z rb →
Rbar_plus x (Rbar_plus y z) = Rbar_plus (Rbar_plus x y) z.
Proof.
intros x y z rb Hx Hy Hz; destruct x, y, z; try easy; simpl.
rewrite Rplus_assoc; easy.
Qed.
Record Rbp : Set := mk_Rbp_ {
Rbp_val :> Rbar;
Rbp_nonneg : Rbar_le 0%R Rbp_val;
}.
Definition mk_Rbp {x} Hx := mk_Rbp_ x Hx.
Lemma Rbp_val_inj : injective Rbp_val.
Proof.
intros [x Hx] [y Hy]; simpl; intros H; subst; f_equal; apply proof_irrel.
Qed.
Definition Rbp_plus (x y : Rbp) : Rbp :=
mk_Rbp (Rbar_plus_nonneg (Rbp_nonneg x) (Rbp_nonneg y)).
Definition Rbp_zero : Rbp := mk_Rbp (Rbar_le_refl 0%R).
Lemma Rpb_plus_comm : ∀ x y, Rbp_plus x y = Rbp_plus y x.
Proof. intros; apply Rbp_val_inj, Rbar_plus_comm. Qed.
Lemma Rbp_plus_assoc :
∀ x y z, Rbp_plus x (Rbp_plus y z) = Rbp_plus (Rbp_plus x y) z.
Proof.
intros; apply Rbp_val_inj, (Rbar_plus_assoc_bounded_l 0%R); apply Rbp_nonneg.
Qed.
Lemma Rbp_plus_0_r : ∀ x, Rbp_plus x Rbp_zero = x.
Proof. intros; apply Rbp_val_inj, Rbar_plus_0_r. Qed.
Definition Rbp_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ Rpb_plus_comm Rbp_plus_assoc Rbp_plus_0_r.
Canonical Structure Rbp_AbelianMonoid :=
AbelianMonoid.Pack _ Rbp_AbelianMonoid_mixin Rbp.
End Some_Monoids.
Section Fct_AbelianMonoid.
Context {T : Type}.
Context {G : AbelianMonoid}.
Definition fct_plus (f g : T → G) : T → G := fun x ⇒ plus (f x) (g x).
Definition fct_zero : T → G := fun _ ⇒ zero.
Lemma fct_plus_comm : ∀ (f g : T → G), fct_plus f g = fct_plus g f.
Proof. intros; apply fun_ext; intro; apply plus_comm. Qed.
Lemma fct_plus_assoc :
∀ (f g h : T → G),
fct_plus f (fct_plus g h) = fct_plus (fct_plus f g) h.
Proof. intros; apply fun_ext; intro; apply plus_assoc. Qed.
Lemma fct_plus_zero_r : ∀ (f : T → G), fct_plus f fct_zero = f.
Proof. intros; apply fun_ext; intro; apply plus_zero_r. Qed.
Definition fct_AbelianMonoid_mixin :=
AbelianMonoid.Mixin _ _ _ fct_plus_comm fct_plus_assoc fct_plus_zero_r.
Canonical Structure fct_AbelianMonoid :=
AbelianMonoid.Pack _ fct_AbelianMonoid_mixin (T → G).
Lemma fct_zero_eq : ∀ x, (0 : T → G) x = 0.
Proof. easy. Qed.
Lemma fct_plus_eq : ∀ (f g : T → G) x, (f + g) x = f x + g x.
Proof. easy. Qed.
End Fct_AbelianMonoid.
Section Fct_AbelianGroup.
Context {T : Type}.
Context {G : AbelianGroup}.
Definition fct_opp (f : T → G) : T → G := fun x ⇒ - (f x).
Lemma fct_plus_opp_r: ∀ (f : T → G), f + (fct_opp f) = 0.
Proof. intros f; apply fun_ext; intro; apply plus_opp_r. Qed.
Definition fct_AbelianGroup_mixin := AbelianGroup.Mixin _ _ fct_plus_opp_r.
Canonical Structure fct_AbelianGroup :=
AbelianGroup.Pack _ (AbelianGroup.Class _ _ fct_AbelianGroup_mixin) (T → G).
Lemma fct_opp_eq : ∀ (f : T → G) x, (- f) x = - f x.
Proof. easy. Qed.
Lemma fct_minus_eq : ∀ (f g : T → G) x, (f - g) x = f x - g x.
Proof. easy. Qed.
End Fct_AbelianGroup.
Section Fct_Ring.
Context {T : Type}.
Context {K : Ring}.
Definition fct_mult (f g : T → K) : (T → K) := fun x ⇒ f x × g x.
Definition fct_one : (T → K) := fun _ ⇒ 1.
Lemma fct_mult_assoc :
∀ (f g h : T → K),
fct_mult f (fct_mult g h) = fct_mult (fct_mult f g) h.
Proof. intros; apply fun_ext; intro; apply mult_assoc. Qed.
Lemma fct_mult_one_r : ∀ (f : T → K), fct_mult f fct_one = f.
Proof. intros; apply fun_ext; intro; apply mult_one_r. Qed.
Lemma fct_mult_one_l : ∀ (f : T → K), fct_mult fct_one f = f.
Proof. intros; apply fun_ext; intro; apply mult_one_l. Qed.
Lemma fct_mult_distr_r :
∀ (f g h : T → K),
fct_mult (f + g) h = fct_mult f h + fct_mult g h.
Proof. intros; apply fun_ext; intro; apply mult_distr_r. Qed.
Lemma fct_mult_distr_l :
∀ (f g h : T → K),
fct_mult f (g + h) = fct_mult f g + fct_mult f h.
Proof. intros; apply fun_ext; intro; apply mult_distr_l. Qed.
Definition fct_Ring_mixin :=
Ring.Mixin _ _ _ fct_mult_assoc fct_mult_one_r fct_mult_one_l
fct_mult_distr_r fct_mult_distr_l.
Canonical Structure fct_Ring :=
Ring.Pack _ (Ring.Class _ _ fct_Ring_mixin) (T → K).
Lemma fct_one_eq : ∀ t, (1 : T → K) t = 1.
Proof. easy. Qed.
Lemma fct_mult_eq : ∀ (f g : T → K) t, (f × g) t = f t × g t.
Proof. easy. Qed.
End Fct_Ring.
Section Fct_ModuleSpace.
Context {T : Type}.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition fct_scal (a : K) (f : T → E) : (T → E) := fun x ⇒ scal a (f x).
Lemma fct_scal_assoc :
∀ a b (f : T → E), fct_scal a (fct_scal b f) = fct_scal (a × b) f.
Proof. intros; apply fun_ext; intro; apply scal_assoc. Qed.
Lemma fct_scal_one : ∀ (f : T → E), fct_scal 1 f = f.
Proof. intros; apply fun_ext; intro; apply scal_one. Qed.
Lemma fct_scal_distr_l :
∀ a (f g : T → E), fct_scal a (f + g) = fct_scal a f + fct_scal a g.
Proof. intros; apply fun_ext; intro; apply scal_distr_l. Qed.
Lemma fct_scal_distr_r :
∀ a b (f : T → E), fct_scal (a + b) f = fct_scal a f + fct_scal b f.
Proof. intros; apply fun_ext; intro; apply scal_distr_r. Qed.
Definition fct_ModuleSpace_mixin :=
ModuleSpace.Mixin _ _ _
fct_scal_assoc fct_scal_one fct_scal_distr_l fct_scal_distr_r.
Canonical Structure fct_ModuleSpace :=
ModuleSpace.Pack _ _ (ModuleSpace.Class _ _ _ fct_ModuleSpace_mixin) (T → E).
Lemma fct_scal_eq : ∀ a (f : T → E) t, scal a f t = scal a (f t).
Proof. easy. Qed.
Definition fct_scal_l (f : T → K) (x : E) (t : T) : E := scal (f t) x.
Lemma fct_scal_l_eq : ∀ (f : T → K) x t, fct_scal_l f x t = scal (f t) x.
Proof. easy. Qed.
Definition fct_scal_r_eq := fct_scal_eq.
End Fct_ModuleSpace.