The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

>In order to get an inhabitant you would need a function which constructs 
from an inhabitant of any type ‘A’ an inhabitant of ‘Ens’

There is a subtlety here: a constructor like "C : forall x, ..." inhabits the inductive 
when there exists an "x", so the universal quantification turns into an existential 
quantification.

So you do not need to inhabit for all A, but only for some A. Then as you 
noted this can be started using A := False.

Gaëtan Gilbert

On 08/12/2022 22:06, Helmut Brandl wrote:
> 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.
>
> Could you explain a little bit the basic idea of your construction and the 
> helper functions you have used.
>
> 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