Stream: Coq users

Topic: List restricted to some types


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

view this post on Zulip Guillaume Melquiond (Apr 20 2022 at 07:00):

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

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

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

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

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

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Apr 20 2022 at 09:09):

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

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

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

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

view this post on Zulip Julin S (Apr 20 2022 at 09:37):

Oh wait, I missed the denotedType.

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC