-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDistSubtyping.v
2185 lines (1935 loc) · 74.7 KB
/
DistSubtyping.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
(** This file contains the declarative and algorithmic subtyping formalization.
The algorithmic system is proved to be sound and complete w.r.t the
declarative one (in Thereoem dsub2asub).
Some inversion lemmas (end with _inv) are provided to justify the algorithm.
*)
Require Import LibTactics.
Require Import Coq.micromega.Lia.
Require Import LN_Lemmas.
Require Export Definitions.
(************************ Notations related to types **************************)
Notation "[ z ~~> u ] t" := (typsubst_typ u z t) (at level 0).
Notation "t ^-^ u" := (open_typ_wrt_typ t u) (at level 67).
Notation "t -^ x" := (open_typ_wrt_typ t (t_tvar_f x))(at level 67).
Notation "[[ A ]]" := (typefv_typ A) (at level 0).
Notation "A <: B" := (declarative_subtyping A B)
(at level 65, B at next level, no associativity) : type_scope.
(************************************ Ltac ************************************)
(* redefine gather_atoms for pick fresh *)
Ltac gather_atoms ::= (* for type var *)
let A := gather_atoms_with (fun x : atoms => x) in
let B := gather_atoms_with (fun x : atom => singleton x) in
let C := gather_atoms_with (fun x : list (var * typ) => dom x) in
let E := gather_atoms_with (fun x : typ => typefv_typ x) in
constr:(A `union` B `union` C `union` E).
(* autorewrite with open *)
Create HintDb open.
Lemma open_into_and : forall B C X, (t_and B C) -^ X = t_and (B -^ X) (C -^ X).
Proof. eauto. Qed.
Lemma open_into_or : forall B C X, (t_or B C) -^ X = t_or (B -^ X) (C -^ X).
Proof. eauto. Qed.
Lemma open_into_top : forall X, t_top -^ X = t_top.
Proof. eauto. Qed.
Lemma open_into_bot : forall X, t_bot -^ X = t_bot.
Proof. eauto. Qed.
#[export] Hint Rewrite open_into_and open_into_or open_into_top open_into_bot : open.
(* try solve the goal by contradiction *)
Create HintDb FalseHd.
Ltac solve_false := try intro; try solve [false; eauto 4 with FalseHd].
(* destrcut conjunctions *)
Ltac destruct_conj :=
repeat match goal with H: ?T |- _ =>
lazymatch T with
| exists _ , _ => destruct H
| _ /\ _ => destruct H
end
end.
Ltac detect_fresh_var_and_do t :=
match goal with
| Fr : ?x `notin` ?L1 |- _ => t x
| _ =>
let x := fresh "x" in
pick fresh x; t x
end.
Ltac instantiate_cofinite_with H X :=
match type of H with
| forall x, x `notin` ?L -> _ =>
let H1 := fresh "H" in
assert (H1 : X `notin` L) by solve_notin;
specialize (H X H1); clear H1
| X `notin` ?L -> _ =>
let H1 := fresh "H" in
assert (H1 : X `notin` L) by solve_notin;
specialize (H H1); clear H1
end.
Ltac specialize_with X :=
repeat match goal with
| H : forall X : typevar, _ |- _ => specialize (H X)
end.
Ltac instantiate_cofinites_with x :=
repeat match goal with
| H : forall x, x `notin` ?L -> _ |- _ =>
instantiate_cofinite_with H x
| H : x `notin` ?L -> _ |- _ =>
instantiate_cofinite_with H x
end;
destruct_conj.
Ltac instantiate_cofinites :=
detect_fresh_var_and_do instantiate_cofinites_with.
Ltac applys_and_instantiate_cofinites_with H x :=
applys H x; try solve_notin; instantiate_cofinites_with x.
Ltac pick_fresh_applys_and_instantiate_cofinites H :=
let X:= fresh in
pick fresh X; applys_and_instantiate_cofinites_with H X.
Ltac detect_fresh_var_and_apply H :=
let f x := applys_and_instantiate_cofinites_with H x in
detect_fresh_var_and_do f.
(******************************* type sizes ***********************************)
(** defines size on types and proves some related
lemmas. It aims to make later proofs easier if they do
induction on the size of types *)
Lemma splu_decrease_size: forall A B C,
splu A B C -> size_typ B < size_typ A /\ size_typ C < size_typ A.
Proof with (pose proof (size_typ_min); simpl in *; try lia).
introv H.
induction H; simpl in *; eauto...
pick fresh X. forwards* (?&?): H0.
rewrite 2 size_typ_open_typ_wrt_typ_var in H3.
rewrite 2 size_typ_open_typ_wrt_typ_var in H2.
eauto...
Qed.
Lemma spli_decrease_size: forall A B C,
spli A B C -> size_typ B < size_typ A /\ size_typ C < size_typ A.
Proof with (pose proof (size_typ_min); simpl in *; try lia).
introv H.
induction H; simpl in *; eauto...
- forwards (?&?): splu_decrease_size H0...
- pick fresh X. forwards* (?&?): H0.
rewrite 2 size_typ_open_typ_wrt_typ_var in H3.
rewrite 2 size_typ_open_typ_wrt_typ_var in H2.
eauto...
Qed.
Ltac spl_size :=
try repeat match goal with
| [ H: splu _ _ _ |- _ ] =>
( lets (?&?): splu_decrease_size H; clear H)
| [ H: spli _ _ _ |- _ ] =>
( lets (?&?): spli_decrease_size H; clear H)
end.
(********************************************)
(* *)
(* Ltac elia *)
(* enhanced lia with split_decrease_size *)
(* *)
(********************************************)
Ltac elia :=
try solve [pose proof (size_typ_min);
let x := fresh "x" in
pick fresh x; try instantiate_cofinites_with x; (* forall x, x `notin` .. -> spli .. *)
spl_size; simpl in *; simpl;
try repeat rewrite size_typ_open_typ_wrt_typ_var in *; (* spl A-^X ... *)
try lia].
(* eauto with typSize lngen ? *)
Ltac indTypSize s :=
assert (SizeInd: exists i, s < i) by eauto;
destruct SizeInd as [i SizeInd];
repeat match goal with | [ h : typ |- _ ] => (gen h) end;
induction i as [|i IH]; [
intros; match goal with | [ H : _ < 0 |- _ ] => inverts H end
| intros ].
(********************************************)
(* *)
(* Ltac solve_false *)
(* try solve the goal by contradiction *)
(* *)
(********************************************)
#[export] Hint Extern 1 => progress instantiate_cofinites : FalseHd.
(* splittable types and ordinary types do not overlap *)
Lemma splu_ord_false : forall A B C,
splu A B C -> ordu A -> False.
Proof with solve_false.
introv Spl Ord. gen B C.
induction Ord; intros; inverts* Spl...
Qed.
Lemma spli_ord_false : forall A B C,
spli A B C -> ordi A -> False.
Proof.
introv Spl Ord. gen B C.
induction Ord; intros; inverts* Spl.
eauto using splu_ord_false. solve_false.
Qed.
Ltac find_contradiction_on_split :=
match goal with
| [ H1: splu ?T _ _ , H2: ordu ?T |- _ ] => applys~ splu_ord_false H1 H2
| [ H1: spli ?T _ _ , H2: ordi ?T |- _ ] => applys~ spli_ord_false H1 H2
| [ H: ordu _ |- _ ] => inverts H; fail
| [ H: splu _ _ _ |- _ ] => inverts H; fail
| [ H: ordi _ |- _ ] => inverts H; fail
| [ H: spli _ _ _ |- _ ] => inverts H; fail
end.
#[export] Hint Extern 1 => find_contradiction_on_split : FalseHd.
#[export] Hint Extern 1 => applys splu_ord_false; [ eassumption | ] : FalseHd.
#[export] Hint Extern 1 => applys spli_ord_false; [ eassumption | ] : FalseHd.
(*********************** locally closed types and terms ***********************)
Lemma lc_forall_inv : forall A X,
lc_typ (t_forall A) -> lc_typ (A -^ X).
Proof. intros. inverts~ H. Qed.
#[export] Hint Immediate lc_forall_inv : core.
Ltac solve_lc_by_inv A :=
match goal with
| H: lc_typ A |- _ => exact H
| H: lc_typ (_ -^ _) |- _ => match type of H with context[ A ] => autorewrite with open in H end
| H: lc_typ (t_or _ _) |- _ => match type of H with context[ A ] => inverts H end
| H: lc_typ (t_and _ _) |- _ => match type of H with context[ A ] => inverts H end
| H: lc_typ (t_rcd _ _) |- _ => match type of H with context[ A ] => inverts H end
| H: lc_typ (t_arrow _ _) |- _ => match type of H with context[ A ] => inverts H end
| H: lc_typ (t_forall _) |- _ => match type of H with context[ A ] => inverts H end
end.
#[export] Hint Extern 1 (lc_typ ?A ) => progress repeat solve_lc_by_inv A : core.
#[export] Hint Extern 1 (lc_typ (?A -^ _) ) => progress instantiate_cofinites : core.
#[export] Hint Extern 1 (lc_typ (?A -^ _) ) => progress repeat solve_lc_by_inv A : core.
#[export] Hint Extern 1 (lc_typ (?A -^ ?X) ) =>
match goal with
H: forall x, lc_typ _ |- _ =>
match type of H with context [A] => specialize (H X) end
end : core.
Lemma ordu_lc : forall A, ordu A -> lc_typ A.
Proof. introv H. induction~ H. Qed.
Lemma ordi_lc : forall A, ordi A -> lc_typ A.
Proof. introv H. induction~ H. eauto using ordu_lc. Qed.
Lemma orduFty_lc : forall Fty, UnionOrdinaryFty Fty -> lc_Fty Fty.
Proof with eauto using ordu_lc. introv H. induction H... Qed.
Lemma splu_lc : forall A B C, splu A B C-> lc_typ A /\ lc_typ B /\ lc_typ C.
Proof.
introv H.
induction H; repeat split; firstorder using ordu_lc, ordi_lc.
Qed.
Lemma spli_lc : forall A B C, spli A B C -> lc_typ A /\ lc_typ B /\ lc_typ C.
Proof with firstorder using ordu_lc, ordi_lc, splu_lc.
introv H.
induction H; repeat split~; constructor...
Qed.
Lemma declarative_subtyping_lc : forall A B, declarative_subtyping A B -> lc_typ A /\ lc_typ B.
Proof.
introv H. induction H; destruct_conj; split*.
all: eauto.
all: inverts H; inverts H0; econstructor;
intros; autorewrite with open; eauto.
Qed.
Lemma algo_sub_lc : forall A B, algo_sub A B -> lc_typ A /\ lc_typ B.
Proof with firstorder using ordu_lc, ordi_lc, splu_lc, spli_lc.
introv H.
induction~ H; split; destruct_conj...
Qed.
Lemma new_splu_lc : forall A B C, new_splu A B C-> lc_typ A /\ lc_typ B /\ lc_typ C.
Proof. introv H. induction* H. splits; eauto. Qed.
Lemma new_spli_lc : forall A B C, new_spli A B C-> lc_typ A /\ lc_typ B /\ lc_typ C.
Proof with firstorder using new_splu_lc.
introv H.
induction~ H; split; destruct_conj...
Qed.
Ltac solve_lc_by_regularity A :=
match goal with
| H: ordu _ |- _ => match type of H with context[ A ] => apply ordu_lc in H end
| H: ordi _ |- _ => match type of H with context[ A ] => apply ordi_lc in H end
| H: UnionOrdinaryFty _ |- _ => match type of H with context[ A ] => apply orduFty_lc in H end
| H: splu _ _ _ |- _ => match type of H with context[ A ] => apply splu_lc in H end
| H: spli _ _ _ |- _ => match type of H with context[ A ] => apply spli_lc in H end
| H: algo_sub _ _ |- _ => match type of H with context[ A ] => apply algo_sub_lc in H end
| H: new_splu _ _ _ |- _ => match type of H with context[ A ] => apply new_splu_lc in H end
| H: new_spli _ _ _ |- _ => match type of H with context[ A ] => apply new_spli_lc in H end
| H: declarative_subtyping _ _ |- _ => match type of H with context[ A ] => apply declarative_subtyping_lc in H end
end;
destruct_conj.
#[export] Hint Extern 1 (lc_typ ?A ) => progress solve_lc_by_regularity A : core.
#[export] Hint Extern 1 (lc_typ (?A -^ _) ) => progress solve_lc_by_regularity A : core.
(* destruct hypotheses *)
Ltac inverts_all_lc :=
repeat lazymatch goal with
| H: lc_typ (t_or _ _) |- _ => inverts H
| H: lc_typ (t_and _ _) |- _ => inverts H
| H: lc_typ (t_rcd _ _) |- _ => inverts H
| H: lc_typ (t_arrow _ _) |- _ => inverts H
| H: lc_typ (t_forall _) |- _ => inverts H
end.
Ltac inverts_all_ord :=
repeat lazymatch goal with
| H: ordi (t_and _ _) |- _ => inverts H
| H: ordu (t_and _ _) |- _ => inverts H
| H: ordi (t_or _ _) |- _ => inverts H
| H: ordu (t_or _ _) |- _ => inverts H
| H: ordi (t_rcd _ _) |- _ => inverts H
| H: ordu (t_rcd _ _) |- _ => inverts H
| H: ordi (t_arrow _ _) |- _ => inverts H
| H: ordu (t_arrow _ _) |- _ => inverts H
| H: ordi (t_forall _) |- _ => inverts H
| H: ordu (t_forall _) |- _ => inverts H
end.
Ltac inverts_all_spl :=
repeat lazymatch goal with
| H: spli (t_and _ _) _ _ |- _ => inverts H
| H: splu (t_and _ _) _ _ |- _ => inverts H
| H: spli (t_or _ _) _ _ |- _ => inverts H
| H: splu (t_or _ _) _ _ |- _ => inverts H
| H: spli (t_rcd _ _) _ _ |- _ => inverts H
| H: splu (t_rcd _ _) _ _ |- _ => inverts H
| H: spli (t_arrow _ _) _ _ |- _ => inverts H
| H: splu (t_arrow _ _) _ _ |- _ => inverts H
| H: spli (t_forall _) _ _ |- _ => inverts H
| H: splu (t_forall _) _ _ |- _ => inverts H
end.
(********************* lc & rename & subst **********************************)
Lemma lc_typ_rename : forall A X Y,
X \notin (typefv_typ A) -> lc_typ (A -^ X) -> lc_typ (A -^ Y).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: lc_typ [X ~~> (t_tvar_f Y)] (A -^ X)).
applys~ typsubst_typ_lc_typ.
simpl in H. rewrite typsubst_typ_spec in H.
rewrite close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
Ltac solve_lc_4 :=
progress (* in case X is Y *)
( match goal with
| |- lc_typ (?A -^ ?y) => unfold open_typ_wrt_typ; simpl
end;
try econstructor;
match goal with
| H: ?y `notin` _ |- lc_typ (open_typ_wrt_typ_rec 0 (t_tvar_f ?x) ?A) => applys lc_typ_rename y; [solve_notin | ]
end ).
#[export] Hint Extern 1 (lc_typ _) => progress solve_lc_4 : core.
(* rename / typsubst in ord & split *)
#[local] Hint Resolve typsubst_typ_lc_typ : core.
(*********************************)
(* some useful lemmas *)
(* for proving typsubst lemmas: *)
(* lc_t_forall_exists *)
(* typsubst_typ_spec *)
(* typsubst_typ_open_typ_wrt_typ *)
(*********************************)
(* mimic typsubst_lc *)
Lemma rename_ordu : forall A X Y,
ordu A ->
ordu ( [X ~~> (t_tvar_f Y)] A ).
Proof with (simpl in *; eauto).
introv Ord. gen X Y. induction Ord; intros...
- destruct (X==X0)...
- applys~ (OrdU_forall (L \u {{X}})).
introv Fr. forwards* Ord: H0 X0 X Y.
rewrite typsubst_typ_open_typ_wrt_typ in Ord...
case_eq (@eq_dec typevar EqDec_eq_of_X X0 X); intuition...
rewrite H1 in Ord...
Qed.
Lemma rename_ordi : forall A X Y,
ordi A ->
ordi ( [X ~~> (t_tvar_f Y)] A ).
Proof with (simpl in *; eauto using rename_ordu).
introv Ord. gen X Y. induction Ord; intros...
- destruct (X==X0)...
- applys~ (OrdI_forall (L \u {{X}})).
introv Fr. forwards* Ord: H0 X0 X Y.
rewrite typsubst_typ_open_typ_wrt_typ in Ord...
case_eq (@eq_dec typevar EqDec_eq_of_X X0 X); intuition...
rewrite H1 in Ord...
Qed.
#[export] Hint Immediate rename_ordu rename_ordi : core.
Lemma rename_splu : forall A B C X Y,
splu A B C->
splu ([X ~~> (t_tvar_f Y)] A) ([X ~~> (t_tvar_f Y)] B) ([X ~~> (t_tvar_f Y)] C).
Proof with (simpl in *; eauto).
introv Spl. gen X Y.
induction Spl; intros...
- applys~ (SpU_forall (L \u {{X}})).
introv Fr. forwards* Spl: H0 X0 X Y.
rewrite 3 typsubst_typ_open_typ_wrt_typ in Spl...
case_eq (@eq_dec typevar EqDec_eq_of_X X0 X); intuition...
rewrite H1 in Spl...
Qed.
Lemma rename_spli : forall A B C X Y,
spli A B C->
spli ([X ~~> (t_tvar_f Y)] A) ([X ~~> (t_tvar_f Y)] B) ([X ~~> (t_tvar_f Y)] C).
Proof with (simpl in *; eauto using rename_ordi, rename_splu).
introv Spl. gen X Y.
induction Spl; intros...
- applys~ (SpI_forall (L \u {{X}})).
introv Fr. forwards* Spl: H0 X0 X Y.
rewrite 3 typsubst_typ_open_typ_wrt_typ in Spl...
case_eq (@eq_dec typevar EqDec_eq_of_X X0 X); intuition...
rewrite H1 in Spl...
Qed.
Lemma rename_algo_sub : forall A B X Y,
algo_sub A B ->
algo_sub ([X ~~> (t_tvar_f Y)] A) ([X ~~> (t_tvar_f Y)] B).
Proof with (simpl in *; eauto using rename_spli, rename_splu).
introv s. gen X Y.
induction s; intros...
- applys~ (ASub_forall (L \u {{X}})).
introv Fr. forwards* HS: H0 X0 X Y.
rewrite 2 typsubst_typ_open_typ_wrt_typ in HS...
case_eq (@eq_dec typevar EqDec_eq_of_X X0 X); intuition...
rewrite H1 in HS...
Qed.
#[export] Hint Immediate rename_ordu rename_ordi
rename_spli rename_splu rename_algo_sub : core.
Lemma ordu_rename_open : forall A X Y,
X \notin (typefv_typ A) -> ordu( A -^ X ) -> ordu( A -^ Y ).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: ordu[X ~~> (t_tvar_f Y)] (A -^ X) ).
applys~ rename_ordu.
simpl in H. rewrite typsubst_typ_spec in H.
rewrite close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
Lemma ordi_rename_open : forall A X Y,
X \notin (typefv_typ A) -> ordi ( A -^ X ) -> ordi ( A -^ Y ).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: ordi [X ~~> (t_tvar_f Y)] (A -^ X) ).
applys~ rename_ordi.
simpl in H. rewrite typsubst_typ_spec in H.
rewrite close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
Lemma splu_rename_open : forall A B C X Y,
X \notin (typefv_typ A) \u (typefv_typ B) \u (typefv_typ C)->
splu ( A -^ X ) ( B -^ X ) ( C -^ X ) ->
splu ( A -^ Y ) ( B -^ Y ) ( C -^ Y ).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: splu [X ~~> (t_tvar_f Y)] (A -^ X) [X ~~> (t_tvar_f Y)] (B -^ X) [X ~~> (t_tvar_f Y)] (C -^ X)).
applys~ rename_splu.
simpl in H. rewrite 3 typsubst_typ_spec in H.
rewrite 3 close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
Lemma spli_rename_open : forall A B C X Y,
X \notin (typefv_typ A) \u (typefv_typ B) \u (typefv_typ C)->
spli ( A -^ X ) ( B -^ X ) ( C -^ X ) ->
spli ( A -^ Y ) ( B -^ Y ) ( C -^ Y ).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: spli [X ~~> (t_tvar_f Y)] (A -^ X) [X ~~> (t_tvar_f Y)] (B -^ X) [X ~~> (t_tvar_f Y)] (C -^ X)).
applys~ rename_spli.
simpl in H. rewrite 3 typsubst_typ_spec in H.
rewrite 3 close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
Lemma algo_sub_rename_open : forall A B X Y,
X \notin (typefv_typ A) \u (typefv_typ B) ->
algo_sub ( A -^ X ) ( B -^ X ) ->
algo_sub ( A -^ Y ) ( B -^ Y ).
Proof with (simpl in *; eauto).
introv Fr Lc.
assert (H: algo_sub [X ~~> (t_tvar_f Y)] (A -^ X) [X ~~> (t_tvar_f Y)] (B -^ X)).
applys~ rename_algo_sub.
simpl in H. rewrite 2 typsubst_typ_spec in H.
rewrite 2 close_typ_wrt_typ_open_typ_wrt_typ in H...
Qed.
#[export]
Hint Extern 1 (ordu ( ?A -^ ?Y )) =>
match goal with
| H: ordu ( A -^ ?X ) |- _ => let Fr := fresh in
assert (Fr: X \notin (typefv_typ A)) by solve_notin;
applys ordu_rename_open Fr H
end : core.
#[export]
Hint Extern 1 (ordi ( ?A -^ ?Y )) =>
match goal with
| H: ordi ( A -^ ?X ) |- _ => let Fr := fresh in
assert (Fr: X \notin (typefv_typ A)) by solve_notin;
applys ordi_rename_open Fr H
end : core.
#[export]
Hint Extern 1 (splu ( ?A -^ ?Y ) _ _) =>
match goal with
| H: splu ( A -^ ?X ) ( ?B -^ ?X ) ( ?C -^ ?X ) |- _ => applys splu_rename_open H; solve_notin
end : core.
#[export]
Hint Extern 1 (spli ( ?A -^ ?Y ) _ _) =>
match goal with
| H: spli ( A -^ ?X ) ( ?B -^ ?X ) ( ?C -^ ?X ) |- _ => applys spli_rename_open H; solve_notin
end : core.
#[export]
Hint Extern 1 (algo_sub ( ?A -^ ?Y ) _ ) =>
match goal with
| H: algo_sub ( A -^ ?X ) ( ?B -^ ?X ) |- _ => applys algo_sub_rename_open H; solve_notin
end : core.
#[local] Hint Immediate ordi_rename_open ordu_rename_open spli_rename_open
splu_rename_open algo_sub_rename_open : core.
Lemma ordu_forall_exists : forall X B,
X `notin` typefv_typ B ->
ordu (open_typ_wrt_typ B (t_tvar_f X)) ->
ordu (t_forall B).
Proof with (simpl in *; eauto).
introv Fr Ord.
applys~ OrdU_forall (typefv_typ B).
Qed.
Lemma ordi_forall_exists : forall X B,
X `notin` typefv_typ B ->
ordi (open_typ_wrt_typ B (t_tvar_f X)) ->
ordi (t_forall B).
Proof with (simpl in *; eauto).
introv Fr Ord.
applys~ OrdI_forall (typefv_typ B).
Qed.
#[export]
Hint Extern 1 =>
match goal with
| H: ordi (open_typ_wrt_typ ?B (t_tvar_f ?X)) |- ordi (t_forall _ ?B) =>
applys~ ordi_forall_exists H; solve_notin
end : core.
#[export]
Hint Extern 1 =>
match goal with
| H: ordu (open_typ_wrt_typ ?B (t_tvar_f ?X)) |- ordu (t_forall _ ?B) =>
applys~ ordu_forall_exists H; solve_notin
end : core.
Lemma splu_fv_1 : forall A B C,
splu A B C -> (typefv_typ B) [<=] (typefv_typ A).
Proof with (subst; simpl in *).
introv Hspl.
induction Hspl; simpl in *; try fsetdec.
remember ((typefv_typ A) \u (typefv_typ A1)).
pick fresh X.
forwards~ Aux1: H0 X.
lets* Aux2: typefv_typ_open_typ_wrt_typ_upper A (t_tvar_f X).
lets* Aux3: typefv_typ_open_typ_wrt_typ_lower A1 (t_tvar_f X).
assert (HS: typefv_typ A1 [<=] union (typefv_typ (t_tvar_f X)) (typefv_typ A)) by fsetdec.
clear Aux1 Aux2 Aux3...
fsetdec.
Qed.
Lemma splu_fv_2 : forall A B C,
splu A B C -> (typefv_typ C) [<=] (typefv_typ A).
Proof with (subst; simpl in *).
introv Hspl.
induction Hspl; simpl in *; try fsetdec.
remember ((typefv_typ A) \u (typefv_typ A2)).
pick fresh X.
forwards~ Aux1: H0 X.
lets* Aux2: typefv_typ_open_typ_wrt_typ_upper A (t_tvar_f X).
lets* Aux3: typefv_typ_open_typ_wrt_typ_lower A2 (t_tvar_f X).
assert (HS: typefv_typ A2 [<=] union (typefv_typ (t_tvar_f X)) (typefv_typ A)) by fsetdec.
clear Aux1 Aux2 Aux3...
fsetdec.
Qed.
Lemma splu_forall_exists : forall X B B1 B2,
X `notin` typefv_typ B ->
splu (B -^ X) B1 B2->
splu (t_forall B) (t_forall (close_typ_wrt_typ X B1)) (t_forall (close_typ_wrt_typ X B2)).
Proof with (simpl in *; eauto).
introv Fr H.
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ B1 X) in H.
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ B2 X) in H.
applys SpU_forall. intros. applys splu_rename_open H.
repeat rewrite typefv_typ_close_typ_wrt_typ.
solve_notin.
Unshelve. applys empty.
Qed.
Lemma spli_fv_1 : forall A B C,
spli A B C -> (typefv_typ B) [<=] (typefv_typ A).
Proof with (subst; simpl in *).
introv Hspl.
induction Hspl; simpl in *; try fsetdec.
- lets: splu_fv_1 H0. fsetdec.
-
remember ((typefv_typ A) \u (typefv_typ A1)).
pick fresh X.
forwards~ Aux1: H0 X.
lets* Aux2: typefv_typ_open_typ_wrt_typ_upper A (t_tvar_f X).
lets* Aux3: typefv_typ_open_typ_wrt_typ_lower A1 (t_tvar_f X).
assert (HS: typefv_typ A1 [<=] union (typefv_typ (t_tvar_f X)) (typefv_typ A)) by fsetdec.
clear Aux1 Aux2 Aux3...
fsetdec.
Qed.
Lemma spli_fv_2 : forall A B C,
spli A B C -> (typefv_typ C) [<=] (typefv_typ A).
Proof with (subst; simpl in *).
introv Hspl.
induction Hspl; simpl in *; try fsetdec.
- lets: splu_fv_2 H0. fsetdec.
-
remember ((typefv_typ A) \u (typefv_typ A2)).
pick fresh X.
forwards~ Aux1: H0 X.
lets* Aux2: typefv_typ_open_typ_wrt_typ_upper A (t_tvar_f X).
lets* Aux3: typefv_typ_open_typ_wrt_typ_lower A2 (t_tvar_f X).
assert (HS: typefv_typ A2 [<=] union (typefv_typ (t_tvar_f X)) (typefv_typ A)) by fsetdec.
clear Aux1 Aux2 Aux3...
fsetdec.
Qed.
Lemma spli_forall_exists : forall X B B1 B2,
X `notin` typefv_typ B ->
spli (B -^ X) B1 B2->
spli (t_forall B) (t_forall (close_typ_wrt_typ X B1)) (t_forall (close_typ_wrt_typ X B2)).
Proof with (simpl in *; eauto).
introv Fr H.
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ B1 X) in H.
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ B2 X) in H.
applys SpI_forall. intros. applys spli_rename_open H.
repeat rewrite typefv_typ_close_typ_wrt_typ.
solve_notin.
Unshelve. applys empty.
Qed.
#[export]
Hint Extern 1 =>
match goal with
| H: spli (?B -^ ?X) ?B1 ?B2 |-
spli (t_forall ?B) (t_forall ?A (close_typ_wrt_typ ?X ?B1)) (t_forall ?A (close_typ_wrt_typ ?X ?B2)) =>
applys spli_forall_exists H; solve_notin
| H: splu (?B -^ ?X) ?B1 ?B2 |-
splu (t_forall ?B) (t_forall ?A (close_typ_wrt_typ ?X ?B1)) (t_forall ?A (close_typ_wrt_typ ?X ?B2)) =>
applys splu_forall_exists H; solve_notin
| H: spli (?B -^ ?X) _ _ |-
spli (t_forall ?B) _ _ =>
apply spli_forall_exists in H; try rewrite close_typ_wrt_typ_open_typ_wrt_typ in *; try solve_notin
| H: splu (?B -^ ?X) _ _ |-
splu (t_forall ?B) _ _ =>
apply splu_forall_exists in H; try rewrite close_typ_wrt_typ_open_typ_wrt_typ in *; try solve_notin
end : core.
(*********************************** ord & split *******************************)
#[export] Hint Extern 1 (ordi _) =>
progress match goal with
| H: forall X : atom, X `notin` _ -> ordi (?B -^ X) |- ordi (t_forall ?B) => applys OrdI_forall H
| |- ordi (t_forall _) => detect_fresh_var_and_apply ordi_forall_exists
(* | _ => applys OrdI_var + applys OrdI_top + applys OrdI_bot + applys OrdI_arrow + applys OrdI_forall *)
end : core.
#[export] Hint Extern 1 (ordu _) =>
progress match goal with
| H: forall X : atom, X `notin` _ -> ordu (?B -^ X) |- ordu (t_forall ?B) => applys OrdU_forall H
| |- ordu (t_forall _) => detect_fresh_var_and_apply ordu_forall_exists
(* | _ => applys OrdU_var + applys OrdU_top + applys OrdU_bot + applys OrdU_arrow + applys OrdU_forall *)
end : core.
#[export] Hint Extern 0 (spli (t_and _ _) _ _) => applys SpI_and : core.
#[export] Hint Extern 0 (splu (t_or _ _) _ _) => applys SpU_or : core.
#[export] Hint Extern 0 (spli (t_arrow _ (t_and _ _)) _ _) => applys SpI_arrow : core.
(*
#[export] Hint Extern 1 (spli (t_arrow (t_or _ _) _) _ _) => applys SpI_arrowUnion : core.
#[export] Hint Extern 1 (spli _ _ _) => applys SpI_arrow + applys SpI_in + applys SpI_and : core.
#[export] Hint Extern 1 (splu _ _ _) => applys SpU_in + applys SpU_or : core.
#[export] Hint Extern 1 (spli (t_forall _) _ _) => applys SpI_forall : core.
#[export] Hint Extern 1 (splu (t_forall _) _ _) => applys SpU_forall : core.
*)
(* Types are Either Ordinary or Splittable *)
Lemma ordu_or_split: forall A,
lc_typ A -> ordu A \/ exists B C, splu A B C.
Proof with (subst~; simpl in *; eauto).
introv Lc. induction Lc...
- forwards* [?|(?&?&?)]: IHLc.
- (* and *)
forwards* [?|(?&?&?)]: IHLc1.
forwards* [?|(?&?&?)]: IHLc2.
- (* forall *)
pick fresh x for [[B]].
forwards* [?|(?&?&?)]: H0 x.
Defined.
Lemma ordi_or_split: forall A,
lc_typ A -> ordi A \/ exists B C, spli A B C.
Proof with (subst~; simpl in *; eauto).
introv Lc. induction Lc...
- forwards* [?|(?&?&?)]: IHLc.
- (* and *)
forwards* [?|(?&?&?)]: IHLc1.
forwards* [?|(?&?&?)]: IHLc2.
- (* arrow *)
forwards* [?|(?&?&?)]: IHLc2.
forwards* [?|(?&?&?)]: ordu_or_split A.
- (* forall *)
pick fresh x for [[B]].
forwards* [?|(?&?&?)]: H0 x.
Defined.
(* lemmas for ordinary *)
Lemma spli_keep_ord_l : forall A B C,
spli A B C -> ordu A -> ordu B.
Proof.
introv Hspl Hord.
inductions Hspl; try destruct m; inverts Hord; eauto with *.
Qed.
Lemma spli_keep_ord_r : forall A B C,
spli A B C -> ordu A -> ordu C.
Proof.
introv Hspl Hord.
inductions Hspl; try destruct m; inverts Hord; eauto with *.
Qed.
Lemma splu_keep_ord_l : forall A B C,
splu A B C -> ordi A -> ordi B.
Proof.
introv Hspl Hord.
inductions Hspl; try destruct m; inverts Hord; eauto with *.
Qed.
Lemma splu_keep_ord_r : forall A B C,
splu A B C -> ordi A -> ordi C.
Proof.
introv Hspl Hord.
inductions Hspl; try destruct m; inverts Hord; eauto with *.
Qed.
#[export] Hint Extern 1 (ordi _) => applys splu_keep_ord_l; [ eassumption | ] : core.
#[export] Hint Extern 1 (ordi _) => applys splu_keep_ord_r; [ eassumption | ] : core.
#[export] Hint Extern 1 (ordu _) => applys spli_keep_ord_l; [ eassumption | ] : core.
#[export] Hint Extern 1 (ordu _) => applys spli_keep_ord_r; [ eassumption | ] : core.
(*********************** binding ********************************)
Ltac close_typ_var X :=
repeat match goal with
| H: ?A = ?B -^ X |- _ =>
let H' := fresh "Heq" in
forwards~ H': close_typ_wrt_typ_open_typ_wrt_typ B;
rewrite <- H in H'; clear H
end.
Ltac simpl_rename H :=
match type of H with
| context [ [?X ~~> _] (_ -^ ?X) ] =>
rewrite typsubst_typ_spec in H; rewrite close_typ_wrt_typ_open_typ_wrt_typ in H
| context [ [?X ~~> _] ?A ] =>
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ A X) in H;
rewrite typsubst_typ_spec in H; rewrite close_typ_wrt_typ_open_typ_wrt_typ in H
end.
Ltac simpl_rename_goal :=
match goal with
| |- context [ [?X ~~> _] (_ -^ ?X) ] =>
rewrite typsubst_typ_spec; rewrite close_typ_wrt_typ_open_typ_wrt_typ
| |- context [ [?X ~~> _] ?A ] =>
rewrite <- (open_typ_wrt_typ_close_typ_wrt_typ A X);
rewrite typsubst_typ_spec; rewrite close_typ_wrt_typ_open_typ_wrt_typ
end.
Local Ltac open_typ_by_var_in_goal A X :=
let HR := fresh "Heq" in
assert (HR: A = close_typ_wrt_typ X (A -^X));
try solve [rewrite close_typ_wrt_typ_open_typ_wrt_typ; auto];
rewrite HR.
(* Splitting types is deterministic *)
(********************************************)
(* *)
(* Lemma split_unique *)
(* *)
(********************************************)
Lemma splu_unique : forall T A1 A2 B1 B2,
splu T A1 B1 -> splu T A2 B2 -> A1 = A2 /\ B1 = B2.
Proof with eauto.
introv s1 s2. gen A2 B2.
induction s1; intros;
inverts* s2;
try solve [forwards* (eq1&eq2): IHs1; subst; split*]; solve_false.
pick fresh X.
forwards* HS: H2 X.
forwards* (eq1&eq2): H0 HS.
open_typ_by_var_in_goal A1 X.
open_typ_by_var_in_goal A2 X.
open_typ_by_var_in_goal A4 X.
open_typ_by_var_in_goal A5 X.
rewrite eq1. rewrite eq2. split*.
Qed.
Lemma spli_unique : forall T A1 A2 B1 B2,
spli T A1 B1 -> spli T A2 B2 -> A1 = A2 /\ B1 = B2.
Proof with eauto.
introv s1 s2. gen A2 B2.
induction s1; intros;
inverts* s2;
try solve [forwards* (eq1&eq2): IHs1; subst; split*]; solve_false.
- forwards~ (?&?): splu_unique H0 H6. subst~.
-
pick fresh X.
forwards* HS: H2 X.
forwards* (eq1&eq2): H0 HS.
open_typ_by_var_in_goal A1 X.
open_typ_by_var_in_goal A2 X.
open_typ_by_var_in_goal A4 X.
open_typ_by_var_in_goal A5 X.
rewrite eq1. rewrite eq2. split*.
Qed.
(********************************************)
(* *)
(* Ltac auto_unify *)
(* *)
(* extends choose_unify *)
(* no solve_false at the end *)
(* *)
(********************************************)
Ltac auto_unify :=
simpl in *;
try solve [applys SpI_and];
try solve [applys SpU_or];
try repeat match goal with
| [ H1: spli (t_and _ _) _ _ |- _ ] =>
inverts H1
| [ H1: splu (t_or _ _) _ _ |- _ ] =>
inverts H1
| [ H1: spli ?A _ _ , H2: spli ?A _ _ |- _ ] =>
(forwards (?&?): spli_unique H1 H2;
subst; clear H2)
| [ H1: splu ?A _ _ , H2: splu ?A _ _ |- _ ] =>
(forwards (?&?): splu_unique H1 H2;
subst; clear H2)
end.
Ltac basic_auto :=
destruct_conj; auto_unify;
try exists; try splits;
try reflexivity;
try lazymatch goal with
| |- lc_typ _ => eauto
| |- spli _ _ _ => try eapply spli_rename_open; try eassumption; econstructor; try eassumption;
eauto
| |- splu _ _ _ => try eapply splu_rename_open; try eassumption; econstructor; try eassumption;
eauto
end; try eassumption; elia.
(*****************************************************************************)
Ltac solve_algo_sub :=
match goal with
| |- algo_sub (t_tvar_f _) (t_tvar_f _) => simple apply ASub_refl
| |- algo_sub _ t_top => simple apply ASub_top
| |- algo_sub t_bot _ => simple apply ASub_bot
| |- algo_sub (t_and ?A ?B) (t_and ?A ?B) => applys ASub_and; [ | applys ASub_andl | applys ASub_andr ]
| |- algo_sub _ (t_and _ _) => applys ASub_and
| H1: spli ?A ?A1 ?A2 |- algo_sub _ ?A => applys ASub_and H1
| H: algo_sub ?A ?C |- algo_sub (t_and ?A _) ?C => applys ASub_andl H
| H: algo_sub ?B ?C |- algo_sub (t_and _ ?B) ?C => applys ASub_andr H
| |- algo_sub (t_and ?A _) ?A => applys ASub_andl
| |- algo_sub (t_and _ ?A) ?A => applys ASub_andr
| H1: spli ?A ?A1 ?A2 , H2: algo_sub ?A1 ?C |- algo_sub ?A ?C => applys ASub_andl H1 H2
| H1: spli ?A ?A1 ?A2 , H2: algo_sub ?A2 ?C |- algo_sub ?A ?C => applys ASub_andr H1 H2
| |- algo_sub (t_or ?A ?B) (t_or ?A ?B) => applys ASub_or; [ | applys ASub_or | applys ASub_or ]
| |- algo_sub (t_or _ _) _ => applys ASub_or
| H1: splu ?A ?A1 ?A2 |- algo_sub ?A _ => applys ASub_or H1
| H: algo_sub ?C ?A |- algo_sub ?C (t_or ?A _) => applys ASub_orl H
| H: algo_sub ?C ?B |- algo_sub ?C (t_or _ ?B) => applys ASub_orr H
| |- algo_sub ?A (t_or ?A _) => applys ASub_orl
| |- algo_sub ?A (t_or _ ?A) => applys ASub_orr
| H1: splu ?A ?A1 ?A2 , H2: algo_sub ?C ?A1 |- algo_sub ?C ?A => applys ASub_orl H1 H2
| H1: splu ?A ?A1 ?A2 , H2: algo_sub ?C ?A2 |- algo_sub ?C ?A => applys ASub_orr H1 H2
| |- algo_sub (t_arrow _ _) (t_arrow _ _) => simple apply ASub_arrow
| |- algo_sub (t_forall _) (t_forall _) => simple apply ASub_forall
| |- algo_sub (t_rcd _ _) (t_rcd _ _) => simple apply ASub_rcd
end.
#[local] Hint Extern 1 (algo_sub _ _) => solve_algo_sub : core.
(* algorithm correctness *)
(* Lemma Inversion of Subtyping [1] *)
Lemma algo_sub_rcd_inv : forall l1 l2 A B,
algo_sub (t_rcd l1 A) (t_rcd l2 B) -> l1=l2 /\ algo_sub A B.
Proof.
introv H.
indTypSize (size_typ A + size_typ B).
inverts H; inverts_all_spl; inverts_all_ord; try assumption;
repeat match goal with
| H: algo_sub (t_rcd _ _) (t_rcd _ _) |- _ => forwards (?&?): IH H; elia; clear H
end.
all: eauto.
Qed.
Lemma algo_sub_forall_inv : forall A B X,
algo_sub (t_forall A) (t_forall B) -> algo_sub (A -^ X) (B -^ X).
Proof with (try eassumption).
intros.
indTypSize (size_typ A + size_typ B).
inverts H; inverts_all_spl; inverts_all_lc; try assumption;
repeat match goal with
| H: algo_sub (t_forall _) (t_forall _) |- _ => forwards: IH H; elia; clear H
end.
1: eauto.
all: pick_fresh Y; instantiate_cofinites_with Y...
1: try solve [applys~ algo_sub_rename_open].
all: repeat match goal with
| H: spli (_ -^ ?Y) _ _ |- _ => forwards~: spli_rename_open X H; clear H
| H: splu (_ -^ ?Y) _ _ |- _ => forwards~: splu_rename_open X H; clear H
end.
Qed.
Lemma algo_sub_arrow_inv : forall A B C D,
algo_sub (t_arrow A B) (t_arrow C D) -> (algo_sub C A) /\ (algo_sub B D).
Proof with (try eassumption).
introv s.
indTypSize (size_typ (t_arrow A B) + size_typ (t_arrow C D)).
inverts s; inverts_all_spl; inverts_all_ord; try assumption;
repeat match goal with
| H: algo_sub (t_arrow _ _) (t_arrow _ _) |- _ => forwards (?&?): IH H; elia; clear H
end; inverts_all_lc.
all: split*.
Qed.
(* A very useful inversion lemma when the type T is both intersection- and
union- splittable *)
Lemma double_split : forall T A1 A2 B1 B2,
splu T A1 A2 -> spli T B1 B2 ->
((exists C1 C2, spli A1 C1 C2 /\ splu B1 C1 A2 /\ splu B2 C2 A2) \/
(exists C1 C2, spli A2 C1 C2 /\ splu B1 A1 C1 /\ splu B2 A1 C2)) \/
((exists C1 C2, splu B1 C1 C2 /\ spli A1 C1 B2 /\ spli A2 C2 B2) \/
(exists C1 C2, splu B2 C1 C2 /\ spli A1 B1 C1 /\ spli A2 B1 C2)).
Proof with exists; repeat split*.
introv Hu Hi.
indTypSize (size_typ T).
inverts keep Hu; inverts keep Hi.
- (* spli or *) left. left...
- (* spli or *) left. right...
- (* splu and *) right. left...
- (* splu and *) right. right...
- (* forall *) pick fresh X. instantiate_cofinites_with X.
forwards [ [?|?] | [?|?] ] : IH (A -^ X); try eassumption; elia; destruct_conj.
left; left... left; right... right; left... right; right...
- (* rcd *) inverts_all_spl.
forwards [ [?|?] | [?|?] ] : IH A; try eassumption; elia; destruct_conj.
left; left... left; right... right; left... right; right...
Qed.
Lemma algo_sub_or_inv : forall A A1 A2 B,
algo_sub A B -> splu A A1 A2 ->
algo_sub A1 B /\ algo_sub A2 B.
Proof with (auto_unify; auto; try eassumption; elia; try solve [split; auto]; eauto 4).
introv Hsub Hspl.
indTypSize (size_typ A + size_typ B).
inverts Hsub; inverts_all_spl; inverts_all_ord; solve_false; auto_unify; auto.