Library mathcomp.ssreflect.tuple

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
From mathcomp Require Import seq choice fintype path.

Set Implicit Arguments.

This file defines tuples, i.e., sequences with a fixed (known) length, and sequences with bounded length. For tuples 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 For bounded sequences we define: n.-bseq T == the type of bounded sequences of elements of type T, the length of a bounded sequence is smaller or or equal to n [bseq of s] == the bounded sequence whose underlying value is s The size of s must be known. in_bseq s == the (size s).-bseq with value s [bseq] == the empty bseq insub_bseq n s == the n.-bseq of value s if size s <= n, else [bseq] [bseq x1; ..; xn] == the explicit n.-bseq <x1; ..; xn> cast_bseq Emn t == the m.-bseq t cast as an n.-tuple using Emn : m = n widen_bseq Lmn t == the m.-bseq t cast as an n.-tuple using Lmn : m <= n Most seq constructors (cons, behead, cat, rcons, belast, take, drop, rot, rotr, map, ...) can be used to build tuples and bounded sequences via the [tuple of s] and [bseq of s] constructs respectively. Tuples and bounded sequences are actually instances of subType of seq, and inherit all combinatorial structures, including the finType structure. Some useful lemmas and definitions: tuple0 : [tuple] is the only 0.-tuple bseq0 : [bseq] is the only 0.-bseq tupleP : elimination view for n.+1.-tuple ord_tuple n : the n.-tuple of all i : 'I_n

Section TupleDef.

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

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

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 TupleDef.

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) : type_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 val_tcast m n (eq_mn : m = n) (t : m .-tuple T) :
  tcast eq_mn t = t :> seq 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).

Lemma sort_tupleP r t : size (sort r t) == n.
Canonical sort_tuple r t := Tuple (sort_tupleP r t).

Definition thead (u : n .+1 .-tuple T) := tnth u ord0.

Lemma tnth0 x t : tnth [tuple of x :: t ] ord0 = x.

Lemma tnthS x t i : tnth [tuple of x :: t ] (lift ord0 i) = tnth t i.

Lemma theadE x t : thead [tuple of x :: t ] = x.

Lemma tuple0 : all_equal_to ([tuple ] : 0.-tuple T).

Variant 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.

Lemma tnth_nseq x i : tnth [tuple of nseq n x ] i = x.

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.

Arguments all_tnthP {n T a t}.
Arguments has_tnthP {n T a t}.

Section EqTuple.

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

Canonical tuple_predType := PredType (pred_of_seq : n .-tuple T → pred T).

Lemma eqEtuple (t1 t2 : n .-tuple T) :
  (t1 == t2 ) = [∀ i , tnth t1 i == tnth t2 i ].

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 }.

Lemma tuple_uniqP (t : n .-tuple T) : reflect (injective (tnth t)) (uniq t).

End EqTuple.

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).

tuple_finMixin could, in principle, be made Canonical to allow for folding Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), but in practice it will not work because the mixin_enum projector has been buried under an opaque alias, to avoid some performance issues during type inference.

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.

Lemma eq_mktuple T' (f1 f2 : 'I_n → T') :
  f1 =1 f2 → mktuple f1 = mktuple f2.

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.

Arguments eq_mktuple {n T'} [f1] f2 eq_f12.

Section BseqDef.

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

Structure bseq_of : Type := Bseq {bseqval :> seq T; _ : size bseqval ≤ n}.

Implicit Type bs : bseq_of.

Lemma size_bseq bs : size bs ≤ n.

Definition bseq bs mkB : bseq_of :=
  mkB (let: Bseq _ bsP := bs return size bs ≤ n in bsP).

Lemma bseqE bs : bseq (fun sP ⇒ @Bseq bs sP) = bs.

End BseqDef.

Canonical nil_bseq n T := Bseq (isT : @size T [::] ≤ n).
Canonical cons_bseq n T x (t : bseq_of n T) :=
  Bseq (valP t : size (x :: t) ≤ n .+1).

Notation "n .-bseq" := (bseq_of n)
  (at level 2, format "n .-bseq") : type_scope.

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

Notation "[ 'bseq' 'of' s ]" := (bseq (fun sP ⇒ @Bseq _ _ s sP))
  (at level 0, format "[ 'bseq' 'of' s ]") : form_scope.

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

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

Coercion bseq_of_tuple n T (t : n .-tuple T) : n .-bseq T :=
  Bseq (eq_leq (size_tuple t)).

Definition insub_bseq n T (s : seq T) : n .-bseq T := insubd [bseq ] s.

Lemma size_insub_bseq n T (s : seq T) : size (insub_bseq n s) ≤ size s.

Section CastBseq.

Variable T : Type.

Definition in_bseq (s : seq T) : (size s ).-bseq T := Bseq (leqnn (size s)).

Definition cast_bseq m n (eq_mn : m = n) bs :=
  let: erefl in _ = n := eq_mn return n .-bseq T in bs.

Definition widen_bseq m n (lemn : m ≤ n) (bs : m .-bseq T) : n .-bseq T :=
  @Bseq n T bs (leq_trans (size_bseq bs) lemn).

Lemma cast_bseq_id n (eq_nn : n = n) bs : cast_bseq eq_nn bs = bs.

Lemma cast_bseqK m n (eq_mn : m = n) :
  cancel (cast_bseq eq_mn) (cast_bseq (esym eq_mn)).

Lemma cast_bseqKV m n (eq_mn : m = n) :
  cancel (cast_bseq (esym eq_mn)) (cast_bseq eq_mn).

Lemma cast_bseq_trans m n p (eq_mn : m = n) (eq_np : n = p) bs :
  cast_bseq (etrans eq_mn eq_np) bs = cast_bseq eq_np (cast_bseq eq_mn bs).

Lemma size_cast_bseq m n (eq_mn : m = n) (bs : m .-bseq T) :
  size (cast_bseq eq_mn bs) = size bs.

Lemma widen_bseq_id n (lenn : n ≤ n) (bs : n .-bseq T) :
  widen_bseq lenn bs = bs.

Lemma cast_bseqEwiden m n (eq_mn : m = n) (bs : m .-bseq T) :
  cast_bseq eq_mn bs = widen_bseq (eq_leq eq_mn) bs.

Lemma widen_bseqK m n (lemn : m ≤ n) (lenm : n ≤ m) :
   cancel (@widen_bseq m n lemn) (widen_bseq lenm).

Lemma widen_bseq_trans m n p (lemn : m ≤ n) (lenp : n ≤ p) (bs : m .-bseq T) :
  widen_bseq (leq_trans lemn lenp) bs = widen_bseq lenp (widen_bseq lemn bs).

Lemma size_widen_bseq m n (lemn : m ≤ n) (bs : m .-bseq T) :
  size (widen_bseq lemn bs) = size bs.

Lemma in_bseqE s : in_bseq s = s :> seq T.

Lemma widen_bseq_in_bseq n (bs : n .-bseq T) :
  widen_bseq (size_bseq bs) (in_bseq bs) = bs.

End CastBseq.

Section SeqBseq.

Variables (n m : nat) (T U rT : Type).
Implicit Type s : n .-bseq T.

Lemma rcons_bseqP s x : size (rcons s x) ≤ n .+1.
Canonical rcons_bseq s x := Bseq (rcons_bseqP s x).

Lemma behead_bseqP s : size (behead s) ≤ n .-1.
Canonical behead_bseq s := Bseq (behead_bseqP s).

Lemma belast_bseqP x s : size (belast x s) ≤ n.
Canonical belast_bseq x s := Bseq (belast_bseqP x s).

Lemma cat_bseqP s (s' : m .-bseq T) : size (s ++ s') ≤ n + m.
Canonical cat_bseq s (s' : m .-bseq T) := Bseq (cat_bseqP s s').

Lemma take_bseqP s : size (take m s) ≤ n.
Canonical take_bseq s := Bseq (take_bseqP s).

Lemma drop_bseqP s : size (drop m s) ≤ n - m.
Canonical drop_bseq s := Bseq (drop_bseqP s).

Lemma rev_bseqP s : size (rev s) ≤ n.
Canonical rev_bseq s := Bseq (rev_bseqP s).

Lemma rot_bseqP s : size (rot m s) ≤ n.
Canonical rot_bseq s := Bseq (rot_bseqP s).

Lemma rotr_bseqP s : size (rotr m s) ≤ n.
Canonical rotr_bseq s := Bseq (rotr_bseqP s).

Lemma map_bseqP f s : @size rT (map f s) ≤ n.
Canonical map_bseq f s := Bseq (map_bseqP f s).

Lemma scanl_bseqP f x s : @size rT (scanl f x s) ≤ n.
Canonical scanl_bseq f x s := Bseq (scanl_bseqP f x s).

Lemma pairmap_bseqP f x s : @size rT (pairmap f x s) ≤ n.
Canonical pairmap_bseq f x s := Bseq (pairmap_bseqP f x s).

Lemma allpairs_bseqP f s (s' : m .-bseq U) : @size rT (allpairs f s s') ≤ n × m.
Canonical allpairs_bseq f s (s' : m .-bseq U) := Bseq (allpairs_bseqP f s s').

Lemma sort_bseqP r s : size (sort r s) ≤ n.
Canonical sort_bseq r s := Bseq (sort_bseqP r s).

Lemma bseq0 : all_equal_to ([bseq ] : 0.-bseq T).

End SeqBseq.

Canonical bseq_predType n (T : eqType) :=
  Eval hnf in PredType (fun t : n .-bseq T ⇒ mem_seq t).

Lemma membsE n (T : eqType) (bs : n .-bseq T) : mem bs = mem (bseqval bs).

Definition bseq_tagged_tuple n T (s : n .-bseq T) : {k : 'I_n .+1 & k .-tuple T } :=
  Tagged _ (in_tuple s : (Ordinal (size_bseq s : size s < n .+1)).-tuple _).
Arguments bseq_tagged_tuple {n T}.

Definition tagged_tuple_bseq n T (t : {k : 'I_n .+1 & k .-tuple T }) : n .-bseq T :=
  widen_bseq (leq_ord (tag t)) (tagged t).
Arguments tagged_tuple_bseq {n T}.

Lemma bseq_tagged_tupleK {n T} :
  cancel (@bseq_tagged_tuple n T) tagged_tuple_bseq.

Lemma tagged_tuple_bseqK {n T} :
  cancel (@tagged_tuple_bseq n T) bseq_tagged_tuple.

Lemma bseq_tagged_tuple_bij {n T} : bijective (@bseq_tagged_tuple n T).

Lemma tagged_tuple_bseq_bij {n T} : bijective (@tagged_tuple_bseq n T).

#[global] Hint Resolve bseq_tagged_tuple_bij tagged_tuple_bseq_bij : core.

#[non_forgetful_inheritance]
HB.instance Definition _ n (T : finType) := isFinite.Build (n .-bseq T)
  (pcan_enumP (can_pcan (@bseq_tagged_tupleK n T))).