-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathModelCC.v
140 lines (115 loc) · 3.16 KB
/
ModelCC.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
Require Import basic.
Require Import Sublogic.
Require Import Models GenModelSyntax.
Require Import ZF ZFrelations ZFcoc ModelZF.
(** Set-theoretical model of the Calculus of Constructions in IZF *)
(** * Instantiating the generic model construction *)
Module BuildModel := MakeModel(CCM).
Import BuildModel T J R.
Lemma El_int_arr T U i :
int (Prod T (lift 1 U)) i == cc_arr (int T i) (int U i).
simpl.
apply cc_prod_ext.
reflexivity.
red; intros.
rewrite simpl_int_lift.
rewrite lift0_term; reflexivity.
Qed.
(** Subtyping *)
(*
Definition sub_typ_covariant : forall 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).
intros.
apply sub_typ_covariant; trivial.
intros.
unfold eqX, lam, app.
unfold inX in H2.
unfold prod, ZFuniv_real.prod in H2; rewrite El_def in H2.
apply cc_eta_eq in H2; trivial.
Qed.
*)
(** Universes *)
(*
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 (grot_succ_typ gr).
apply (grot_succ_in gr).
Qed.
*)
(** The model in ZF implies the consistency of CC *)
Require Import Term Env.
Require Import TypeJudge.
Load "template/Library.v".
Lemma cc_consistency : forall M M', ~ eq_typ nil M M' FALSE.
Proof.
unfold FALSE; red in |- *; intros.
specialize BuildModel.int_sound with (1 := H); intro.
destruct H0 as (H0,_).
simpl in H0.
apply abstract_consistency with (M:=int_trm(unmark_app M)) (FF:=empty); trivial.
unfold props; apply empty_in_power.
red; intros.
apply empty_ax with (1:=H1); trivial.
Qed.
(*begin hide*)
Module TypChoice (C : Choice_Sig CoqSublogicThms IZF).
Import C.
Import BuildModel.
Import CCM.
Import T J R.
Require Import ZFrepl.
Definition CH_spec a f1 f2 z :=
a == empty /\ z == app f2 (lam empty (fun _ => empty))
\/ (exists w, w ∈ a) /\ z == app f1 (choose a).
Parameter CH_spec_u : forall a f1 f2, uchoice_pred (CH_spec a f1 f2).
Definition CH : term.
left; exists (fun i => uchoice (CH_spec (i 3) (i 1) (i 0))).
admit.
Defined.
(* forall X, X + (X->False) is inhabited *)
Lemma typ_choice :
typ
((*f1*)Prod (Prod (*X*)(Ref 2) (Prod prop (Ref 0))) (*P*)(Ref 2) ::
(*f2*)Prod (*X*)(Ref 1) (*P*)(Ref 1) ::
(*P*)kind::(*X*)kind::nil)
CH (*P*)(Ref 2).
red; simpl; intros.
generalize (H 0 _ (eq_refl _)); simpl; unfold V.lams, V.shift; simpl; intros.
generalize (H 1 _ (eq_refl _)); simpl; unfold V.lams, V.shift; simpl; intros.
clear H.
set (P := i 2) in *; clearbody P.
set (Y := i 3) in *; clearbody Y.
generalize (uchoice_def _ (CH_spec_u Y (i 1) (i 0))).
set (w := uchoice (CH_spec Y (i 1) (i 0))) .
clearbody w; unfold CH_spec; intros.
destruct H.
destruct H.
rewrite H2.
refine (prod_elim _ _ _ _ _ H0 _).
admit.
apply eq_elim with (prod empty (fun _ => prod props (fun P=>P))).
apply prod_ext.
auto with *.
red; reflexivity.
apply prod_intro; intros.
admit.
admit.
elim empty_ax with x; trivial.
destruct H.
rewrite H2.
refine (prod_elim _ _ _ _ _ H1 _).
admit.
apply choose_ax; trivial.
Qed.
End TypChoice.
(*end hide*)