Basic tuples in Coq

tuple.v

Require Import Vector.
Import VectorNotations.
Set Implicit Arguments.

Inductive tuple : forall {n : nat}, Vector.t Set n -> Type :=
| unit : tuple []
| push : forall {T : Set} (x : T)
           {n : nat} {ts : Vector.t Set n},
           tuple ts -> tuple (T :: ts).

Check unit.
Check push true unit.
Check push 5 (push true unit).

Module TupleNotations.
  Notation "(| |)" := unit (format "(| |)") : tuple_scope.
  Notation "(| x |)" := (push x unit) : tuple_scope.
  Notation "(| x1 , .. , xn |)" :=
    (push x1 .. (push xn unit) .. ) : tuple_scope.
End TupleNotations.

Import TupleNotations.

Open Scope tuple_scope.

Example unitTupleNotation: (||) = unit.
Proof. reflexivity. Qed.
Example oneElementTupleNotation: (| false |) = push false unit.
Proof. reflexivity. Qed.
Example manyElementTupleNotation: (| 5, true |) = push 5 (push true unit).
Proof. reflexivity. Qed.


Definition length : forall {n:nat} {ts:Vector.t Set n}, tuple ts -> nat :=
  fun n _ _ => n.

Example lengthOfUnitIsZero: length (||) = 0.
Proof. reflexivity. Qed.
Example lengthOfTwoElementTupleIsTwo: length (| 5, true |) = 2.
Proof. reflexivity. Qed.

Definition typeSig : forall {n:nat} {ts:Vector.t Set n},
                       tuple ts -> Vector.t Set n :=
  fun _ ts _ => ts.

Example complexTypeSig: typeSig (|true, Some false, 5|) =
                        [bool; option bool; nat].
Proof. reflexivity. Qed.



Close Scope tuple_scope.

do these not come built in?