aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/univ.ml6
-rw-r--r--library/declare.ml2
-rw-r--r--library/universes.ml2
-rw-r--r--pretyping/pretyping.ml30
-rw-r--r--test-suite/bugs/closed/4287.v6
-rw-r--r--theories/Classes/CMorphisms.v14
-rw-r--r--theories/Logic/ClassicalFacts.v1
-rw-r--r--theories/Logic/Hurkens.v121
8 files changed, 102 insertions, 80 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index dc0a4b43c..2b3a2bdb1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1707,7 +1707,9 @@ struct
else if Array.length y = 0 then x
else Array.append x y
- let of_array a = a
+ let of_array a =
+ assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+ a
let to_array a = a
@@ -1715,7 +1717,7 @@ struct
let subst_fn fn t =
let t' = CArray.smartmap fn t in
- if t' == t then t else t'
+ if t' == t then t else of_array t'
let levels x = LSet.of_array x
diff --git a/library/declare.ml b/library/declare.ml
index 5968fbf38..994a6557a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -431,7 +431,7 @@ let cache_universes (p, l) =
Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
- Global.push_context_set false ctx;
+ Global.push_context_set p ctx;
if p then Lib.add_section_context ctx;
Universes.set_global_universe_names glob'
diff --git a/library/universes.ml b/library/universes.ml
index 1b6f7a9d5..a8e9478e1 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
let cstrs' = List.fold_left (fun cstrs (d, r) ->
if d == Univ.Le then
enforce_leq inst (Universe.make r) cstrs
- else
+ else
try let lev = Option.get (Universe.level inst) in
Constraint.add (lev, d, r) cstrs
with Option.IsNone -> failwith "")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dd4fcf198..faba5c756 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -394,18 +394,22 @@ let pretype_global loc rigid env evd gr us =
match us with
| None -> evd, None
| Some l ->
- let _, ctx = Universes.unsafe_constr_of_global gr in
- let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
- let len = Array.length arr in
- if len != List.length l then
- user_err_loc (loc, "pretype",
- str "Universe instance should have length " ++ int len)
- else
- let evd, l' = List.fold_left (fun (evd, univs) l ->
+ let _, ctx = Universes.unsafe_constr_of_global gr in
+ let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+ let len = Array.length arr in
+ if len != List.length l then
+ user_err_loc (loc, "pretype",
+ str "Universe instance should have length " ++ int len)
+ else
+ let evd, l' = List.fold_left (fun (evd, univs) l ->
let evd, l = interp_universe_level_name evd l in
(evd, l :: univs)) (evd, []) l
- in
- evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+ in
+ if List.exists (fun l -> Univ.Level.is_prop l) l' then
+ user_err_loc (loc, "pretype",
+ str "Universe instances cannot contain Prop, polymorphic" ++
+ str " universe instances must be greater or equal to Set.");
+ evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
in
Evd.fresh_global ~rigid ?names:instance env evd gr
@@ -440,13 +444,15 @@ let pretype_sort evdref = function
let new_type_evar env evdref loc =
let e, s =
- evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
+ evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
+ univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
in e
let get_projection env cst =
let cb = lookup_constant cst env in
match cb.Declarations.const_proj with
- | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} ->
+ | Some {Declarations.proj_ind = mind; proj_npars = n;
+ proj_arg = m; proj_type = ty} ->
(cst,mind,n,m,ty)
| None -> raise Not_found
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b8..43c9b5129 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
let foo (A : Type@{j}) := A in foo B.
Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}. \ No newline at end of file
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index fdedbf672..b13671cec 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -269,16 +269,6 @@ Section GenericInstances.
Unset Strict Universe Declaration.
(** The complement of a crelation conserves its proper elements. *)
- Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
- `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
- Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
-
- Next Obligation.
- Proof.
- unfold complement.
- pose (mR x y X x0 y0 X0).
- intuition.
- Qed.
(** The [flip] too, actually the [flip] instance is a bit more general. *)
Program Definition flip_proper
@@ -521,8 +511,8 @@ Ltac proper_reflexive :=
Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
-Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper
- : typeclass_instances.
+(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper *)
+(* : typeclass_instances. *)
Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper
: typeclass_instances.
Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6f736e45f..cdc3e0461 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -658,4 +658,3 @@ Proof.
exists x; intro; exact Hx.
exists x0; exact Hnot.
Qed.
-
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index ede51f57f..4e582934a 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -344,53 +344,6 @@ End Paradox.
End NoRetractToImpredicativeUniverse.
-(** * Prop is not a retract *)
-
-(** The existence in the pure Calculus of Constructions of a retract
- from [Prop] into a small type of [Prop] is inconsistent. This is a
- special case of the previous result. *)
-
-Module NoRetractFromSmallPropositionToProp.
-
-Section Paradox.
-
-(** ** Retract of [Prop] in a small type *)
-
-(** The retract is axiomatized using logical equivalence as the
- equality on propositions. *)
-
-Variable bool : Prop.
-Variable p2b : Prop -> bool.
-Variable b2p : bool -> Prop.
-Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
-Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-
-(** ** Paradox *)
-
-Theorem paradox : forall B:Prop, B.
-Proof.
- intros B.
- pose proof
- (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
- refine (P _ _ _ _ _ _ _ _ _ _);clear P.
- + exact bool.
- + exact (fun x => forall P:Prop, (x->P)->P).
- + cbn. exact (fun _ x P k => k x).
- + cbn. intros F P x.
- apply P.
- intros f.
- exact (f x).
- + cbn. easy.
- + exact b2p.
- + exact p2b.
- + exact p2p2.
- + exact p2p1.
-Qed.
-
-End Paradox.
-
-End NoRetractFromSmallPropositionToProp.
-
(** * Modal fragments of [Prop] are not retracts *)
(** In presence of a a monadic modality on [Prop], we can define a
@@ -534,6 +487,80 @@ End Paradox.
End NoRetractToNegativeProp.
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+ from [Prop] into a small type of [Prop] is inconsistent. This is a
+ special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+(** ** The universe of propositions. *)
+
+Definition NProp := { P:Prop | P -> P}.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section MParadox.
+
+(** ** Retract of [Prop] in a small type, using the identity modality. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem mparadox : forall B:NProp, El B.
+Proof.
+ intros B.
+ refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+ + exact (fun P => P).
+ + cbn. auto.
+ + cbn. auto.
+ + cbn. auto.
+ + exact bool.
+ + exact p2b.
+ + exact b2p.
+ + auto.
+ + auto.
+ + exact B.
+ + exact h.
+Qed.
+
+End MParadox.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+ equality on propositions. *)
+Variable bool : Prop.
+Variable p2b : Prop -> bool.
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
+Proof.
+ intros B.
+ refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+ (exist _ B (fun x => x))).
+ + intros p. red. red. exact (p2b (El p)).
+ + cbn. intros b. red. exists (b2p b). exact (fun x => x).
+ + cbn. intros [A H]. cbn. apply p2p1.
+ + cbn. intros [A H]. cbn. apply p2p2.
+Qed.
+
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+
(** * Large universes are no retracts of [Prop]. *)
(** The existence in the Calculus of Constructions with universes of a
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 16:30:17 +0000