-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathModelECC.v
159 lines (120 loc) · 3.26 KB
/
ModelECC.v
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
158
159
(** Model construction (entailing consistency) for ECC based on
ZF + infinitely many Grothendieck universes.
*)
Require Import List Bool Models TypModels.
Require Import ZF ZFsum ZFnats ZFrelations ZFord ZFfix ZFgrothendieck ZFcoc ZFecc.
Require Import ModelCC.
Import BuildModel.
Import T J R.
Lemma sub_typ_covariant e U1 U2 V1 V2 :
U1 <> kind ->
eq_typ e U1 U2 ->
sub_typ (U1::e) V1 V2 ->
sub_typ e (Prod U1 V1) (Prod U2 V2).
red; intros.
revert H3; apply cc_prod_covariant.
do 2 red; intros.
rewrite H4; reflexivity.
apply H0; trivial.
red; intros.
revert H4; apply H1.
apply vcons_add_var; trivial.
Qed.
(** Universes: version where type 0 is a universe of hereditarily
finite sets (HF). Hence it does not contain nat. It is a model
of ECC.
*)
Module Type ECC := ECC_Rules BuildModel.
Module WithFinitistUniverse <: ECC.
Definition type (n:nat) := cst (ecc n).
Lemma typ_Prop : forall e, typ e prop (type 0).
red; intros; simpl.
apply (ecc_in1 0).
Qed.
Lemma typ_Type : forall e n, typ e (type n) (type (S n)).
red; intros; simpl.
apply (ecc_in2 n).
Qed.
Lemma cumul_Type : forall e n, sub_typ e (type n) (type (S n)).
red; simpl; intros.
red; intros.
apply ecc_incl; trivial.
Qed.
Lemma cumul_Prop : forall e, sub_typ e prop (type 0).
red; simpl; intros.
red; intros.
apply G_trans with props; trivial.
apply (ecc_grot 0).
apply (ecc_in1 0).
Qed.
Lemma typ_prod2 : forall e n T U,
typ e T (type n) ->
typ (T :: e) U (type n) ->
typ e (Prod T U) (type n).
Proof.
unfold typ, Prod; simpl; red; intros e n T U ty_T ty_U i is_val.
apply G_cc_prod.
apply ecc_grot.
red; red; intros.
rewrite H0; auto with *.
apply ty_T; trivial.
intros.
apply ty_U.
apply vcons_add_var; auto.
Qed.
Definition sub_typ_covariant := sub_typ_covariant.
End WithFinitistUniverse.
(** Universes: version where type 0 contains an infinite set,
hence nat can be in type 0.
*)
Module WithoutFinitistUniverse <: ECC.
Definition type (n:nat) := cst (ecc (S n)).
Lemma typ_Prop : forall e, typ e prop (type 0).
red; intros; simpl.
apply G_trans with (grot_succ (ZFcoc.props)); auto.
apply (ecc_grot 1).
apply (ecc_in1 0).
apply (ecc_in2 0).
Qed.
Lemma typ_Type : forall e n, typ e (type n) (type (S n)).
red; intros; simpl.
apply (ecc_in2 (S n)).
Qed.
Lemma cumul_Type : forall e n, sub_typ e (type n) (type (S n)).
red; simpl; intros.
red; intros.
apply ecc_incl with (n:=S n); trivial.
Qed.
Lemma cumul_Prop : forall e, sub_typ e prop (type 0).
red; simpl; intros.
red; intros.
apply G_trans with ZFcoc.props; trivial.
apply (ecc_grot 1).
apply G_trans with (grot_succ ZFcoc.props); trivial.
apply (ecc_grot 1).
apply (ecc_in1 0).
apply (ecc_in2 0).
Qed.
Lemma typ_prod2 : forall e n T U,
typ e T (type n) ->
typ (T :: e) U (type n) ->
typ e (Prod T U) (type n).
Proof.
red; intros e n T U ty_T ty_U i is_val.
apply G_cc_prod.
apply ecc_grot.
red; red; intros.
rewrite H0; auto with *.
apply ty_T; trivial.
intros.
red in ty_U.
change (int (type n) i) with (int (type n) (V.cons x i)).
apply in_int_not_kind.
2:discriminate.
apply ty_U.
apply vcons_add_var; auto.
Qed.
Definition sub_typ_covariant := sub_typ_covariant.
End WithoutFinitistUniverse.
(** By default we take the second version (without universe of HF) *)
Export WithoutFinitistUniverse.