Library Algebra.Monoid.MonoidComp

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

Support for iterated composition of functions.

Description

The composition of functions is not commutative, hence the underlying monoid structure cannot be represented with an AbelianMonoid structure. However, it is still possible to iterate composition by using bigops from the Mathematical Components library.
Let T : Type and f : '(T T)^n.
  • comp_n f is the composition of all items of f (from 0 to n-1);
  • comp_n_part f i is the partial composition of items of f, from 0 to i-1.

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 ssr_wMC.
From mathcomp Require Import bigop.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Monoid_compl Monoid_morphism Monoid_sub.

Section Compose_n_Def.

Context {E : Type}.
Context {n : nat}.

Definition comp_m : Monoid.law (ssrfun.id : E E).
Proof. ssrfun.comp; easy. Defined.

Lemma comp_m_correct : (f g : E E), f \o g = comp_m f g.
Proof. easy. Qed.

Definition comp_n (f : '(E E)^n) : E E :=
  \big[comp_m/ssrfun.id]_(i < n) f i.

Lemma comp_n_eq : (f g : '(E E)^n), f = g comp_n f = comp_n g.
Proof. intros; subst; easy. Qed.

Lemma comp_n_ext :
   (f g : '(E E)^n), same_funF f g comp_n f = comp_n g.
Proof. move=>> H; apply eq_bigr; intros; apply fun_ext, H. Qed.

End Compose_n_Def.

Section Compose_n_Bigop_Wrapper.


Context {E : Type}.
Context {n : nat}.

Lemma comp_n_id_compat :
   (f : '(E E)^n),
    eqAF f (constF n ssrfun.id) comp_n f = ssrfun.id.
Proof. move=>> Hf; apply big1; intros i _; apply (Hf i). Qed.

Lemma comp_n_nil : (f : '(E E)^n), n = 0 comp_n f = ssrfun.id.
Proof. intros; subst; apply big_ord0. Qed.

Lemma comp_n_ind_l :
   (f : '(E E)^n.+1) , comp_n f = f ord0 \o comp_n (liftF_S f).
Proof. intros; apply big_ord_recl. Qed.

Lemma comp_n_ind_r :
   (f : '(E E)^n.+1), comp_n f = comp_n (widenF_S f) \o f ord_max.
Proof. intros; apply big_ord_recr. Qed.

End Compose_n_Bigop_Wrapper.

Section Compose_n_Facts.

Context {E : Type}.

Lemma comp_n_ext_alt :
   {n1 n2} (H : n1 = n2) (f1 : '(E E)^n1) (f2 : '(E E)^n2),
    same_funF (castF H f1) f2 comp_n f1 = comp_n f2.
Proof. move=>>; subst; rewrite castF_id; apply comp_n_ext. Qed.

End Compose_n_Facts.

Section Compose_n_part_Def.

Context {E : Type}.
Context {n : nat}.

Definition comp_n_part (f : '(E E)^n) (j : 'I_n.+1) : E E :=
  comp_n (widenF (leq_ord j) f).

Lemma comp_n_part_eq :
   (f g : '(E E)^n) (j : 'I_n.+1),
    widenF (leq_ord j) f = widenF (leq_ord j) g
    comp_n_part f j = comp_n_part g j.
Proof. move=>>; apply comp_n_eq. Qed.

Lemma comp_n_part_ext :
   (f g : '(E E)^n) (j : 'I_n.+1),
    same_funF (widenF (leq_ord j) f) (widenF (leq_ord j) g)
    comp_n_part f j = comp_n_part g j.
Proof. move=>>; apply comp_n_ext. Qed.

End Compose_n_part_Def.

Section Compose_n_part_Facts.

Context {E : Type}.
Context {n : nat}.

Lemma comp_n_part_id_compat :
   (f : '(E E)^n) j,
    eqAF f (constF n ssrfun.id) comp_n_part f j = ssrfun.id.
Proof. move=>> H; apply comp_n_id_compat; intro; apply H. Qed.

Lemma comp_n_part_0 :
   {n} (f : '(E E)^n) j, j = ord0 comp_n_part f j = ssrfun.id.
Proof. intros; subst; apply comp_n_nil; easy. Qed.

Lemma comp_n_part_nil :
   (f : '(E E)^n) j, n = 0 comp_n_part f j = ssrfun.id.
Proof. intros; subst; apply comp_n_part_0, I_1_is_unit. Qed.

Lemma comp_n_part_max :
   {n} (f : '(E E)^n) j, j = ord_max comp_n_part f j = comp_n f.
Proof. intros; subst; unfold comp_n_part; rewrite widenF_full; easy. Qed.

Lemma comp_n_part_ind_l :
   (f : '(E E)^n.+1) {j} (H : j ord0),
    comp_n_part f j = f ord0 \o comp_n_part (liftF_S f) (lower_S H).
Proof.
intros f j H; unfold comp_n_part.
rewrite widenF_liftF_S -(widenF_0 (leqS (leq_ord (lower_S H)))) -comp_n_ind_l.
assert (H' : j = (lower_S H).+1 :> nat)
    by now rewrite -lift_S_correct lift_lower_S.
apply: comp_n_ext_alt; intros i x.
unfold castF, widenF; f_equal; apply ord_inj; easy.
Qed.

Lemma comp_n_part_ind_r :
   (f : '(E E)^n) j,
    comp_n_part f (lift_S j) = comp_n_part f (widen_S j) \o f j.
Proof.
intros; unfold comp_n_part; rewrite comp_n_ind_r; repeat f_equal;
    [apply extF; intro |]; unfold widenF_S, widenF; f_equal; apply ord_inj; easy.
Qed.

End Compose_n_part_Facts.

Section Compose_n_Monoid_Facts1.

Context {E : AbelianMonoid}.
Context {n : nat}.

Variable f : '(E E)^n.

Lemma comp_n_f_plus_compat :
  ( i, f_plus_compat (f i)) f_plus_compat (comp_n f).
Proof.
intros Hf; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply f_plus_compat_comp; [apply Hn1; intro; apply Hf | easy].
Qed.

Lemma comp_n_f_zero_compat :
  ( i, f_zero_compat (f i)) f_zero_compat (comp_n f).
Proof.
intros Hf; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply f_zero_compat_comp; [apply Hn1; intro; apply Hf | easy].
Qed.

Lemma comp_n_mm :
  ( i, morphism_m (f i)) morphism_m (comp_n f).
Proof.
intros Hf; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply mm_comp; [apply Hn1; intro; apply Hf | easy].
Qed.

End Compose_n_Monoid_Facts1.

Section Compose_n_Monoid_Facts2.

Context {E : AbelianMonoid}.
Context {PE : E Prop}.

Lemma comp_n_funS :
   {n} (f : '(E E)^n),
    ( i, funS PE PE (f i)) funS PE PE (comp_n f).
Proof.
intros n f Hf; induction n as [| n Hn];
    [rewrite comp_n_nil; [apply funS_id |]; easy | rewrite comp_n_ind_l].
apply (funS_comp_compat PE); [apply Hn; unfold liftF_S |]; easy.
Qed.

Context {n : nat}.

Variable f : '(E E)^n.
Hypothesis Hf : i, funS PE PE (f i).

Lemma comp_n_f_plus_compat_sub :
  ( i, f_plus_compat_sub PE (f i)) f_plus_compat_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (f_plus_compat_comp_sub PE);
    [apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.

Lemma comp_n_f_zero_compat_sub :
  ( i, f_zero_compat_sub PE (f i)) f_zero_compat_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (f_zero_compat_comp_sub PE);
    [apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.

Lemma comp_n_mm_sub : ( i, mm_sub PE (f i)) mm_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
    [rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (mm_comp_sub PE);
    [apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.

End Compose_n_Monoid_Facts2.

Section Compose_n_part_Monoid_Facts1.

Context {E : AbelianMonoid}.
Context {n : nat}.

Variable f : '(E E)^n.
Variable j : 'I_n.+1.

Lemma comp_n_part_f_plus_compat :
  ( i, f_plus_compat (widenF (leq_ord j) f i))
  f_plus_compat (comp_n_part f j).
Proof. intros Hf; apply comp_n_f_plus_compat; intro; apply Hf. Qed.

Lemma comp_n_part_f_zero_compat :
  ( i, f_zero_compat (widenF (leq_ord j) f i))
  f_zero_compat (comp_n_part f j).
Proof. intros Hf; apply comp_n_f_zero_compat; intro; apply Hf. Qed.

Lemma comp_n_part_mm :
  ( i, morphism_m (widenF (leq_ord j) f i))
  morphism_m (comp_n_part f j).
Proof. intros Hf; apply comp_n_mm; intro; apply Hf. Qed.

End Compose_n_part_Monoid_Facts1.

Section Compose_n_part_Monoid_Facts2.

Context {E : AbelianMonoid}.
Context {PE : E Prop}.

Lemma comp_n_part_funS :
   {n} (f : '(E E)^n) j,
    ( i, funS PE PE (widenF (leq_ord j) f i))
    funS PE PE (comp_n_part f j).
Proof.
intros n f j Hf; induction n as [| n Hn];
    [rewrite comp_n_part_nil; [apply funS_id |]; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
    [rewrite (comp_n_part_0 _ _ Hj0); apply funS_id; easy |].
rewrite comp_n_part_ind_l; apply (funS_comp_compat PE); [apply Hn |].
intros; apply (widenF_liftF_S_P_compat _ Hj0 Hf); easy.
apply (widenF_0_P_compat Hj0 Hf).
Qed.

Context {n : nat}.

Variable f : '(E E)^n.
Variable j : 'I_n.+1.
Hypothesis Hf : i, funS PE PE (widenF (leq_ord j) f i).


Lemma comp_n_part_f_plus_compat_sub :
  ( i, f_plus_compat_sub PE (widenF (leq_ord j) f i))
  f_plus_compat_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
    [rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (f_plus_compat_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.

Lemma comp_n_part_f_zero_compat_sub :
  ( i, f_zero_compat_sub PE (widenF (leq_ord j) f i))
  f_zero_compat_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
    [rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (f_zero_compat_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.

Lemma comp_n_part_mm_sub :
  ( i, mm_sub PE (widenF (leq_ord j) f i))
  mm_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
    [rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (mm_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.

End Compose_n_part_Monoid_Facts2.