Library Coquelicot.Iter

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
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.

Require Import Reals Ssreflect.ssreflect.
Require Import Rcomplements.
Require Import List Omega.
Require Import Ssreflect.seq Ssreflect.ssrbool Ssreflect.eqtype.

This file describes iterators on lists. This is mainly used for Riemannn sums.

Section Iter.

Context {I T : Type}.

Context (op : TTT).
Context (x0 : T).
Context (neutral_l : x, op x0 x = x).
Context (neutral_r : x, op x x0 = x).
Context (assoc : x y z, op x (op y z) = op (op x y) z).

Fixpoint iter (l : list I) (f : IT) :=
  match l with
  | nilx0
  | cons h l'op (f h) (iter l' f)
  end.

Definition iter' (l : list I) (f : IT) :=
  fold_right (fun i accop (f i) acc) x0 l.

Lemma iter_iter' l f :
  iter l f = iter' l f.

Lemma iter_cat l1 l2 f :
  iter (l1 ++ l2) f = op (iter l1 f) (iter l2 f).
Lemma iter_ext l f1 f2 :
  ( x, In x lf1 x = f2 x) →
  iter l f1 = iter l f2.

Lemma iter_comp (l : list I) f (g : II) :
  iter l (fun xf (g x)) = iter (map g l) f.

End Iter.

Lemma iter_const {I} (l : list I) (a : R) :
  iter Rplus 0 l (fun _a) = INR (length l) × a.

Lemma In_mem {T : eqType} (x : T) l :
  reflect (In x l) (in_mem x (mem l)).

Lemma In_iota (n m k : nat) :
  (n m k)%nat In m (iota n (S k - n)).

Section Iter_nat.

Context {T : Type}.

Context (op : TTT).
Context (x0 : T).
Context (neutral_l : x, op x0 x = x).
Context (neutral_r : x, op x x0 = x).
Context (assoc : x y z, op x (op y z) = op (op x y) z).

Definition iter_nat (a : natT) n m :=
  iter op x0 (iota n (S m - n)) a.

Lemma iter_nat_ext_loc (a b : natT) (n m : nat) :
  ( k, (n k m)%nata k = b k) →
  iter_nat a n m = iter_nat b n m.

Lemma iter_nat_point a n :
  iter_nat a n n = a n.

Lemma iter_nat_Chasles a n m k :
  (n S m)%nat → (m k)%nat
  iter_nat a n k = op (iter_nat a n m) (iter_nat a (S m) k).

Lemma iter_nat_S a n m :
  iter_nat (fun na (S n)) n m = iter_nat a (S n) (S m).

End Iter_nat.