Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Behold another issue with Set. In this case, the problem is that the theorem that Contr (Unit : Set) doesn't also prove Contr (Unit : Type) for other universes, even though its proof term does.
Perhaps the problem is that sometimes I use Set to mean Type > Prop, and, much more rarely, I use it to mean Type <= Type_0, but Coq doesn't give me a way to distinguish these. Perhaps I want a way to declare an inductive type
Inductive unit : Type := tt.
which will not land in Prop, but won't land in Set either, i.e., so that all three Checks in the following code work:
Set Universe Polymorphism.
Set Printing Universes.
Section u.
Let U := Type.
Inductive unit : U := tt.
End u.
Print unit. (* Inductive unit : Type (* Top.35 *) :=
tt : unit (* Top.35 *)
(* Top.35 |= Prop <= Top.35
*) *)
Check unit. (* unit
(* Prop *)
: Prop *)
Definition same_univ : $(let U := constr:(Type) in exact (U -> U -> True))$
:= fun _ _ => I.
Definition foo := same_univ unit.
Check unit : Set.
Check foo nat.
Check foo Set.
(It might be nice if Check unit : Prop. also works, in addition to the ones above.)
Here's some more code that breaks:
(* File reduced by coq-bug-finder from original input, then from 4171 lines to 78 lines, then from 88 lines to 53 lines *)
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y" := (@paths _ x y) : type_scope.
Class Contr_internal (A : Type) := BuildContr {
center : A ;
contr : (forall y : A, center = y)
}.
Inductive Unit : Set := tt.
Instance contr_unit : Contr_internal Unit | 0 := let x := {|
center := tt;
contr := fun t : Unit => match t with tt => idpath end
|} in x.
Section local.
Let type_cast_up_type : Type.
Proof.
let U0 := constr:(Type) in
let U1 := constr:(Type) in
let unif := constr:(U0 : U1) in
exact (U0 -> U1).
Defined.
Definition Lift : type_cast_up_type
:= fun T => T.
End local.
Record hProp := hp { hproptype :> Type ; isp : Contr_internal hproptype}.
Set Printing All.
Definition foo : hProp.
exact (hp (Lift Unit) (BuildContr Unit tt (fun t => match t as t0 return (@paths Unit tt t0) with
| tt => idpath
end))).
Undo.
Set Printing Universes.
exact (hp (Lift Unit) (contr_unit)).
(* Toplevel input, characters 23-33:
Error:
The term "contr_unit" has type "Contr_internal (* Set *) Unit"
while it is expected to have type
"Contr_internal (* Top.50 *) (Lift (* Top.51 Top.52 Top.53 Top.54 *) Unit)"
(Universe inconsistency: Cannot enforce Top.50 = Set because Set <= Top.54
< Top.51 <= Top.50)). *)
Behold another issue with
Set
. In this case, the problem is that the theorem thatContr (Unit : Set)
doesn't also proveContr (Unit : Type)
for other universes, even though its proof term does.Perhaps the problem is that sometimes I use
Set
to meanType > Prop
, and, much more rarely, I use it to meanType <= Type_0
, but Coq doesn't give me a way to distinguish these. Perhaps I want a way to declare an inductive typewhich will not land in
Prop
, but won't land inSet
either, i.e., so that all threeCheck
s in the following code work:(It might be nice if
Check unit : Prop.
also works, in addition to the ones above.)Here's some more code that breaks: