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

Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
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 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 : forall x, op x0 x = x).
Context (neutral_r : forall x, op x x0 = x).
Context (assoc : forall 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.
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: l => [ | h l IH] //=.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite IH.
Qed.

Lemma iter_cat l1 l2 f :
  iter (l1 ++ l2) f = op (iter l1 f) (iter l2 f).
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: l1 => [ | h1 l1 IH] /=.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite neutral_l.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite IH assoc.
Qed.
Lemma iter_ext l f1 f2 :
  (forall x, In x l -> f1 x = f2 x) ->
  iter l f1 = iter l f2.
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: l => [ | h l IH] /= Heq.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by [].
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite IH.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite Heq //.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by left.
(* Goal: forall (x : I) (_ : @In I x l), @eq T (f1 x) (f2 x) *)
  intros x Hx.
(* Goal: @eq T (a k) (b k) *)
  apply Heq.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by right.
Qed.

Lemma iter_comp (l : list I) f (g : I -> I) :
  iter l (fun x => f (g x)) = iter (map g l) f.
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: l => [ | s l IH] //=.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite IH.
Qed.

End Iter.

Lemma iter_const {I} (l : list I) (a : R) :
  iter Rplus 0 l (fun _ => a) = INR (length l) * a.
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: l => /= [ | h l ->].
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite /= Rmult_0_l.
(* Goal: @eq R (Rplus a (Rmult (INR (@length I l)) a)) (Rmult match @length I l with | O => IZR (Zpos xH) | S n0 => Rplus (INR (@length I l)) (IZR (Zpos xH)) end a) *)
  case: (length l) => [ | n] ; simpl ; ring.
Qed.

Lemma In_mem {T : eqType} (x : T) l :
  reflect (In x l) (in_mem x (mem l)).
Proof.
(* Goal: Bool.reflect (@In (Equality.sort T) x l) (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) l)) *)
apply iffP with (P := x \in l).
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
by case: (x \in l) => // ; constructor.

(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
elim: l => [ | h l IH] //= E.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
rewrite in_cons in E.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
case/orP: E => E.
(* Goal: or (@eq (Equality.sort T) h x) (@In (Equality.sort T) x l) *)
(* Goal: or (@eq (Equality.sort T) h x) (@In (Equality.sort T) x l) *)
(* Goal: forall _ : @In (Equality.sort T) x l, is_true (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) l)) *)
now left ; apply sym_eq ; apply / eqP.
(* Goal: or (@eq (Equality.sort T) h x) (@In (Equality.sort T) x l) *)
(* Goal: forall _ : @In (Equality.sort T) x l, is_true (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) l)) *)
right ; by apply IH.

(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
elim: l => [ | h l IH] E //=.
(* Goal: is_true (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) (@Datatypes.cons (Equality.sort T) h l))) *)
simpl in E.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
case : E => E.
(* Goal: is_true (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) (@Datatypes.cons (Equality.sort T) h l))) *)
(* Goal: is_true (@in_mem (Equality.sort T) x (@mem (Equality.sort T) (seq_predType T) (@Datatypes.cons (Equality.sort T) h l))) *)
rewrite E ; apply mem_head.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
rewrite in_cons.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
rewrite IH.
(* Goal: is_true (orb (@eq_op T x h) true) *)
(* Goal: @In (Equality.sort T) x l *)
apply orbT.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
by [].
Qed.

Lemma In_iota (n m k : nat) :
  (n <= m <= k)%nat <-> In m (iota n (S k - n)).
Proof.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  generalize (mem_iota n (S k - n) m).
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  case: In_mem => // H H0.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  apply sym_eq in H0.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  case/andP: H0 => H0 H1.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  apply Rcomplements.SSR_leq in H0.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  apply SSR_leq in H1.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  change ssrnat.addn with Peano.plus in H1.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  split => // _.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  split => //.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  case: (le_dec n (S m)).
(* Goal: forall _ : le n (S m), le m k *)
(* Goal: forall _ : not (le n (S m)), le m k *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  intro ; omega.
(* Goal: forall _ : not (le n (S m)), le m k *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  intro H2.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  rewrite not_le_minus_0 in H1 => //.
(* Goal: not (le n (S k)) *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  contradict H2.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by eapply le_trans, le_n_Sn.
(* Goal: not (le n (S k)) *)
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  contradict H2.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by eapply le_trans, le_n_Sn.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  change ssrnat.addn with Peano.plus in H0.
(* Goal: iff (and (le n m) (le m k)) (@In nat m (iota n (Init.Nat.sub (S k) n))) *)
  split => // H1.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  case: H1 => /= H1 H2.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  apply sym_eq in H0.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  apply Bool.andb_false_iff in H0.
(* Goal: @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  case: H0 => //.
(* Goal: forall _ : @eq bool (ssrnat.leq (S m) (S k)) false, @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  move/SSR_leq: H1 ; by case: ssrnat.leq.
(* Goal: forall _ : @eq bool (ssrnat.leq (S m) (Init.Nat.add n (Init.Nat.sub (S k) n))) false, @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  rewrite -le_plus_minus ; try omega.
(* Goal: forall _ : @eq bool (ssrnat.leq (S m) (S k)) false, @In nat m (iota n match n with | O => S k | S l => Init.Nat.sub k l end) *)
  move/le_n_S/SSR_leq: H2 ; by case: ssrnat.leq.
Qed.

Section Iter_nat.

Context {T : Type}.

Context (op : T -> T -> T).
Context (x0 : T).
Context (neutral_l : forall x, op x0 x = x).
Context (neutral_r : forall x, op x x0 = x).
Context (assoc : forall 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) :
  (forall k, (n <= k <= m)%nat -> a k = b k) ->
  iter_nat a n m = iter_nat b n m.
Proof.
(* Goal: forall _ : forall (k : nat) (_ : and (le n k) (le k m)), @eq T (a k) (b k), @eq T (iter_nat a n m) (iter_nat b n m) *)
  intros Heq.
(* Goal: @eq T (iter_nat a n m) (iter_nat b n m) *)
  apply iter_ext.
(* Goal: forall (x : nat) (_ : @In nat x (iota n (Init.Nat.sub (S m) n))), @eq T (a x) (b x) *)
  intros k Hk.
(* Goal: @eq T (a k) (b k) *)
  apply Heq.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by apply In_iota.
Qed.

Lemma iter_nat_point a n :
  iter_nat a n n = a n.
Proof.
(* Goal: @eq T (iter_nat a n n) (a n) *)
  unfold iter_nat.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite -minus_Sn_m // minus_diag /=.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by apply neutral_r.
Qed.

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).
Proof.
(* Goal: forall (_ : le n (S m)) (_ : le m k), @eq T (iter_nat a n k) (op (iter_nat a n m) (iter_nat a (S m) k)) *)
  intros Hnm Hmk.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite -iter_cat //.
  pattern (S m) at 2 ;
  replace (S m) with (ssrnat.addn n (S m - n)).
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite -(iota_add n (S m - n)).
(* Goal: @eq T (iter_nat a n k) (@iter nat T op x0 (iota n (ssrnat.addn (Init.Nat.sub (S m) n) (Init.Nat.sub (S k) (S m)))) a) *)
(* Goal: @eq nat (ssrnat.addn n (Init.Nat.sub (S m) n)) (S m) *)
  apply (f_equal (fun k => iter _ _ (iota n k) _)).
(* Goal: @eq nat (ssrnat.addn n (Init.Nat.sub (S m) n)) (S m) *)
  change ssrnat.addn with Peano.plus.
(* Goal: @eq nat (Init.Nat.add n (Init.Nat.sub (S m) n)) (S m) *)
  omega.
(* Goal: @eq nat (ssrnat.addn n (Init.Nat.sub (S m) n)) (S m) *)
  change ssrnat.addn with Peano.plus.
(* Goal: @eq nat (Init.Nat.add n (Init.Nat.sub (S m) n)) (S m) *)
  omega.
Qed.

Lemma iter_nat_S a n m :
  iter_nat (fun n => a (S n)) n m = iter_nat a (S n) (S m).
Proof.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite /iter_nat iter_comp.
(* Goal: @eq T (@iter nat T op x0 (@map nat nat S (iota n (Init.Nat.sub (S m) n))) a) (@iter nat T op x0 (iota (S n) (Init.Nat.sub (S (S m)) (S n))) a) *)
  apply (f_equal (fun l => iter _ _ l _)).
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S (S m)) (S n))) *)
  rewrite MyNat.sub_succ.
(* Goal: @eq (list nat) (@map nat nat S (iota n (Init.Nat.sub (S m) n))) (iota (S n) (Init.Nat.sub (S m) n)) *)
  elim: (S m - n)%nat {1 3}(n) => {n m} [ | n IH] m //=.
(* Goal: @eq (list nat) (@Datatypes.cons nat (S m) (@map nat nat S (iota (S m) n))) (@Datatypes.cons nat (S m) (iota (S (S m)) n)) *)
  by rewrite IH.
Qed.

End Iter_nat.
