The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

Dear Amin,

thanks again for your nice example constructing a contradiction with a universe inconsistent type. I have found out that even a weaker definition of your type ‘Ens’ which is still universe inconsistent allows the same construction of a contradiction.

Inductive Ens@{i} : Type@{i} :=

ens_intro : forall A : Type@{i}, (A -> Ens) -> Ens.

Note the minor difference in the first constructor argument. An object of type Ens lives in the universe i. However it contains an object A of type Type@{i} living in the universe i+1. This definition makes sure that coq rejects the definition without the option type-in-type an accepts all the following with the option type-in-type.

Regards

Helmut

On 8. Dec 2022, at 11:44, Amin Timany <amintimany AT gmail.com> wrote:

Dear Helmut,

Perhaps the following counterexample can be helpful which directly constructs "the set of all sets that are not elements of themselves” as in Russel’s paradox. (I checked this example with Coq version 8.15.2 with the “-type-in-type” option.)

Inductive Ens@{i} : Type@{i} :=
 ens_intro : forall A : Type@{i+1}, (A -> Ens) -> Ens.

Definition idx (A : Ens) : Type := match A with ens_intro T _ => T end.

Definition elem (A : Ens) (i : idx A) : Ens :=
 match A as u return idx u -> Ens with ens_intro B f => fun j => f j end i.

Definition elem_of (x A : Ens) := exists a, elem A a = x.

Definition Union {T} (f : T -> Ens) :=
 ens_intro {x : T & idx (f x)} (fun u => elem (f (projT1 u)) (projT2 u)).

Lemma elem_of_union {T} (f : T -> Ens) A : elem_of A (Union f) <-> exists t, elem_of A (f t).
Proof.
 split.
 - intros [[z idx] Hzidx]; exists z, idx; assumption.
 - intros [z [idx Hzidx]]; exists (existT _ z idx); assumption.
Qed.

Definition singleton_if (a : Ens) (P : Prop) : Ens := ens_intro {x : unit | P} (fun _ => a).

Lemma elem_of_singleton_if a b P : (P /\ a = b) <-> elem_of b (singleton_if a P).
Proof.
 split.
 - intros [HP ->].
   exists (exist _ tt HP); reflexivity.
 - intros [[z Hz1] Hz2]; tauto.
Qed.

Definition Russel : Ens := Union (fun A : Ens => singleton_if A (not (elem_of A A))).

Theorem Russel's_Paradox : elem_of Russel Russel <-> not (elem_of Russel Russel).
Proof.
 split.
 - intros Helem.
   apply elem_of_union in Helem as [t Ht].
   apply elem_of_singleton_if in Ht as [? ->].
   assumption.
 - intros Hnelem.
   apply elem_of_union.
   exists Russel.
   apply elem_of_singleton_if; split; [assumption|reflexivity].
Qed.

Regards,
Amin

On 17 Nov 2022, at 12.05, Helmut Brandl <helmut.brandl AT gmx.net> wrote:

Thanks Gaëtan for your effort and your patience with my questions.

However the situation remains somehow unsatisfactory. By reading and rereading the documentation I cannot find a clear rule which states what is allowed and what is not allowed with respect to universes. As opposed to that, the positivity condition is stated very clearly and to my surprise, the justification of the positivity rule is explained with some examples which are short and to the point.

My intuitive explanation with the “hiding” of a higher universe type within a lower universe inductive definition might be correct. But it is not very precise and does not give a justification. Furthermore the example of the existential quantification does give a constraint on the universes without explaining the general rule.

Sorry for me insisting on this topic. Maybe it cannot be resolved easily.

Anyhow thanks for your efforts.

Helmut

On 17 Nov 2022, at 11:12, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

Unfortunately I have not found the rule that every argument of a constructor must be at a smaller or equal universe to the output universe

I can't find it either although it's mentioned, eg

One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative sorts SProp and Prop but may fail to define inductive type on sort Set and generate constraints between universes for inductive types in the Type hierarchy.

Probably a doc bug.

The reason for the rule is basically what you said earlier

I suspect that if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ in the list which resides in the universe ‘u’.

which leads to inconsistency. See also https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.Hurkens.html and mentioned references.

Gaëtan Gilbert

On 17/11/2022 10:45, Helmut Brandl wrote:

On 16 Nov 2022, at 23:35, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net <mailto:gaetan.gilbert AT skyskimmer.net>> wrote:

The rules for inductives https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions <https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions>
basically every argument of a constructor must be at a smaller or equal universe to the output universe of the inductive. The first argument of cons fails this.

Thanks for the explanation. I have tried to read the description in the link. Unfortunately I have not found the rule that every argument of a constructor must be at a smaller or equal universe to the output universe. Could you point to the specific paragraph which states that rule. Since the rules are very technical I might have overlooked it.
My intention is to understand not only the “what” of the rules, but also the “why” of the rules. What is the justification of such a rule? E.g. first I didn’t understand the necessity of the positivity rule of the constructor types. Then I have found an example which makes the necessity of the positivity rule clear. If the following inductive type were allowed
 Inductive T: Type :=
 | co: (T -> T) -> T.
I could define a fixpoint with infinite recursion
 Fixpoint run (t: T): T :=
    match t with
    | co f => run (f (co f))
    end.
Is there a similar justification for the rule you have mentioned? Does the rule inhibit an inconsistency like infinite recursion?
— Helmut

Gaëtan Gilbert

On 16/11/2022 22:32, Helmut Brandl wrote:

On 16 Nov 2022, at 22:06, Helmut Brandl <helmut.brandl AT gmx.net <mailto:helmut.brandl AT gmx.net> <mailto:helmut.brandl AT gmx.net <mailto:helmut.brandl AT gmx.net>>> wrote:

On 16 Nov 2022, at 21:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net <mailto:gaetan.gilbert AT skyskimmer.net> <mailto:gaetan.gilbert AT skyskimmer.net <mailto:gaetan.gilbert AT skyskimmer.net>>> wrote:

I.e. the argument type of a function type can live in a higher universe than the result type.

Yes, but "lst" is an _inhabitant_ of the function type, it's not the function type itself.

Similarly "(fun A:Type@{u+1} => A) : Type@{u+1} -> Type@{u}" is rejected

In that case the rejection is clear to me. The term ‘A’ has type ’Type@{u+1}’. Therefore the function returns a result of type ’Type@{u+1}’ and not ’Type@{u}’ as required by the type annotation. I.e. the function on the left hand side of the colon is not an inhabitant of the type on the right hand side of the colon. The compiler must reject it.

Are you saying that the type ’Type@{u+1} -> Type@{u}’ is not allowed to be inhabited? Is there such a typing rule? If there is such a typing rule, I would like to understand why it is there. Does the violation of such a typing rule create any inconsistencies like an inhabitant of the type ‘forall A: Type, A’?

According to coq the type ’Type@{u+1} -> Type@{u}’ can have inhabitants. E.g. the following is accepted by coq:
 Check (fun A: Type@{u+1} => nat): Type@{u+1} -> Type@{u}.
However my construction of the inductive type ‘lst’ which is an inhabitant of exactly that type is rejected. Why is it possible to construct a function of that type but not an inductive definition?

— Helmut

On 16/11/2022 21:02, Helmut Brandl wrote:

I’d like to understand universes and universe polymorphism better. Therefore I have some questions:
The following term is well typed in coq:
Universe u.
Check forall A:Type@{u+1}, Type@{u}.
I.e. the argument type of a function type can live in a higher universe than the result type. If I try the same with an inductive type, I get an error.
Inductive lst (A: Type@{u+1}): Type@{u} :=
| nil: lst A
| cons: A -> lst A -> lst A.
*Error:*Universe inconsistency. Cannot enforce u = max(Set, u+1).
What is the theoretical background of this consistency error. The type of ‘lst’ is exactly the type I have checked above as well typed. I suspect that if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ in the list which resides in the universe ‘u’. Can anybody help to give a more precise explanation.
Regards
Helmut