Inductive inductive types

[mattam82]

Kind: feature

Fixes / closes #???? (certainly some wishes are related)

This is an extraction and rebase of the "reasonable part" of my old induction-recursion/induction-recursion branch. I think inductive recursive types should rather be handled using a global fixpoint notion, but inductive-inductives pose no such problem (almost).

This both allows inductives to depend on previous ones in the same block (and their constructors) and mutual fixpoints to depend on each other in their types.

CAUTION: the guard checking is currently disabled in match predicates for this to work currently. No guarantees about consistency, decidability of typechecking or subject reduction are made.

This is all done by generalizing inductive blocks to have dependencies betwee arities and for constructors to be typed in a context with the previous arities and constructors available (i.e. we are really building a signature). This can give rise to name clashes in existing definitions but it should be quite rare (none in the stdlib or test-suite).

Positivity checking is not verifying anything about the use of constructors, it might have to.

For recursive-recursive fixpoints, tying the know is not easy and there are two more hacky parts in pretyping and more importantly in the kernel where we might be calling reduction on ill-typed or at least not guarded terms, but I think that's avoidable by having a notion of partial fixpoint definition (where some bodies are not reducible): to typecheck fixpoint n ones needs the computational content of the n-1 previous fixpoints only, but the way fixpoints are encoded in blocks does not allow to express that.

A few parts of the system are not adapted yet, e.g. some elaboration code which does not allow for the dependencies available in the kernel calculus. For uniformity I allowed mutual dependent cofixpoints, but I'm not sure they are of any use (yet?), or maybe could cause trouble. So, many questions remain :) But one can play with it to interpret a small type-theory in type theory, for example.

Anyway, I'll write more about this here when we figure out how to make progress with @herbelin and @Alizter.

• Added / updated test-suite
• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[SkySkimmer]

I updated the part of hottclasses which uses II to this branch + hott master.
I get Anomaly "make_resolve_hyp." on https://github.com/SkySkimmer/HoTTClasses/blob/c3e809bdc2f75f7b2c9f3e0664cdf1ce6d450fed/theories/partiality.v#L355
See log https://travis-ci.org/github/SkySkimmer/HoTTClasses/builds/748640810

[SkySkimmer]

Attempted rebase, let's see how it goes (note FIXME in cclosure norm_head)

[Alizter]

@SkySkimmer Why did the windows job succeed if the others failed?

[SkySkimmer]

Because the windows job builds nothing (see #14561)

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[Alizter]

Here is something that gives a nonsense error message:

Inductive nat : Set :=
| zero : nat
| succ : nat
with iseven : nat -> Prop :=
| iseven_zero : iseven zero
| iseven_succ_isodd x
  : isodd x -> iseven (succ x)
with isodd : nat -> Prop :=
| isodd_succ_iseven x
  : iseven x -> isodd (succ x)
.

Illegal application (Non-functional construction): 
The expression "succ" of type 
"nat"
cannot be applied to the term
 "x" : "nat"

[SkySkimmer]

That looks fine to me (did you really intend to write succ : nat on line 3?)

[Alizter]

No but I am still getting a weird message after fixing it to succ : nat -> nat:

In environment
P : nat -> Prop
f : P zero
f0 :
forall x : nat,
isodd x -> P (succ x)
n : nat
i : iseven n
The term "i" has type "iseven n"
which should be Set, Prop or Type.
nat, iseven, isodd are defined
nat_rect is defined
nat_ind is defined
nat_rec is defined
nat_sind is defined

Those things shouldn't be defined right?

[ppedrot]

@Alizter this looks like a failure of some scheme generation, so it's not so surprising.

[Alizter]

Here is an example (I don't know if we want to accept this) that shows mutual fixpoints aren't sharing bodies correctly:

Fixpoint foo (A : Type) (a : A) (n : nat) : Type :=
  match n with
  | 0   => False
  | S k => True + {x : foo A a k & bar x = a}
  end
with bar (A : Type) (x : A) (n : nat) : foo A x n -> A :=
  match n with
  | 0   => fun _ => x
  | S k => fun t => foo k (projT1 t)
  end.

The reference foo
was not found in the current
environment.

(* Ali: The environment being the type of bar *)

Also there is the question of universes for these kinds of things. If I were to bundle up this definition as a recursion into a sigma type for example, I would need a larger universe for that sigma type to live in. But then projecting out, I no longer need the larger universe but I am forced to carry it around anyway. At the moment, I can't write @{u+1} I believe, which is a separate project.

If we can directly write these recursive-recursive definitions then we can probably avoid this extra universe, but I have no idea if that is a sensible thing to do.

[Alizter]

@ppedrot Do you think the printing of "defined" messages after the scheme generation failure is a bug from this PR or a bug in general?

[ppedrot]

@Alizter it's a general bug, I think we even have an open issue about it already.

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[Alizter]

@mattam82 At some point the guard checker got worse. Having trouble getting

File "./theories/micromega/ZMicromega.v", line 1049, characters 0-497:

accepted.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.