-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathterm.v
388 lines (348 loc) · 16.5 KB
/
term.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
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
(** * Annotated Terms syntax
In this file, we describe a slightly different syntax for terms: we add two
annotations to applications. If the head of an application if a function from
[A] to [B], we had both informations in the application, in order to keep
track of the conversion during the typing that would be impossible to rebuild
after.
*)
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.
Unset Standard Proposition Elimination Names.
(** Term syntax. Notice the two additional [Term] in the application.*)
Module Type term_mod (X:term_sig).
Import X.
Inductive Term : Set:=
| Var : Vars -> Term
| Sort : Sorts -> Term
| App : Term -> Term -> Term -> Term -> Term
| Pi : Term -> Term -> Term
| La :Term -> Term -> Term
.
(** this notation means that the product x y is annotated by the function space
A -> B.**)
Notation "x ·( A , B ) y" := (App x A B y) (at level 15, left associativity) : Typ_scope.
Notation "! s" := (Sort s) (at level 1) : Typ_scope.
Notation "# v" := (Var v) (at level 1) : Typ_scope.
Notation "'Π' ( U ) , V " := (Pi U V) (at level 20, U, V at level 30) : Typ_scope.
Notation "'λ' [ U ] , v " := (La U v) (at level 20, U , v at level 30) : Typ_scope.
Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity).
Delimit Scope Typ_scope with Typ.
(** Same as for usual terms, we need lift and subst functions, with the very
same properties. They are just extended to deal with the two annotations.*)
Open Scope Typ_scope.
(* lift c n times *)
Fixpoint lift_rec (n:nat) (k:nat) (T:Term) {struct T} := match T with
| # x => if le_gt_dec k x then Var (n+x) else Var x
| ! s => Sort s
| M ·(A, B) N=> App (M ↑ n # k) (A↑ n # k) (B ↑ n # (S k)) (N ↑ n # k)
| Π ( A ), B => Π (A ↑ n # k), (B ↑ n # (S k))
| λ [ A ], M => λ [A ↑ n # k], (M ↑ n # (S k))
end
where "t ↑ n # k" := (lift_rec n k t) : Typ_scope.
Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity) : Typ_scope.
Lemma inv_lift : forall M N n m , M ↑ n # m = N ↑ n # m -> M = N.
intros M; induction M; destruct N; intros;
simpl in *; try (discriminate || intuition); (try (destruct (le_gt_dec m v) ; discriminate)).
destruct (le_gt_dec m v); destruct (le_gt_dec m v0) ; injection H; intros; subst; intuition.
apply plus_reg_l in H0; rewrite H0; trivial.
elim (lt_irrefl m). apply le_lt_trans with v. trivial. induction n; intuition.
elim (lt_irrefl v0). apply lt_le_trans with m. induction n; intuition. trivial.
injection H; intros; subst; clear H. rewrite (IHM1 N1 n m H3); rewrite (IHM2 N2 n m H2);
rewrite (IHM3 N3 n (S m) H1); rewrite (IHM4 N4 n m H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
Qed.
Lemma lift_rec0 : forall M n, M ↑ 0 # n = M.
induction M; intros; simpl.
destruct (le_gt_dec n v); reflexivity.
reflexivity.
rewrite IHM1; rewrite IHM2; rewrite IHM3; rewrite IHM4; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
Qed.
Lemma lift0 : forall M, M ↑ 0 = M .
intros; apply lift_rec0.
Qed.
Lemma liftP1 : forall M i j k, (M ↑ j # i) ↑ k # (j+i) = M ↑ (j+k) # i.
intros M; induction M; intros;simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec (j+i) (j+v)); simpl.
rewrite plus_assoc. replace (k+j) with (j+k) by (apply plus_comm). trivial.
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with i; intuition.
simpl; destruct (le_gt_dec (j+i)); intuition.
elim (lt_irrefl v).
apply lt_le_trans with i; intuition. induction j; intuition.
reflexivity.
rewrite IHM1. rewrite IHM2. rewrite IHM4. rewrite <- IHM3.
replace (j+S i) with (S(j+i)) by intuition. trivial.
rewrite IHM1; rewrite <-IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
rewrite IHM1; rewrite <- IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
Qed.
Lemma liftP2: forall M i j k n, i <= n ->
(M ↑ j # i) ↑ k # (j+n) = (M ↑ k # n) ↑ j # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (le_gt_dec n v).
simpl.
destruct le_gt_dec. destruct le_gt_dec.
rewrite 2! plus_assoc. replace (k+j) with (j+k) by (apply plus_comm). trivial.
elim (lt_irrefl v). apply lt_le_trans with i. induction k; intuition. trivial.
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with n; intuition.
simpl.
destruct le_gt_dec. apply plus_le_reg_l in l0. elim (lt_irrefl v).
apply lt_le_trans with n; intuition. destruct le_gt_dec. trivial.
elim (lt_irrefl v). apply lt_le_trans with i; intuition.
simpl. destruct le_gt_dec. elim (lt_irrefl n). apply lt_le_trans with i.
apply le_lt_trans with v; intuition. trivial. elim (lt_irrefl v).
apply lt_le_trans with n. apply lt_le_trans with i; intuition. trivial.
simpl. destruct le_gt_dec. elim (lt_irrefl v). apply lt_le_trans with n.
intuition. induction j; intuition. destruct le_gt_dec. elim (lt_irrefl i).
apply le_lt_trans with v; intuition. trivial.
trivial.
rewrite IHM1; intuition. replace (S(j+n)) with (j+S n) by intuition.
rewrite IHM2; intuition. rewrite IHM3; intuition. rewrite IHM4; intuition.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n)); intuition.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n) ); intuition.
Qed.
Lemma liftP3 : forall M i k j n , i <= k -> k <= (i+n) ->
(M ↑ n # i) ↑ j # k = M ↑ (j+n) # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec k (n+v)); intuition.
elim (lt_irrefl (i+n)). apply lt_le_trans with k.
apply le_lt_trans with (n+v). rewrite plus_comm. intuition. intuition. trivial.
destruct (le_gt_dec k v); intuition. elim (lt_irrefl k).
apply lt_le_trans with i. apply le_lt_trans with v. trivial. intuition. trivial.
reflexivity.
rewrite IHM1; intuition. rewrite IHM2; intuition. rewrite IHM3; intuition. rewrite IHM4; intuition.
change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition;rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
Qed.
Lemma lift_lift : forall M n m, (M ↑ m) ↑ n = M ↑ (n+m).
intros.
apply liftP3; intuition.
Qed.
(* i = index to replace
t = term we are replacing
k = limit between free and bound indices
*)
Reserved Notation "M [ n ← N ]" (at level 5, n at level 0, left associativity).
Fixpoint subst_rec U T n {struct T} :=
match T with
| # x => match (lt_eq_lt_dec x n) with
| inleft (left _) => # x (* x < n *)
| inleft (right _) => U ↑ n (* x = n *)
| inright _ => # (x - 1) (* x > n *)
end
| ! s => ! s
| M ·(A,B) N => (M [ n ← U ]) ·(A[n← U], B [ S n ← U]) ( N [ n ← U ])
| Π ( A ), B => Π ( A [ n ← U ] ), (B [ S n ← U ])
| λ [ A ], M => λ [ A [ n ← U ] ], (M [ S n ← U ])
end
where " t [ n ← w ] " := (subst_rec w t n) : Typ_scope.
Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5) : Typ_scope.
Lemma expand_term_with_subst : forall M n, (M ↑ 1 # (S n)) [ n ← #0 ] = M.
induction M; intros.
unfold lift_rec.
destruct (le_gt_dec (S n) v). unfold subst_rec.
destruct (lt_eq_lt_dec (1+v) n) as [[] | ].
apply le_not_lt in l. elim l. intuition.
elim (lt_irrefl v). apply lt_le_trans with (S (S v)). intuition. subst; trivial.
change (1+v) with (S v). destruct v; simpl; trivial.
simpl.
destruct (lt_eq_lt_dec v n) as [[] | ].
trivial.
simpl; subst; trivial.
rewrite <- plus_n_O. trivial.
elim (lt_irrefl n). apply lt_le_trans with v; intuition.
simpl; trivial.
simpl. rewrite IHM1. rewrite IHM2. rewrite IHM3. rewrite IHM4. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
Qed.
Lemma substP1: forall M N i j k ,
( M [ j ← N] ) ↑ k # (j+i) = (M ↑ k # (S (j+i))) [ j ← (N ↑ k # i ) ].
intros M; induction M; intros.
simpl (#v [j ← N] ↑ k # (j+i)).
change (#v ↑ k # (S (j+i))) with (if le_gt_dec (S (j+i)) v then #(k+v) else #v).
destruct (lt_eq_lt_dec v j) as [[] | ].
destruct (le_gt_dec (S (j+i)) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition.
apply le_trans with (S (j+i)); intuition.
simpl.
destruct (le_gt_dec (j+i) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition. apply le_trans with (j+i); intuition.
destruct (lt_eq_lt_dec v j) as [[] | ]. trivial.
subst. elim (lt_irrefl j);trivial.
elim (lt_irrefl j); apply lt_trans with v; trivial.
destruct (le_gt_dec (S(j+i)) v). subst.
elim (lt_irrefl j). apply lt_le_trans with (S (j+i)). intuition. trivial.
simpl. destruct (lt_eq_lt_dec v j) as [[] | ].
subst. elim (lt_irrefl j); trivial.
apply liftP2; intuition.
subst. elim (lt_irrefl j); trivial.
destruct (le_gt_dec (S (j+i)) v).
simpl.
destruct (le_gt_dec (j+i) (v-1)). destruct (lt_eq_lt_dec (k+v) j) as [[] | ].
elim (lt_irrefl j). apply lt_le_trans with v. trivial. induction k; intuition.
subst. elim (lt_irrefl v). apply lt_le_trans with (S(k+v+i)). intuition. trivial.
destruct v. apply lt_n_O in l; elim l. rewrite <- 2! pred_of_minus. replace (k+ S v) with (S (k+v)) by intuition.
simpl. trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). destruct v. apply lt_n_O in l; elim l.
rewrite <- pred_of_minus in g. simpl in g. intuition. trivial.
simpl.
destruct (le_gt_dec (j+i) (v-1)). destruct (lt_eq_lt_dec v j) as [[] | ].
elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). intuition.
destruct v. apply lt_n_O in l; elim l. rewrite <- pred_of_minus in l0. simpl in l0. intuition.
destruct (lt_eq_lt_dec) as [[] | ]. elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial. trivial.
simpl; trivial.
simpl. rewrite IHM1; intuition; rewrite IHM2; intuition. rewrite IHM4; intuition.
replace (S(S(j+i))) with (S((S j)+i)) by intuition.
rewrite <- (IHM3 N i (S j) k ); intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with (S((S j)+i)) by intuition.
rewrite <- (IHM2 N i (S j) k ); intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with ((S ((S j)+i))) by intuition.
rewrite <- (IHM2 N i (S j) k ); intuition.
Qed.
Lemma substP2: forall M N i j n, i <= n ->
(M ↑ j # i ) [ j+n ← N ] = ( M [ n ← N]) ↑ j # i .
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v n) as [[] | ].
simpl.
destruct (le_gt_dec i v). destruct (lt_eq_lt_dec (j+v) (j+n)) as [[] | ].
reflexivity.
apply plus_reg_l in e. subst. elim (lt_irrefl n); trivial.
apply plus_lt_reg_l in l2. elim (lt_asym v n); trivial.
elim (lt_irrefl i). apply le_lt_trans with v; intuition. subst.
simpl.
destruct (lt_eq_lt_dec (j+n) (j+n)) as [[] | ].
apply lt_irrefl in l0; elim l0.
symmetry.
apply liftP3; intuition.
apply lt_irrefl in l0; elim l0.
simpl.
destruct (le_gt_dec i (v-1)). destruct (lt_eq_lt_dec (j+v) (j+n))as [[] | ].
apply plus_lt_reg_l in l2. elim (lt_asym v n ); trivial.
apply plus_reg_l in e; subst. elim (lt_irrefl n); trivial.
destruct v. apply lt_n_O in l0; elim l0. rewrite <- 2! pred_of_minus. replace (j+ S v) with (S (j+v)) by intuition.
simpl. trivial.
unfold gt in g. unfold lt in g. rewrite <- pred_of_minus in g.
rewrite <- (S_pred v n l0) in g.
elim (lt_irrefl n). apply lt_le_trans with v; trivial. apply le_trans with i; trivial.
simpl.
destruct (le_gt_dec i v). elim (lt_irrefl i). apply le_lt_trans with v; trivial.
destruct (lt_eq_lt_dec v (j+n)) as [[] | ]. reflexivity.
subst. elim (lt_irrefl n). apply le_lt_trans with (j+n); intuition.
elim (lt_irrefl n). apply lt_trans with v. apply le_lt_trans with (j+n); intuition. trivial.
simpl. subst.
elim (lt_irrefl n). apply lt_le_trans with i; intuition.
simpl. elim (lt_irrefl n). apply lt_le_trans with v; intuition.
apply le_trans with i; intuition.
trivial.
rewrite IHM1; intuition. replace (S(j+n)) with (j+(S n)) by intuition. rewrite IHM3; intuition.
rewrite IHM2; intuition; rewrite IHM4; intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
Qed.
Lemma substP3: forall M N i k n, i <= k -> k <= i+n ->
(M↑ (S n) # i) [ k← N] = M ↑ n # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v).
unfold subst_rec.
destruct (lt_eq_lt_dec (S(n+v)) k) as [[] | ].
elim (lt_irrefl (i+n)). apply lt_le_trans with k; intuition.
apply le_lt_trans with (v+n). intuition. rewrite plus_comm; intuition.
subst. replace (i+n) with (n+i) in H0 by (apply plus_comm) . replace (S (n+v)) with (n + S v) in H0 by intuition.
apply plus_le_reg_l in H0. elim (lt_irrefl i). apply le_lt_trans with v; intuition.
simpl. rewrite <- minus_n_O. trivial.
simpl. destruct (lt_eq_lt_dec v k) as [[] | ].
reflexivity. subst. elim (lt_irrefl i). apply le_lt_trans with k; intuition.
elim (lt_irrefl k). apply lt_trans with v; trivial. apply lt_le_trans with i; intuition.
reflexivity.
rewrite IHM1; intuition;rewrite IHM4; intuition.
rewrite IHM2; intuition. change (S i + n) with (S (i+n)). rewrite IHM3; intuition.
change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
Qed.
Lemma substP4: forall M N P i j,
(M [ i← N]) [i+j ← P] = (M [S(i+j) ← P]) [i← N[j← P]].
intro M; induction M; intros; simpl.
destruct (lt_eq_lt_dec v i) as [[] | ] ; destruct (lt_eq_lt_dec v (S(i+j))) as [[] | ].
simpl.
destruct (lt_eq_lt_dec v (i+j)) as [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
trivial.
subst. apply lt_irrefl in l; elim l. elim ( lt_asym v i); trivial.
subst. rewrite plus_comm in l. elim (lt_irrefl i). induction j; simpl in *; intuition.
elim (lt_irrefl i). apply le_lt_trans with v;intuition. rewrite plus_comm in l1; intuition. induction j; simpl in *; intuition.
subst. elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition.
elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition. apply lt_trans with v; trivial.
simpl. subst. destruct (lt_eq_lt_dec i i) as [[] | ].
elim (lt_irrefl i); trivial. apply substP2; intuition.
elim (lt_irrefl i); trivial.
subst v. rewrite plus_comm in e0. apply succ_plus_discr in e0. elim e0.
subst. elim (lt_irrefl i). apply le_lt_trans with (i+j); intuition.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
elim (lt_asym v i); trivial. subst. elim (lt_irrefl i); trivial.
trivial. rewrite <- e in l0. rewrite <- pred_of_minus in l0.
rewrite <- (S_pred v i l) in l0. elim (lt_irrefl v); trivial.
apply lt_n_S in l1. elim (lt_irrefl v).
apply lt_trans with (S(i+j)); trivial.
rewrite <- pred_of_minus in l1. rewrite <- (S_pred v i l) in l1. trivial.
subst. simpl. rewrite <- minus_n_O.
destruct (lt_eq_lt_dec (i+j) (i+j)) as [[] | ].
elim (lt_irrefl (i+j)) ; trivial.
symmetry. apply substP3; intuition.
elim (lt_irrefl (i+j)) ; trivial.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ].
elim (lt_irrefl v). apply lt_trans with (S (i+j)) ;trivial.
apply lt_n_S in l1. rewrite <- pred_of_minus in l1. rewrite <- (S_pred v i l) in l1. trivial.
apply eq_S in e. rewrite <- pred_of_minus in e. rewrite <- (S_pred v i l) in e.
subst. elim (lt_irrefl (S(i+j))); trivial.
destruct (lt_eq_lt_dec (v-1) i) as [[] | ].
elim (lt_irrefl v). apply le_lt_trans with i; trivial. destruct v. apply lt_n_O in l; elim l.
rewrite <- pred_of_minus in l2. simpl in l2. trivial.
destruct v. elim (lt_n_O i); trivial. rewrite <- pred_of_minus in e. simpl in e. subst.
rewrite <- pred_of_minus in l1. simpl in l1. elim (lt_irrefl i).
apply le_lt_trans with (i+j); intuition.
trivial.
trivial.
rewrite IHM1; rewrite IHM4; intuition. rewrite IHM2; intuition.
replace (S(S(i+j))) with (S((S i)+ j)) by intuition. rewrite <- IHM3; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+ j)) by intuition;
rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+j)) by intuition;
rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
Qed.
Lemma subst_travers :
forall M N P n, (M [← N]) [n ← P] = (M [n+1 ← P])[← N[n← P]].
intros.
rewrite plus_comm. change n with (O+n). apply substP4.
Qed.
End term_mod.