coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Amin Timany <amintimany AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition
- Date: Thu, 14 Sep 2017 12:45:02 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=amintimany AT gmail.com; spf=Pass smtp.mailfrom=amintimany AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f66.google.com
- Ironport-phdr: 9a23:Tucrkx87mxls7f9uRHKM819IXTAuvvDOBiVQ1KB+1u8cTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS46tL2HV93a19HsZHgj1HQtzPOX8XIDI3Oqt0OXn0pjSZU10hT+0Z6I6eByzrAPNt8wfh5pKJaM4yx+PqXxNLbcFjVh0LE6eyk6vrvy7+4Rupnxd
Hi,
Another solution, if you are using 8.7beta1 or the development branch of Coq,
is to enable cumulativity for inductive types. In this case, the inferred
cumulativity (subtyping) relation for trees is as that every small tree is
also a large one.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.
Inductive Tree : Type :=
sup : forall A : Type, (A -> Tree) -> Tree.
Fixpoint emb' (s : Tree) :=
let (A, f) := s in
sup A (fun a => emb' (f a)).
Definition T := sup Tree emb’.
Considering the code above “Print Tree.” command prints:
Cumulative Inductive Tree@{Top.8} : Type@{Top.8+1} :=
sup : forall A : Type@{Top.8},
(A -> Tree@{Top.8}) -> Tree@{Top.8}
(* Top.8 |=
~@{Top.8} <= ~@{Top.9} iff
Top.8 <= Top.9
*)
For sup: Argument scopes are [type_scope function_scope]
Here “ ~@{Top.8} <= ~@{Top.9} iff Top.8 <= Top.9” that any term of type
Tree@{i} is also a term of type Tree@{j} whenever i <= j.
Regards,
Amin
> On 14 Sep 2017, at 12:36, Guillaume Melquiond
> <guillaume.melquiond AT inria.fr>
> wrote:
>
> On 13/09/2017 10:26, Dominik Kirst wrote:
>
>> When tagging the function type explicitly with two (unconstrained)
>> universe variables, the exact level of the codomain is kept variable and
>> the supremum becomes definable. Is this behaviour an intended minimisation?
>
> I would not even qualify that behavior as minimization; it looks like
> plain inference.
>
> For example, (fun x : Type => x) is inferred as (Type@{i} -> Type@{i}),
> not as (Type@{i} -> Type@{j} | i <= j), and this is intended.
>
> So, if you want extra universes and constraints, just add them by hand:
>
> Fixpoint emb'@{i j} (s : Tree@{i}) : Tree@{j} :=
> let (A, f) := s in
> sup A (fun a => emb' (f a)).
>
> Best regards,
>
> Guillaume
- [Coq-Club] Unexpected restriction in universe-polymorphic definition, Dominik Kirst, 09/13/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Guillaume Melquiond, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Amin Timany, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Dominik Kirst, 09/18/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Amin Timany, 09/14/2017
- Re: [Coq-Club] Unexpected restriction in universe-polymorphic definition, Guillaume Melquiond, 09/14/2017
Archive powered by MHonArc 2.6.18.