## Stream: Coq users

### Topic: Problems with some tiny function

#### Lessness (Jul 03 2021 at 16:15):

``````Fixpoint tuple (n: nat) :=
match n with
| O => R
| S m => prod R (tuple m)
end.

Definition tuple_head {n: nat} (t: tuple n): R.
Proof.
destruct n.
+ exact t.
+ destruct t as [x t]. exact x.
Defined.

Definition tuple_tail {n: nat} (t: tuple (S n)): tuple n.
Proof.
destruct t as [x t]. exact t.
Defined.

Fixpoint nth_of_tuple (n i: nat) (t: tuple n): option R :=
match n, i with
| _, O => Some (tuple_head t)
| O, _ => None
| S n', S i' => Some (nth_of_tuple n' i' (tuple_tail t))
end.
``````

Function `nth_of_tuple` causes error: `The term "t" has type "tuple n" while it is expected to have type "tuple (S ?n)"`.
How to convince it that `t` has type `tuple (S n')` too, as `n` is equal to `S n'`?

#### Kenji Maillard (Jul 03 2021 at 16:22):

The solution is to use dependent pattern matching and keep `tuple n` in the return type of the match:

``````Fixpoint nth_of_tuple (n i: nat) : forall (t: tuple n), option R :=
match n, i with
| _, O => fun t => Some (tuple_head t)
| O, _ => fun t => None
| S n', S i' => fun t => nth_of_tuple n' i' (tuple_tail t)
end.
``````

#### Lessness (Jul 03 2021 at 16:32):

Thank you!

Last updated: Sep 28 2023 at 10:01 UTC