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 *)
```

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.

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?

I had thought `Set`

could fit comfortably in places where a `Type`

was expected.

I mean, I know that there are type universes. And that `Set : Type1 : Type2 ....`

, but maybe I'm missing something related to that?

a `Set`

can be used as a type; not so for `list Set`

, but `[nat ; nat : Type]`

might already be enough

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`

.

You need to be more explicit. Instead of writing `[nat;nat]`

, you need to write `@cons Type nat (@cons Type nat nil)`

.

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

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

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]).
*)
```

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.

[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]

you can do `[nat:Type; nat:Type]`

or you can do `Arguments cons {_} & _ _`

Last updated: Jun 15 2024 at 05:01 UTC