blob: 216338615d335221b0be18070407b8fb4e21a45a (
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
|
Inductive equivalent P Q := Equivalent (P_to_Q : P -> Q) (Q_to_P : Q -> P).
Inductive equal T (x : T) : T -> Type := Equal : equal T x x.
(* Arithmetic *)
Inductive natural := Zero | Add_1_to (n : natural).
Fixpoint add (m n : natural) : natural :=
match m with Zero => n | Add_1_to m_minus_1 => add m_minus_1 (Add_1_to n) end.
Definition double (n : natural) : natural := add n n.
Inductive odd (n : natural) :=
Odd (half : natural)
(n_odd : equal natural n (Add_1_to (double half))).
Inductive less_than (m n : natural) :=
LessThan (diff : natural)
(m_lt_n : equal natural n (Add_1_to (add m diff))).
(* Finite subsets *)
Definition injective_in T R (D : T -> Type) (f : T -> R) :=
forall x y, D x -> D y -> equal R (f x) (f y) -> equal T x y.
Inductive in_image T R (D : T -> Type) (f : T -> R) (a : R) :=
InImage (x : T) (x_in_D : D x) (a_is_fx : equal R a (f x)).
Inductive finite_of_order T (D : T -> Type) (n : natural) :=
FiniteOfOrder (rank : T -> natural)
(rank_injective : injective_in T natural D rank)
(rank_onto :
forall i, equivalent (less_than i n) (in_image T natural D rank i)).
(* Constraints *)
Universes i j.
Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
Constraint i < j.
Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
Universes i' j'.
Constraint i' = j'.
Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
Inductive constraint4 : (Type -> Type) -> Type
:= mk_constraint4 : let U1 := Type in
let U2 := Type in
constraint4 (fun x : U1 => (x : U2)).
Module CMP_CON.
(* Comparison of opaque constants MUST be up to the universe graph.
See #6798. *)
Universe big.
Polymorphic Lemma foo@{u} : Type@{big}.
Proof. exact Type@{u}. Qed.
Universes U V.
Definition yo : foo@{U} = foo@{V} := eq_refl.
End CMP_CON.
Set Universe Polymorphism.
Module POLY_SUBTYP.
Module Type T.
Axiom foo : Type.
Parameter bar@{u v|u = v} : foo@{u}.
End T.
Module M.
Axiom foo : Type.
Axiom bar@{u v|u = v} : foo@{v}.
End M.
Module F (A:T). End F.
Module X := F M.
End POLY_SUBTYP.
Module POLY_IND.
Polymorphic Inductive ind@{u v | u < v} : Prop := .
Polymorphic Definition cst@{u v | v < u} := Prop.
End POLY_IND.
|
