-
Notifications
You must be signed in to change notification settings - Fork 1
/
proof.v
1361 lines (1239 loc) · 50.3 KB
/
proof.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 Coq.Classes.DecidableClass.
Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Require Import SquiggleEq.export.
Require Import SquiggleEq.UsefulTypes.
Require Import SquiggleEq.list.
Require Import SquiggleEq.LibTactics.
Require Import SquiggleEq.tactics.
Require Import SquiggleEq.AssociationList.
Require Import ExtLib.Structures.Monads.
Require Import templateCoqMisc.
Require Import Template.Template.
Require Import Template.Ast.
Require Import paramDirect.
Require Import Program.
Open Scope program_scope.
(* Reserved Notation " A ↪ B " (at level 80). *)
Lemma NoDupSinleton {A:Type} (a:A): NoDup [a].
Proof using.
repeat constructor.
simpl. tauto.
Qed.
(* Move to templateCoqMisc. change it to 5 or more *)
Definition varCycleLen := 3.
(* TODO: preproc : unflatten all applications to binary *)
(* similar to PTS.Beta. need to take one step *)
Inductive red (substf: list V -> STerm -> Substitution -> STerm):
((*outerBVars*)list V) -> STerm -> STerm -> Prop :=
| beta : forall outerBvars x A Sa b arg,
red substf outerBvars (mkApp (mkLamS x A Sa b) [arg]) (substf outerBvars b [(x,arg)])
| congruence :
forall outerBvars n o lbt1 lbt2,
n < length (lbt1) (* reduction happens only in the nth bterm *)
-> length lbt1 = length lbt2
-> (forall m, m<>n -> selectbt lbt1 m = selectbt lbt2 m)
-> let b1 := (selectbt lbt1 n) in let b2 := (selectbt lbt2 n) in
get_vars b1= get_vars b2
-> red substf (get_vars b1 ++ outerBvars) (get_nt b1) (get_nt b2)
-> red substf outerBvars (oterm o lbt1) (oterm o lbt2).
(* clause for alpha equality? *)
Require Import Coq.Relations.Relation_Operators.
Definition redS := red bcSubst.
(** for the correctness of translate on [tl] and [tr], we need to assume that
[outerBvars] includes the free vars of [tl] and [tr]. No such assumption is needed here *)
Lemma redPreservesBC: forall (outerBvars:list V) (tl tr : STerm),
redS outerBvars tl tr -> checkBC outerBvars tl = true -> checkBC outerBvars tr = true.
Proof using.
intros ? ? ? Hred.
induction Hred.
Local Opaque decide.
- simpl.
rewrite decide_true by (try constructor).
rewrite decide_true by disjoint_reasoning.
rewrite decide_true by (try apply NoDupSinleton).
intros Hr. fold V in x.
ring_simplify in Hr.
repeat rewrite andb_true in Hr.
repeat rewrite Decidable_spec in Hr.
repnd. apply bcSubstBetaPreservesBC with (o:=CApply 1).
simpl.
setoid_rewrite decide_true;
try apply NoDupSinleton; try constructor; try disjoint_reasoningv2.
ring_simplify. repeat rewrite andb_true.
tauto.
- simpl. do 2 rewrite ball_map_true.
intros Hl ? Hin. pose proof Hin as Hsel.
apply in_selectbt in Hsel. exrepnd. subst.
rename n0 into m.
destruct (decideP (m=n));
[subst | rewrite <- H1 by assumption; apply Hl; apply selectbt_in; congruence].
pose proof Hsel1 as Hsel2.
rewrite <- H0 in Hsel2.
eapply selectbt_in in Hsel2.
specialize (Hl _ Hsel2).
destruct (selectbt lbt1 n) as [lv1 tl].
destruct (selectbt lbt2 n) as [lv tr]. simpl in *. subst.
repeat rewrite andb_true in *. repnd. dands; auto.
Qed.
Definition defEqS (outerBVars:list V) : STerm -> STerm -> Prop :=
clos_refl_sym_trans _ (redS outerBVars).
(* Infix "≡" := defEq (at level 80). *)
(* (free_vars (tvmap vprime t)) = map vprime (free_vars t) *)
(* Lemma 2.1 in Lasson.
Unlike in Certicoq, here we are talking about reduction, which
can happen even under binders. So, we don't have the luxury
of only talking about closed terms. So alpha equality is inevitable in later lemmas.
In this lemma, by ensuring that freshVars commutes with vprime, we may be
able to get it with strict equality
*)
Require Import Psatz.
Local Opaque BinNat.N.add .
Lemma vPrimeNeqV : forall v, v <> vprime v.
Proof.
intros ? Heq. apply (f_equal fst) in Heq.
simpl in Heq. lia.
Qed.
Lemma vRelNeqV : forall v, v <> vrel v.
Proof.
intros ? Heq. apply (f_equal fst) in Heq.
simpl in Heq. lia.
Qed.
Lemma vRelNeqVPrime : forall (v:V), vprime v <> vrel v.
Proof.
intros ? Heq. apply (f_equal fst) in Heq.
simpl in Heq. lia.
Qed.
Require Import NArith.
(** Move to templateCoqMisc *)
Definition vBase (v: V) : N :=
let vn := fst v in
(vn - (N.modulo vn varCycleLen))%N.
Lemma vBaseId v :
varClass v = userVar -> vBase v = fst v.
Proof using.
intros Heq.
destruct v; simpl in *.
apply (f_equal (@proj1_sig _ _ )) in Heq. unfold vBase.
simpl in *. setoid_rewrite Heq. lia.
Qed.
Lemma vBasePrime v :
varClass v = userVar -> vBase (vprime v) = fst v.
Proof using.
intros Heq.
destruct v; simpl in *.
apply (f_equal (@proj1_sig _ _ )) in Heq. unfold vBase.
simpl in *. rewrite N.add_mod by (compute;lia).
setoid_rewrite Heq. unfold varCycleLen.
change ((1 mod 3 + 0) mod 3) with 1.
lia.
Qed.
Lemma vBaseRel v :
varClass v = userVar -> vBase (vrel v) = fst v.
Proof using.
intros Heq.
destruct v; simpl in *.
apply (f_equal (@proj1_sig _ _ )) in Heq. unfold vBase.
simpl in *. rewrite N.add_mod by (compute;lia).
setoid_rewrite Heq. unfold varCycleLen.
change ((2 mod 3 + 0) mod 3) with 2.
lia.
Qed.
Hint Rewrite (fun v => not_eq_beq_var_false _ _ (vPrimeNeqV v)) : Param.
Hint Rewrite (fun v => not_eq_beq_var_false _ _ (vRelNeqVPrime v)) : Param.
Hint Rewrite (fun v => not_eq_beq_var_false _ _ (vRelNeqV v)) : Param.
Require Import NArith.
Definition varClass1 (v:V) : N := proj1_sig (varClass v).
Lemma varClassVPrime : forall v, varClass1 (vprime v) =
(1+ varClass1 v) mod varCycleLen.
Proof using.
intros. unfold varClass1. simpl.
rewrite N.add_mod;[| lia].
refl.
Qed.
Lemma varClassVRel : forall v, varClass1 (vrel v) =
(2+ varClass1 v) mod varCycleLen.
Proof using.
intros. unfold varClass1. simpl.
rewrite N.add_mod;[| lia].
refl.
Qed.
Hint Rewrite varClassVPrime varClassVRel : Param.
Lemma varClassNotEq : forall v1 v2,
(varClass1 v1 <> varClass1 v2) -> beq_var v1 v2 = false.
Proof.
intros ? ? Heq.
apply not_eq_beq_var_false.
congruence.
Qed.
Hint Resolve vRelNeqVPrime vRelNeqV vPrimeNeqV : Param.
Lemma decideFalse P `{Decidable P} : ~P -> decide P = false.
Proof.
apply Decidable_sound_alt.
Qed.
Lemma nameMapAppInj s :
injective_fun (nameMap (fun x : ident => String.append x s)).
(** append is injective at the first argument *)
Admitted. (** very confident about this *)
(** unconditional, even though we use vrel only userVars *)
Lemma vRelInjective : injective_fun vrel.
Proof using.
intros v1 v2 Heq.
destruct v1, v2.
unfold vrel in *.
simpl in *.
inverts Heq.
f_equal; [lia|].
unfold nameMap.
apply nameMapAppInj in H1.
assumption.
Qed.
(** unconditional, even though we use vrel only userVars *)
Lemma vPrimeInjective : injective_fun vprime.
Proof using.
intros v1 v2 Heq.
destruct v1, v2.
unfold vrel in *.
simpl in *.
inverts Heq.
f_equal; [lia|].
apply nameMapAppInj in H1.
assumption.
Qed.
Lemma vRelInjective2 v1 v2 : v1 <> v2 ->
vrel v1 <> vrel v2.
Proof using.
intros Heq.
intros Hc.
apply vRelInjective in Hc. contradiction.
Qed.
Hint Rewrite varClassVPrime: Param.
Hint Rewrite varClassVRel: Param.
Hint Resolve vPrimeInjective : injective_fun.
Hint Resolve vRelInjective : injective_fun.
Local Transparent BinNat.N.add .
Ltac hideRHS rhs :=
match goal with
[ |- _ = ?r] => set (rhs:= r)
end.
Local Opaque vprime.
Local Opaque vrel.
(* use parametricity? *)
Lemma substAuxPrimeCommute: forall (t: STerm) (sub:Substitution),
(* NO need to assume that vars in a and b and the var x have class 0 *)
tprime (ssubst_aux t sub) =
ssubst_aux (tprime t) (ALMap vprime tprime sub).
Proof using.
induction t using NTerm_better_ind; intro.
- simpl. unfold sub_find. rewrite ALFindMap by eauto with injective_fun.
dALFind ss; setoid_rewrite <- Heqss; refl.
- simpl. unfold tprime, tvmap. simpl. f_equal. repeat rewrite map_map.
apply eq_maps.
intros b Hin. destruct b.
specialize (H _ _ Hin). unfold compose. simpl. f_equal.
unfold sub_filter. rewrite ALEndoMapFilterCommute by eauto with injective_fun.
apply H.
Qed.
Corollary substAuxPrimeCommute1 : forall (A B: STerm) (x:V),
(* NO need to assume that vars in a and b and the var x have class 0 *)
tprime (ssubst_aux A [(x,B)]) =
ssubst_aux (tprime A) [(vprime x,tprime B)].
Proof using.
intros. rewrite substAuxPrimeCommute. refl.
Qed.
(* can use parametricity instead, once we deal with universe-polymorpic types such as NTerm *)
Lemma fvarsPrimeCommute t:
free_vars (tprime t) =
map vprime (free_vars t).
Proof using.
induction t using NTerm_better_ind;[refl|].
simpl. rewrite flat_map_map, map_flat_map.
apply eq_flat_maps.
intros b Hin. destruct b. unfold compose. simpl.
specialize (H _ _ Hin). setoid_rewrite H.
unfold remove_nvars.
erewrite <- map_diff_commute by eauto with injective_fun.
refl.
Qed.
Lemma ifThenElseMap {A B:Type} (f: A->B) (b:bool) (t e : A):
f (if b then t else e) = if b then (f t) else (f e).
Proof using.
destruct b; auto.
Qed.
Lemma translateFvars ienv (t:STerm) :
subset
(free_vars (translate true ienv t))
(flat_map vAllRelated (free_vars t)).
Proof using.
Admitted. (** confident about this. note that it is unconditional, and it says [subset] not [eq_set]*)
(* generalize vAllRelated as a function that returns disjoint lists on different inputs *)
Lemma vAllRelatedFlatDisjFst lva lvb:
varsOfClass (lva ++ lvb) userVar
-> disjoint (map fst lva) (map fst lvb)
-> disjoint (flat_map vAllRelated lva) (flat_map vAllRelated lvb).
Proof using.
intros Hvc Hd.
apply disjoint_map with (f:= vBase).
apply varsOfClassApp in Hvc.
destruct Hvc as [Hvca Hvcb].
do 2 rewrite map_flat_map.
unfold vAllRelated, compose. simpl.
setoid_rewrite flat_map_fapp with (f:= fun x => [vBase x]).
setoid_rewrite flat_map_fapp with (f:= fun x => [vBase (vprime x)]).
(* let rec tac l :=
match l with
| ?h::?tl =>
setoid_rewrite eqset_flat_maps at ltac:h;
[| intros ? ?;
try rewrite vBaseId;
try rewrite vBasePrime;
try rewrite vBaseRel;
[apply eq_set_refl | eauto]]; tac tl
| _ => idtac "nil"
end in tac ([1]). *)
setoid_rewrite eqset_flat_maps at 1.
Focus 2.
intros ? ?. rewrite vBaseId; [apply eq_set_refl | eauto].
setoid_rewrite eqset_flat_maps at 2.
Focus 2.
intros ? ?. rewrite vBasePrime; [apply eq_set_refl | eauto].
setoid_rewrite eqset_flat_maps at 3.
Focus 2.
intros ? ?. rewrite vBaseRel; [apply eq_set_refl | eauto].
setoid_rewrite eqset_flat_maps at 4.
Focus 2.
intros ? ?. rewrite vBaseId; [apply eq_set_refl | eauto].
setoid_rewrite eqset_flat_maps at 5.
Focus 2.
intros ? ?. rewrite vBasePrime; [apply eq_set_refl | eauto].
setoid_rewrite eqset_flat_maps at 6.
Focus 2.
intros ? ?. rewrite vBaseRel; [apply eq_set_refl | eauto].
repeat rewrite flat_map_single.
disjoint_reasoningv.
Qed.
(* generalize vAllRelated as a function that returns disjoint lists on different inputs *)
Lemma vAllRelatedFlatDisj lva lvb:
varsOfClass (lva ++ lvb) userVar
-> disjoint lva lvb
-> disjoint (flat_map vAllRelated lva) (flat_map vAllRelated lvb).
Proof using.
intros Hvc Hd. unfold disjoint.
setoid_rewrite in_flat_map.
unfold disjoint in Hd.
apply varsOfClassApp in Hvc.
destruct Hvc as [Hvca Hvcb].
intros ? H1ex. destruct H1ex as [v1 H1ex].
destruct H1ex.
intros H2ex. destruct H2ex as [v2 H2ex].
destruct H2ex.
unfold vAllRelated in *.
repeat (in_reasoning); subst; try contradiction; eauto with Param.
firstorder.
- apply Hvcb in H1. apply (f_equal (@proj1_sig _ _ )) in H1.
setoid_rewrite varClassVPrime in H1.
apply Hvca in H. apply (f_equal (@proj1_sig _ _ )) in H.
setoid_rewrite H in H1. compute in H1. lia.
- apply Hvcb in H1. apply (f_equal (@proj1_sig _ _ )) in H1.
setoid_rewrite varClassVRel in H1.
apply Hvca in H. apply (f_equal (@proj1_sig _ _ )) in H.
setoid_rewrite H in H1. compute in H1. lia.
- apply Hvcb in H1. apply (f_equal (@proj1_sig _ _ )) in H1.
apply Hvca in H. apply (f_equal (@proj1_sig _ _ )) in H.
setoid_rewrite varClassVPrime in H.
setoid_rewrite H1 in H. compute in H. lia.
- apply vPrimeInjective in H2. subst. firstorder.
- apply (f_equal varClass1) in H2.
autorewrite with Param in H2.
unfold varClass1 in H2.
setoid_rewrite (Hvca _ H) in H2.
setoid_rewrite (Hvcb _ H1) in H2.
compute in H2. lia.
- apply Hvcb in H1. apply (f_equal (@proj1_sig _ _ )) in H1.
apply Hvca in H. apply (f_equal (@proj1_sig _ _ )) in H.
setoid_rewrite varClassVRel in H.
setoid_rewrite H1 in H. compute in H. lia.
- apply (f_equal varClass1) in H2.
autorewrite with Param in H2.
unfold varClass1 in H2.
setoid_rewrite (Hvca _ H) in H2.
setoid_rewrite (Hvcb _ H1) in H2.
compute in H2. lia.
- apply vRelInjective in H2. subst. firstorder.
Qed.
Lemma translateFvarsDisj ienv (t:STerm) lv:
varsOfClass (free_vars t ++ lv) userVar
-> disjoint (free_vars t ) lv
-> disjoint (free_vars (translate true ienv t)) (flat_map vAllRelated lv).
Proof using.
intros Hvc Hd.
eapply subset_disjoint;[apply translateFvars|].
apply vAllRelatedFlatDisj; auto.
Qed.
Fixpoint mkAppUnFlattened (f: STerm) (args: list STerm) : STerm :=
match args with
| [] => f
| h::tl => mkAppUnFlattened (mkAppNoCheck f [h]) tl
end.
(* beta reduction in mkApp was only for efficiency and we dont consider
that in the proof *)
Lemma mkAppNoBeta : mkAppBeta = mkAppNoCheck. Admitted.
Local Opaque castIfNeeded mkAppBeta.
(* this comes up again and again *)
Lemma vDisjointUserVar (la lb: list V) :
varsOfClass la userVar
-> varsOfClass lb userVar
-> disjoint la (map vprime lb ++ map vrel lb).
Proof using.
intros Ha Hb.
disjoint_reasoning; intros ? Hin Hc; apply in_map_iff in Hc; exrepnd;
try apply Ha in Hin; try apply Hb in Hin; subst;
try apply Ha in Hc1; try apply Hb in Hc1;
apply (f_equal (@proj1_sig _ _ )) in Hc1;
apply (f_equal (@proj1_sig _ _ )) in Hin;
try setoid_rewrite varClassVPrime in Hin;
try setoid_rewrite varClassVRel in Hin;
rewrite N.add_mod in Hin by (unfold varCycleLen; lia);
setoid_rewrite Hc1 in Hin; inverts Hin.
Qed.
Lemma vDisjointPrimeUserVar (la lb: list V) :
varsOfClass la userVar
-> varsOfClass lb userVar
-> disjoint (map vprime la) (lb ++ map vrel lb).
Proof using.
intros Ha Hb.
pose proof (vDisjointUserVar _ _ Hb Ha).
repeat disjoint_reasoning2.
clear H H0.
intros ? Hin Hinc.
apply in_map_iff in Hin.
apply in_map_iff in Hinc.
exrepnd. subst.
apply (f_equal varClass1) in Hinc0.
apply Ha in Hin1.
apply Hb in Hinc1.
apply (f_equal (@proj1_sig _ _ )) in Hinc1.
apply (f_equal (@proj1_sig _ _ )) in Hin1.
rewrite varClassVPrime in Hinc0.
rewrite varClassVRel in Hinc0.
setoid_rewrite Hin1 in Hinc0.
setoid_rewrite Hinc1 in Hinc0.
invertsn Hinc0.
Qed.
Lemma vDisjointTPrimeUserVar (t:STerm) (lb: list V) :
varsOfClass (free_vars t) userVar
-> varsOfClass lb userVar
-> disjoint (free_vars (tprime t)) (lb ++ map vrel lb).
Proof using.
rewrite fvarsPrimeCommute.
apply vDisjointPrimeUserVar.
Qed.
Lemma ssubst_trim (t:STerm) x b1 b2 b3:
varsOfClass (free_vars t) userVar
-> varsOfClass [x] userVar
-> ssubst_aux t [(x, b1); (vprime x, b2); (vrel x, b3)] = ssubst_aux t [(x, b1)].
Proof using.
intros H1v H2v.
rewrite <- ssubst_aux_sub_filter2 with (l:= [vprime x; vrel x]);
[| apply vDisjointUserVar with (lb:=[x]); assumption].
simpl.
do 2 rewrite deq_refl.
do 3 rewrite decideFalse by eauto with Param.
refl.
Qed.
Lemma ssubst_trim_prime (t:STerm) x b1 b2 b3:
varsOfClass (free_vars t) userVar
-> varsOfClass [x] userVar
-> ssubst_aux (tprime t) [(x, b1); (vprime x, b2); (vrel x, b3)] =
ssubst_aux (tprime t) [(vprime x, b2)].
Proof using.
intros H1v H2v.
rewrite <- ssubst_aux_sub_filter2 with (l:= [x; vrel x]);
[|rewrite fvarsPrimeCommute; apply vDisjointPrimeUserVar with (lb:=[x]); assumption].
simpl.
do 2 rewrite deq_refl.
do 3 rewrite decideFalse by eauto with Param. refl.
Qed.
Require Import Morphisms.
(*
Ltac procVc Hvc :=
simpl in Hvc;
rewrite all_vars_ot in Hvc;
simpl in Hvc;
do 2 rewrite allvars_bterm in Hvc;
rewrite app_nil_l in Hvc;
unfold all_vars in Hvc;
autorewrite with list in Hvc;
rewrite cons_as_app in Hvc;
rwsimpl Hvc.
*)
(*
(* for this to work, replace mkAppBeta with mkApp in lambda case of translate *)
Lemma translateSubstCommute ienv : forall (A B: STerm) (x:V),
(* A must have been preprocessed with change_bvars_alpha *)
disjoint (bound_vars B) (bound_vars A) (* A will be alpha renamed before substitution to ensure this *)
-> checkBC (free_vars B ++ (remove_nvars [x] (free_vars A))) B = true
-> checkBC (free_vars A ++ free_vars B) A = true
-> varsOfClass (x::(all_vars A (* ++ all_vars B*) )) userVar
->
let tr := translate true ienv in
tr (ssubst_aux A [(x,B)])
= (ssubst_aux (tr A) [(x,B); (vprime x, tprime B); (vrel x, tr B)]).
Proof.
simpl.
induction A as [| o lbt Hind] using NTerm_better_ind ;
intros B x Hdis H1bc H2bc Hvc;[|destruct o]; try refl;
[ | | | | | | | | | |].
(* variable *)
- hideRHS rhs.
simpl.
rewrite beq_deq.
cases_if as hd; subst.
+ simpl. unfold rhs. simpl.
rewrite <- beq_var_refl.
autorewrite with Param. refl.
+ simpl. unfold rhs. clear rhs.
unfold all_vars in Hvc. simpl in *.
unfold varsOfClass, lforall in Hvc.
simpl in *; dLin_hyp.
let tac:=
autorewrite with Param;
unfold varClass1;
try setoid_rewrite Hyp; try setoid_rewrite Hyp0;
compute; congruence in
do 2 rewrite varClassNotEq by tac.
rewrite not_eq_beq_var_false; auto;[].
apply vRelInjective2. assumption.
- (* Lambda *)
Local Opaque transLam.
simpl. destruct lbt as [| b lbt]; simpl; [refl|].
let tac := try reflexivity in destructbtdeep2 b tac.
rename bnt into lamTyp.
(* process each BTerm before going to the next *)
destruct lbt as [| b2 lbt]; [refl |].
let tac := try reflexivity in destructbtdeep2 b2 tac.
rename b2lv1 into lamVar.
rename b2nt into lamBody.
Local Opaque sub_filter.
destruct lbt; [ |refl].
Local Opaque decide.
simpl in *.
repeat rewrite app_nil_r in H1bc.
repeat rewrite app_nil_r in H2bc.
rewrite decide_true in H2bc;[| disjoint_reasoningv].
ring_simplify in H2bc.
fold V in lamVar.
repeat rewrite andb_true in H2bc. repnd.
rewrite Decidable_spec in H2bc.
rwsimpl Hdis. rwsimpl Hdup. rwsimpl Hvc.
fold V in lamVar. repnd.
clear Hvc4 Hvc2. unfold singleton in *.
rewrite sub_filter_nil_r.
Abort.
*)
Lemma checkBCLamAux (lamVar x:V) (lamBody lamTyp B: STerm ):
disjoint (bound_vars B) [lamVar]
-> (checkBC (free_vars B ++ remove x (free_vars lamTyp ++ remove lamVar (free_vars lamBody))) B =
true)
-> (checkBC (free_vars B ++ remove x (free_vars lamBody)) B = true).
Proof using.
intros Hdis H2nd.
apply (fst (checkBCStrengthen [lamVar])) in H2nd;[| assumption].
revert H2nd. apply (fst checkBCSubset).
rewrite remove_app.
setoid_rewrite eqset_app_comm at 4.
do 2 rewrite app_assoc.
apply subset_app_r.
setoid_rewrite eqset_app_comm at 3.
do 1 rewrite <- app_assoc.
apply subsetvAppLR;[eauto|].
rewrite remove_comm. apply removeConsCancel.
Qed.
(* used in the lambda case and the pi case *)
Lemma transLamSubstCommute:
forall (ienv : indEnv) (argSort : option sort) (lamTyp : STerm) (lamVar : V) (lamBody : STerm),
(
forall (nt : STerm) (lv : list (N * name)),
bterm [] lamTyp = bterm lv nt \/ bterm [lamVar] lamBody = bterm lv nt \/ False ->
forall (B : STerm) (x : V),
disjoint (bound_vars B) (bound_vars nt) ->
checkBC (free_vars B ++ remove x (free_vars nt)) B = true ->
checkBC (free_vars nt ++ free_vars B) nt = true ->
varsOfClass (x :: all_vars nt) userVar ->
translate true ienv (ssubst_aux nt [(x, B)]) =
ssubst_aux (translate true ienv nt)
[(x, B); (vprime x, tprime B); (vrel x, translate true ienv B)] )
->
forall (B : STerm) (x : V),
disjoint (bound_vars B) (bound_vars lamTyp ++ lamVar :: bound_vars lamBody) ->
checkBC ((free_vars lamTyp ++ remove lamVar (free_vars lamBody)) ++ free_vars B) lamTyp =
true ->
checkBC (lamVar :: (free_vars lamTyp ++ remove lamVar (free_vars lamBody)) ++ free_vars B)
lamBody = true ->
checkBC (free_vars B ++ remove x (free_vars lamTyp ++ remove lamVar (free_vars lamBody))) B =
true ->
disjoint [lamVar] ((free_vars lamTyp ++ remove lamVar (free_vars lamBody)) ++ free_vars B) ->
varsOfClass [x] userVar ->
varsOfClass (all_vars lamTyp) userVar ->
varsOfClass [lamVar] userVar ->
varsOfClass (all_vars lamBody) userVar ->
transLam true (translate true ienv) (lamVar, (ssubst_aux lamTyp [(x, B)], argSort))
(translate true ienv (ssubst_aux lamBody (sub_filter [(x, B)] [lamVar]))) =
ssubst_aux
(transLam true (translate true ienv) (lamVar, (lamTyp, argSort)) (translate true ienv lamBody))
[(x, B ); (vprime x, tprime B); (vrel x, translate true ienv B)].
Proof using.
intros ? ? ? ? ? Hind ? ? H2d H1nd H3nd H2nd H1d H1vc H2vc H3vc H4vc.
hideRHS rhs. simpl.
Local Opaque ssubst_bterm_aux.
unfold rhs. clear rhs. simpl.
Local Transparent ssubst_bterm_aux.
simpl ssubst_bterm_aux at 1.
unfold all_vars in *. rwsimpl H2vc. rwsimpl H4vc.
rwsimpl Hvc.
rewrite ssubst_trim by tauto.
Local Opaque ssubst_bterm_aux.
symmetry.
simpl in *. repeat rewrite app_nil_r in *.
do 2 progress f_equal.
Local Transparent ssubst_bterm_aux.
Local Opaque ssubst_aux sub_filter.
simpl.
do 2 progress f_equal. simpl.
Local Transparent ssubst_aux.
simpl ssubst_aux at 1. rewrite sub_filter_nil_r.
rewrite <- ssubst_aux_sub_filter2
with
(l:=[x; vrel x])
(sub:= (sub_filter [(x, B); (vprime x, tprime B); (vrel x, translate true ienv B)] [lamVar]));
[ |apply vDisjointTPrimeUserVar with (lb := [x]); tauto].
rewrite sub_filter_swap.
rewrite sub_filter_nil_r.
Local Transparent sub_filter. simpl sub_filter at 1.
Local Opaque sub_filter.
do 2 rewrite deq_refl. symmetry.
symmetry. do 3 rewrite decideFalse by eauto with Param.
rename H3vc into Hvclv.
rename H1vc into Hvcxb.
pose proof (vDisjointPrimeUserVar _ _ Hvcxb Hvclv) as Hdiss.
rewrite disjoint_app_r in Hdiss. apply proj1 in Hdiss.
rewrite sub_filter_disjoint1 by assumption.
clear Hdiss.
rewrite <- substAuxPrimeCommute1.
do 5 progress f_equal.
(* the type of the (vrel lamVar) and the body lamBody remain.
the type of lamVar and (tprime lamTyp) are already taken care of *)
simpl.
rewrite decide_decideP.
destructDecideP.
+ clear Hind. (* ssubst gets filtered out. so no Hind needed *)
subst. Local Transparent sub_filter. simpl.
do 1 rewrite deq_refl.
do 2 rewrite decideFalse by eauto with Param. simpl.
do 1 rewrite deq_refl.
do 1 rewrite decideFalse by eauto with Param.
simpl.
do 1 rewrite deq_refl.
(* get the second BTerm [translate lamBody] to match up *)
do 2 rewrite ssubst_aux_nil.
do 4 f_equal. symmetry.
(* now we only have [translate lamTyp] to worry about.
In the RHS subst (after translate), we have a subst of length 1 (only for [vrel x]):
the first 2 items have been filtered out.
In the translation, [translate lamTyp] is in the scope of the binders
[x:lamType] and [(vprime x):tprime lamType]. So those get filtered out in the RHS
substitution. That's why no shadowing.
We don't (can't) use the induction hypothesis.
Indeed, it was filtered out in the first step after +.
In the next branch (+), we will have a substitution of length 3 and use the induction
hypothesis.*)
rewrite ssubst_aux_trivial_disj;[| simpl; noRepDis2].
rewrite ssubst_aux_trivial_disj;[refl|].
rewrite mkAppNoBeta. simpl.
disjoint_reasoningv2; try apply disjoint_neq_iff;
try apply vRelNeqVPrime;
try apply vRelNeqV.
Local Transparent castIfNeeded.
unfold castIfNeeded, projTyRel. rename H1d1 into H1d2.
assert (disjoint (free_vars (translate true ienv lamTyp)) [vrel x]).
apply disjoint_sym in H1d2.
apply translateFvarsDisj with (ienv:=ienv) in H1d2;
[unfold vAllRelated in H1d2; simpl in H1d2; noRepDis2 |].
rwsimplC. dands; eauto with SquiggleEq.
case_if; rwsimplC; unfold id in *; auto.
disjoint_reasoningv2; auto.
* pose proof (vDisjointUserVar _ _ H2vc0 Hvcxb).
simpl in *. disjoint_reasoningv2.
* pose proof (vDisjointTPrimeUserVar _ _ H2vc0 Hvcxb).
simpl in *. disjoint_reasoningv2.
+ (* here, substitution for [x] actually happens *)
pose proof n as Hd. apply disjoint_neq_iff in Hd.
apply vAllRelatedFlatDisj in Hd; [| rwsimplC; eauto with SquiggleEq; fail].
simpl in Hd.
rewrite sub_filter_disjoint1 with (lf := [lamVar]) (* start from innermost filter *)
by (simpl; disjoint_reasoningv2).
rewrite sub_filter_disjoint1 with (lf := [vprime lamVar]) (* start from innermost filter *)
by (simpl; disjoint_reasoningv2).
rewrite sub_filter_disjoint1 with (lf := [vrel lamVar]) (* start from innermost filter *)
by (simpl; disjoint_reasoningv2).
assert (checkBC (free_vars B ++ remove x (free_vars lamTyp)) B = true).
revert H2nd. apply (fst checkBCSubset).
rewrite remove_app. rewrite app_assoc. apply subset_app_r. eauto; fail.
assert (checkBC (free_vars B ++ remove x (free_vars lamBody)) B = true).
revert H2nd. apply checkBCLamAux. disjoint_reasoningv2.
assert (checkBC (free_vars lamBody ++ free_vars B) lamBody = true).
revert H3nd. apply (fst checkBCSubset).
rewrite cons_as_app. rewrite app_assoc.
apply subsetvAppLR;[| reflexivity].
rewrite eqset_app_comm.
rewrite <- app_assoc.
apply subset_app_l.
rewrite eqset_app_comm.
apply removeConsCancel.
assert (checkBC (free_vars lamTyp ++ free_vars B) lamTyp = true).
revert H1nd. apply (fst checkBCSubset).
apply subsetvAppLR;[| reflexivity].
apply subset_app_r. reflexivity.
disjoint_reasoningv2.
(* setoid_rewrite (disjoint_remove_nvars_l [lamVar]) in H1d5.
setoid_rewrite remove_nvars_nop in H1d5;[| disjoint_reasoningv2]. *)
rewrite <- Hind with (lv := [lamVar]); auto; try disjoint_reasoningv2;
[ | rwsimplC; dands; eauto with SquiggleEq].
do 2 progress f_equal.
symmetry.
(* Unlike the previous bullet (+), here we need to use the induction hypothesis
for [translate lamTyp]. See the last comment in the above bullet.
Unlike the subgoal there, here the substitution in RHS has length 3.
*)
rewrite mkAppNoBeta. simpl. unfold mkAppNoCheck. simpl.
do 6 (rewrite not_eq_beq_var_false; [ | noRepDis2]).
do 3 (progress f_equal).
Ltac tac Hind := (apply Hind with (lv:=[]); auto;
try (disjoint_reasoningv2); try (rewrite cons_as_app; rwsimplC; eauto with SquiggleEq)).
Ltac tacOld Hind := (apply Hind with (lv:=[]); auto;
[disjoint_reasoningv2| rewrite cons_as_app; rwsimplC; eauto with SquiggleEq]).
cases_if;
[
simpl; unfold projTyRel, mkConstApp, mkApp, mkAppNoCheck;
simpl; do 4 (progress f_equal);
[ | f_equal | do 2 progress f_equal; tac Hind]
| unfold id; tac Hind
];
symmetry;[ apply ssubst_trim| rewrite ssubst_trim_prime]; auto.
rewrite substAuxPrimeCommute1. refl.
Qed.
Ltac revertAll :=
repeat match goal with
| [H:_ |- _] => revert H
end.
Ltac eqList :=
repeat match goal with
[|- cons _ _ = cons _ _] => f_equal
end.
(**
Note that in the LHS, [translate] is called on [(ssubst_aux A [(x,B)])], which
may have duplicate bound variables, even though [A] has unique bound variables.
Consider [A:= x x] and [B:= \y.y].
In the paper, we said that [translate] assumes that the input has unique boundvars.
That would make the LHS illegitimate.
We do need some condition: see examples/capture.v where a form of repeated boundvars
causes capture.
Perhaps we need a weaker condition: Barendredgt convention seems to suffice for this proof.
Why not make the weakest condition that suffices?
Then, if we prove that [translate] preserves alpha equality for terms only containing
uservars and in barendredgt convention, we'll be done.
beta does not preserve BC. so the subst function used in red will
need to take [B], which is already in BC and rename
it ti [B'] such that its bvars to be disjoint from [all_vars A]. [B'] is also in BC.
(this is kinda what would happen if we did the substitution A[B/x] in DB world and converted back to named)
in LHS, we will have [B']. In RHS, we will have something alpha equal to [translate B]
such that its bvars are disjoint from [all_vars (translate A)].
But, [translate B] is alpha equal to [translate B']. after rewriting, we can invoke this lemma
(We could instead precompose [translate] with a function to make boundvars [NoDup].
But then we would have to reason about alpha equality in the proof below.
[translate] does not unconditionally
respect alpha equality, as examples/capture.v shows. so we cannot "rewrite" after the proof)
When proving preservation of reduction, we will get in trouble because [NoDup].
*)
(* for this to work, replace mkAppBeta with mkApp in lambda case of translate *)
Lemma translateSubstCommute ienv : forall (A B: STerm) (x:V),
(* A must have been preprocessed with change_bvars_alpha *)
disjoint (bound_vars B) (bound_vars A) (* A will be alpha renamed before substitution to ensure this *)
-> checkBC (free_vars B ++ (remove_nvars [x] (free_vars A))) B = true
-> checkBC (free_vars A ++ free_vars B) A = true
-> varsOfClass (x::(all_vars A (* ++ all_vars B*) )) userVar
->
let tr := translate true ienv in
tr (ssubst_aux A [(x,B)])
= (ssubst_aux (tr A) [(x,B); (vprime x, tprime B); (vrel x, tr B)]).
(* currently, nothing prevents the translation of A from picking bvars that free in B. tr A
only looks at A and is free to pick anything that is not free on parts of A that it looks at.
unless we have all free vars of B free in all subterms of A (impossible), there can be
a problem if we allow the translation to keep picking arbitrary bound vars. All the bvars
in the translation
must be obtained by a function of the input. Then we may also be able to obtain many free
theorems by parametricity. Seems we need 5 class. Or use a combinator for Pi. But then we need
to tackle universe issues *)
Proof.
simpl.
induction A as [| o lbt Hind] using NTerm_better_ind ;
intros B x Hdis H1bc H2bc Hvc;[|destruct o]; try refl;
[ | | | | | | | | | |].
(* variable *)
- hideRHS rhs.
simpl.
rewrite beq_deq.
cases_if as hd; subst.
+ simpl. unfold rhs. simpl.
rewrite <- beq_var_refl.
autorewrite with Param. refl.
+ simpl. unfold rhs. clear rhs.
unfold all_vars in Hvc. simpl in *.
unfold varsOfClass, lforall in Hvc.
simpl in *; dLin_hyp.
let tac:=
autorewrite with Param;
unfold varClass1;
try setoid_rewrite Hyp; try setoid_rewrite Hyp0;
compute; congruence in
do 2 rewrite varClassNotEq by tac.
rewrite not_eq_beq_var_false; auto;[].
apply vRelInjective2. assumption.
- (* Lambda *)
Local Opaque transLam.
simpl. destruct lbt as [| b lbt]; simpl; [refl|].
let tac := try reflexivity in destructbtdeep2 b tac.
rename bnt into lamTyp.
(* process each BTerm before going to the next *)
destruct lbt as [| b2 lbt]; [refl |].
let tac := try reflexivity in destructbtdeep2 b2 tac.
rename b2lv1 into lamVar.
rename b2nt into lamBody.
Local Opaque sub_filter.
destruct lbt; [ |refl].
Local Opaque decide.
simpl in *.
repeat rewrite app_nil_r in H1bc.
repeat rewrite app_nil_r in H2bc.
rewrite decide_true in H2bc;[| disjoint_reasoningv].
ring_simplify in H2bc.
fold V in lamVar.
repeat rewrite andb_true in H2bc. repnd.
rewrite Decidable_spec in H2bc.
rwsimpl Hdis. rwsimpl Hdup. rwsimpl Hvc.
fold V in lamVar. repnd.
clear Hvc4 Hvc2. unfold singleton in *.
rewrite sub_filter_nil_r.
eapply transLamSubstCommute; eauto.
- (* Pi *)
Local Opaque transLam.
simpl. destruct lbt as [| b lbt]; simpl; [refl|].
let tac := try reflexivity in destructbtdeep2 b tac.
rename bnt into piVarType.
(* process each BTerm before going to the next *)
destruct lbt as [| b2 lbt]; [refl |].
let tac := try reflexivity in destructbtdeep2 b2 tac.
rename b2lv1 into piVar.
rename b2nt into piRangeType.
simpl in *.
destruct lbt; [ |refl].
rwsimpl Hdis. rwsimpl Hdup. rwsimpl Hvc.
unfold all_vars in Hvc. rwsimpl Hvc.
fold V in piVar. repnd.
repnd.
repeat match goal with
[H: varsOfClass [] _ |- _ ] => clear H
end.
unfold singleton in *.
repeat rewrite sub_filter_nil_r.
(* so far, same as that of the lambda case, except for different naming *)
unfold mkPiRNew.
simpl in *.
repeat rewrite app_nil_r in H1bc.
repeat rewrite app_nil_r in H2bc.
rewrite decide_true in H2bc;[| disjoint_reasoningv].
ring_simplify in H2bc.
repeat rewrite andb_true in H2bc. repnd.
rewrite Decidable_spec in H2bc.
(* The 2 cases generated by the destruct below are very different.
In the None (anyrel) case, we manually make the lambdas.
(Initially, I used a combinator, but ran into universe issues)
In the Some (isorel case), we make make a constant (combinator) applied to arguments:
in this case we know that the domain and the codomain are in Set/Prop:
We have disabled forall T:Type: True : Prop. *)
Local Transparent sub_filter.
assert (checkBC (free_vars B ++ remove x (free_vars piVarType)) B = true).
revert H1bc. apply checkBCSubset. rewrite remove_app.
rewrite app_assoc.
apply subset_app_r. reflexivity.
assert (checkBC (free_vars piVarType ++ free_vars B) piVarType = true).
revert H2bc3.
apply checkBCSubset. apply subsetvAppLR;[| reflexivity].
apply subset_app_r. reflexivity.
destruct (needGoodnessPi true argsort bodySort).
+ simpl. unfold mkAppNoCheck, tvmap. simpl.
repeat rewrite sub_filter_nil_r. simpl. f_equal.
let rwTac := (clear Hind; repeat rewrite decideFalse by eauto with Param;
rewrite ssubst_aux_nil, ssubst_aux_trivial_disj;[refl|];
try (apply vDisjointTPrimeUserVar with (lb:=[x]); assumption);
try (apply vDisjointUserVar with (lb:=[x]); assumption)) in
eqList; f_equal; symmetry;
[ apply ssubst_trim
| rewrite ssubst_trim_prime by auto; rewrite substAuxPrimeCommute1 | | | | ]; auto;
symmetry;
[ eapply Hind; eauto; [disjoint_reasoningv2| unfold all_vars; rwsimplC;
eauto with SquiggleEq; fail]
| f_equal; eqList; f_equal; symmetry; [apply ssubst_trim; assumption|]
| f_equal; eqList; f_equal; symmetry;
[rewrite ssubst_trim_prime by assumption;symmetry; apply substAuxPrimeCommute1 |]
| eapply transLamSubstCommute; eauto; [|]; unfold all_vars; rwsimplC;
eauto with SquiggleEq ];[|];
simpl;
rewrite (@decide_decideP (piVar=x) _);
destructDecideP; subst; repeat rewrite deq_refl;
[rwTac | | rwTac |]; simpl; [|];
rename n into Hd;
apply disjoint_neq_iff in Hd;
(apply vAllRelatedFlatDisj in Hd; [| rwsimplC; eauto with SquiggleEq; fail]);
simpl in Hd; repeat rewrite decideFalse by
(apply disjoint_neq_iff;simpl; disjoint_reasoningv2);
[apply ssubst_trim; auto |]; [].
rewrite ssubst_trim_prime by assumption.
symmetry. apply substAuxPrimeCommute1.
Local Transparent decide.
+ (* no extra proofs because this Pi Type is in a higher universe. This part
is same as the AnyRel translation *)
admit.
- (* sort *)
simpl. destruct lbt; [ | refl]. simpl map. cbv iota.
rewrite ssubst_aux_trivial_disj;[refl | simpl; disjoint_reasoningv2].