The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Thanks Amin and Helmut for this nice discussion,

Le 08/12/2022 à 22:06, Helmut Brandl a écrit :
> Thanks Amin,
>
> I was looking for such an example. I have checked it with my installation of 
> coq and it is rejected without the ’type-in-type’ option and accepted with 
> the option. Excellent, thanks.
>
> As opposed to the other examples which I have seen up to now, your example 
> has a size that one has a chance to understand it mentally.
>
> However I am struggling in mentally understanding the example. The type ‘Ens’ 
> seems to be uninhabited. In order to get an inhabitant you would need a 
> function which constructs from an inhabitant of any type ‘A’ an inhabitant of 
> ‘Ens’ without having an inhabitant in the first place. For me this seems to 
> be possible only for uninhabited types like ‘False’ but nor for all types.

I do not understand your point. You can easily build an inhabitant of 
Ens (exactly by using an empty type in the first place, as you have just 
explained).

---
Inductive Empty: Type :=.

Lemma EmptyEns: Ens.
Proof.
  refine (ens_intro Empty _).
  destruct 1.
Qed.
---

From this first element, then you can you can wrap any "Type" in Ens.

---
Definition lift_ens (A:Type): Ens := ens_intro A (fun _ => EmptyEns).
---

Anyway, you can do anything, because Russel's_Paradox leads enables a 
proof of False.

---
Lemma absurd: False.
Proof.
  generalize Russel's_Paradox. intuition.
Qed.
---

> Could you explain a little bit the basic idea of your construction and the 
> helper functions you have used.

Yes, the name helps a bit on the underlying intuition, but a little more 
explanation would help more ;-)

Regards,

Sylvain.

> Regards
> Helmut
>
>
>
> > On 8 Dec 2022, at 18: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