Library CoqApprox.seq_compl

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and Inria.
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.

Section NatCompl.

Lemma nat_ind_gen (P : nat -> Prop) :
  (forall x, (forall y, (y < x)%N -> P y) -> P x) -> (forall x, P x).

Lemma predn_leq (m n : nat) : m <= n -> m.-1 <= n.-1.

Lemma ltn_subr (m n p : nat) : m < n -> n - p.+1 < n.

Lemma minnl (m n : nat) : m <= n -> minn m n = m.

Lemma minnr (m n : nat) : n <= m -> minn m n = n.

End NatCompl.

Section Take.
Variable (T : Type).

Lemma size_take_minn (n : nat) (s : seq T) : size (take n s) = minn n (size s).

End Take.

Section Map2.
Variables (A : Type) (B : Type) (C : Type).
Variable f : A -> B -> C.

Fixpoint map2 (s1 : seq A) (s2 : seq B) : seq C :=
  match s1, s2 with
    | a :: s3, b :: s4 => f a b :: map2 s3 s4
    | _, _ => [::]
  end.

Lemma size_map2 (s1 : seq A) (s2 : seq B) :
  size (map2 s1 s2) = minn (size s1) (size s2).

Lemma nth_map2 s1 s2 (k : nat) da db dc :
  dc = f da db -> size s2 = size s1 ->
  nth dc (map2 s1 s2) k = f (nth da s1 k) (nth db s2 k).

End Map2.

Section Head_Last.
Variables (T : Type) (d : T).

Lemma head_cons : forall s, s <> [::] -> s = head d s :: behead s.

Definition hb s := head d (behead s).

Lemma nth1 : forall s, nth d s 1 = hb s.

Lemma last_rev : forall s, last d (rev s) = head d s.

Definition rmlast (l : seq T) := (belast (head d l) (behead l)).
End Head_Last.

Lemma rmlast_cons T (d e f : T) (s : seq T) :
  s <> [::] -> rmlast e (f :: s) = f :: rmlast d s.

Section Fold.
Variables (A B : Type) (f : A -> B).

Lemma foldr_cons (r : seq A) (s : seq B) :
  foldr (fun x acc => f x :: acc) s r = map f r ++ s.

Corollary foldr_cons0 (r : seq A) :
  foldr (fun x acc => f x :: acc) [::] r = map f r.

Lemma foldl_cons (r : seq A) (s : seq B) :
  foldl (fun acc x => f x :: acc) s r = (catrev (map f r) s).

Corollary foldl_cons0 (r : seq A) :
  foldl (fun acc x => f x :: acc) [::] r = rev (map f r).

End Fold.