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.

Brief description

Complements for the Hierarchy module of the Coquelicot library.

Description

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:
  • notations,
  • some instances of AbelianMonoid,
  • support for functions to types equipped with one of the algebraic structure listed above.

Additional notations

Monoid scope Monoid_scope (delimitor = 'M')
  • x + y is for plus x y;
  • 0 is for zero.
See also Algebra.Monoid.MonoidMult.
Group scope Group_scope (delimitor = 'G')
  • - x is for opp x;
  • x - y is for minus x y.
Ring scope Ring_scope (delimitor = 'R')
  • two is one + one;
  • notation x × y is for mult x y;
  • notation 1 is for one;
  • notation 2 is for two.

Some commutative monoids

Support for functions to an AbelianMonoid

Let T be any type. Let f g : T G.

Support for functions to an AbelianGroup

Let T be any type. Let G : AbelianGroup. Let f g : T G.
  • 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

Let T be any type. Let f g : T K.
  • 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

Let K : Ring and E : ModuleSpace K. Let T : Type and f : T E.

Used logic axioms

Usage

This module may be used through the import of Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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 xplus (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 xf 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 xscal 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.