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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
From Coq Require Import Reals Lia List ssreflect ssrbool.
From mathcomp Require Import seq eqtype.
Require Import Rcomplements.
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.