## Stream: Coq users

### Topic: Project nth element of n-tuple

#### Julin S (Oct 12 2022 at 13:30):

Is there a way to project the nth element of an n-tuple in coq?

Something like:

``````Fixpoint nth_tup {A B:Type} (x:A*B) (n:nat) :=
match n with
| O => fst x
| S n'=> nth_tup (snd x) n'
end.
(* this won't type check, though *)
``````

To behave like:

``````Compute nth_tup (10,20,30,40) 0.  (* 10 *)
Compute nth_tup (10,20,30,40) 1.  (* 20 *)
Compute nth_tup (10,20,30,40) 2.  (* 30 *)
Compute nth_tup (10,20,30,40) 3.  (* 40 *)
``````

#### Guillaume Melquiond (Oct 12 2022 at 14:31):

Sure, but writing the `match with` properly is a bit tedious, so it is better to go through the proof mode.

``````Definition nth_tup {l : list Type} (x : fold_right prod unit l) (n : nat) : nth n l unit.
Proof.
revert x n.
induction l as [|t l IH].
- intros _ [|] ; exact tt.
- intros [a b] [|n].
exact a.
now apply IH.
Defined.
``````

You will have to replace `fold_right` by a custom function if you do not want the tuples to systematically end with `unit` and if you want them to have the intuitive associativity. But the idea is the same.

Thanks.

#### Julin S (Oct 13 2022 at 04:02):

This worked when all tuple elements are in `Type`. Like:

``````Inductive Foo : Type := cfoo: forall (n:nat), Type -> Foo.

Compute @nth_tup [Foo] (cfoo 3 nat, tt) 0.
(*
= cfoo 3 nat
: nth 0 (cons Foo nil) unit
*)
``````

But got error when I tried to make a tuple like `(1,2)` with

``````Check @nth_tup [nat;nat] (1,2,tt).
(*
The term "cons nat (cons nat nil)" has type "list Set"
while it is expected to have type "list Type"
(universe inconsistency: Cannot enforce Set = nth_tup.u0).
*)
``````

What does this error mean? And how can it be fixed?

#### Julin S (Oct 13 2022 at 04:03):

I had thought `Set` could fit comfortably in places where a `Type` was expected.

#### Julin S (Oct 13 2022 at 04:13):

I mean, I know that there are type universes. And that `Set : Type1 : Type2 ....`, but maybe I'm missing something related to that?

#### Paolo Giarrusso (Oct 13 2022 at 04:31):

a `Set` can be used as a type; not so for `list Set`, but `[nat ; nat : Type]` might already be enough

#### Julin S (Oct 13 2022 at 04:35):

Neither of these worked either:

``````Check @nth_tup ([nat;nat]:list Type) (3,4,tt).
Check @nth_tup [nat;nat:Type] (3,4,tt).
``````

Okay so roughly saying, `list Set` and `list Type` aren't compatible like `Set` and `Type`.

#### Guillaume Melquiond (Oct 13 2022 at 05:08):

You need to be more explicit. Instead of writing `[nat;nat]`, you need to write `@cons Type nat (@cons Type nat nil)`.

#### Julin S (Oct 13 2022 at 05:32):

Would it be possible to have a coercion that can make Set values to Type on the fly?

#### Julin S (Oct 13 2022 at 05:33):

And if that is possible, how bad/good an idea would it be?

#### Julin S (Oct 13 2022 at 05:38):

Tried something but it gave error:

``````Definition set_in_type (s:Set) := s:Type.
Coercion set_in_type : Set >-> Type.
(*
Syntax error: [class_rawexpr] expected after ':' (in [gallina_ext]).
*)
``````

#### Guillaume Melquiond (Oct 13 2022 at 06:14):

A coercion from `Set` to `Type` is pointless, because types from `Set` already fit into `Type`. What you need is a coercion from `list Set` to `list Type`, but this cannot be make to work, because it would be a coercion `list >-> list`. Thus, the only proper solution is to improve Coq's pretyping algorithm, so that `@cons _ A` gets inferred as `@cons Type A` when needed.

#### Pierre Roux (Oct 13 2022 at 07:46):

[off topic]That being said, having a way to make `List.map f` a coercion from `list A` to `list B` whenever `f` is a coercion from `A` to `B` would be nice.[/off topic]

#### Gaëtan Gilbert (Oct 13 2022 at 08:41):

you can do `[nat:Type; nat:Type]`
or you can do `Arguments cons {_} & _ _`

Last updated: Jun 15 2024 at 05:01 UTC