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: Feb 01 2023 at 11:04 UTC