Stream: Coq users

Topic: List restricted to some types

Julin S (Apr 20 2022 at 04:51):

I was trying to make a form of list restricted to just nat and bool.

So I did:

Inductive type : Type :=
| Int
| Bool.

Definition typeDenote (t:type) : Type :=
  match t with
  | Int => nat
  | Bool => bool
  end.

Inductive listmod (A:type) : Type :=
| mnil : listmod A
| mcons : (typeDenote A) -> listmod A -> listmod A.
Arguments mnil {A}.
Arguments mcons {A}.

It works okay if I try this without the implicit arguments of mcons:

Check @mcons Int 3 mnil.
(*
mcons 3 mnil
     : listmod Int
*)

Check mnil.
(*
mnil
     : listmod ?A
where
?A : [ |- type]
*)

but gives error upon actually having the type argument implicitly:

Check mcons 3 mnil.
(*
The term "3" has type "nat" while it is expected to have type
 "typeDenote ?A".
*)

Why is this happening? And how can we get around this?

Guillaume Melquiond (Apr 20 2022 at 07:00):

Presumably, you need bidirectional typing. Adding something like Arguments mcons {A} & h t should help.

Guillaume Melquiond (Apr 20 2022 at 07:04):

That said, this might not even be sufficient, since Coq still needs to invert typeDenote, which bidirectional typing does not help with.

Michael Soegtrop (Apr 20 2022 at 07:04):

I don't think that this will help. Imagine what would happen if type would have Int1 and Int2 and typeDenote would map both to nat-

Michael Soegtrop (Apr 20 2022 at 07:06):

But I find the error message rather strange. I would expect to get an error that Coq can't derive the implicit argument of mcons and mnil. What seems to be happening is that Coq silently denies to make the argument implicit - probably because there is no chance to derive it even if all other arguments are given.

Guillaume Melquiond (Apr 20 2022 at 07:10):

You would get a message about the inability to derive the implicit argument only once no unification problems remain. Here, there is one single remaining failure: nat == typeDenote A.

Guillaume Melquiond (Apr 20 2022 at 07:20):

Anyway, while bidirectional typing does not solve the issue, it still helps a bit, as Coq will therefore accept mcons 3 mnil : listmod Int.

Michael Soegtrop (Apr 20 2022 at 07:25):

Sorry, please forget my note about the error message - I just didn't read it properly. It is perfectly clear.

Gaëtan Gilbert (Apr 20 2022 at 09:00):

you can do some stuff with canonical structures

Inductive type : Type :=
| Int
| Bool.

Definition typeDenote0 (t:type) : Type :=
  match t with
  | Int => nat
  | Bool => bool
  end.

Record denotedType := {
    reified :> type;
    typeDenote :> Type;
    typeDenote_ok : typeDenote = typeDenote0 reified;
  }.

Inductive listmod (A:denotedType) : Type :=
| mnil : listmod A
| mcons : (typeDenote A) -> listmod A -> listmod A.
Arguments mnil {A}.
Arguments mcons {A}.

Canonical Structure denotedInt :=
  {|
    reified := Int;
    typeDenote := nat;
    typeDenote_ok := eq_refl;
  |}.

Check mcons 3 mnil.

This makes Check @mcons Int 3 mnil. fail but https://github.com/coq/coq/pull/15693 makes it work again.

Julin S (Apr 20 2022 at 09:07):

Okay, we can achieve almost the same result using additional features.

Could there be some simpler way to achieve this? Am I approaching this from a wrong perspective?

I just needed a version of list which can be used to make just boolean or nat lists (lists of other types disallowed using the new list type).

Gaëtan Gilbert (Apr 20 2022 at 09:09):

tbh listmod is useless here, you can just use list (typeDenote bla)

Julin S (Apr 20 2022 at 09:13):

Can we place the 'type restriction' while constructing list objects as well?

Like cons 2 nil being okay, but cons "hi"%string nil being not okay.

Gaëtan Gilbert (Apr 20 2022 at 09:19):

what's the point?
you can do Definition listmod (A:denotedType) := list (typeDenote A). and similar for mnil and mcons (that way you can still enjoy all the lemmas on list)

Julin S (Apr 20 2022 at 09:36):

You mean something like this:

Definition listmod (A:type) := list (typeDenote A).

Definition mnil (A:type) : list (typeDenote A) := nil.

Definition mcons (A:type) (a:(typeDenote A))
  (l:list (typeDenote A))
  : list (typeDenote A) := cons a l.

Arguments mnil {A}.
Arguments mcons {A} a l.

with the canonical structure way to have implicit args?

Julin S (Apr 20 2022 at 09:37):

Oh wait, I missed the denotedType.

Julin S (Apr 20 2022 at 09:40):

This worked:

Definition listmod (A:denotedType) := list (typeDenote A).
Definition mnil (A:denotedType) : list (typeDenote A) := nil.
Definition mcons (A:denotedType) (a:(typeDenote A))
  (l:list (typeDenote A))
  : list (typeDenote A) := cons a l.
Arguments mnil {A}.
Arguments mcons {A} a l.

Compute mnil.
Compute mcons 2 mnil.
(*
= (2 :: nil)%list
     : list denotedInt
*)

Compute mcons "h"%string mnil.
(*
The term ""h"%string" has type "string" while it is expected to have type
 "typeDenote ?A".
*)

I need to read up about canonical structures.

Thanks!

Last updated: Oct 04 2023 at 23:01 UTC