```
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'`

?

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

Thank you!

Last updated: Jun 24 2024 at 12:02 UTC