The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

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
>>>>>> 
>