The Coq mailing list

[Dan Frumin <dfrumin AT cs.ru.nl>]

On 01/19, Matej Kosik wrote:
> On 01/19/2017 05:56 PM, Pierre Courtieu wrote:
> > Hi,
> >
> > Something that may confuse Matej is also that the only way of defining
> > an inductive in Coq is to declare it via a definition. Which Matej
> > associates to "changing the type Set by adding new inhabitants in it"
> > but this is a wrong interpretation.
>
> I was probably spoiled by Coq's implementation where are perceived the 
> commands such as:
>
>  Axiom ...
>  Definition ...
>  Theorem ...
>  Inductive ...
>
> as atomic transactions that manipulate the global environment.
> (adding things, most of the time or undoing of previous transactions)
>
> Even though this viewpoint was strange at the beginning
> (having E[Γ] monster instead of merely Γ)
> I got used to it and over time I stopped noticing this strangeness.
>
> In a way Coq is similar to Prolog or LISP which smash definitions into the 
> global space.
>
> It would be extremely attactive to make it more Scheme-like
> (dropping the need for the global environment and enriching just the local 
> context)
>
> > All inductive types exists from
> > the beginning,
>
> This is what Théo has said and which totally baffeled me,
> but I should probably have read Martin-Löf's work where this may be the case 
> (?).

I don't think it is the case in Martin-Loef's work, however there is a
Martin-Loef type theory with W-types, using which you can define all
the usual inductive types. And those exist "from the beginning". By
contrast in CiC the W-types are definable just like any other
inductive types.

> > it is just that the implementation of Coq does not have
> > a anonymous syntax for them (and maybe other deeper problem I am not
> > aware of).
> >
> > You can define anonymous functions like this: (fun x:Prop => Prop).
> > And everyone will probably admit that this function existed even
> > before we write it (although we may reach philosophical problems with
> > this formulation).
>
> I think this this makes sense.
>
> > But you cannot declare an anonymous inductive in such a way in coq
> > (say for instance with a binder syntax like this: (Ind nat:Set =>
> > O:nat | S: nat -> nat). So one could conclude that nat "does not exist
> > until it is declared".
>
> This is my perception, which valid if we restrict ourselves to Coq but I see 
> that it would be invalid in case we made it more Scheme-like instead of 
> keeping it more LISP/Prolog-like.
> (e.g. provide mechanisms you mentioned which would force us to consider all 
> valid inductive types to exist a priori. Now they exist a posteriori.)
>
> I find this idea very attractive.
>
> > But actually the underlying theory do have this kind of anonymous
> > inductive (see constr.ml as suggested by Maxime).
>
> I failed to find it.
>
> You do not mean this:
>
>  https://github.com/coq/coq/blob/trunk/kernel/constr.ml#L96
>
> or this:
>
>  https://github.com/coq/coq/blob/trunk/kernel/constr.ml#L97
>
> Do you? Because these values just designate (they do not define) inductive 
> types / constructors.
>
> The definition of inductive types is part of the global environment.
>
>  https://github.com/coq/coq/blob/trunk/kernel/pre_env.ml#L43
>
> > So all typable
> > inductives types always existed as every typable other terms.
>
> I do not think this is the case in case of Coq, or is it?
> > Hope this helps,
> > Pierre