Library tuple

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.

Import Prenex Implicits.

Tuples, i.e., lists with a fixed (known) length. We define:               
  n.-tuple T   : the type of n-tuples of elements of type T.              
  [tuple of s] : the tuple whose underlying sequence (value) is s, which  
                 must have a known size; specifically, Coq must be able   
                 to infer a tuple whose Canonical Projection is s, e.g.,  
    [tuple]            is the empty tuple, and                            
    [tuple x1; ..; xn] the explicit n.-tuple <x1; ..; xn>.                
As n.-tuple T coerces to seq t, all operations for seq (size, nth, ...)   
can be applied to t : n.-tuple T; we provide a few specialized instances  
when this avoids the need for a default value.                            
  tsize t      : the size of t (the n in n.-tuple T)                      
  tnth t i     : the i'th component of t, where i : 'I_n.                 
  [tnth t i]   : the i'th component of t, where i : nat.                  
  thead t      : the first element of t, when n is canonically positive.  
Most seq constructors (behead, cat, belast, take, drop, rot, map, ...)    
can be used to build tuples via the [tuple of s] construct.               
  Tuples are actually a subType of seq, and inherit all combinatorial     
structures, including the finType structure.                              
  Some useful lemmas and definitions:                                     
    tuple0 : [tuple] is the only 0.-tuple                                 
    tupleP : elimination view for n.+1.-tuple                             
    ord_tuple n : the n.-tuple of all i : 'I_n                            

Section Def.

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

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

Canonical Structure tuple_subType :=
  Eval hnf in [subType for tval by tuple_of_rect].

Implicit Type t : tuple_of.

Definition tsize of tuple_of := n.

Lemma size_tuple : forall t, size t = n.

Lemma tnth_default : forall t (i : 'I_n), T.

Definition tnth t i := nth (tnth_default t i) t i.

Lemma tnth_nth : forall x t i, tnth t i = nth x t i.

Lemma map_tnth_enum : forall t, map (tnth t) (enum 'I_n) = t.

Lemma eq_from_tnth : forall t1 t2, tnth t1 =1 tnth t2 -> t1 = t2.

Definition tuple t mkT : tuple_of :=
  mkT (let: Tuple _ tP := t return size t == n in tP).

Lemma tupleE : forall t, tuple (fun sP => @Tuple t sP) = t.

End Def.

Notation "n .-tuple" := (tuple_of n)
  (at level 2, format "n .-tuple") : type_scope.

Notation "{ 'tuple' n 'of' T }" := (n.-tuple T : predArgType)
  (at level 0, only parsing) : form_scope.

Notation "[ 'tuple' 'of' s ]" := (tuple (fun sP => @Tuple _ _ s sP))
  (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.

Canonical Structure nil_tuple T :=
   Tuple (erefl _ : @size T [::] == 0).
Canonical Structure cons_tuple n T x (t : n.-tuple T) :=
   Tuple (valP t : size (x :: t) == n.+1).

Notation "[ 'tuple' x1 ; .. ; xn ]" := [tuple of x1 :: ..

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

Section SeqTuple.

Variables (n : nat) (T rT : Type).
Notation tT := (n.-tuple T).

Lemma nseq_tupleP : forall x : T, size (nseq n x) == n.
Canonical Structure nseq_tuple x := Tuple (nseq_tupleP x).

Lemma iota_tupleP : forall m, size (iota m n) == n.
Canonical Structure iota_tuple m := Tuple (iota_tupleP m).

Lemma behead_tupleP : forall t : tT, size (behead t) == n.-1.
Canonical Structure behead_tuple t := Tuple (behead_tupleP t).

Lemma belast_tupleP : forall x (t : tT), size (belast x t) == n.
Canonical Structure belast_tuple x t := Tuple (belast_tupleP x t).

Lemma cat_tupleP : forall n1 n2 (t1 : n1.-tuple T) (t2 : n2.-tuple T),
  size (t1 ++ t2) == n1 + n2.
Canonical Structure cat_tuple n1 n2 t1 t2 := Tuple (@cat_tupleP n1 n2 t1 t2).

Lemma take_tupleP : forall m (t : tT), size (take m t) == minn m n.
Canonical Structure take_tuple m t := Tuple (take_tupleP m t).

Lemma drop_tupleP : forall m (t : tT), size (drop m t) == n - m.
Canonical Structure drop_tuple m t := Tuple (drop_tupleP m t).

Lemma rev_tupleP : forall t : tT, size (rev t) == n.
Canonical Structure rev_tuple t := Tuple (rev_tupleP t).

Lemma rot_tupleP : forall m (t : tT), size (rot m t) == n.
Canonical Structure rot_tuple m t := Tuple (rot_tupleP m t).

Lemma rotr_tupleP : forall m (t : tT), size (rotr m t) == n.
Canonical Structure rotr_tuple m t := Tuple (rotr_tupleP m t).

Lemma map_tupleP : forall f (t : tT), @size rT (map f t) == n.
Canonical Structure map_tuple f t := Tuple (map_tupleP f t).

Lemma scanl_tupleP : forall f x (t : tT), @size rT (scanl f x t) == n.
Canonical Structure scanl_tuple f x t := Tuple (scanl_tupleP f x t).

Lemma pairmap_tupleP : forall f x (t : tT), @size rT (pairmap f x t) == n.
Canonical Structure pairmap_tuple f x t := Tuple (pairmap_tupleP f x t).

Lemma zip_tupleP : forall t1 t2 : tT, size (zip t1 t2) == n.
Canonical Structure zip_tuple t1 t2 := Tuple (zip_tupleP t1 t2).

Definition thead (n : pos_nat) (t : n.-tuple T) := tnth t ord0.

Lemma tnth0 : forall x n (t : n.-tuple T), tnth [tuple of x :: t] ord0 = x.

Lemma theadE : forall x n (t : n.-tuple T), thead [tuple of x :: t] = x.

Lemma tuple0 : forall t : 0.-tuple T, t = [tuple].

CoInductive tuple1_spec : n.+1.-tuple T -> Type :=
  Tuple1spec x (t : tT) : tuple1_spec [tuple of x :: t].

Lemma tupleP : forall t, tuple1_spec t.

Lemma tnth_map : forall f (t : tT) i,
  tnth [tuple of map f t] i = f (tnth t i) :> rT.

End SeqTuple.

Lemma tnth_behead : forall (n : pos_nat) T (t : n.+1.-tuple T) i,
  tnth [tuple of behead t] i = tnth t (inord i.+1).

Lemma tuple_eta : forall n T (t : n.+1.-tuple T),
  t = [tuple of thead t :: behead t].

Section EqTuple.

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

Definition tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple(T) by <:].
Canonical Structure tuple_eqType := Eval hnf in EqType tuple_eqMixin.

Canonical Structure tuple_predType :=
  Eval hnf in mkPredType (fun t : n.-tuple T => mem_seq t).

Lemma memtE : forall t : n.-tuple T, mem t = mem (tval t).

End EqTuple.

Definition tuple_choiceMixin n (T : choiceType) :=
  [choiceMixin of n.-tuple(T) by <:].

Canonical Structure tuple_choiceType n T :=
  Eval hnf in ChoiceType (tuple_choiceMixin n T).

Definition tuple_countMixin n (T : countType) :=
  [countMixin of n.-tuple(T) by <:].

Canonical Structure tuple_countType n T :=
  Eval hnf in CountType (tuple_countMixin n T).

Canonical Structure tuple_subCountType n (T : countType) :=
  Eval hnf in [subCountType of n.-tuple(T)].

Module Type FinTupleSig.
Section FinTupleSig.
Variables (n : nat) (T : finType).
Parameter enum : seq (n.-tuple T).
Axiom enumP : Finite.axiom enum.
Axiom size_enum : size enum = #|T| ^ n.
End FinTupleSig.
End FinTupleSig.

Module FinTuple : FinTupleSig.
Section FinTuple.
Variables (n : nat) (T : finType).

Definition enum : seq (n.-tuple(T)) :=
  let extend e := flatten (map (fun x => map (cons x) e) (Finite.enum T)) in
  pmap insub (iter n extend [::[::]]).

Lemma enumP : Finite.axiom enum.

Lemma size_enum : size enum = #|T| ^ n.

End FinTuple.
End FinTuple.

Section UseFinTuple.

Variables (n : nat) (T : finType).
Notation tT := (n.-tuple T).

Canonical Structure tuple_finMixin := FinMixin (@FinTuple.enumP n T).
Canonical Structure tuple_finType := Eval hnf in FinType tuple_finMixin.
Canonical Structure tuple_subFinType := Eval hnf in [subFinType of tT].

Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.

Lemma enum_tupleP : forall A : pred T, size (enum A) == #|A|.
Canonical Structure enum_tuple A := Tuple (enum_tupleP A).

Definition ord_tuple : n.-tuple 'I_n := Tuple (introT eqP (size_enum_ord n)).
Lemma val_ord_tuple : val ord_tuple = enum 'I_n. Qed.

Lemma tuple_map_ord : forall T' (t : n.-tuple T'),
  t = [tuple of map (tnth t) ord_tuple].

End UseFinTuple.