Stream: Coq users

Topic: Project nth element of n-tuple


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

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

view this post on Zulip Julin S (Oct 13 2022 at 03:57):

Thanks.

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

view this post on Zulip Julin S (Oct 13 2022 at 04:03):

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

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

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

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

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

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

view this post on Zulip Julin S (Oct 13 2022 at 05:33):

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

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

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

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

view this post on Zulip Gaƫtan Gilbert (Oct 13 2022 at 08:41):

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


Last updated: Jan 28 2023 at 05:02 UTC