From 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 16 Feb 2018 15:44:44 +0100 Subject: Allow using cumulativity without forcing strict constraints. Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. --- test-suite/bugs/closed/6661.v | 259 ++++++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/6775.v | 43 +++++++ test-suite/coqchk/cumulativity.v | 2 +- test-suite/success/cumulativity.v | 56 ++------- 4 files changed, 311 insertions(+), 49 deletions(-) create mode 100644 test-suite/bugs/closed/6661.v create mode 100644 test-suite/bugs/closed/6775.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/6661.v b/test-suite/bugs/closed/6661.v new file mode 100644 index 0000000000..e88a3704d8 --- /dev/null +++ b/test-suite/bugs/closed/6661.v @@ -0,0 +1,259 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *) +(* + The Coq Proof Assistant, version 8.7.1 (January 2018) + compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0 + from commit 391bb5e196901a3a9426295125b8d1c700ab6992 + *) + + +Require Export Coq.Init.Notations. +Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Reserved Notation "p @ q" (at level 60, right associativity). +Reserved Notation "! p " (at level 50). + +Monomorphic Universe uu. +Monomorphic Universe uu0. +Monomorphic Universe uu1. +Constraint uu0 < uu1. + +Global Set Universe Polymorphism. +Global Set Polymorphic Inductive Cumulativity. +Global Unset Universe Minimization ToSet. + +Notation UU := Type (only parsing). +Notation UU0 := Type@{uu0} (only parsing). + +Global Set Printing Universes. + + Inductive unit : UU0 := tt : unit. + +Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a. +Hint Resolve idpath : core . +Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope. + +Set Primitive Projections. +Set Nonrecursive Elimination Schemes. + +Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i} + := tpair { pr1 : T; pr2 : P pr1 }. + +Arguments tpair {_} _ _ _. +Arguments pr1 {_ _} _. +Arguments pr2 {_ _} _. + +Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..)) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. + induction xy as [x y]. + exact x. +Defined. + +Unset Automatic Introduction. + +Definition idfun (T : UU) := λ t:T, t. + +Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. +Proof. + intros. induction e1. exact e2. +Defined. + +Hint Resolve @pathscomp0 : pathshints. + +Notation "p @ q" := (pathscomp0 p q). + +Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Notation "! p " := (pathsinv0 p). + +Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1} + (e: t1 = t2) : f t1 = f t2. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') : + f x y = f x' y'. +Proof. + intros. induction ex. induction ey. exact (idpath _). +Defined. + + +Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X} + (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) : + maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2. +Proof. + intros. induction e1. induction e2. exact (idpath _). +Defined. + +Definition maponpathsinv0 {X Y : UU} (f : X -> Y) + {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e). +Proof. + intros. induction e. exact (idpath _). +Defined. + + + +Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') : + ∑ (f : P x -> P x'), + ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)), + ∏ (pp : P x), maponpaths pr1 (ee pp) = e. +Proof. + intros. induction e. + split with (idfun (P x)). + split with (λ p, idpath _). + unfold maponpaths. simpl. + intro. exact (idpath _). +Defined. + +Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X} + (e : x = x') : P x -> P x' := pr1 (constr1 P e). + +Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2} + (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2. +Proof. + intros. induction p. induction q. exact (idpath _). +Defined. + +Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr. + +Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'. +Proof. + intros. + induction is as [y fe]. + exact (fe x @ !(fe x')). +Defined. + + +Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y). + +Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y} + (x : X) (e : f x = y) : hfiber f y := + tpair _ x e. + +Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t. + +Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t + := tpair _ t' e. + +Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2. +Proof. + intros. + induction c1 as [x0 x]. + induction x. + induction c2 as [x1 y]. + induction y. + exact (idpath _). +Defined. + +Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} := + ∏ y : Y, iscontr (hfiber f y). + +Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'. +Proof. + intros. induction x. induction x'. exact (idpath _). +Defined. + +Lemma unitl0 : tt = tt -> coconustot _ tt. +Proof. + intros e. exact (coconustotpair unit e). +Defined. + +Lemma unitl1: coconustot _ tt -> tt = tt. +Proof. + intro cp. induction cp as [x t]. induction x. exact t. +Defined. + +Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e. +Proof. + intros. unfold unitl0. simpl. exact (idpath _). +Defined. + +Lemma unitl3: ∏ e : tt = tt, e = idpath tt. +Proof. + intros. + + assert (e0 : unitl0 (idpath tt) = unitl0 e). + { simple refine (connectedcoconustot _ _). } + + set (e1 := maponpaths unitl1 e0). + + exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))). +Defined. + +Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x'). +Proof. + intros. + split with (isProofIrrelevantUnit x x'). + intros e'. + induction x. + induction x'. + simpl. + apply unitl3. +Qed. + +Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2. +Proof. + intros. + simple refine (proofirrelevancecontr _ _ _). + exact (iscontrpathsinunit tt tt). +Qed. + +Section isweqcontrtounit. + + Universe i. + + (* To see the bug, run it both with and without this constraint: *) + + (* Constraint uu0 < i. *) + + (* Without this constraint, we get i = uu0 in the next definition *) + Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt). + Proof. + intros. intro y. induction y. + induction is as [c h]. + split with (hfiberpair@{i i i} _ c (idpath tt)). + intros ha. + induction ha as [x e]. + simple refine (two_arg_paths_f (h x) _). + simple refine (ifcontrthenunitl0 _ _). + Defined. + + (* + Explanation of the bug: + + With the constraint uu0 < i above we get: + + |= uu0 <= bug.3 + uu0 <= i + uu1 <= i + i <= bug.3 + + from this print statement: *) + + Print isweqcontrtounit. + + (* + + Without the constraint uu0 < i above we get: + + |= i <= bug.3 + uu0 = i + + Since uu0 = i is not inferred when we impose the constraint uu0 < i, + it is invalid to infer it when we don't. + + *) + + Context (X : Type@{uu1}). + + Check (@isweqcontrtounit X). (* detect a universe inconsistency *) + +End isweqcontrtounit. diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v new file mode 100644 index 0000000000..206df23bce --- /dev/null +++ b/test-suite/bugs/closed/6775.v @@ -0,0 +1,43 @@ +(* Issue caused and fixed during the lifetime of #6775: unification + failing on partially applied cumulative inductives. *) + +Set Universe Polymorphism. + +Set Polymorphic Inductive Cumulativity. + +Unset Elimination Schemes. + +Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Arguments inverse {A x y} p : simpl nomatch. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Arguments concat {A x y z} p q : simpl nomatch. + +Notation "1" := idpath. + +Reserved Notation "p @ q" (at level 20). +Notation "p @ q" := (concat p q). + +Reserved Notation "p ^" (at level 3, format "p '^'"). +Notation "p ^" := (inverse p). + +Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) : + (p @ q^) @ q = p + := + (match q as i return forall p, (p @ i^) @ i = p with + idpath => + fun p => + match p with idpath => 1 end + end) p. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index d63a3548e5..5f45007157 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -25,7 +25,7 @@ Section ListLower. End ListLower. -Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Lemma LowerL_Lem@{i j|j List A -> List A. -Section ListLift. - Universe i j. - - Constraint i < j. - - Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. - -End ListLift. +Definition LiftL@{k i j|k <= i, k <= j} {A:Type@{k}} : List@{i} A -> List@{j} A := fun x => x. Lemma LiftL_Lem A (l : List A) : l = LiftL l. Proof. reflexivity. Qed. -Section ListLower. - Universe i j. - - Constraint i < j. - - Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. - -End ListLower. - -Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. -Proof. reflexivity. Qed. - Inductive Tp := tp : Type -> Tp. -Section TpLift. - Universe i j. +Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x. - Constraint i < j. - - Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. - -End TpLift. +Fail Definition LowerTp@{i j|j < i} : Tp@{i} -> Tp@{j} := fun x => x. Record Tp' := { tp' : Tp }. @@ -51,22 +27,12 @@ Definition CTp := Tp. (* here we have to reduce a constant to infer the correct subtyping. *) Record Tp'' := { tp'' : CTp }. -Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x. -Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x. +Definition LiftTp'@{i j|i <= j} : Tp'@{i} -> Tp'@{j} := fun x => x. +Definition LiftTp''@{i j|i <= j} : Tp''@{i} -> Tp''@{j} := fun x => x. Lemma LiftC_Lem (t : Tp) : LiftTp t = t. Proof. reflexivity. Qed. -Section TpLower. - Universe i j. - - Constraint i < j. - - Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. - -End TpLower. - - Section subtyping_test. Universe i j. Constraint i < j. @@ -82,14 +48,8 @@ Record B (X : A) : Type := { b : X; }. NonCumulative Inductive NCList (A: Type) := ncnil | nccons : A -> NCList A -> NCList A. -Section NCListLift. - Universe i j. - - Constraint i < j. - - Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. - -End NCListLift. +Fail Definition LiftNCL@{k i j|k <= i, k <= j} {A:Type@{k}} + : NCList@{i} A -> NCList@{j} A := fun x => x. Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. @@ -114,7 +74,7 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. -Definition arrow_lift@{i i' j j' | i' = i, j < j'} +Definition arrow_lift@{i i' j j' | i' = i, j <= j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. -- cgit v1.2.3 From db0918bfa5089f9ab44374504cbd0ddc758ea1e5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 20 Feb 2018 00:27:40 +0100 Subject: Cumulativity: improve treatment of irrelevant universes. In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit. --- test-suite/success/cumulativity.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 0394ea340a..dfa305dc6e 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -115,3 +115,16 @@ Definition checkcumul := (* They can only be compared at the highest type *) Fail Definition checkcumul' := eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). + +(* An inductive type with an irrelevant universe *) +Inductive foo@{i} : Type@{i} := mkfoo { }. + +Definition bar := foo. + +(* The universe on mkfoo is flexible and should be unified with i. *) +Definition foo1@{i} : foo@{i} := let x := mkfoo in x. (* fast path for conversion *) +Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *) + +(* Rigid universes however should not be unified unnecessarily. *) +Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x. +Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x. -- cgit v1.2.3 From 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 18:28:36 +0100 Subject: Delayed weak constraints for cumulative inductive types. When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified. --- test-suite/coqchk/cumulativity.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index 5f45007157..034684054d 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -25,7 +25,7 @@ Section ListLower. End ListLower. -Lemma LowerL_Lem@{i j|j