Inductive cumulativity supports sort cumulativity (Prop <= Type)

[SkySkimmer]

Overlays:

• Adapt to rocq-prover/rocq#21773 (sort polymorphic cumulativity) LPCIC/coq-elpi#982
• Adapt to rocq-prover/rocq#21773 (sort poly cumulativity) MetaRocq/metarocq#1250

[JasonGross]

This does not look right:

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

Inductive Box@{s;l} (A : Type@{l}) : Type@{s;l} := box : A -> Box A.

Definition unbox (x : Box@{Prop;Type} Type) := match (x : Box@{Type;Type} Type) return Type with box _ A => A end.

Hm, this is supposed to be justified by η-expansion (match (x : Box@{Prop;u} A) return Box@{Type;u} A with box v => box v end and vice versa). I guess there is some interaction between sorts appearing in the return type of the inductive and elimination into the connected component of that sort.

[JasonGross]

I think the following two files fail with this PR (I haven't quite narrowed it down to being this PR rather than another one in my stack of patches):

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.EqualityLemmas") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1889 lines to 24 lines, then from 38 lines to 192 lines, then from 199 lines to 46 lines, then from 61 lines to 46 lines, then from 61 lines to 37 lines, then from 52 lines to 37 lines *)
(* coqc version 9.2+rc2 compiled with OCaml 4.14.2
   coqtop version 9.2+rc2
   Expected coqc runtime on this file: 3.272 sec
   Expected coqc peak memory usage on this file: 181856.0 kb *)
#[export]
Set Universe Polymorphism.
#[local] Set Primitive Projections.
Inductive eq@{s|u|} {α:Type@{s|u}} (a:α) : α -> SProp
  := eq_refl : eq a a.

#[local] Notation "x = y" := (eq x y) : type_scope.
Arguments eq_refl {α a} , [α] a.
#[export]
Set Implicit Arguments.
Record Iso@{s s'|u u'|} (A : Type@{s|u}) (B : Type@{s'|u'}) := {
    to :> A -> B;
    from : B -> A;
    to_from : forall x, to (from x) = x;
    from_to : forall x, from (to x) = x;
}.
Record > rel_iso@{s s'|u u'|} {A B} (i : Iso@{s s'|u u'} A B) (x : A) (y : B) : SProp := { proj_rel_iso :> i.(to) x = y }.
Axiom functional_extensionality_dep@{s s'|u u' u''|u<=u'',u'<=u''}
  : forall {A : Type@{s|u}} {B : A -> Type@{s'|u'}} (f g : forall x : A, B x), (forall x : A, f x = g x) -> eq@{s'|u''} f g.

Definition IsoForall@{s0 s1 s2 s3|u0 u1 u2 u3 u4 u5|u0 <= u4,u1 <= u5,u2 <= u4,u3 <= u5}
  {A A'} (isoA : Iso@{s0 s1|u0 u1} A A') (B : A -> Type@{s2|u2}) (B' : A' -> Type@{s3|u3})
  : (forall a a' (He : rel_iso isoA a a'), Iso (B a) (B' a'))
    -> Iso@{s2 s3|u4 u5} (forall a, B a) (forall a', B' a').
Proof.
  intro H; unshelve esplit; [ intros f a .. | intro x; shelve | intro x; shelve ].
  all: first [ specialize (H a) | specialize (fun a' => H a' a) ].
  all: first [ specialize (H (isoA.(to) a)) | specialize (H (isoA.(from) a)) ].
  all: first [ specialize (H eq_refl) | specialize (H (isoA.(to_from) a)) ].
  all: [ > first [ apply H.(to) | apply H.(from) ]; auto .. ].
  Unshelve.
  all: cbn.
  all: apply functional_extensionality_dep; intro.
  {
 destruct to_from. (* Error: Unable to find an instance for the variables A, B, i, x. *)

and

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.EqualityLemmas") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1889 lines to 9 lines, then from 23 lines to 176 lines, then from 183 lines to 20 lines, then from 35 lines to 20 lines, then from 35 lines to 14 lines, then from 29 lines to 14 lines *)
(* coqc version 9.1.0 compiled with OCaml 4.14.2
   coqtop version 9.1.0
   Expected coqc runtime on this file: 1.191 sec
   Expected coqc peak memory usage on this file: 329464.0 kb *)
Module Export IsomorphismDefinitions.
#[export]
Set Universe Polymorphism.
#[export]
Set Polymorphic Inductive Cumulativity.
Inductive eq@{s|u|} {α:Type@{s|u}} (a:α) : α -> SProp
  := eq_refl : eq a a.
#[local] Notation "x = y" := (IsomorphismDefinitions.eq x y) : type_scope.
Lemma seq_of_peq@{u} {A : Prop} {x y : A} (H : Logic.eq x y) : IsomorphismDefinitions.eq@{Prop|u} x y.
Proof.
destruct H; reflexivity.
Defined.
(* File "./bug_eq_refl_01.v", line 18, characters 0-8:
Error: In pattern-matching on term "H" the branch for constructor
"Logic.eq_refl" has type "@eq@{Type ; bug_eq_refl_01.23} A x x"
which should be "@eq@{Prop ; bug_eq_refl_01.23} A x x". *)

[SkySkimmer]

I think the following two files fail with this PR (I haven't quite narrowed it down to being this PR rather than another one in my stack of patches):

first one fails in master (050e23e) and 9.2 (#21781)
second one succeeds in the PR

[ppedrot]

Sounds fine now (famous last words).

[ppedrot]

I'm leaving a bit of time before merging for others to chime in and double check that we did not miss a case both in the code and in the theory.

[yannl35133]

This feature needs documentation (universe cumulative inductives also lack a formal specification in the reference manual).

[yannl35133]

Isn't that Array.chop flipped?

[yannl35133]

Suggested change

	let quals = Array.map2 (fun a b -> a,b) quals qvariances in
	let univs = Array.map2 (fun a b -> a,b) univs uvariances in
	let quals = Array.combine quals qvariances in
	let univs = Array.combine univs uvariances in

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

[SkySkimmer]

The inconsistency scared me enough that I'm not sure if we want to continue this, especially considering we intend to remove Prop <= Type eventually.

[coqbot-app]

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