-
Notifications
You must be signed in to change notification settings - Fork 2
/
SN_ord.v
154 lines (133 loc) · 3.18 KB
/
SN_ord.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
Require Import ZF ZFnats ZFord ZFcoc.
Require Import Sat.
Require Import ZFuniv_real SN_ECC_Real.
Module Lc := Lambda.
(** Typing rules for ordinals
*)
(** * Ordinals *)
Definition Ordt (o:set) : term :=
SN.T.cst (mkTY o (fun _ => snSAT)) Lc.K (fun _ _ => eq_refl) (fun _ _ _ => eq_refl).
Definition typ_ord_kind : forall e o, typ e (Ordt o) kind.
red; simpl; intros.
split; [|split]; simpl.
discriminate.
exists nil; exists (Ordt o);[reflexivity|].
exists zero; intros; simpl.
unfold inX; rewrite El_def; trivial.
apply Lc.sn_K.
Qed.
Lemma El_int_ord o i :
zero ∈ o ->
El (int (Ordt o) i) == o.
intros; simpl.
rewrite El_def.
apply eq_intro; intros; auto.
rewrite cc_bot_ax in H0; destruct H0; trivial.
rewrite H0; trivial.
Qed.
Definition OSucc : term -> term.
(*begin show*)
intros o; left; exists (fun i => osucc (int o i)) (fun j => tm o j).
(*end show*)
do 2 red; intros.
rewrite H; reflexivity.
(**)
do 2 red; intros.
rewrite H; reflexivity.
(**)
red; intros.
apply tm_liftable.
(**)
red; intros.
apply tm_substitutive.
Defined.
Definition OSucct : term -> term.
(*begin show*)
intros o; left; exists (fun i => mkTY (osucc (int o i)) (fun _ => snSAT)) (fun j => tm o j).
(*end show*)
do 2 red; intros.
apply mkTY_ext; auto with *.
rewrite H; reflexivity.
(**)
do 2 red; intros.
rewrite H; reflexivity.
(**)
red; intros.
apply tm_liftable.
(**)
red; intros.
apply tm_substitutive.
Defined.
Lemma El_int_osucc O' i :
El (int (OSucct O') i) == osucc (int O' i).
simpl; rewrite El_def.
apply eq_intro; intros; auto.
rewrite cc_bot_ax in H; destruct H; trivial.
rewrite H.
apply ole_lts; auto.
Qed.
Lemma tyord_inv : forall e i j o o',
isOrd o' ->
zero ∈ o' ->
typ e o (Ordt o') ->
val_ok e i j ->
isOrd (int o i) /\ int o i < o' /\ Lc.sn (tm o j).
unfold typ; intros.
specialize H1 with (1:=H2).
apply in_int_not_kind in H1.
2:discriminate.
destruct H1.
red in H1; rewrite El_int_ord in H1; trivial.
split;[apply isOrd_inv with o'; trivial|].
split; trivial.
apply sat_sn in H3; trivial.
Qed.
(** * Ordinal judgment *)
Definition typ_ord (e:env) (O:term) : Prop :=
forall i j, val_ok e i j -> isOrd (int O i) /\ Lc.sn (tm O j).
Lemma typ_ord_cst e o :
isOrd o ->
typ_ord e (cst o).
split; simpl; trivial.
apply Lc.sn_K.
Qed.
Hint Resolve typ_ord_cst.
Lemma OSucc_typ e O :
typ_ord e O ->
typ_ord e (OSucc O).
unfold typ_ord; intros.
destruct H with (1:=H0).
split; simpl; auto.
Qed.
Hint Resolve OSucc_typ.
Lemma typ_ord_varS e n T :
typ_ord e (Ref n) ->
typ_ord (T::e) (Ref (S n)).
unfold typ_ord; simpl; intros.
apply val_ok_shift1 in H0.
apply H with (1:=H0).
Qed.
Lemma typ_ord_var0_ord e O :
O <> kind ->
typ_ord e O ->
typ_ord (OSucct O::e) (Ref 0).
red; simpl; intros.
destruct (H1 0 _ eq_refl).
apply val_ok_shift1 in H1.
red in H0; specialize H0 with (1:=H1).
destruct H0 as (?,_).
destruct H3.
red in H3; rewrite int_lift_eq in H3.
apply sat_sn in H4; split; trivial.
apply cc_bot_ax in H3; destruct H3.
simpl in H3; rewrite H3; auto.
simpl in H3; rewrite Elt_def in H3.
apply isOrd_inv with (2:=H3); auto.
Qed.
Lemma typ_ord_var0 e o :
isOrd o ->
typ_ord (OSucct (cst o)::e) (Ref 0).
intros.
apply typ_ord_var0_ord; auto.
discriminate.
Qed.