blob: 4dda3604231edc4d0710b6caf76986ac3c70eb43 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
Polymorphic Cumulative Inductive T1 := t1 : T1.
Fail Monomorphic Cumulative Inductive T2 := t2 : T2.
Polymorphic Cumulative Record R1 := { r1 : T1 }.
Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.
Inductive List (A: Type) := nil | cons : A -> 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.
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.
Constraint i < j.
Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
End TpLift.
Record Tp' := { tp' : Tp }.
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.
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.
Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
End subtyping_test.
Record A : Type := { a :> Type; }.
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.
Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
:= forall f g : (forall a, B a),
(forall x, eq@{e} (f x) (g x))
-> eq@{e} f g.
Section down.
Universes a b e e'.
Constraint e' < e.
Lemma funext_down {A B}
: @funext_type@{a b e} A B -> @funext_type@{a b e'} A B.
Proof.
intros H f g Hfg. exact (H f g Hfg).
Defined.
End down.
Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }.
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'}
: Arrow@{i j} -> Arrow@{i' j'}
:= fun x => x.
Inductive Mut1 A :=
| Base1 : Type -> Mut1 A
| Node1 : (A -> Mut2 A) -> Mut1 A
with Mut2 A :=
| Base2 : Type -> Mut2 A
| Node2 : Mut1 A -> Mut2 A.
(* If we don't reduce T while inferring cumulativity for the
constructor we will see a Rel and believe i is irrelevant. *)
Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams.
Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j}
:= fun x => x.
Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j}
:= fun x => x.
(** Cumulative constructors *)
Record twotys@{u v w} : Type@{w} :=
twoconstr { fstty : Type@{u}; sndty : Type@{v} }.
Monomorphic Universes i j k l.
Monomorphic Constraint i < j.
Monomorphic Constraint j < k.
Monomorphic Constraint k < l.
Parameter Tyi : Type@{i}.
Definition checkcumul :=
eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
(* 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).
|
