Library mathcomp.ssreflect.tuple
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+Set Implicit Arguments.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+Set Implicit Arguments.
+ +
+
+ Tuples, i.e., sequences 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.
+ The size of s must be known: specifically, Coq must
+ be able to infer a Canonical tuple projecting on s.
+ in_tuple s == the (size s)-tuple with value s.
+ [tuple] == the empty tuple.
+ [tuple x1; ..; xn] == the explicit n.-tuple <x1; ..; xn>.
+ [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound
+ in E).
+ tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n.
+ As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be
+ applied to t : n.-tuple T; we provide a few specialized instances when
+ 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 and i < n
+ is convertible to true.
+ thead t == the first element of t, when n is m.+1 for some m.
+ Most seq constructors (cons, behead, cat, rcons, 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 tuple_subType := Eval hnf in [subType for tval].
+ +
+Implicit Type t : tuple_of.
+ +
+Definition tsize of tuple_of := n.
+ +
+Lemma size_tuple t : size t = n.
+ +
+Lemma tnth_default t : 'I_n → T.
+ +
+Definition tnth t i := nth (tnth_default t i) t i.
+ +
+Lemma tnth_nth x t i : tnth t i = nth x t i.
+ +
+Lemma map_tnth_enum t : map (tnth t) (enum 'I_n) = t.
+ +
+Lemma eq_from_tnth 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 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 nil_tuple T := Tuple (isT : @size T [::] == 0).
+Canonical cons_tuple n T x (t : n.-tuple T) :=
+ Tuple (valP t : size (x :: t) == n.+1).
+ +
+Notation "[ 'tuple' x1 ; .. ; xn ]" := [tuple of x1 :: .. [:: xn] ..]
+ (at level 0, format "[ 'tuple' '[' x1 ; '/' .. ; '/' xn ']' ]")
+ : form_scope.
+ +
+Notation "[ 'tuple' ]" := [tuple of [::]]
+ (at level 0, format "[ 'tuple' ]") : form_scope.
+ +
+Section CastTuple.
+ +
+Variable T : Type.
+ +
+Definition in_tuple (s : seq T) := Tuple (eqxx (size s)).
+ +
+Definition tcast m n (eq_mn : m = n) t :=
+ let: erefl in _ = n := eq_mn return n.-tuple T in 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 tvalK n (t : n.-tuple T) : in_tuple t = tcast (esym (size_tuple t)) t.
+ +
+Lemma in_tupleE s : in_tuple s = s :> seq T.
+ +
+End CastTuple.
+ +
+Section SeqTuple.
+ +
+Variables (n m : nat) (T U rT : Type).
+Implicit Type t : n.-tuple T.
+ +
+Lemma rcons_tupleP t x : size (rcons t x) == n.+1.
+ Canonical rcons_tuple t x := Tuple (rcons_tupleP t x).
+ +
+Lemma nseq_tupleP x : @size T (nseq n x) == n.
+ Canonical nseq_tuple x := Tuple (nseq_tupleP x).
+ +
+Lemma iota_tupleP : size (iota m n) == n.
+ Canonical iota_tuple := Tuple iota_tupleP.
+ +
+Lemma behead_tupleP t : size (behead t) == n.-1.
+ Canonical behead_tuple t := Tuple (behead_tupleP t).
+ +
+Lemma belast_tupleP x t : size (belast x t) == n.
+ Canonical belast_tuple x t := Tuple (belast_tupleP x t).
+ +
+Lemma cat_tupleP t (u : m.-tuple T) : size (t ++ u) == n + m.
+ Canonical cat_tuple t u := Tuple (cat_tupleP t u).
+ +
+Lemma take_tupleP t : size (take m t) == minn m n.
+ Canonical take_tuple t := Tuple (take_tupleP t).
+ +
+Lemma drop_tupleP t : size (drop m t) == n - m.
+ Canonical drop_tuple t := Tuple (drop_tupleP t).
+ +
+Lemma rev_tupleP t : size (rev t) == n.
+ Canonical rev_tuple t := Tuple (rev_tupleP t).
+ +
+Lemma rot_tupleP t : size (rot m t) == n.
+ Canonical rot_tuple t := Tuple (rot_tupleP t).
+ +
+Lemma rotr_tupleP t : size (rotr m t) == n.
+ Canonical rotr_tuple t := Tuple (rotr_tupleP t).
+ +
+Lemma map_tupleP f t : @size rT (map f t) == n.
+ Canonical map_tuple f t := Tuple (map_tupleP f t).
+ +
+Lemma scanl_tupleP f x t : @size rT (scanl f x t) == n.
+ Canonical scanl_tuple f x t := Tuple (scanl_tupleP f x t).
+ +
+Lemma pairmap_tupleP f x t : @size rT (pairmap f x t) == n.
+ Canonical pairmap_tuple f x t := Tuple (pairmap_tupleP f x t).
+ +
+Lemma zip_tupleP t (u : n.-tuple U) : size (zip t u) == n.
+ Canonical zip_tuple t u := Tuple (zip_tupleP t u).
+ +
+Lemma allpairs_tupleP f t (u : m.-tuple U) : @size rT (allpairs f t u) == n × m.
+ Canonical allpairs_tuple f t u := Tuple (allpairs_tupleP f t u).
+ +
+Definition thead (u : n.+1.-tuple T) := tnth u ord0.
+ +
+Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x.
+ +
+Lemma theadE x t : thead [tuple of x :: t] = x.
+ +
+Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T).
+ +
+CoInductive tuple1_spec : n.+1.-tuple T → Type :=
+ Tuple1spec x t : tuple1_spec [tuple of x :: t].
+ +
+Lemma tupleP u : tuple1_spec u.
+ +
+Lemma tnth_map f t i : tnth [tuple of map f t] i = f (tnth t i) :> rT.
+ +
+End SeqTuple.
+ +
+Lemma tnth_behead n T (t : n.+1.-tuple T) i :
+ tnth [tuple of behead t] i = tnth t (inord i.+1).
+ +
+Lemma tuple_eta n T (t : n.+1.-tuple T) : t = [tuple of thead t :: behead t].
+ +
+Section TupleQuantifiers.
+ +
+Variables (n : nat) (T : Type).
+Implicit Types (a : pred T) (t : n.-tuple T).
+ +
+Lemma forallb_tnth a t : [∀ i, a (tnth t i)] = all a t.
+ +
+Lemma existsb_tnth a t : [∃ i, a (tnth t i)] = has a t.
+ +
+Lemma all_tnthP a t : reflect (∀ i, a (tnth t i)) (all a t).
+ +
+Lemma has_tnthP a t : reflect (∃ i, a (tnth t i)) (has a t).
+ +
+End TupleQuantifiers.
+ +
+ +
+Section EqTuple.
+ +
+Variables (n : nat) (T : eqType).
+ +
+Definition tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple T by <:].
+Canonical tuple_eqType := Eval hnf in EqType (n.-tuple T) tuple_eqMixin.
+ +
+Canonical tuple_predType :=
+ Eval hnf in mkPredType (fun t : n.-tuple T ⇒ mem_seq t).
+ +
+Lemma memtE (t : n.-tuple T) : mem t = mem (tval t).
+ +
+Lemma mem_tnth i (t : n.-tuple T) : tnth t i \in t.
+ +
+Lemma memt_nth x0 (t : n.-tuple T) i : i < n → nth x0 t i \in t.
+ +
+Lemma tnthP (t : n.-tuple T) x : reflect (∃ i, x = tnth t i) (x \in t).
+ +
+Lemma seq_tnthP (s : seq T) x : x \in s → {i | x = tnth (in_tuple s) i}.
+ +
+End EqTuple.
+ +
+Definition tuple_choiceMixin n (T : choiceType) :=
+ [choiceMixin of n.-tuple T by <:].
+ +
+Canonical tuple_choiceType n (T : choiceType) :=
+ Eval hnf in ChoiceType (n.-tuple T) (tuple_choiceMixin n T).
+ +
+Definition tuple_countMixin n (T : countType) :=
+ [countMixin of n.-tuple T by <:].
+ +
+Canonical tuple_countType n (T : countType) :=
+ Eval hnf in CountType (n.-tuple T) (tuple_countMixin n T).
+ +
+Canonical 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 (codom (fun x ⇒ map (cons x) e)) 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).
+ +
+Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
+Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
+Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].
+ +
+Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.
+ +
+Lemma enum_tupleP (A : pred T) : size (enum A) == #|A|.
+ Canonical 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.
+ +
+Lemma tuple_map_ord U (t : n.-tuple U) : t = [tuple of map (tnth t) ord_tuple].
+ +
+Lemma tnth_ord_tuple i : tnth ord_tuple i = i.
+ +
+Section ImageTuple.
+ +
+Variables (T' : Type) (f : T → T') (A : pred T).
+ +
+Canonical image_tuple : #|A|.-tuple T' := [tuple of image f A].
+Canonical codom_tuple : #|T|.-tuple T' := [tuple of codom f].
+ +
+End ImageTuple.
+ +
+Section MkTuple.
+ +
+Variables (T' : Type) (f : 'I_n → T').
+ +
+Definition mktuple := map_tuple f ord_tuple.
+ +
+Lemma tnth_mktuple i : tnth mktuple i = f i.
+ +
+Lemma nth_mktuple x0 (i : 'I_n) : nth x0 mktuple i = f i.
+ +
+End MkTuple.
+ +
+End UseFinTuple.
+ +
+Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n ⇒ F))
+ (at level 0, i at level 0,
+ format "[ '[hv' 'tuple' F '/' | i < n ] ']'") : form_scope.
+ +
+
++Section Def.
+ +
+Variables (n : nat) (T : Type).
+ +
+Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
+ +
+Canonical tuple_subType := Eval hnf in [subType for tval].
+ +
+Implicit Type t : tuple_of.
+ +
+Definition tsize of tuple_of := n.
+ +
+Lemma size_tuple t : size t = n.
+ +
+Lemma tnth_default t : 'I_n → T.
+ +
+Definition tnth t i := nth (tnth_default t i) t i.
+ +
+Lemma tnth_nth x t i : tnth t i = nth x t i.
+ +
+Lemma map_tnth_enum t : map (tnth t) (enum 'I_n) = t.
+ +
+Lemma eq_from_tnth 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 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 nil_tuple T := Tuple (isT : @size T [::] == 0).
+Canonical cons_tuple n T x (t : n.-tuple T) :=
+ Tuple (valP t : size (x :: t) == n.+1).
+ +
+Notation "[ 'tuple' x1 ; .. ; xn ]" := [tuple of x1 :: .. [:: xn] ..]
+ (at level 0, format "[ 'tuple' '[' x1 ; '/' .. ; '/' xn ']' ]")
+ : form_scope.
+ +
+Notation "[ 'tuple' ]" := [tuple of [::]]
+ (at level 0, format "[ 'tuple' ]") : form_scope.
+ +
+Section CastTuple.
+ +
+Variable T : Type.
+ +
+Definition in_tuple (s : seq T) := Tuple (eqxx (size s)).
+ +
+Definition tcast m n (eq_mn : m = n) t :=
+ let: erefl in _ = n := eq_mn return n.-tuple T in 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 tvalK n (t : n.-tuple T) : in_tuple t = tcast (esym (size_tuple t)) t.
+ +
+Lemma in_tupleE s : in_tuple s = s :> seq T.
+ +
+End CastTuple.
+ +
+Section SeqTuple.
+ +
+Variables (n m : nat) (T U rT : Type).
+Implicit Type t : n.-tuple T.
+ +
+Lemma rcons_tupleP t x : size (rcons t x) == n.+1.
+ Canonical rcons_tuple t x := Tuple (rcons_tupleP t x).
+ +
+Lemma nseq_tupleP x : @size T (nseq n x) == n.
+ Canonical nseq_tuple x := Tuple (nseq_tupleP x).
+ +
+Lemma iota_tupleP : size (iota m n) == n.
+ Canonical iota_tuple := Tuple iota_tupleP.
+ +
+Lemma behead_tupleP t : size (behead t) == n.-1.
+ Canonical behead_tuple t := Tuple (behead_tupleP t).
+ +
+Lemma belast_tupleP x t : size (belast x t) == n.
+ Canonical belast_tuple x t := Tuple (belast_tupleP x t).
+ +
+Lemma cat_tupleP t (u : m.-tuple T) : size (t ++ u) == n + m.
+ Canonical cat_tuple t u := Tuple (cat_tupleP t u).
+ +
+Lemma take_tupleP t : size (take m t) == minn m n.
+ Canonical take_tuple t := Tuple (take_tupleP t).
+ +
+Lemma drop_tupleP t : size (drop m t) == n - m.
+ Canonical drop_tuple t := Tuple (drop_tupleP t).
+ +
+Lemma rev_tupleP t : size (rev t) == n.
+ Canonical rev_tuple t := Tuple (rev_tupleP t).
+ +
+Lemma rot_tupleP t : size (rot m t) == n.
+ Canonical rot_tuple t := Tuple (rot_tupleP t).
+ +
+Lemma rotr_tupleP t : size (rotr m t) == n.
+ Canonical rotr_tuple t := Tuple (rotr_tupleP t).
+ +
+Lemma map_tupleP f t : @size rT (map f t) == n.
+ Canonical map_tuple f t := Tuple (map_tupleP f t).
+ +
+Lemma scanl_tupleP f x t : @size rT (scanl f x t) == n.
+ Canonical scanl_tuple f x t := Tuple (scanl_tupleP f x t).
+ +
+Lemma pairmap_tupleP f x t : @size rT (pairmap f x t) == n.
+ Canonical pairmap_tuple f x t := Tuple (pairmap_tupleP f x t).
+ +
+Lemma zip_tupleP t (u : n.-tuple U) : size (zip t u) == n.
+ Canonical zip_tuple t u := Tuple (zip_tupleP t u).
+ +
+Lemma allpairs_tupleP f t (u : m.-tuple U) : @size rT (allpairs f t u) == n × m.
+ Canonical allpairs_tuple f t u := Tuple (allpairs_tupleP f t u).
+ +
+Definition thead (u : n.+1.-tuple T) := tnth u ord0.
+ +
+Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x.
+ +
+Lemma theadE x t : thead [tuple of x :: t] = x.
+ +
+Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T).
+ +
+CoInductive tuple1_spec : n.+1.-tuple T → Type :=
+ Tuple1spec x t : tuple1_spec [tuple of x :: t].
+ +
+Lemma tupleP u : tuple1_spec u.
+ +
+Lemma tnth_map f t i : tnth [tuple of map f t] i = f (tnth t i) :> rT.
+ +
+End SeqTuple.
+ +
+Lemma tnth_behead n T (t : n.+1.-tuple T) i :
+ tnth [tuple of behead t] i = tnth t (inord i.+1).
+ +
+Lemma tuple_eta n T (t : n.+1.-tuple T) : t = [tuple of thead t :: behead t].
+ +
+Section TupleQuantifiers.
+ +
+Variables (n : nat) (T : Type).
+Implicit Types (a : pred T) (t : n.-tuple T).
+ +
+Lemma forallb_tnth a t : [∀ i, a (tnth t i)] = all a t.
+ +
+Lemma existsb_tnth a t : [∃ i, a (tnth t i)] = has a t.
+ +
+Lemma all_tnthP a t : reflect (∀ i, a (tnth t i)) (all a t).
+ +
+Lemma has_tnthP a t : reflect (∃ i, a (tnth t i)) (has a t).
+ +
+End TupleQuantifiers.
+ +
+ +
+Section EqTuple.
+ +
+Variables (n : nat) (T : eqType).
+ +
+Definition tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple T by <:].
+Canonical tuple_eqType := Eval hnf in EqType (n.-tuple T) tuple_eqMixin.
+ +
+Canonical tuple_predType :=
+ Eval hnf in mkPredType (fun t : n.-tuple T ⇒ mem_seq t).
+ +
+Lemma memtE (t : n.-tuple T) : mem t = mem (tval t).
+ +
+Lemma mem_tnth i (t : n.-tuple T) : tnth t i \in t.
+ +
+Lemma memt_nth x0 (t : n.-tuple T) i : i < n → nth x0 t i \in t.
+ +
+Lemma tnthP (t : n.-tuple T) x : reflect (∃ i, x = tnth t i) (x \in t).
+ +
+Lemma seq_tnthP (s : seq T) x : x \in s → {i | x = tnth (in_tuple s) i}.
+ +
+End EqTuple.
+ +
+Definition tuple_choiceMixin n (T : choiceType) :=
+ [choiceMixin of n.-tuple T by <:].
+ +
+Canonical tuple_choiceType n (T : choiceType) :=
+ Eval hnf in ChoiceType (n.-tuple T) (tuple_choiceMixin n T).
+ +
+Definition tuple_countMixin n (T : countType) :=
+ [countMixin of n.-tuple T by <:].
+ +
+Canonical tuple_countType n (T : countType) :=
+ Eval hnf in CountType (n.-tuple T) (tuple_countMixin n T).
+ +
+Canonical 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 (codom (fun x ⇒ map (cons x) e)) 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).
+ +
+Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
+Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
+Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].
+ +
+Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.
+ +
+Lemma enum_tupleP (A : pred T) : size (enum A) == #|A|.
+ Canonical 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.
+ +
+Lemma tuple_map_ord U (t : n.-tuple U) : t = [tuple of map (tnth t) ord_tuple].
+ +
+Lemma tnth_ord_tuple i : tnth ord_tuple i = i.
+ +
+Section ImageTuple.
+ +
+Variables (T' : Type) (f : T → T') (A : pred T).
+ +
+Canonical image_tuple : #|A|.-tuple T' := [tuple of image f A].
+Canonical codom_tuple : #|T|.-tuple T' := [tuple of codom f].
+ +
+End ImageTuple.
+ +
+Section MkTuple.
+ +
+Variables (T' : Type) (f : 'I_n → T').
+ +
+Definition mktuple := map_tuple f ord_tuple.
+ +
+Lemma tnth_mktuple i : tnth mktuple i = f i.
+ +
+Lemma nth_mktuple x0 (i : 'I_n) : nth x0 mktuple i = f i.
+ +
+End MkTuple.
+ +
+End UseFinTuple.
+ +
+Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n ⇒ F))
+ (at level 0, i at level 0,
+ format "[ '[hv' 'tuple' F '/' | i < n ] ']'") : form_scope.
+ +
+