-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathEquiv_Tuples.v
373 lines (321 loc) · 15.2 KB
/
Equiv_Tuples.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
(*
============================================================================
Project : Nominal A, AC and C Unification
File : Equiv_Tuples.v
Authors : Washington Luis R. de Carvalho Segundo and
Mauricio Ayala Rincon
Universidade de Brasilia (UnB) - Brazil
Group of Theory of Computation
Description : This file contains preliminaries results about
tuples and the relation ~aacc .
Last Modified On: Sep 17, 2018.
============================================================================
*)
Require Export Equiv Omega.
Lemma aacc_equiv_TPlength : forall C t1 t2 E n,
C |- t1 ~aacc t2 -> TPlength t1 E n = TPlength t2 E n.
Proof.
intros. induction H; trivial. simpl; auto.
case (nat_pair_eqdec (E0,n0) (E,n)); intro H1. inverts H1.
autorewrite with tuples; trivial.
rewrite 2 TPlength_Fc_diff; trivial.
case (nat_pair_eqdec (0,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples.
case (nat_eqdec (TPlength t 0 n) 1); case (nat_eqdec (TPlength t' 0 n) 1);
intros H2 H3; try omega.
rewrite TPithdel_TPlength_1 in H1;
autorewrite with tuples; try omega.
rewrite TPithdel_Fc_eq in H1; try omega. inverts H1.
rewrite TPithdel_Fc_eq in H1; try omega.
rewrite TPithdel_TPlength_1 with (t:=Fc 0 n t') in H1;
autorewrite with tuples; try omega. inverts H1.
rewrite 2 TPithdel_Fc_eq in IHequiv2; try omega.
autorewrite with tuples in IHequiv2;
rewrite 2 TPlength_TPithdel in IHequiv2; try omega.
rewrite 2 TPlength_Fc_diff; trivial.
case (nat_pair_eqdec (1,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples.
case (nat_eqdec (TPlength t 1 n) 1); case (nat_eqdec (TPlength t' 1 n) 1);
intros H2 H3; try omega.
rewrite TPithdel_TPlength_1 in H1;
autorewrite with tuples; try omega.
rewrite TPithdel_Fc_eq in H1; try omega. inverts H1.
rewrite TPithdel_Fc_eq in H1; try omega.
rewrite TPithdel_TPlength_1 with (t:=Fc 1 n t') in H1;
autorewrite with tuples; try omega. inverts H1.
rewrite 2 TPithdel_Fc_eq in IHequiv2; try omega.
autorewrite with tuples in IHequiv2;
rewrite 2 TPlength_TPithdel in IHequiv2; try omega.
rewrite 2 TPlength_Fc_diff; trivial.
case (nat_pair_eqdec (2,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples. simpl. omega.
rewrite 2 TPlength_Fc_diff; trivial.
case (nat_pair_eqdec (2,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples. simpl. omega.
rewrite 2 TPlength_Fc_diff; trivial.
Qed.
Lemma aacc_equiv_TPith_l1 : forall C t t' E n, C |- t ~aacc t' ->
exists j, j > 0 /\ j <= TPlength t' E n /\
C |- TPith 1 t E n ~aacc TPith j t' E n /\
C |- TPithdel 1 t E n ~aacc TPithdel j t' E n.
Proof.
intros. induction H; intros.
exists 1. simpl; split~. exists 1. simpl; split~.
generalize H. intro H'.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H'.
case IHequiv1; trivial. intros j Hj. clear IHequiv1 IHequiv2.
destruct Hj. destruct H2. destruct H3. exists j.
simpl TPlength. rewrite 2 TPith_Pr_le; try omega; auto.
case (nat_eqdec (TPlength t1' E n) 1); intro H5.
rewrite 2 TPithdel_t1_Pr; try omega. repeat split~; try omega; trivial.
rewrite 2 TPithdel_Pr_le; try omega; trivial.
repeat split~; try omega; auto.
destruct IHequiv. destruct H1. destruct H2. destruct H3.
generalize H0; intro H0'.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H0.
case (nat_pair_eqdec (E0,n0) (E,n)); intro H5. inverts H5. exists x.
autorewrite with tuples. repeat split~; trivial.
case (nat_eqdec (TPlength t E n) 1); intro H5.
rewrite 2 TPithdel_TPlength_1; autorewrite with tuples; try omega; auto.
rewrite 2 TPithdel_Fc_eq; try omega; auto.
destruct H. apply equiv_Fc. left~. trivial.
destruct H. rewrite H in *|-*. apply equiv_Fc_c; trivial.
exists 1. rewrite TPlength_Fc_diff; trivial.
rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_TPlength_1; try rewrite TPlength_Fc_diff; trivial.
repeat split~; auto.
exists 1. simpl; split~. exists 1. simpl; split~.
exists 1. simpl; split~.
exists 1. clear IHequiv1 IHequiv2.
case (nat_pair_eqdec (0,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples in *|-*. repeat split~; try omega; trivial.
rewrite TPlength_Fc_diff; trivial. rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_Fc_diff; trivial. repeat split~; try omega; auto.
case (nat_pair_eqdec (1,n0) (E,n)); intro H2. inverts H2.
case (nat_eqdec i 0); intro H2.
exists 1. rewrite H2 in *|-; rewrite TPith_0 in *|-; rewrite TPithdel_0 in *|-.
autorewrite with tuples in *|-*. repeat split~; try omega; trivial.
case (le_dec i (TPlength t' 1 n)); intro H3.
exists i. autorewrite with tuples in *|-*. repeat split~; try omega; trivial.
exists (TPlength t' 1 n).
rewrite TPith_overflow with (i:=i) in H0; autorewrite with tuples in *|-*; try omega.
rewrite TPithdel_overflow with (i:=i) in H1; autorewrite with tuples in * |-*; try omega.
repeat split~; try omega; trivial.
exists 1. rewrite TPlength_Fc_diff in *|-*; trivial. rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_Fc_diff; trivial. repeat split~; try omega; auto.
apply equiv_AC with (i:=i); trivial.
case (nat_pair_eqdec (2,n0) (E,n)); intro H2. inverts H2.
generalize H0. intro H'.
apply aacc_equiv_TPlength with (E:=2) (n:=n) in H'.
case IHequiv1; trivial. intros j Hj. clear IHequiv1 IHequiv2.
destruct Hj. destruct H3. destruct H4.
exists j. autorewrite with tuples. simpl TPlength.
rewrite 2 TPith_Pr_le; try omega; auto.
rewrite 2 TPithdel_Fc_eq. repeat split~; try omega.
case (nat_eqdec (TPlength s0 2 n) 1); intros H6.
assert (Q:j=1). omega. rewrite Q in *|-*; trivial.
rewrite 2 TPithdel_t1_Pr; try omega.
apply equiv_Fc_c; trivial.
rewrite 2 TPithdel_Pr_le; try omega. apply equiv_C1; trivial.
assert (Q0 : TPlength t1 2 n >= 1). auto. simpl; try omega.
assert (Q1 : TPlength s1 2 n >= 1). auto. simpl; try omega.
exists 1. rewrite TPlength_Fc_diff; trivial.
rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_TPlength_1;
try rewrite TPlength_Fc_diff; trivial.
try omega. repeat split~.
case (nat_pair_eqdec (2,n0) (E,n)); intro H2. inverts H2.
generalize H0. intro H'.
apply aacc_equiv_TPlength with (E:=2) (n:=n) in H'.
case IHequiv1; trivial. intros j Hj. clear IHequiv1 IHequiv2.
destruct Hj. destruct H3. destruct H4.
exists (TPlength t0 2 n + j). autorewrite with tuples. simpl TPlength.
rewrite TPith_Pr_le; try omega; auto.
rewrite TPith_Pr_gt; try omega; auto.
replace (TPlength t0 2 n + j - TPlength t0 2 n) with j; try omega.
rewrite 2 TPithdel_Fc_eq. repeat split~; try omega.
case (nat_eqdec (TPlength s0 2 n) 1); intros H6.
assert (Q:j=1). omega. rewrite Q in *|-*; trivial.
rewrite TPithdel_t1_Pr; try omega.
rewrite TPithdel_t2_Pr; try omega.
apply equiv_Fc_c; trivial.
rewrite TPithdel_Pr_le; try omega.
rewrite TPithdel_Pr_gt; try omega.
replace (TPlength t0 2 n + j - TPlength t0 2 n) with j; try omega.
apply equiv_C2; trivial.
assert (Q0 : TPlength t0 2 n >= 1). auto. simpl; try omega.
assert (Q1 : TPlength s1 2 n >= 1). auto. simpl; try omega.
exists 1. rewrite TPlength_Fc_diff; trivial.
rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_TPlength_1;
try rewrite TPlength_Fc_diff; trivial.
try omega. repeat split~.
Qed.
Lemma aacc_equiv_TPith_E_diff_1_2 : forall C t t' i E n,
~ set_In E (1::|[2]|) -> C |- t ~aacc t' ->
(C |- TPith i t E n ~aacc TPith i t' E n /\
C |- TPithdel i t E n ~aacc TPithdel i t' E n).
Proof.
intros. gen i. induction H0; intro.
simpl; split~. simpl; split~.
generalize H0_ H0_0. intros H0' H0_0'.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H0_.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H0_0.
case (le_dec i (TPlength t1 E n)); intro H1.
rewrite 2 TPith_Pr_le; try omega.
case (nat_eqdec (TPlength t1 E n) 1); intro H2.
rewrite 2 TPithdel_t1_Pr; try omega.
split~; trivial. apply IHequiv1.
rewrite 2 TPithdel_Pr_le; try omega.
split~. apply IHequiv1. apply equiv_Pr; trivial. apply IHequiv1.
rewrite 2 TPith_Pr_gt; try omega.
case (nat_eqdec (TPlength t2 E n) 1); intro H2.
rewrite TPithdel_t2_Pr; try omega. rewrite H0_.
rewrite TPithdel_t2_Pr; try omega.
split~; trivial. apply IHequiv2.
rewrite 2 TPithdel_Pr_gt; try omega.
rewrite H0_. split~. apply IHequiv2.
apply equiv_Pr; trivial. apply IHequiv2.
generalize H1; intro H1'.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H1.
case (nat_pair_eqdec (E0,n0) (E,n)); intro H2. inverts H2.
autorewrite with tuples in *|-*. split~. apply IHequiv.
case (nat_eqdec (TPlength t E n) 1); intro H2.
rewrite 2 TPithdel_TPlength_1;
autorewrite with tuples; try omega; auto.
rewrite 2 TPithdel_Fc_eq; try omega. destruct H0.
apply equiv_Fc; trivial. left~. apply IHequiv. destruct H0.
rewrite H0 in *|-*. apply equiv_Fc_c. apply IHequiv.
rewrite 2 TPithdel_TPlength_1; try rewrite TPlength_Fc_diff; trivial.
rewrite 2 TPith_Fc_diff; trivial. split~; auto.
simpl; split~. simpl; split~. simpl; split~.
clear H0 IHequiv1.
case (nat_pair_eqdec (0,n0) (E,n)); intro H1. inverts H1. clear H.
case (le_dec i 1); intro H2. case (nat_eqdec i 0); intro H3; try rewrite H3;
repeat rewrite TPith_0; repeat rewrite TPithdel_0. split~; trivial.
assert (Qi:i=1). omega. rewrite Qi. split~; trivial.
autorewrite with tuples in *|-*.
assert (Q: C |- Fc 0 n t ~aacc Fc 0 n t').
apply equiv_A; simpl set_In; try omega; autorewrite with tuples; trivial.
apply aacc_equiv_TPlength with (E:=0) (n:=n) in Q.
autorewrite with tuples in Q. case (nat_eqdec (TPlength t 0 n) 1); intro H1.
rewrite 2 TPithdel_TPlength_1;
try rewrite 2 TPith_overflow with (i:=i);
autorewrite with tuples; try omega. rewrite <- Q. rewrite H1; split~; trivial.
rewrite 2 TPithdel_Fc_eq in *|-*; try omega.
case (le_dec i (TPlength t 0 n)); intro H3.
assert (Q1: C |- TPith (i-1) (Fc 0 n (TPithdel 1 t 0 n)) 0 n ~aacc
TPith (i-1) (Fc 0 n (TPithdel 1 t' 0 n)) 0 n /\
C |- TPithdel (i-1) (Fc 0 n (TPithdel 1 t 0 n)) 0 n ~aacc
TPithdel (i-1) (Fc 0 n (TPithdel 1 t' 0 n)) 0 n).
apply IHequiv2. clear IHequiv2.
destruct Q1. autorewrite with tuples in H.
rewrite 2 TPith_TPithdel_geq in H; try omega.
replace (i - 1 + 1) with i in H; try omega; trivial.
split~; trivial. apply equiv_A; simpl set_In; try omega.
autorewrite with tuples. rewrite 2 TPith_TPithdel_lt; try omega; trivial.
case (nat_eqdec (TPlength t 0 n) 2); intro H4.
rewrite 2 TPithdel_TPlength_1; auto; autorewrite with tuples;
try rewrite TPlength_TPithdel; try omega.
rewrite 2 TPithdel_Fc_eq in *|-*; autorewrite with tuples;
try rewrite TPlength_TPithdel; try omega.
rewrite TPithdel_lt_comm; try omega.
rewrite TPithdel_lt_comm with (i:=1); try omega; trivial.
assert (Q1: C |- TPith (TPlength t 0 n -1) (Fc 0 n (TPithdel 1 t 0 n)) 0 n ~aacc
TPith (TPlength t 0 n -1) (Fc 0 n (TPithdel 1 t' 0 n)) 0 n /\
C |- TPithdel (TPlength t 0 n -1) (Fc 0 n (TPithdel 1 t 0 n)) 0 n ~aacc
TPithdel (TPlength t 0 n -1) (Fc 0 n (TPithdel 1 t' 0 n)) 0 n).
apply IHequiv2. clear IHequiv2. destruct Q1.
rewrite 2 TPith_overflow with (i:=i); try omega.
rewrite 2 TPithdel_overflow with (i:=i); autorewrite with tuples; try omega.
autorewrite with tuples in H.
assert (Q1: TPlength t 0 n >= 1 /\ TPlength t 0 n >= 1). auto. destruct Q1.
rewrite 2 TPith_TPithdel_geq in H; try omega.
replace (TPlength t 0 n - 1 + 1) with (TPlength t 0 n) in H; try omega; trivial.
rewrite <- Q. split~; trivial. apply equiv_A; simpl set_In; try omega.
autorewrite with tuples. rewrite 2 TPith_TPithdel_lt; try omega; trivial.
case (nat_eqdec (TPlength t 0 n) 2); intro H6.
rewrite 2 TPithdel_TPlength_1; auto; autorewrite with tuples;
try rewrite TPlength_TPithdel; try omega.
rewrite 2 TPithdel_Fc_eq in *|-*; autorewrite with tuples;
try rewrite TPlength_TPithdel; try omega.
rewrite 2 TPithdel_lt_comm with (i:=1); try omega; trivial.
rewrite 2 TPith_Fc_diff; trivial. rewrite 2 TPithdel_Fc_diff; trivial.
split~; auto. apply equiv_A; simpl set_In; try omega; trivial.
assert (Q:(1,n0) <> (E,n)). intro H'. inverts H'.
simpl in H. apply H. right~.
rewrite 2 TPith_Fc_diff; trivial. rewrite 2 TPithdel_Fc_diff; trivial.
split~. apply equiv_AC with (i:=i); simpl set_In; try omega; trivial.
case (nat_pair_eqdec (2,n0) (E,n)); intro H1. inverts H1.
simpl in H. false. apply H. right~.
rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_TPlength_1; try rewrite TPlength_Fc_diff; trivial.
split~; auto.
case (nat_pair_eqdec (2,n0) (E,n)); intro H1. inverts H1.
simpl in H. false. apply H. right~.
rewrite 2 TPith_Fc_diff; trivial.
rewrite 2 TPithdel_TPlength_1; try rewrite TPlength_Fc_diff; trivial.
split~; auto.
Qed.
Lemma aacc_equiv_Fc : forall C t t' E n, C |- t ~aacc t' ->
C |- Fc E n t ~aacc Fc E n t'.
Proof.
intros. gen_eq l : (TPlength t E n); intro H0.
gen t t' H0 H. induction l using peano_induction; intros.
case (set_In_dec nat_eqdec E (0 :: 1 :: (|[2]|))); intro H2.
Focus 2.
(* 2:{ *) apply equiv_Fc. left~. trivial. (* } *)
generalize H1; intro H1'.
apply aacc_equiv_TPlength with (E:=E) (n:=n) in H1'.
assert (Q: TPlength t E n >= 1). auto.
simpl in H2. destruct H2.
rewrite <- H2 in *|-*. clear H2.
apply aacc_equiv_TPith_E_diff_1_2 with
(E:=0) (n:=n) (i:=1) in H1; try omega.
destruct H1. apply equiv_A; simpl set_In; try omega; trivial.
autorewrite with tuples; trivial.
case (nat_eqdec (TPlength t 0 n) 1); intro H3.
rewrite 2 TPithdel_TPlength_1; autorewrite with tuples; auto; try omega.
rewrite 2 TPithdel_Fc_eq; try omega.
apply H with (m:=TPlength (TPithdel 1 t 0 n) 0 n); trivial.
rewrite TPlength_TPithdel; try omega.
simpl. intro. omega. destruct H2.
rewrite <- H2 in *|-*. clear H2.
apply aacc_equiv_TPith_l1 with (E:=1) (n:=n) in H1.
destruct H1. destruct H1. destruct H2. destruct H3.
apply equiv_AC with (i:=x); simpl set_In;
repeat split~; try omega; trivial.
autorewrite with tuples; trivial.
case (nat_eqdec (TPlength t 1 n) 1); intro H5.
rewrite 2 TPithdel_TPlength_1;
autorewrite with tuples; try omega; auto.
rewrite 2 TPithdel_Fc_eq; try omega.
apply H with (m:=TPlength (TPithdel 1 t 1 n) 1 n); trivial.
rewrite TPlength_TPithdel; try omega.
destruct H2; try contradiction.
rewrite <- H2. apply equiv_Fc_c; trivial.
Qed.
Lemma aacc_equiv_Fc_A_TPith : forall C t t' n,
TPlength t 0 n = TPlength t' 0 n ->
(forall i, i <= TPlength t 0 n ->
C |- TPith i t 0 n ~aacc TPith i t' 0 n) ->
C |- Fc 0 n t ~aacc Fc 0 n t' .
Proof.
intros. gen_eq l : (TPlength t 0 n). intro H1.
gen t t' H1 H H0. induction l using peano_induction; intros.
assert (Q : TPlength t 0 n >= 1). auto.
apply equiv_A. left~. rewrite 2 TPith_Fc_eq. apply H2. omega.
case (nat_eqdec l 1); intro H3.
rewrite 2 TPithdel_TPlength_1;
try rewrite TPlength_Fc_eq; try omega; auto.
rewrite 2 TPithdel_Fc_eq; try omega.
apply H with (m := TPlength (TPithdel 1 t 0 n) 0 n); trivial.
rewrite H1. rewrite TPlength_TPithdel; try omega.
rewrite 2 TPlength_TPithdel; omega.
intros. case (le_dec i 1); intro H5.
rewrite 2 TPith_TPithdel_leq_1; try omega.
apply H2; try omega.
rewrite TPlength_TPithdel in H4; try omega.
rewrite 2 TPith_TPithdel_geq; try omega.
apply H2. omega.
Qed.