Stream: Coq users

Topic: Problems with some tiny function


view this post on Zulip 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'?

view this post on Zulip 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.

view this post on Zulip Lessness (Jul 03 2021 at 16:32):

Thank you!


Last updated: Feb 01 2023 at 11:04 UTC