Project nth element of n-tuple · Coq users

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

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.

Julin S (Oct 13 2022 at 03:57):

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

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

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

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):

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):

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

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]

Stream: Coq users

Topic: Project nth element of n-tuple

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