-
Notifications
You must be signed in to change notification settings - Fork 4
/
alphaeq.v
4465 lines (3975 loc) · 151 KB
/
alphaeq.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
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import bin_rels.
Require Import eq_rel.
Require Import universe.
Require Import LibTactics.
Require Import tactics.
Require Import Coq.Bool.Bool.
Require Import Coq.Program.Tactics.
Require Import Omega.
Require Import Coq.Program.Basics.
Require Import Coq.Lists.List.
Require Import Coq.Init.Notations.
Require Import UsefulTypes.
Require Import Coq.Classes.DecidableClass.
Require Import Coq.Classes.Morphisms.
Require Import list.
Require Import Ring.
Require Import Recdef.
Require Import Eqdep_dec.
Require Import varInterface.
Require Import terms.
Require Import terms2.
Require Import substitution.
(* Move *)
Lemma and_weaken_l : forall (A B C : Prop),
(A -> B)
-> (A # C)
-> (B # C).
Proof using.
intros. tauto.
Qed.
(* Move *)
Lemma forall_combine : forall (A : Type) (P Q R: A -> Prop),
(forall a:A, P a -> Q a /\ R a)
-> ((forall a:A, P a -> Q a)#(forall a:A, P a -> R a)).
Proof using.
intros. firstorder.
Qed.
Generalizable Variable Opid.
Section AlphaGeneric.
Context {NVar VarClass} {deqnvar : Deq NVar} {varcl freshv}
{varclass: @VarType NVar VarClass deqnvar varcl freshv}
`{hdeq : Deq Opid} {gts : GenericTermSig Opid}.
Notation NTerm := (@NTerm NVar Opid).
Notation BTerm := (@BTerm NVar Opid).
Notation WTerm := (@WTerm NVar Opid).
Notation CTerm := (@CTerm NVar Opid).
Notation Substitution := (@Substitution NVar Opid).
(** printing # $\times$ #×# *)
(** printing <=> $\Leftrightarrow$ #⇔# *)
(** printing < $<$ #<# *)
(** printing $ $\times$ #×# *)
(** Most of the operations and relations in functional languages
are invariant under renaming of variables. Alpha equality
helps us express this property. We define it as follows:
*)
Inductive alpha_eq : NTerm -> NTerm -> [univ] :=
| al_vterm : forall v, alpha_eq (vterm v) (vterm v)
| al_oterm : forall (op: Opid) (lbt1 lbt2 : list BTerm),
length lbt1 = length lbt2
-> (forall n, n < length lbt1
-> alpha_eq_bterm (selectbt lbt1 n)
(selectbt lbt2 n))
-> alpha_eq (oterm op lbt1) (oterm op lbt2)
with alpha_eq_bterm : BTerm -> BTerm -> [univ] :=
| al_bterm :
forall (lv1 lv2 lv: list NVar) (nt1 nt2 : NTerm) ,
disjoint lv (all_vars nt1 ++ all_vars nt2)
-> length lv1 = length lv2
-> length lv1 = length lv
-> no_repeats lv
-> alpha_eq (ssubst nt1 (var_ren lv1 lv))
(ssubst nt2 (var_ren lv2 lv))
-> alpha_eq_bterm (bterm lv1 nt1) (bterm lv2 nt2).
(** % \noindent \\* %
The interesting case is in the definition of [alpha_eq_bterm].
We list some useful properties about [ssubst] and [alpha_eq].
Just like the above definitions, these proofs are independent
of the operators of the language.
*)
(** ** Key Properties about Substitution and Alpha Equality *)
Definition alphaeqc t1 t2 := alpha_eq (get_cterm t1) (get_cterm t2).
Inductive alpha_eq3 (lva: list NVar): NTerm -> NTerm -> [univ] :=
| al_vterm3 : forall v, alpha_eq3 lva (vterm v) (vterm v)
| al_oterm3 :
forall op lbt1 lbt2,
length lbt1 = length lbt2
-> (forall n, n < length lbt1
-> alpha_eq_bterm3 lva (selectbt lbt1 n)
(selectbt lbt2 n))
-> alpha_eq3 lva (oterm op lbt1) (oterm op lbt2)
with alpha_eq_bterm3 (lva: list NVar) : BTerm -> BTerm -> [univ] :=
| al_bterm3 :
forall (lv1 lv2 lv: list NVar) (nt1 nt2 : NTerm) ,
disjoint lv (all_vars nt1 ++ all_vars nt2 ++ lva)
-> length lv1 = length lv2
-> length lv1 = length lv
-> no_repeats lv
-> alpha_eq3 lva (ssubst_aux nt1 (var_ren lv1 lv))
(ssubst_aux nt2 (var_ren lv2 lv))
-> alpha_eq_bterm3 lva (bterm lv1 nt1) (bterm lv2 nt2).
(* Scheme alpha_eq_mut := Induction for alpha_eq Sort Type
with alpha_eq_bterm_mut := Induction for alpha_eq_bterm Sort Type.
*)
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import list.
(* Definition alphaeq (t1 t2 :NTerm) := alpha_eq t1 t2. *)
Definition alphaeqbt (t1 t2 :BTerm) := alpha_eq_bterm t1 t2.
Lemma alpha_eq3_refl:
forall nt lva, alpha_eq3 lva nt nt.
Proof using.
nterm_ind1s nt as [v | o lbt Hind] Case; [constructor ; fail | idtac].
Case "oterm".
simpl.
constructor; auto.
intros m Hlt.
remember (selectbt lbt m) as bt.
destruct bt as [lv nt].
apply selectbt_eq_in in Heqbt; trivial.
simpl.
pose proof (fresh_vars (length lv) (all_vars nt ++ lva))
as Hfresh.
exrepnd.
rename lvn into newbtv.
apply al_bterm3 with (lv:=newbtv); auto;
[disjoint_reasoningv|].
eapply Hind; eauto.
rewrite ssubst_aux_allvars_preserves_size2; auto.
Qed.
Theorem alpha_eq_if3: forall nt1 nt2 lv,
(alpha_eq3 lv nt1 nt2)
-> (alpha_eq nt1 nt2).
Proof using.
nterm_ind1s nt1 as [v1 | o1 lbt1 Hind] Case; introv Hal;
inverts Hal as Ha1 Ha2; constructor; auto.
introv Hlt. duplicate Hlt. apply Ha2 in Hlt.
inverts Hlt as Hb1 Hb2 Hb3 Hb4 Hb5 Hb6 Hb7.
apply al_bterm with (lv:=lv0); auto.
disjoint_reasoningv.
change_to_ssubst_aux8.
apply Hind with(lv0:=lv)(lv:=lv1)(nt:=nt1); auto.
rewrite Hb6. apply selectbt_in; auto.
rewrite ssubst_aux_allvars_preserves_size; [ omega |]. apply allvars_combine; fail.
Qed.
Lemma alpha_eq_refl:
forall nt, alpha_eq nt nt.
Proof using.
intros. apply alpha_eq_if3 with (lv:=nil).
apply alpha_eq3_refl.
Qed.
Lemma alpha_eq_sym:
forall nt1 nt2, alpha_eq nt1 nt2 -> alpha_eq nt2 nt1.
Proof using.
nterm_ind1s nt1 as [v1| o lbt1 Hind] Case; introv Hal;
inverts Hal as Hlen Hal; constructor; [auto | ].
introv Hlt. rewrite <- Hlen in Hlt. applydup Hal in Hlt.
pose proof (selectbt_in2 n lbt1 Hlt) as XX. exrepnd. destruct bt as [lv1 nt1].
revert Hlt0. intros Hlt0. allrw XX0.
destruct (selectbt lbt2 n) as [lv2 nt2].
inverts Hlt0 as Ha1 Ha2 Ha3 Ha4 Ha5. apply al_bterm with (lv:=lv); spc.
- disjoint_reasoningv.
- eapply Hind; eauto.
change_to_ssubst_aux8. rewrite ssubst_aux_allvars_preserves_size; [ omega |].
apply allvars_combine.
Qed.
(** exact same proof as above*)
Lemma alpha_eq3_sym:
forall nt1 nt2 lva, alpha_eq3 lva nt1 nt2 -> alpha_eq3 lva nt2 nt1.
Proof using.
nterm_ind1s nt1 as [v1| o lbt1 Hind] Case; introv Hal;
inverts Hal as Hlen Hal; constructor; [auto | ].
introv Hlt. rewrite <- Hlen in Hlt. applydup Hal in Hlt.
pose proof (selectbt_in2 n lbt1 Hlt) as XX. exrepnd. destruct bt as [lv1 nt1].
revert Hlt0. intros Hlt0. allrw XX0.
destruct (selectbt lbt2 n) as [lv2 nt2].
inverts Hlt0 as Ha1 Ha2 Ha3 Ha4 Ha5. apply al_bterm3 with (lv:=lv); spc.
- disjoint_reasoningv.
- eapply Hind; eauto.
rewrite ssubst_aux_allvars_preserves_size; [ omega |].
apply allvars_combine.
Qed.
Definition strong_alphaeqbt (bt1 bt2 : BTerm) :=
match (bt1, bt2) with
| (bterm lv1 nt1, bterm lv2 nt2) =>
(length lv1=length lv2) #
forall lv, (** in the weak version, this was an existential *)
length lv1 = length lv
-> disjoint lv (all_vars nt1 ++ all_vars nt2)
-> no_repeats lv
-> alpha_eq (ssubst nt1 (combine lv1 (map vterm lv)))
(ssubst nt2 (combine lv2 (map vterm lv)))
end.
(* there is a stronger version of it later. But as of now,
the proof of that indirectly depends on this weaker version *)
Lemma alpha3_ssubst_allvars_congr : forall nt1 nt2 lvi lvo lva,
length lvi=length lvo
-> alpha_eq3 (lvi++lvo++lva) nt1 nt2
-> disjoint (lvi++lvo) (bound_vars nt1 ++ bound_vars nt2)
-> alpha_eq3 lva (ssubst_aux nt1 (var_ren lvi lvo))
(ssubst_aux nt2 (var_ren lvi lvo)).
Proof using .
clear hdeq.
nterm_ind1s nt1 as [v1 | o1 lbt1 Hind] Case; introv Hllll Hal Hdis; inverts Hal as Hlen Hal.
- Case "vterm"; apply alpha_eq3_refl.
- Case "oterm". constructor;
repeat(rewrite map_length); auto.
introv Hlt. rewrite selectbt_map; auto.
duplicate Hlt. rewrite Hlen in Hlt0.
rewrite selectbt_map; auto.
fold @ssubst_bterm_aux.
applydup Hal in Hlt.
clear Hal.
pose proof (selectbt_in2 n lbt1 Hlt) as [bt99 pp].
exrepnd. destruct bt99 as [blv1 bnt1].
rewrite pp. rewrite pp in Hlt1.
pose proof (selectbt_in2 n lbt2 Hlt0) as [bt99 p2p].
exrepnd. destruct bt99 as [blv2 bnt2].
rewrite p2p. rewrite p2p in Hlt1.
inverts Hlt1 as Ha1 Ha2 Ha3 Ha4 Ha5.
allsimpl. duplicate Hdis as Hdiso.
apply disjoint_app_r in Hdis. repnd.
eapply disjoint_lbt_bt2 in Hdis0; eauto. repnd.
eapply disjoint_lbt_bt2 in Hdis; eauto. repnd.
allsimpl.
rename Ha5 into XX.
try (rw fold_var_ren in XX).
try (rw fold_var_ren in XX).
rewrite sub_filter_disjoint;auto;
[|apply disjoint_app_l in Hdis1; sp; fail].
rewrite sub_filter_disjoint;auto;
[|apply disjoint_app_l in Hdis2; sp; fail].
apply al_bterm3 with (lv:=lv); auto.
+ introv Hin Hc. apply Ha1 in Hin.
apply_clear Hin.
repeat(rw in_app_iff).
repeat(rw in_app_iff in Hc).
rewrite boundvars_ssubst_aux_vars in Hc;auto.
rewrite boundvars_ssubst_aux_vars in Hc;auto.
repeat(dorn Hc); auto; [|];
apply free_vars_ssubst_aux in Hc;try(apply wf_sub_vars);try(apply disjoint_bv_vars;disjoint_reasoningv);
[|];
dorn Hc; exrepnd; auto;[|];
apply in_var_ren in Hc0; exrepnd; subst; allsimpl; dorn Hc1; subst; sp.
+ apply Hind with(lv:=blv1) (lvi:=lvi) (nt:=bnt1) in XX; eauto.
Focus 2. rewrite ssubst_aux_allvars_preserves_size; [ omega |]. apply allvars_combine; fail.
Focus 2.
introv Hin Hc.
rewrite boundvars_ssubst_aux_vars in Hc; auto.
rewrite boundvars_ssubst_aux_vars in Hc; auto.
apply in_app_iff in Hc; auto.
dorn Hc; [apply Hdis0 in Hin|apply Hdis in Hin];sp; fail.
rewrite ssubst_aux_nest_swap; try congruence; disjoint_reasoningv.
apply alpha_eq3_sym. (** because o/w rw undo the above *)
simpl. rewrite ssubst_aux_nest_swap; try congruence; dands; disjoint_reasoningv.
apply alpha_eq3_sym; trivial.
Qed.
Theorem alpha_eq3_if: forall nt1 nt2,
(alpha_eq nt1 nt2) -> forall lv, (alpha_eq3 lv nt1 nt2).
Proof using.
nterm_ind1s nt1 as [v1 | o1 lbt1 Hind] Case; introv Hyp;
destruct nt2 as [v2 | o2 lbt2];
inverts Hyp as Hlen Hbt;
constructor;auto;
[]; introv Hlt; applydup Hbt in Hlt; clear Hbt;
destructr (selectbt lbt1 n) as [lv1 nnt1];
destructr (selectbt lbt2 n) as [lv2 nnt2];
inverts Hlt0 as Hb1 Hb2 Hb3 Hb4 Hb5.
pose proof (fresh_vars (length lv1)
(all_vars nnt1 ++ all_vars nnt2 ++lv))
as Hfresh.
exrepnd.
apply al_bterm3 with(lv:=lvn);auto.
pose proof (selectbt_in _ _ Hlt) as XX.
rewrite <- HeqHdeq in XX.
eapply Hind with(lv0:=(lv4++lvn++lv)) (nt:=nnt1) (lv:=lv1) in Hb5; auto.
Focus 2. change_to_ssubst_aux8.
rewrite ssubst_aux_allvars_preserves_size; [ omega |]. apply allvars_combine; fail.
try (rw fold_var_ren in Hb5).
try (rw fold_var_ren in Hb5).
try (rw fold_var_ren).
try (rw fold_var_ren).
apply alpha3_ssubst_allvars_congr in Hb5; try congruence.
+ revert Hb5. change_to_ssubst_aux8. intro Hb5.
rewrite ssubst_aux_nest_vars_same in Hb5; auto;
[ |congruence| disjoint_reasoningv | disjoint_reasoningv ].
rewrite ssubst_aux_nest_vars_same in Hb5; auto;
[ congruence | congruence | disjoint_reasoningv| disjoint_reasoningv].
+ rewrite boundvars_ssubst_vars; [|congruence|disjoint_reasoningv].
rewrite boundvars_ssubst_vars;disjoint_reasoningv.
Qed.
Theorem alpha_eq3_change_avoidvars:
forall lv lv' nt1 nt2, alpha_eq3 lv nt1 nt2
-> alpha_eq3 lv' nt1 nt2.
Proof using.
introv Hal.
apply alpha_eq_if3 in Hal.
apply alpha_eq3_if; auto.
Qed.
Notation vterm := (@vterm NVar Opid).
Lemma alpha3_ssubst_aux_allvars_congr2 : forall nt1 nt2 lvi lvo lva,
length lvi=length lvo
-> alpha_eq3 (lvi++lvo++lva) nt1 nt2
-> disjoint (lvo) (bound_vars nt1 ++ bound_vars nt2)
-> alpha_eq3 lva (ssubst_aux nt1 (var_ren lvi lvo))
(ssubst_aux nt2 (var_ren lvi lvo)).
Proof using.
nterm_ind1s nt1 as [v1 | o1 lbt1 Hind] Case; introv Hllll Hal Hdis;
duplicate Hal; inverts Hal as Hlen Hal.
- Case "vterm". apply alpha_eq3_refl.
- Case "oterm". constructor;
repeat(rewrite map_length); auto.
introv Hlt. rewrite selectbt_map; auto.
duplicate Hlt. rewrite Hlen in Hlt0.
rewrite selectbt_map; auto.
fold @ssubst_bterm_aux. clear Hal.
pose proof (selectbt_in2 n lbt1 Hlt) as [bt99 pp].
exrepnd. destruct bt99 as [blv1 bnt1].
pose proof (selectbt_in2 n lbt2 Hlt0) as [bt99 p2p].
exrepnd. destruct bt99 as [blv2 bnt2].
apply alpha_eq3_change_avoidvars with (lv':= (lvi ++ lvo ++ lva ++ blv1 ++ blv2)) in Hal0.
inverts Hal0 as H1len Hbal. GC.
applydup Hbal in Hlt.
rewrite pp. rewrite pp in Hlt1.
rewrite p2p. rewrite p2p in Hlt1.
clear Hbal.
inverts Hlt1 as Ha1 Ha2 Ha3 Ha4 Ha5.
allsimpl. duplicate Hdis as Hdiso.
apply disjoint_app_r in Hdis. repnd.
eapply disjoint_lbt_bt2 in Hdis0; eauto. repnd.
eapply disjoint_lbt_bt2 in Hdis; eauto. repnd.
repeat (rewrite (bvar_renamings_subst_disjoint_bound_vars); auto;[|
apply disjoint_sub_as_flat_map;
rewrite flat_map_free_var_vars_range;spc;sp;fail]).
allsimpl.
rename Ha5 into XX.
simpl. pose proof (@allvars_sub_filter _ _ Opid lvi lvo blv1) as X1.
pose proof (get_sub_dom_vars_eta _ X1) as X1X. exrepnd.
repeat(rewrite X1X0).
simpl. pose proof (@allvars_sub_filter _ _ Opid lvi lvo blv2) as X2.
pose proof (get_sub_dom_vars_eta _ X2) as X2X. exrepnd.
repeat(rewrite X2X0).
apply al_bterm3 with (lv:=lv); auto.
+ disjoint_reasoningv.
* apply disjoint_sym. apply disjoint_free_vars_ssubst_aux;sp;
rewrite flat_map_free_var_vars_range;spc;spc;disjoint_reasoningv.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
* apply disjoint_sym. apply disjoint_bound_vars_ssubst_aux;sp;
try(rewrite flat_map_free_var_vars_range;spc);
try(rewrite flat_map_bound_var_vars_range;spc;spc);simpl;
simpl_vlist;
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
* apply disjoint_sym. apply disjoint_free_vars_ssubst_aux;sp;
rewrite flat_map_free_var_vars_range;spc;disjoint_reasoningv.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
* apply disjoint_sym. apply disjoint_bound_vars_ssubst_aux;sp;
try(rewrite flat_map_free_var_vars_range;spc);
try(rewrite flat_map_bound_var_vars_range;spc);simpl;
simpl_vlist;
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
+ apply Hind with(lv:=blv1) (lvi:=lvi) (nt:=bnt1) in XX; eauto.
Focus 2. rewrite ssubst_aux_allvars_preserves_size; [ omega |]. apply allvars_combine; fail.
Focus 2.
introv Hin Hc.
rewrite boundvars_ssubst_aux_vars in Hc; auto.
rewrite boundvars_ssubst_aux_vars in Hc; auto.
apply in_app_iff in Hc; auto.
dorn Hc; [apply Hdis0 in Hin|apply Hdis in Hin];sp; fail.
rewrite ssubst_aux_nest_swap; try congruence;[|disjoint_reasoningv| disjoint_reasoningv].
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 2.
apply disjoint_sym. introv Hin Hinc.
apply combine_in_left with (l2:= map vterm lvo0) in Hinc;
[| rewrite map_length;sp];[].
exrepnd. try (rewrite fold_var_ren in Hinc0).
rewrite <- X1X0 in Hinc0.
apply in_sub_filter in Hinc0.
sp;fail.
apply alpha_eq3_sym.
rewrite ssubst_aux_nest_swap; try congruence;[|disjoint_reasoningv| disjoint_reasoningv].
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 3.
let tac1:=(eapply disjoint_sub_filter_vars_r;eauto) in
let tac2:=(eapply disjoint_sub_filter_vars_l;eauto) in
dis_almost_complete1 tac1;dis_almost_complete1 tac2;disjoint_reasoningv.
Focus 2.
apply disjoint_sym. introv Hin Hinc.
apply combine_in_left with (l2:= map vterm lvo1) in Hinc;
[| rewrite map_length;sp];[].
exrepnd. try (rewrite fold_var_ren in Hinc0).
rewrite <- X2X0 in Hinc0.
apply in_sub_filter in Hinc0.
sp;fail.
sp.
rw <- X1X0.
rw <- X2X0.
rewrite ssubst_aux_sub_filter2.
Focus 2.
intros v Hin Hinc.
apply free_vars_ssubst_aux2 in Hin.
dorn Hin.
repnd. unfold var_ren in Hin.
rewrite dom_sub_combine in Hin;[| rw map_length;sp]. sp.
exrepnd. apply in_var_ren in Hin0. exrepnd. subst. allsimpl.
dorn Hin1;sp;subst. rename Ha1 into Hcdis.
assert(disjoint lv blv2) as XXX by disjoint_reasoningv.
apply XXX in Hin4. sp.
rewrite ssubst_aux_sub_filter2.
Focus 2.
intros v Hin Hinc.
apply free_vars_ssubst_aux2 in Hin.
dorn Hin.
repnd. unfold var_ren in Hin.
rewrite dom_sub_combine in Hin;[| rw map_length;sp]. sp.
exrepnd. apply in_var_ren in Hin0. exrepnd. subst. allsimpl.
dorn Hin1;sp;subst. rename Ha1 into Hcdis.
assert(disjoint lv blv1) as XXX by disjoint_reasoningv.
apply XXX in Hin4. sp.
apply alpha_eq3_sym.
eapply alpha_eq3_change_avoidvars; eauto.
Qed.
Theorem alpha3bt_change_var: forall nt1 nt2 lv1 lv2 lv lva,
alpha_eq_bterm3 lva (bterm lv1 nt1) (bterm lv2 nt2)
-> length lv1 = length lv
-> disjoint lv (all_vars nt1 ++ all_vars nt2)
-> no_repeats lv
-> alpha_eq3 lva (ssubst_aux nt1 (var_ren lv1 lv))
(ssubst_aux nt2 (var_ren lv2 lv)).
Proof using.
introv Hal Hlen Hdis Hnr.
inverts Hal as Ha1 Ha2 Ha3 Ha4 Ha5.
apply (alpha_eq3_change_avoidvars _ (lv4++lv++lva)) in Ha5.
apply alpha3_ssubst_aux_allvars_congr2 in Ha5;[| congruence | ].
Focus 2. rewrite boundvars_ssubst_aux_vars.
rewrite boundvars_ssubst_aux_vars;disjoint_reasoningv.
rewrite ssubst_aux_nest_vars_same in Ha5;auto;
[| congruence| disjoint_reasoningv| disjoint_reasoningv].
rewrite ssubst_aux_nest_vars_same in Ha5;auto;
[ congruence | congruence | disjoint_reasoningv| disjoint_reasoningv].
Qed.
Lemma alpha_eq_trans:
forall nt1 nt2 nt3, alpha_eq nt1 nt2 -> alpha_eq nt2 nt3 -> alpha_eq nt1 nt3.
Proof using.
nterm_ind1s nt1 as [v1 | o1 lbt1 Hind] Case;
introv Hal1 Hal2; apply alpha_eq3_if with (lv:=[]) in Hal1;
apply alpha_eq3_if with (lv:=[]) in Hal2;
apply alpha_eq_if3 with (lv:=[]);
inverts Hal1 as Hlen1 Hal1; inverts Hal2 as Hlen2 Hal2; constructor
;try(congruence).
Case "oterm".
- introv Hlt0. duplicate Hlt0. duplicate Hlt0. apply Hal1 in Hlt0.
rewrite Hlen1 in Hlt1. apply Hal2 in Hlt1.
pose proof (selectbt_in _ _ Hlt2).
destruct (selectbt lbt1 n) as [lv1 nt1].
destruct (selectbt lbt2 n) as [lv2 nt2].
destruct (selectbt lbt3 n) as [lv3 nt3].
duplicate Hlt0 as Hl1t.
duplicate Hlt1 as Hl2t.
inverts Hlt0 as Ha1 Ha2 Ha3 Ha4 Ha5.
inverts Hlt1 as Hb1 Hb2 Hb3 Hb4 Hb5.
pose proof (fresh_vars (length lv1)
(all_vars nt1 ++ all_vars nt2 ++ all_vars nt3)) as Hfresh.
exrepnd.
clear Hb5 Ha4 Ha5 Hb1 Hb4 Ha3 Hb3 Hb1.
apply alpha3bt_change_var with (lv:=lvn) in Hl1t;
eauto;[|disjoint_reasoningv].
apply alpha3bt_change_var with (lv:=lvn) in Hl2t;
eauto; [| congruence | disjoint_reasoningv].
apply al_bterm3 with (lv:=lvn);auto;
try congruence;[disjoint_reasoningv| ].
apply alpha_eq_if3 with (lv:=[]) in Hl1t.
apply alpha_eq_if3 with (lv:=[]) in Hl2t.
apply alpha_eq3_if with (lv:=[]).
eapply Hind with(lv:=lv1) (nt:=nt1); eauto.
rewrite ssubst_aux_allvars_preserves_size; [ omega |]. apply allvars_combine.
Qed.
Lemma alphaeqbt_numbvars : forall a b,
alpha_eq_bterm a b -> num_bvars a = num_bvars b.
Proof using. intros ? ? Hal. invertsn Hal; auto.
Qed.
Theorem alphaeqbt_refl: forall b, alpha_eq_bterm b b.
Proof using. intros. destruct b.
pose proof (fresh_vars (length l) (all_vars n)) as Hfresh.
exrepnd. apply al_bterm with (lv:=lvn); auto.
apply disjoint_app_r; auto.
apply alpha_eq_refl.
Qed.
Definition alphaeqbtw (t1 t2: BTerm) := (bt_wf t1) # (bt_wf t2)
# alphaeqbt t1 t2.
Theorem alphaeqbtw_refl: forall b, bt_wf b -> alphaeqbtw b b.
Proof using. intros. destruct b. split; auto; split; auto.
apply alphaeqbt_refl.
Qed.
Theorem alpha_eq_ot_numvars: forall o lbt1 lbt2,
alpha_eq (oterm o lbt1) (oterm o lbt2)
-> map num_bvars lbt1 = map num_bvars lbt2.
Proof using.
introv Hal. duplicate Hal. inverts Hal as Hlen Hal.
apply eq_maps_bt; auto. introv Hlt.
pose proof (Hal _ Hlt) as Halb. inverts Halb.
auto.
Qed.
Theorem alphaeq3_preserves_wf:
forall t1 t2, alpha_eq3 [] t1 t2 -> (nt_wf t2 <=> nt_wf t1).
Proof using.
intros ?. nterm_ind1s t1 as [v | o lbt1 Hind] Case; intros t2 Hal.
Case "vterm". inverts Hal as . split; constructor.
Case "oterm". duplicate Hal. inverts Hal as Hmap Hal.
apply alpha_eq_if3 in Hal0. apply alpha_eq_ot_numvars in Hal0.
allrw ntot_wf_iff.
rewrite Hmap. rewrite Hal0.
apply and_tiff_compat_l; auto.
apply iff_push_down_forallT. intros n.
apply iff_push_down_impliesT.
remember (selectbt lbt2 n) as bt2.
remember (selectbt lbt1 n) as bt1.
destruct bt2 as [lv2 nt2].
destruct bt1 as [lv1 nt1].
intros Hlt. rewrite <- Hmap in Hlt.
repeat(rw bt_wf_iff).
applydup_clear Hal in Hlt.
rewrite <- Heqbt1 in Hlt0. rewrite <- Heqbt2 in Hlt0.
inverts Hlt0 as Hi1 Hi2 Hi3 Hi4 Hi5.
assert(LIn (bterm lv1 nt1) lbt1) as Hinb
by (rewrite Heqbt1; apply selectbt_in; auto).
eapply Hind with (lv:=lv1) in Hi5; eauto.
- rw <- (ssubst_aux_allvars_wf_iff _ (allvars_combine lv2 lv) ) in Hi5.
rw <- (ssubst_aux_allvars_wf_iff _ (allvars_combine lv1 lv) ) in Hi5.
trivial.
repeat rewrite bt_wf_iff. trivial.
- rewrite ssubst_aux_allvars_preserves_size2; auto.
Qed.
Lemma alphaeq_preserves_wf:
forall t1 t2, alpha_eq t1 t2 -> (nt_wf t2 <=> nt_wf t1).
Proof using.
introv Hal.
apply alpha_eq3_if with (lv:=[]) in Hal.
apply alphaeq3_preserves_wf;sp.
Qed.
(** % \noindent \\* %
The following lemma is the property we promised to prove while definining [ssubst].
*)
Lemma change_bvars_alpha_spec_aux: forall lv,
(forall nt,
let nt' := change_bvars_alpha lv nt in
disjoint lv (bound_vars nt') #alpha_eq nt nt')
* (forall bt,
let bt' := change_bvars_alphabt lv bt in
disjoint lv (bound_vars_bterm bt') #alpha_eq_bterm bt bt').
Proof using.
intros. apply NTerm_BTerm_ind;
[intro v; cpx| |].
- intros ? ? Hind.
simpl. split.
+ rewrite disjoint_flat_map_r.
intros ? Hin.
apply in_map_iff in Hin.
exrepnd. subst.
apply Hind. auto.
+
constructor; try (rw map_length; auto);[].
introv Hlt. rw @selectbt_map; auto.
pose proof (selectbt_in2 n lbt Hlt) as XX; exrepnd.
destruct bt as [blv bnt]. rewrite XX0.
apply Hind. auto.
- intros blv bnt Hnt. split.
+ introv Hin Hinc. rename t into vv.
allsimpl. subst.
simpl in *.
addFreshVarsSpec2 vn pp.
exrepnd. allsimpl.
duplicate Hin.
repnd.
apply Hnt0 in Hin0.
setoid_rewrite boundvars_ssubst_aux_vars in Hinc; sp.
apply disjoint_sym in pp1.
apply disjoint_app_l in pp1. repnd. apply pp2 in Hin.
apply in_app_iff in Hinc.
simpl in *.
dorn Hinc; sp.
+ allsimpl. subst.
simpl. addFreshVarsSpec2 vn pp.
destruct (fresh_vars (length blv) (lv ++ vn ++ (all_vars bnt)
++ all_vars
(change_bvars_alpha lv bnt))) as [lvn pal].
exrepnd. allsimpl.
disjoint_reasoningv.
apply al_bterm with (lv:=lvn); sp.
* unfold all_vars. rw @boundvars_ssubst_aux_vars;sp;
try(disjoint_reasoningv).
introv Hin Hinc.
applydup pal5 in Hin.
apply free_vars_ssubst_aux in Hinc;
[ |apply disjoint_bv_vars; sp].
dorn Hinc; exrepnd; sp. apply in_var_ren in Hinc0. exrepnd.
subst.
allsimpl.
dorn Hinc1; sp.
subst.
apply pal3 in Hin. sp.
* rewrite <- ssubst_ssubst_aux;
spcls; disjoint_reasoningv. rewrite ssubst_nest_vars_same; sp;
try congruence; try disjoint_reasoningv.
apply alpha_eq_if3 with (lv:=nil).
change_to_ssubst_aux8.
apply alpha3_ssubst_aux_allvars_congr2;sp.
Focus 2. disjoint_reasoningv.
apply alpha_eq3_if.
eauto.
Qed.
Lemma change_bvars_alpha_checkbc_aux: forall lv,
(forall nt:NTerm,
let nt' := change_bvars_alpha lv nt in
checkBC ((*free_vars nt++*)lv) nt' = true)
* (forall bt:BTerm,
let bt' := change_bvars_alphabt lv bt in
checkBC_bt ((*free_vars_bterm bt ++ *)lv) bt' = true).
Proof using varclass.
intros. apply NTerm_BTerm_ind;
[intro v; cpx| |].
- intros ? ? Hind.
simpl. rewrite ball_map_true.
intros x Hin. apply in_map_iff in Hin. exrepnd. subst.
eauto.
Local Opaque decide.
- intros blv bnt Hind.
simpl.
addFreshVarsSpec2 vn pp.
exrepnd. allsimpl.
rewrite decide_true;[ring_simplify| disjoint_reasoningv2].
rewrite decide_true;[ring_simplify| disjoint_reasoningv2].
Local Transparent decide.
rewrite (fst (boundvars_substvars_checkbc2 blv vn)).
apply (checkBCStrengthen vn);[| assumption].
disjoint_reasoningv.
Qed.
Lemma bcSubstBetaPreservesBC o (lamVar:NVar) (lamBody appArg:NTerm) lv:
let lam := bterm [lamVar] lamBody in
let appT := (oterm o [lam ; bterm [] appArg]) in
checkBC lv appT =true
-> checkBC lv (bcSubst lv lamBody [(lamVar, appArg)]) = true.
Proof using varclass.
Local Opaque decide.
simpl.
setoid_rewrite decide_true at 4;[| disjoint_reasoningv2; fail].
simpl in *.
setoid_rewrite decide_true at 3;[| constructor].
setoid_rewrite decide_true at 1;[| repeat constructor; noRepDis1].
intros Hc.
ring_simplify in Hc.
repeat rewrite andb_true in Hc. repnd.
unfold bcSubst.
simpl. rewrite app_nil_r.
pose proof (fst (change_bvars_alpha_checkbc_aux (lamVar::lv ++ bound_vars appArg)) lamBody) as Hbc.
pose proof (fst (change_bvars_alpha_spec_aux (lamVar::lv ++ bound_vars appArg)) lamBody) as Hsp.
simpl in *. revert Hbc Hsp.
generalize (change_bvars_alpha (lamVar::lv ++ bound_vars appArg) lamBody).
intros tc ? ?. repnd.
apply betaPreservesBC; auto; simpl;[disjoint_reasoningv2|].
revert Hbc. apply (fst checkBCSubset). apply subset_cons1.
apply subset_app_r. reflexivity.
Qed.
Lemma alpha_eq_cons : forall o1 o2 lbt1 lbt2 b1 b2,
alpha_eq_bterm b1 b2
-> alpha_eq (oterm o1 lbt1) (oterm o1 lbt2)
-> alpha_eq (oterm o2 (b1::lbt1)) (oterm o2 (b2::lbt2)).
Proof using.
introv Halb Halo.
inverts Halo as Hlen Halo.
constructor; simpl; try congruence.
intros.
destruct n as [| n]; unfold selectbt; simpl; eauto;[].
apply Halo. omega.
Qed.
Definition uniqVarLb :BTerm -> list NVar * list BTerm -> list NVar * list BTerm
:= (fun (b : BTerm) (r : list NVar * list BTerm) =>
let (rlv, rb) := r in
(bound_vars_bterm (uniq_change_bvars_alphabt rlv b)++ rlv,
uniq_change_bvars_alphabt rlv b :: rb)).
Lemma uniqVarLbFst : forall lbt lv,
let (rlv, rbt) := fold_right uniqVarLb (lv,[]) lbt in
rlv = flat_map bound_vars_bterm rbt ++ lv.
Proof using.
induction lbt; intros; simpl; auto; autorewrite with list.
specialize (IHlbt lv).
destruct (fold_right uniqVarLb (lv, []) lbt).
unfold uniqVarLb. simpl. subst l.
rewrite app_assoc.
refl.
Qed.
Lemma uniq_change_bvars_alpha_spec_aux:
(forall nt lv,
let nt' := uniq_change_bvars_alpha lv nt in
NoDup (bound_vars nt') # disjoint lv (bound_vars nt') #alpha_eq nt nt')
* (forall bt lv,
let (blv, bnt) := uniq_change_bvars_alphabt lv bt in
let bt' := bterm blv bnt in
NoDup (bound_vars_bterm bt') # disjoint lv (bound_vars_bterm bt') #alpha_eq_bterm bt bt').
Proof using.
clear gts.
intros. apply NTerm_BTerm_ind;
[intro v; cpx| |].
- intros ? ? Hind.
simpl.
induction lbt as [| b lbt]; simpl; [intros; dands; cpx;
constructor; cpx; fail|].
simpl. intros lv. simpl in *.
pose proof (uniqVarLbFst lbt lv) as Hbt.
unfold uniqVarLb in Hbt.
specialize (IHlbt (fun b inb => Hind b (or_intror inb)) lv).
destruct(fold_right
(fun (b : BTerm) (r : list NVar * list BTerm) =>
let (rlv, rb) := r in
(bound_vars_bterm (uniq_change_bvars_alphabt rlv b) ++ rlv,
uniq_change_bvars_alphabt rlv b :: rb))
(lv, []) lbt) as [rlv rnt].
specialize (Hind b ltac:(cpx) rlv).
simpl in *.
destruct (uniq_change_bvars_alphabt rlv b ) as [blv bnt].
subst rlv. repnd.
dands;simpl in *.
+ apply NoDupApp; auto.
repeat disjoint_reasoning.
+ disjoint_reasoningv.
+ apply alpha_eq_cons with (o1:=o); assumption.
- intros blv bnt Hnt lv. allsimpl. subst.
specialize (Hnt lv).
addFreshVarsSpec2 vn pp.
exrepnd. allsimpl.
dands.
+ setoid_rewrite boundvars_ssubst_aux_vars.
apply NoDupApp; noRepDis.
+ introv Hin Hinc. rename t into vv.
allsimpl. subst.
simpl in *.
duplicate Hin.
repnd.
setoid_rewrite boundvars_ssubst_aux_vars in Hinc; sp.
apply disjoint_sym in pp1.
apply disjoint_app_l in pp1. repnd. apply pp2 in Hin.
apply in_app_iff in Hinc.
simpl in *.
dorn Hinc; sp.
unfold disjoint in pp2. firstorder.
+ destruct (fresh_vars (length blv) (lv ++ vn ++ (all_vars bnt)
++ all_vars
(uniq_change_bvars_alpha lv bnt))) as [lvn pal].
exrepnd. allsimpl.
disjoint_reasoningv.
apply al_bterm with (lv:=lvn); sp.
* unfold all_vars. rw @boundvars_ssubst_aux_vars;sp;
try(disjoint_reasoningv).
introv Hin Hinc.
applydup pal5 in Hin.
apply free_vars_ssubst_aux in Hinc;
[ |apply disjoint_bv_vars; sp].
dorn Hinc; exrepnd; sp. apply in_var_ren in Hinc0. exrepnd.
subst.
allsimpl.
dorn Hinc1; sp.
subst.
apply pal3 in Hin. sp.
* rewrite <- ssubst_ssubst_aux;
spcls; disjoint_reasoningv. rewrite ssubst_nest_vars_same; sp;
try congruence; try disjoint_reasoningv.
apply alpha_eq_if3 with (lv:=nil).
change_to_ssubst_aux8.
apply alpha3_ssubst_aux_allvars_congr2;sp.
Focus 2. disjoint_reasoningv.
apply alpha_eq3_if.
eauto.
Qed.
Definition change_bvars_alpha_spec: forall (nt : NTerm) (lv : list NVar),
disjoint lv (bound_vars (change_bvars_alpha lv nt)) # alpha_eq nt (change_bvars_alpha lv nt)
:= fun nt lv => (fst (change_bvars_alpha_spec_aux lv)) nt.
Definition change_bvars_alphabt_spec
: forall (lv : list NVar) (bt : BTerm),
disjoint lv (bound_vars_bterm (change_bvars_alphabt lv bt)) # alpha_eq_bterm bt (change_bvars_alphabt lv bt)
:= fun lv => snd (change_bvars_alpha_spec_aux lv).
Lemma change_bvars_alpha_spec_varclass: forall lv vc,
(forall (nt:NTerm), varsOfClass (bound_vars nt) vc
-> varsOfClass (bound_vars (change_bvars_alpha lv nt)) vc)
*
(forall (bt:BTerm), varsOfClass (bound_vars_bterm bt) vc
-> varsOfClass (bound_vars_bterm (change_bvars_alphabt lv bt)) vc).
Proof using varclass.
intros. apply NTerm_BTerm_ind;
[intro v; simpl; unfold preservesVarclass; tauto| |].
- intros ? ? Hind. simpl.
rewrite flat_map_map.
apply lforall_flatmap.
exact Hind.
- intros blv bnt Hnt.
simpl. repeat rewrite varsOfClassApp.
introv Hin. repnd.
split;[apply freshReplacementsSameClass; assumption|].
eapply lforall_subset;[apply boundvars_ssubst_aux_subset|].
rewrite flat_map_bound_var_vars_range;
[| autorewrite with SquiggleEq; setoid_rewrite freshVarsLen; refl].
autorewrite with list.
unfold varsOfClass in *.
eauto.
Qed.
Lemma change_bvars_alpha_spec2: forall (nt : NTerm) (lv : list NVar),
let cc := change_bvars_alpha lv nt in
checkBC lv cc = true
/\ disjoint lv (bound_vars cc)
/\ alpha_eq nt cc
/\ (forall vc, varsOfClass (bound_vars nt) vc
-> varsOfClass (bound_vars cc) vc).
Proof using. simpl.
intros. dands; intros;
try apply change_bvars_alpha_spec_varclass;
try apply change_bvars_alpha_checkbc_aux;
try apply change_bvars_alpha_spec_aux. assumption.
Qed.
Lemma change_bvars_alphabt_spec2: forall (nt : BTerm) (lv : list NVar),
let cc := change_bvars_alphabt lv nt in
checkBC_bt lv cc = true
/\ disjoint lv (bound_vars_bterm cc)
/\ alpha_eq_bterm nt (change_bvars_alphabt lv nt)
/\ (forall vc, varsOfClass (bound_vars_bterm nt) vc
-> varsOfClass (bound_vars_bterm cc) vc).
Proof using. simpl.
intros. dands; intros;
try apply change_bvars_alpha_spec_varclass;
try apply change_bvars_alpha_checkbc_aux;
try apply change_bvars_alpha_spec_aux. assumption.
Qed.
(*
Lemma change_bvars_alpha_spec_varclass: forall lv vc,
(forall nt, varsOfClass (bound_vars nt) vc
-> varsOfClass (bound_vars (change_bvars_alpha lv nt)) vc)
*)
Ltac add_changebvar_spec cb Hn:=
match goal with
| [ |- context[change_bvars_alpha ?lv ?nt] ] => pose proof (change_bvars_alpha_spec nt lv) as Hn;
remember (change_bvars_alpha lv nt) as cb; simpl in Hn
| [ |- context[change_bvars_alphabt ?lv ?nt] ] => pose proof (change_bvars_alphabt_spec lv nt) as Hn;
remember (change_bvars_alphabt lv nt) as cb; simpl in Hn
end.
Ltac add_changebvar_spec4 cb Hn:=
match goal with
| [ |- context[change_bvars_alpha ?lv ?nt] ] => pose proof (change_bvars_alpha_spec2 nt lv) as Hn;
remember (change_bvars_alpha lv nt) as cb; simpl in Hn
| [ |- context[change_bvars_alphabt ?lv ?nt] ] => pose proof (change_bvars_alphabt_spec2 lv nt) as Hn;
remember (change_bvars_alphabt lv nt) as cb; simpl in Hn
end.
Theorem alphaeqbt_preserves_wf:
forall bt1 bt2, alpha_eq_bterm bt1 bt2 -> (bt_wf bt2 <=> bt_wf bt1).
Proof using.
introv Hal. inverts Hal as Hi1 Hi2 Hi3 Hi4 Hal. repeat(rw bt_wf_iff).
apply alphaeq_preserves_wf in Hal.
revert Hal. change_to_ssubst_aux8. intro Hal.
rw <- (ssubst_aux_allvars_wf_iff _ (allvars_combine lv2 lv) ) in Hal.
rw <- (ssubst_aux_allvars_wf_iff _ (allvars_combine lv1 lv) ) in Hal.
repeat rewrite bt_wf_iff.
trivial.
Qed.
Lemma alpha_eq3_preserves_size: forall nt1 nt2,
alpha_eq3 [] nt1 nt2 -> size nt1 = size nt2.
Proof using.
nterm_ind1s nt1 as [v1| o lbt1 Hind] Case; introv Hal;
inverts Hal as Hlen Hal;sp.
simpl. f_equal. f_equal. eapply eq_maps_bt; try (congruence).
introv Hlt. pose proof (selectbt_in2 _ _ Hlt) as XX.
exrepnd. destruct bt as [lv1 nt1].
apply_clear Hal in Hlt. revert Hlt. rw XX0. introv Hlt.