-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtyped_recursion.v
331 lines (262 loc) · 13.8 KB
/
typed_recursion.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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
(**********************************************************************)
(* Copyright 2024 Barry Jay *)
(* *)
(* Permission is hereby granted, free of charge, to any person *)
(* obtaining a copy of this software and associated documentation *)
(* files (the "Software"), to deal in the Software without *)
(* restriction, including without limitation the rights to use, copy, *)
(* modify, merge, publish, distribute, sublicense, and/or sell copies *)
(* of the Software, and to permit persons to whom the Software is *)
(* furnished to do so, subject to the following conditions: *)
(* *)
(* The above copyright notice and this permission notice shall be *)
(* included in all copies or substantial portions of the Software. *)
(* *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, *)
(* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF *)
(* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND *)
(* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT *)
(* HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, *)
(* WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, *)
(* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
(**********************************************************************)
(**********************************************************************)
(* Typed Recursion *)
(* *)
(* Barry Jay *)
(* *)
(**********************************************************************)
Require Import String Arith Lia Bool List Nat Datatypes.
Require Import terms types subtypes derive typed_lambda.
Open Scope string_scope.
Open Scope nat_scope.
Set Default Proof Using "Type".
(*** Fixpoints *)
Theorem derive_Z:
forall k gamma f uty vty,
derive gamma f (Funty ((quant k (Funty uty vty))) ((quant k (Funty uty vty)))) ->
derive gamma (Z f) (quant k (Funty uty vty)).
Proof.
intros; eapply derive_generalisation_q; eapply derive_wait2; eauto; [ | |
eapply derive_generalisation2_q; eapply derive_subtype; eauto; eapply subtype_lift]; [
| eapply lift_rec_preserves_derive; eapply programs_have_types; program_tac];
eapply derive_subtype; [ eapply lift_rec_preserves_derive; eapply programs_have_types; program_tac |];
eapply sub_trans; [ | do 2 sub_fun_tac; eapply subtype_lift3];
unfold lift; rewrite <- ! lift_rec_funty; eapply lift_rec_preserves_subtype; eapply sub_recursion.
Qed.
Theorem derive_Y2:
forall gamma f uty vty,
derive gamma f (Funty uty (Funty (Funty uty vty) vty)) ->
derive gamma (Yop2 f) (Funty uty vty).
Proof.
intros; eapply derive_subtype; [ eapply (derive_Z 0); eapply derive_swap; eauto | apply sub_zero].
Qed.
(*** Booleans and Arithmetic *)
Definition Bool_ty := Quant (Funty (Var 0) (Funty (Var 0) (Var 0))).
Lemma derive_true: forall gamma, derive gamma K Bool_ty.
Proof. intro; repeat eapply derive_generalisation; eapply derive_K. Qed.
Lemma derive_false: forall gamma, derive gamma KI Bool_ty.
Proof.
intro; repeat eapply derive_generalisation; eapply derive_app; [eapply derive_K | eapply derive_I].
Qed.
Definition Nat_ty := Quant (Funty (Funty (Var 0) (Var 0)) (Funty (Var 0) (Var 0))).
Lemma derive_Kn : forall utys gamma ty, derive gamma (Kn (length utys)) (Funty ty (fold_right Funty ty utys)).
Proof.
induction utys; intros; simpl.
- eapply derive_I.
- rewrite orb_true_r; eapply derive_S2; [
eapply derive_K1; eapply derive_K |
eapply derive_S2; [ | eapply derive_I]; eapply derive_star; eauto].
Qed.
Lemma derive_compose1 :
forall utys gamma vty wty,
derive gamma (compose1 (length utys))
(Funty (fold_right Funty (Funty vty wty) utys)
(Funty (fold_right Funty vty utys)
(fold_right Funty wty utys)
)).
Proof.
induction utys; intros; simpl.
- eapply derive_I.
- rewrite ! orb_true_r; do 2 eapply derive_star; eapply derive_S2; [
eapply derive_S2; [ eapply derive_star; eapply IHutys |] |
eapply derive_S2; [ eapply derive_K1; eapply derive_ref; simpl; eauto; eapply sub_zero | eapply derive_I]];
eapply derive_S2; [ eapply derive_K1; eapply derive_ref; simpl; eauto; eapply sub_zero | eapply derive_I].
Qed.
Lemma derive_compose0 :
forall vtys gamma utys wty,
derive gamma (compose0 (length vtys) (length utys))
(Funty
(fold_right Funty (fold_right Funty wty vtys) utys) (* type of g *)
(fold_right Funty (fold_right Funty wty utys)
(map (fun vty => fold_right Funty vty utys) vtys) (* types of fs *)
)).
Proof.
induction vtys; intros; simpl.
- eapply derive_I.
- rewrite ! orb_true_r;
rewrite compose1_closed; unfold orb;
eapply derive_star; eapply derive_S2. eapply derive_star; eauto.
eapply derive_S2; [ | eapply derive_I]; eapply derive_K1;
eapply derive_app; [ eapply derive_compose1 |
eapply derive_ref; simpl; eauto; eapply sub_zero].
Qed.
Theorem derive_compose :
forall gamma vtys utys wty,
derive gamma (compose (length vtys) (length utys))
(Funty
(fold_right Funty wty vtys) (* type of g *)
(fold_right Funty (fold_right Funty wty utys)
(map (fun vty => fold_right Funty vty utys) vtys) (* types of fs *)
)).
Proof. intros; eapply derive_S2; [ eapply derive_K1; eapply derive_compose0 | eapply derive_Kn]. Qed.
Definition product uty vty :=
Quant (Funty (Funty (lift 1 uty) (Funty (lift 1 vty) (Var 0))) (Var 0)).
Theorem derive_pairL : forall gamma m n uty vty,
derive gamma m uty -> derive gamma n vty -> derive gamma (pairL m n) (product uty vty).
Proof.
intros; eapply derive_generalisation; eapply derive_S2; [ eapply derive_S2; [ eapply derive_I |] |]; eapply derive_K1; eapply lift_rec_preserves_derive; eauto.
Qed.
Theorem derive_fstL : forall gamma uty vty, derive gamma fstL (Funty (product uty vty) uty).
Proof.
intros; eapply derive_S2; [ eapply derive_subtype; [ eapply derive_I | sub_fun_tac; subst_tac] |
eapply derive_K1; eapply derive_K].
Qed.
Theorem derive_sndL : forall gamma uty vty, derive gamma sndL (Funty (product uty vty) vty).
Proof.
intros; eapply derive_S2; [ eapply derive_subtype; [ eapply derive_I | sub_fun_tac; subst_tac] |
eapply derive_K1; eapply derive_app; [ eapply derive_K | eapply derive_I]].
Qed.
Theorem derive_succ1: forall gamma, derive gamma succ1 (Funty Nat_ty Nat_ty).
Proof.
intros; eapply derive_subtype with
(quant 1 (Funty Nat_ty (Funty (Funty (Var 0) (Var 0)) (Funty (Var 0) (Var 0))))); [
|
dist_tac; [ eapply sub_trans; [ eapply sub_lift | cbv; eapply sub_zero] | eapply sub_zero]];
eapply derive_generalisation; eapply derive_app; [
|
eapply derive_app; [
eapply derive_node; eapply sub_leaf_fun |
repeat eapply derive_S2; repeat eapply derive_K1; [ | | eapply derive_K]; eapply derive_node; eapply sub_leaf_fun]];
eapply derive_node; eapply sub_trans; [ eapply subtype_leaf_fork | do 2 sub_fun_tac; repeat sub_fork2_tac; [ | subst_tac]; auto_t].
Qed.
Lemma num_closed: forall k x, occurs x (num k) = false.
Proof. induction k; intros; simpl; auto; rewrite IHk; auto. Qed.
Lemma derive_num: forall k gamma, derive gamma (num k) Nat_ty.
Proof.
induction k; intros; unfold num; fold num; simpl.
- eapply derive_generalisation; simpl; eapply derive_K1; eapply derive_I.
- replace (iter k (fun x => succ1 @ x) zero) with (num k) by auto; eapply derive_app; [ eapply derive_succ1 | eauto].
Qed.
Theorem derive_isZero: forall gamma, derive gamma isZero (Funty Nat_ty Bool_ty).
Proof.
intros; eapply derive_star; eapply derive_app; [ eapply derive_app | ]; [
eapply derive_subtype; [ eapply derive_ref; simpl; eauto; eapply sub_zero | subst_tac] |
eapply derive_K1; eapply derive_false |
eapply derive_true].
Qed.
Theorem derive_cond: forall gamma ty, derive gamma cond (Funty Bool_ty (Funty ty (Funty ty ty))).
Proof.
intros; eapply derive_S2; [ eapply derive_subtype; [ eapply derive_K | do 2 sub_fun_tac; subst_tac] | eapply derive_K].
Unshelve. apply Leaf.
Qed.
Proposition derive_PZero : forall gamma, derive gamma PZero (product Nat_ty Nat_ty).
Proof. intros; eapply derive_pairL; eapply derive_generalisation; eapply derive_K1; eapply derive_I. Qed.
Proposition derive_PSucc : forall gamma, derive gamma PSucc (Funty (product Nat_ty Nat_ty) (product Nat_ty Nat_ty)).
Proof.
intros; unfold PSucc; eapply derive_star; eapply derive_pairL; [
| eapply derive_app; [ eapply derive_succ1 |]];
(eapply derive_app; [ eapply derive_sndL
| eapply derive_ref; simpl; eauto]; eapply sub_zero).
Qed.
Theorem derive_predN : forall gamma, derive gamma predN (Funty Nat_ty Nat_ty).
Proof.
intros; unfold predN; eapply derive_star; eapply derive_app; [
eapply derive_fstL |];
eapply derive_app; [
eapply derive_app; [
eapply derive_ref; simpl; eauto; subst_tac |
eapply derive_PSucc] |
eapply derive_PZero].
Qed.
Proposition derive_primrec0:
forall gamma g h, derive gamma g Nat_ty -> derive gamma h (Funty Nat_ty (Funty Nat_ty Nat_ty)) ->
derive gamma (primrec0 g h) (Funty Nat_ty Nat_ty).
Proof.
intros; unfold primrec0; eapply derive_Y2; repeat eapply derive_S2; try eapply derive_K1; eauto; try eapply derive_K;
try eapply derive_predN; [
| |
eapply derive_subtype; [ eapply derive_isZero | sub_fun_tac; subst_tac] | | |
eapply derive_app; [ | eapply derive_app; [ | eapply derive_I]; eapply derive_node; eapply sub_leaf_fun]];
eapply derive_node; try eapply sub_leaf_fun; try eapply subtype_leaf_fork;
eapply sub_trans; [ eapply subtype_leaf_fork | do 2 sub_fun_tac; auto_t].
Unshelve. all: apply Leaf.
Qed.
Theorem derive_primrec:
forall gamma xs g h, derive gamma g (iter (length xs) (Funty Nat_ty) Nat_ty) ->
derive gamma h (iter (2 + length xs) (Funty Nat_ty) Nat_ty) ->
Forall (fun x => derive gamma x Nat_ty) xs ->
derive gamma (primrec g h xs) (Funty Nat_ty Nat_ty).
Proof.
intros; unfold primrec; eapply derive_primrec0.
- generalize g H H1; clear; induction xs; intros; simpl in *; auto; eapply IHxs; [
eapply derive_app; eauto; inv_out H1; auto |
inv_out H1; auto].
- generalize h H0 H1; clear; induction xs; intros; simpl in *; auto; eapply IHxs; [
eapply derive_app; eauto; inv_out H1; auto | inv_out H1; auto].
Qed.
Proposition derive_minrec0:
forall gamma f, derive gamma f (Funty Nat_ty Bool_ty) ->
derive gamma (minrec0 f) (Funty Nat_ty Nat_ty).
Proof.
intros; eapply derive_Y2; eapply derive_S2; [
|
eapply derive_S2; [
eapply derive_app; [
eapply derive_K |
eapply derive_app; [
eapply derive_node; eapply subtype_leaf_fork |
eapply derive_app; [ eapply derive_node; eapply sub_leaf_fun | eapply derive_I]]] |
eapply derive_star; eapply derive_app; [ eapply derive_K |
eapply derive_app; [ eapply derive_succ1 |]]; eapply derive_ref; simpl; eauto; eapply sub_zero]];
repeat eapply derive_app;
try eapply derive_node;
try eapply derive_ref;
try eapply sub_zero;
try eapply sub_leaf_stem;
try eapply sub_leaf_fork;
try eapply sub_leaf_fun;
try eapply subtype_leaf_fork;
eauto;
eapply sub_trans; [ eapply subtype_leaf_fork | do 2 sub_fun_tac];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_fork_leaf | sub_fun_tac];
eapply sub_trans; [ eapply subtype_leaf_fork | do 2 sub_fun_tac];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_fork_leaf |
eapply sub_trans; [ eapply sub_fork |eapply sub_fork_stem]; eapply sub_zero] |];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [eapply sub_fork_leaf |]; sub_fun_tac; eapply sub_leaf_fun |];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_fork_leaf | sub_fun_tac]; eapply sub_stem_fun |];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_fork_leaf | do 2 sub_fun_tac; subst_tac] |];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_stem_fun | sub_fun_tac]; eapply sub_fork_leaf |];
eapply sub_stem_fun |];
eapply sub_trans; [ eapply sub_fork | eapply sub_fork_stem]; [
eapply sub_stem; eapply sub_trans; [ eapply sub_stem_fun | sub_fun_tac; eapply sub_fork_leaf] |];
eapply sub_stem_fun.
Qed.
Theorem derive_minrec:
forall gamma xs f, derive gamma f (iter (length xs) (Funty Nat_ty) (Funty Nat_ty Bool_ty)) ->
Forall (fun x => derive gamma x Nat_ty) xs ->
derive gamma (minrec f xs) (Funty Nat_ty Nat_ty).
Proof.
intros; unfold minrec; eapply derive_minrec0;
generalize f H H0; clear; induction xs; intros; simpl in *; auto; eapply IHxs; [
eapply derive_app; eauto; inv_out H0; auto |
inv_out H0; auto].
Qed.