Library Coquelicot.Iter

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 mathcomp.ssreflect.ssreflect.
Require Import Rcomplements.
Require Import List Omega.
Require Import mathcomp.ssreflect.seq mathcomp.ssreflect.ssrbool mathcomp.ssreflect.eqtype.

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

Section Iter.

Context {I T : Type}.

Context (op : T → T → T).
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 : I → T) :=
  match l with
  | nil ⇒ x0
  | cons h l' ⇒ op (f h) (iter l' f)
  end.

Definition iter' (l : list I) (f : I → T) :=
  fold_right (fun i acc ⇒ op (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 l → f1 x = f2 x ) →
  iter l f1 = iter l f2.

Lemma iter_comp (l : list I) f (g : I → I) :
  iter l (fun x ⇒ f (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 : T → T → T).
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 : nat → T) n m :=
  iter op x0 (iota n (S m - n)) a.

Lemma iter_nat_ext_loc (a b : nat → T) (n m : nat) :
  (∀ k, (n ≤ k ≤ m)%nat → a 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 n ⇒ a (S n)) n m = iter_nat a (S n) (S m).

End Iter_nat.