The Coq mailing list

[Dominik Kirst <kirst AT ps.uni-saarland.de>]

Thanks for the help!

Dominik




> On 14. Sep 2017, at 12:45, Amin Timany 
> <amintimany AT gmail.com>
>  wrote:
> 
> 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
>