Library CoqApprox.nary_tuple

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 ZArith.
Require Import NaryFunctions.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
Require Import seq_compl.

This theory extends NaryFunctions (from Coq's standard library), relying on an SSReflect formalization style.

Set Implicit Arguments.


Definition Ttoseq := nprod_to_list.
Definition Tofseq := nprod_of_list.

Section NaryTuple.

Variables (n : nat) (T : Type).

Lemma Ttoseq_inj : injective (@Ttoseq T n).

Definition Tsize of (T ^ n) := n.

Lemma size_Tuple (t : T ^ n) : size (Ttoseq t) = n.

End NaryTuple.

Close section to generalize w.r.t. n.

Section NaryTuple1.

Variables (n : nat) (T : Type).

Implicit Type t : T ^ n.

Lemma TofseqK l : Ttoseq (@Tofseq T l) = l.

Lemma Tnth_default t : 'I_n -> T.

Definition Tnth t i := nth (Tnth_default t i) (Ttoseq t) i.

Lemma Tnth_nth (x0 : T) t i : Tnth t i = nth x0 (Ttoseq t) i.

Lemma map_Tnth_enum t : map (Tnth t) (enum 'I_n) = Ttoseq t.

Lemma eq_from_Tnth (t1 t2 : T ^ n) : Tnth t1 =1 Tnth t2 -> t1 = t2.

End NaryTuple1.

Notation "[ 'Tuple' 'of' s ]" := (Tofseq s)
  (at level 0, format "[ 'Tuple' 'of' s ]") : form_scope.

Notation "[ 'Tnth' t i ]" := (Tnth t (@Ordinal (Tsize t) i (erefl true)))
  (at level 0, t, i at level 8, format "[ 'Tnth' t i ]") : form_scope.

Definition cons_Tuple n T : T -> T ^ n -> T ^ n.+1 := @pair T (T ^ n).

Notation "[ 'Tuple' ]" := (tt : _ ^ 0)
  (at level 0, format "[ 'Tuple' ]") : form_scope.

Notation "[ 'Tuple' x ]" := (cons_Tuple x [Tuple])
  (at level 0, format "[ 'Tuple' x ]") : form_scope.

Notation "[ 'Tuple' x1 ; .. ; xn ]" := (cons_Tuple x1 ( .. [Tuple xn] .. ))
  (at level 0, format "[ 'Tuple' '[' x1 ; '/' .. ; '/' xn ']' ]")
  : form_scope.

Section NaryTupleCast.

Variable (T : Type).

Definition Tcast m n (eq_mn : m = n) t := ecast i (T ^ i) eq_mn t.

Lemma TcastE m n (eq_mn : m = n) t i :
  Tnth (Tcast eq_mn t) i = Tnth t (cast_ord (esym eq_mn) i).

Lemma Tcast_id n (eq_nn : n = n) t : Tcast eq_nn t = t.

Lemma TcastK m n (eq_mn : m = n) : cancel (Tcast eq_mn) (Tcast (esym eq_mn)).

Lemma TcastKV m n (eq_mn : m = n) : cancel (Tcast (esym eq_mn)) (Tcast eq_mn).

Lemma Tcast_trans m n p (eq_mn : m = n) (eq_np : n = p) t :
  Tcast (etrans eq_mn eq_np) t = Tcast eq_np (Tcast eq_mn t).

Lemma TtoseqK n (t : T ^ n) : Tofseq (Ttoseq t) = Tcast (esym (size_Tuple t)) t.

End NaryTupleCast.

Section NaryTupleMap.

Variables (T rT : Type) (f : T -> rT).

Fixpoint map_Tuple n (t : T ^ n) {struct n} : rT ^ n :=
  match n, t with
  | 0, _ => [Tuple]
  | S n', (x0, t') => cons_Tuple (f x0) (@map_Tuple n' t')
  end.

Lemma Ttoseq_map n (t : T ^ n) :
  Ttoseq (map_Tuple t) = map f (Ttoseq t).

Lemma Tnth_map_Tuple n (t : T ^ n) i : Tnth (map_Tuple t) i = f (Tnth t i).

End NaryTupleMap.

Section NaryTupleSeq.

Variables (n : nat) (T : Type).

Implicit Type t : T ^ n.

Definition Thead (u : T ^ n.+1) := Tnth u ord0.

Lemma Tnth0 (x : T) t : Tnth (cons_Tuple x t) ord0 = x.

Lemma TheadE x t : Thead (cons_Tuple x t) = x.

Lemma Tuple0 : all_equal_to ([Tuple] : T ^ 0).

Lemma Tuple0eq (H : n = 0) : all_equal_to (Tcast (esym H) ([Tuple] : T^0)).

Fixpoint nseq_Tuple n T (x : T) {struct n} : T ^ n :=
  match n with
  | 0 => [Tuple]
  | S n' => cons_Tuple x (nseq_Tuple n' x)
  end.

Lemma Ttoseq_nseq (x : T) : Ttoseq (nseq_Tuple n x) = nseq n x.

Fixpoint iota_Tuple p m {struct p} : nat ^ p :=
  match p with
  | 0 => [Tuple]
  | S p' => cons_Tuple m (iota_Tuple p' m.+1)
  end.

Lemma Ttoseq_iota p m : Ttoseq (iota_Tuple p m) = iota m p.

End NaryTupleSeq.

Section Tuplify.
Conversions between Tuple and Ssreflect's tuple.

Variables (T : Type).

Fixpoint tuplify n (t : T ^ n) : n.-tuple T :=
  match n, t with
  | 0, _ => [tuple]
  | S _, (x, t') => cons_tuple x (tuplify t')
  end.

Fixpoint Tuplify n (t : n.-tuple T) : T ^ n :=
  match n, t with
  | 0, _ => [Tuple]
  | S n', _ => cons_Tuple (thead t) (Tuplify (behead_tuple t))
  end.

Lemma tnth_tuplify n (t : T ^ n) i : tnth (tuplify t) i = Tnth t i.

Lemma Tnth_Tuplify n (t : n.-tuple T) i : Tnth (Tuplify t) i = tnth t i.

Lemma tuplifyK n : cancel (@tuplify n) (@Tuplify n).

Lemma TuplifyK n : cancel (@Tuplify n) (@tuplify n).

Lemma Ttoseq_Tuplify n (t : n.-tuple T) :
  Ttoseq (Tuplify t) = val t.

Lemma val_tuplify n (t : T ^ n) :
  val (tuplify t) = Ttoseq t.

End Tuplify.

Section NaryTupleMk.

Variable n : nat.

Definition ord_Tuple : 'I_n ^ n := Tuplify (ord_tuple n).

Lemma Ttoseq_ord_Tuple : Ttoseq (ord_Tuple) = enum 'I_n.

Lemma Tnth_ord_Tuple i : Tnth (ord_Tuple) i = i.

Variable U : Type.

Lemma Tuple_map_ord (t : U ^ n) : t = map_Tuple (Tnth t) (ord_Tuple).

Variable (f : 'I_n -> U).

Non-computational function to build a Tuple from an expression.
Definition mkTupleO := map_Tuple f (ord_Tuple).

Lemma Tnth_mkTupleO i : Tnth mkTupleO i = f i.

Lemma nth_mkTupleO (x0 : U) (i : 'I_n) : nth x0 (Ttoseq mkTupleO) i = f i.

End NaryTupleMk.

Section NaryTupleMkNat.

Variables (n : nat) (U : Type) (f : nat -> U).

Computational function to build a Tuple from an expression.
Definition mkTuple := map_Tuple f (iota_Tuple n 0).

Lemma Tnth_mkTuple (i : 'I_n) : Tnth (mkTuple) i = f i.

Lemma nth_mkTuple (x0 : U) (i : nat) : i < n -> nth x0 (Ttoseq mkTuple) i = f i.

End NaryTupleMkNat.

Notation "[ 'Tuple' F | i < n ]" := (mkTupleO (fun i : 'I_n => F))
  (at level 0, i at level 0,
   format "[ '[hv' 'Tuple' F '/' | i < n ] ']'") : form_scope.

Notation "[ 'Tuple' F | 0 <= i < n ]" := (mkTuple (fun i : nat => F) n)
  (at level 0, i at level 0,
   format "[ '[hv' 'Tuple' F '/' | 0 <= i < n ] ']'") : form_scope.

Note that the term represented by the notation [Tuple F | 0 <= i < n] can be evaluated: it roughly correspond to mkseq (fun i => F) n for Tuples.


Section takeN_lastN.

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

Fixpoint takeN (n : nat) (s : seq T) {struct n} : T ^ n :=
  match n with
    | O => [Tuple]
    | S n' =>
      match s with
        | [::] => cons_Tuple d (takeN n' [::])
        | x :: s' => cons_Tuple x (takeN n' s')
      end
  end.

Lemma Ttoseq_takeN (n : nat) (s : seq T) :
  n <= size s -> Ttoseq (takeN n s) = take n s.

Stronger lemma w.r.t. Ttoseq_takeN.
Lemma Ttoseq_takeN' (n : nat) (s : seq T) :
  Ttoseq (takeN n s) = take n s ++ nseq (n - size s) d.

Lemma takeN_Ttoseq (n : nat) (t : T ^ n) : takeN n (Ttoseq t) = t.

Definition lastN (n : nat) (s : seq T) : T ^ n :=
  takeN n (drop (size s - n) s).

Lemma lastN_Ttoseq (n : nat) (t : T ^ n) : lastN n (Ttoseq t) = t.

Lemma Ttoseq_lastN_drop (n : nat) (s : seq T) :
  n <= size s -> Ttoseq (lastN n s) = take n (drop (size s - n) s).

Lemma take_drop_rev (n : nat) (s : seq T) :
  take n (drop (size s - n) s) = rev (take n (rev s)).

Lemma Ttoseq_lastN_rev (n : nat) (s : seq T) :
  n <= size s -> Ttoseq (lastN n s) = rev (take n (rev s)).

Stronger lemma w.r.t. Ttoseq_lastN_drop.
Lemma Ttoseq_lastN_drop' (n : nat) (s : seq T) :
  Ttoseq (lastN n s) = take n (drop (size s - n) s) ++ nseq (n - size s) d.

Stronger lemma w.r.t. Ttoseq_lastN_rev.
Lemma Ttoseq_lastN_rev' (n : nat) (s : seq T) :
  Ttoseq (lastN n s) = rev (take n (rev s)) ++ nseq (n - size s) d.

Lemma Tnth_lastN (n : nat) (i : 'I_n) (s : seq T) :
  Tnth (lastN n s) i = nth d s (size s - n + val i).

End takeN_lastN.