-
Notifications
You must be signed in to change notification settings - Fork 79
/
ErasureFunction.v
2804 lines (2610 loc) · 115 KB
/
ErasureFunction.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
(* Distributed under the terms of the MIT license. *)
From Coq Require Import Program ssreflect ssrbool.
From Equations Require Import Equations.
Set Equations Transparent.
From MetaCoq.Template Require Import config utils Kernames MCRelations.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive
PCUICReduction PCUICReflect PCUICWeakeningEnv PCUICWeakeningEnvTyp PCUICCasesContexts
PCUICWeakeningConv PCUICWeakeningTyp PCUICContextConversionTyp PCUICTyping PCUICGlobalEnv PCUICInversion PCUICGeneration
PCUICConfluence PCUICConversion PCUICUnivSubstitutionTyp PCUICCumulativity PCUICSR PCUICSafeLemmata
PCUICValidity PCUICPrincipality PCUICElimination PCUICOnFreeVars PCUICWellScopedCumulativity PCUICSN PCUICEtaExpand.
From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICSafeReduce PCUICSafeRetyping PCUICRetypingEnvIrrelevance.
From MetaCoq.Erasure Require Import EAstUtils EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness.
Local Open Scope string_scope.
Set Asymmetric Patterns.
Local Set Keyed Unification.
Set Default Proof Using "Type*".
Import MCMonadNotation.
Implicit Types (cf : checker_flags).
#[local] Existing Instance extraction_normalizing.
Notation alpha_eq := (All2 (PCUICEquality.compare_decls eq eq)).
Ltac sq :=
repeat match goal with
| H : ∥ _ ∥ |- _ => destruct H as [H]
end; try eapply sq.
Lemma wf_local_rel_alpha_eq_end {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Δ Δ'} :
wf_local Σ Γ ->
alpha_eq Δ Δ' ->
wf_local_rel Σ Γ Δ -> wf_local_rel Σ Γ Δ'.
Proof.
intros wfΓ eqctx wf.
apply wf_local_app_inv.
eapply wf_local_app in wf => //.
eapply PCUICSpine.wf_local_alpha; tea.
eapply All2_app => //. reflexivity.
Qed.
Section OnInductives.
Context {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ}.
Lemma on_minductive_wf_params_weaken {ind mdecl Γ} {u} :
declared_minductive Σ.1 ind mdecl ->
consistent_instance_ext Σ (ind_universes mdecl) u ->
wf_local Σ Γ ->
wf_local Σ (Γ ,,, (ind_params mdecl)@[u]).
Proof.
intros.
eapply weaken_wf_local; tea.
eapply PCUICArities.on_minductive_wf_params; tea.
Qed.
Context {mdecl ind idecl}
(decli : declared_inductive Σ ind mdecl idecl).
Lemma on_minductive_wf_params_indices_inst_weaken {Γ} (u : Instance.t) :
consistent_instance_ext Σ (ind_universes mdecl) u ->
wf_local Σ Γ ->
wf_local Σ (Γ ,,, (ind_params mdecl ,,, ind_indices idecl)@[u]).
Proof.
intros. eapply weaken_wf_local; tea.
eapply PCUICInductives.on_minductive_wf_params_indices_inst; tea.
Qed.
End OnInductives.
Local Existing Instance extraction_checker_flags.
(* Definition wf_ext_wf Σ : wf_ext Σ -> wf Σ := fst.
#[global]
Hint Resolve wf_ext_wf : core. *)
Ltac specialize_Σ wfΣ :=
repeat match goal with | h : _ |- _ => specialize (h _ wfΣ) end.
Section fix_sigma.
Context {cf : checker_flags} {nor : normalizing_flags}.
Context (X_type : abstract_env_impl).
Context (X : X_type.π2.π1).
Local Definition heΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf_ext Σ ∥ := abstract_env_ext_wf _ wfΣ.
Local Definition HΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf Σ ∥ := abstract_env_ext_sq_wf _ _ _ wfΣ.
Definition term_rel : Relation_Definitions.relation
(∑ Γ t, forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) :=
fun '(Γ2; B; H) '(Γ1; t1; H2) =>
forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥∑ na A, red Σ Γ1 t1 (tProd na A B) × (Γ1,, vass na A) = Γ2∥.
Definition cod B t := match t with tProd _ _ B' => B = B' | _ => False end.
Lemma wf_cod : WellFounded cod.
Proof.
sq. intros ?. induction a; econstructor; cbn in *; intros; try tauto; subst. eauto.
Defined.
Lemma wf_cod' : WellFounded (Relation_Operators.clos_trans _ cod).
Proof.
eapply Subterm.WellFounded_trans_clos. exact wf_cod.
Defined.
Lemma Acc_no_loop A (R : A -> A -> Prop) t : Acc R t -> R t t -> False.
Proof.
induction 1. intros. eapply H0; eauto.
Qed.
Ltac sq' :=
repeat match goal with
| H : ∥ _ ∥ |- _ => destruct H; try clear H
end; try eapply sq.
Definition wf_reduction_aux : WellFounded term_rel.
Proof.
intros (Γ & s & H). sq'.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ']].
pose proof (abstract_env_ext_wf _ wfΣ') as wf. sq.
set (H' := H _ wfΣ').
induction (normalisation Σ _ Γ s H') as [s _ IH]. cbn in IH.
induction (wf_cod' s) as [s _ IH_sub] in Γ, H , H', IH |- *.
econstructor.
intros (Γ' & B & ?) [(na & A & ? & ?)]; eauto. subst.
eapply Relation_Properties.clos_rt_rtn1 in r. inversion r.
+ subst. eapply IH_sub. econstructor. cbn. reflexivity.
intros. eapply IH.
inversion H0.
* subst. econstructor. eapply prod_red_r. eassumption.
* subst. eapply cored_red in H2 as [].
eapply cored_red_trans. 2: eapply prod_red_r. 2:eassumption.
eapply PCUICReduction.red_prod_r. eauto.
* constructor. do 2 eexists. now split.
+ subst. eapply IH.
* eapply red_neq_cored.
eapply Relation_Properties.clos_rtn1_rt. exact r.
intros ?. subst.
eapply Relation_Properties.clos_rtn1_rt in X1.
eapply cored_red_trans in X0; [| exact X1 ].
eapply Acc_no_loop in X0. eauto.
eapply @normalisation; eauto.
* constructor. do 2 eexists. now split.
Unshelve.
- intros. destruct H' as [].
rewrite <- (abstract_env_ext_irr _ H2) in X0; eauto.
rewrite <- (abstract_env_ext_irr _ H2) in wf; eauto.
eapply inversion_Prod in X0 as (? & ? & ? & ? & ?) ; auto.
eapply cored_red in H0 as [].
econstructor. econstructor. econstructor. eauto.
2:reflexivity. econstructor; pcuic.
rewrite <- (abstract_env_ext_irr _ H2) in X0; eauto.
eapply subject_reduction; eauto.
- intros. rewrite <- (abstract_env_ext_irr _ H0) in wf; eauto.
rewrite <- (abstract_env_ext_irr _ H0) in X0; eauto.
rewrite <- (abstract_env_ext_irr _ H0) in r; eauto.
eapply red_welltyped; sq.
3:eapply Relation_Properties.clos_rtn1_rt in r; eassumption.
all:eauto.
Defined.
Instance wf_reduction : WellFounded term_rel.
Proof.
refine (Wf.Acc_intro_generator 1000 _).
exact wf_reduction_aux.
Defined.
Opaque wf_reduction.
#[tactic="idtac"]
Equations? is_arity Γ (HΓ : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥wf_local Σ Γ∥) T
(HT : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ T) : bool
by wf ((Γ;T;HT) : (∑ Γ t, forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t)) term_rel :=
{
is_arity Γ HΓ T HT with inspect (@reduce_to_sort _ _ X_type X Γ T HT) => {
| exist (Checked_comp H) rsort => true ;
| exist (TypeError_comp _) rsort with
inspect (@reduce_to_prod _ _ X_type X Γ T HT) => {
| exist (Checked_comp (na; A; B; H)) rprod := is_arity (Γ,, vass na A) _ B _
| exist (TypeError_comp e) rprod => false } }
}.
Proof.
- clear rprod is_arity rsort a0.
intros Σ' wfΣ'; specialize (H Σ' wfΣ').
repeat specialize_Σ wfΣ'.
destruct HT as [s HT].
pose proof (abstract_env_ext_wf _ wfΣ') as [wf].
sq.
eapply subject_reduction_closed in HT; tea.
eapply inversion_Prod in HT as [? [? [? []]]].
now eapply typing_wf_local in t1. pcuic. pcuic.
- clear rprod is_arity rsort a0.
intros Σ' wfΣ'; specialize (H Σ' wfΣ').
repeat specialize_Σ wfΣ'.
destruct HT as [s HT].
pose proof (abstract_env_ext_wf _ wfΣ') as [wf].
sq.
eapply subject_reduction_closed in HT; tea.
eapply inversion_Prod in HT as [? [? [? []]]].
now eexists. all:pcuic.
- cbn. clear rsort is_arity rprod.
intros Σ' wfΣ'; specialize (H Σ' wfΣ').
pose proof (abstract_env_ext_wf _ wfΣ') as [wf].
repeat specialize_Σ wfΣ'.
destruct HT as [s HT].
sq.
eapply subject_reduction_closed in HT; tea. 2:pcuic.
eapply inversion_Prod in HT as [? [? [? []]]]. 2:pcuic.
exists na, A. split => //.
eapply H.
Defined.
Lemma is_arityP Γ (HΓ : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥wf_local Σ Γ∥) T
(HT : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ T) :
reflect (forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
Is_conv_to_Arity Σ Γ T) (is_arity Γ HΓ T HT).
Proof.
funelim (is_arity Γ HΓ T HT).
- constructor.
destruct H as [s Hs]. clear H0 rsort.
pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
specialize (Hs _ wfΣ) as [Hs].
intros. rewrite (abstract_env_ext_irr _ H wfΣ).
exists (tSort s); split => //.
- clear H0 H1.
destruct X0; constructor; clear rprod rsort.
* red.
pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
specialize_Σ wfΣ. sq.
intros. rewrite (abstract_env_ext_irr _ H0 wfΣ).
destruct i as [T' [[HT'] isa]].
exists (tProd na A T'); split => //. split.
etransitivity; tea. now eapply closed_red_prod_codom.
* pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (abstract_env_ext_wf X wfΣ) as [wfΣ'].
specialize_Σ wfΣ. sq.
intros [T' [[HT'] isa]]; eauto.
destruct (PCUICContextConversion.closed_red_confluence H HT') as (? & ? & ?); eauto.
eapply invert_red_prod in c as (? & ? & []); eauto. subst.
apply n. intros. rewrite (abstract_env_ext_irr _ H0 wfΣ).
red. exists x1.
split => //.
eapply isArity_red in isa. 2:exact c0.
now cbn in isa.
- constructor.
clear H H0. pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (abstract_env_ext_wf X wfΣ) as [wfΣ'].
symmetry in rprod. symmetry in rsort.
intros isc. specialize_Σ wfΣ.
eapply Is_conv_to_Arity_inv in isc as [].
* destruct H as [na [A [B [Hr]]]].
apply e. exists na, A, B.
intros ? H. now rewrite (abstract_env_ext_irr _ H wfΣ).
* destruct H as [u [Hu]].
apply a0. exists u.
intros ? H. now rewrite (abstract_env_ext_irr _ H wfΣ).
Qed.
End fix_sigma.
Opaque wf_reduction_aux.
Transparent wf_reduction.
(** Deciding if a term is erasable or not as a total function on well-typed terms.
A term is erasable if:
- it represents a type, i.e., its type is an arity
- it represents a proof: its sort is Prop.
*)
Derive NoConfusion for typing_result_comp.
Opaque is_arity type_of_typing.
Definition inspect {A} (x : A) : { y : A | x = y } := exist x eq_refl.
Equations inspect_bool (b : bool) : { b } + { ~~ b } :=
inspect_bool true := left eq_refl;
inspect_bool false := right eq_refl.
#[tactic="idtac"]
Equations? is_erasableb X_type X (Γ : context) (T : PCUICAst.term)
(wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ T) : bool :=
is_erasableb X_type X Γ t wt with @type_of_typing extraction_checker_flags _ X_type X Γ t wt :=
{ | T with is_arity X_type X Γ _ T.π1 _ :=
{ | true => true
| false => let s := @sort_of_type extraction_checker_flags _ X_type X Γ T.π1 _ in
is_propositional s.π1 } }.
Proof.
- intros. specialize_Σ H. destruct wt; sq.
pcuic.
- intros. specialize_Σ H. destruct T as [T Ht].
cbn. destruct (Ht Σ H) as [[tT Hp]].
pose proof (abstract_env_ext_wf X H) as [wf].
eapply validity in tT. pcuic.
- intros. destruct T as [T Ht].
cbn in *. specialize (Ht Σ H) as [[tT Hp]].
pose proof (abstract_env_ext_wf X H) as [wf].
eapply validity in tT. now sq.
Qed.
Transparent is_arity type_of_typing.
Lemma is_erasableP {X_type X} {Γ : context} {t : PCUICAst.term}
{wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t} :
reflect (forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥ isErasable Σ Γ t ∥) (is_erasableb X_type X Γ t wt).
Proof.
funelim (is_erasableb X_type X Γ t wt).
- constructor. intros. pose proof (abstract_env_ext_wf _ H) as [wf].
destruct type_of_typing as [x Hx]. cbn -[is_arity sort_of_type] in *.
destruct (Hx _ H) as [[HT ?]].
move/is_arityP: Heq => / (_ _ H) [T' [redT' isar]]. specialize_Σ H.
sq. red. exists T'. eapply type_reduction_closed in HT.
2: eassumption. eauto.
- destruct type_of_typing as [x Hx]. cbn -[sort_of_type is_arity] in *.
destruct (sort_of_type _ _ _ _). cbn.
destruct (is_propositional x0) eqn:isp; constructor.
* clear Heq. intros.
pose proof (abstract_env_ext_wf _ H) as [wf].
specialize_Σ H.
destruct Hx as [[HT ?]].
destruct s as [Hs]. sq.
exists x; split => //. right.
exists x0. now split.
* pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
move => / (_ _ wfΣ) [[T' [HT' er]]].
pose proof (abstract_env_ext_wf _ wfΣ) as [wf].
move/is_arityP: Heq => nisa.
specialize_Σ wfΣ.
destruct Hx as [[HT ?]].
specialize (p _ HT').
destruct er as [isa|[u' [Hu' isp']]].
{ apply nisa. intros. rewrite (abstract_env_ext_irr _ H wfΣ).
eapply invert_cumul_arity_r; tea. }
{ destruct s as [Hs].
unshelve epose proof (H := unique_sorting_equality_propositional _ _ wf Hs Hu' p) => //. reflexivity. reflexivity. congruence. }
Qed.
Equations? is_erasable {X_type X} (Γ : context) (t : PCUICAst.term)
(wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) :
forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
{ ∥ isErasable Σ Γ t ∥ } + { ∥ isErasable Σ Γ t -> False ∥ } :=
is_erasable Γ T wt Σ wfΣ with inspect_bool (is_erasableb X_type X Γ T wt) :=
{ | left ise => left _
| right nise => right _ }.
Proof.
pose proof (abstract_env_ext_wf _ wfΣ) as [wf].
now move/is_erasableP: ise => //.
move/(elimN is_erasableP): nise.
intros; sq => ise. apply nise.
intros. now rewrite (abstract_env_ext_irr _ H wfΣ).
Qed.
Section Erase.
Context {nor : normalizing_flags}.
Context (X_type : abstract_env_impl (cf := extraction_checker_flags)).
Context (X : X_type.π2.π1).
(* Ltac sq' :=
repeat match goal with
| H : ∥ _ ∥ |- _ => destruct H; try clear H
end; try eapply sq. *)
(* Bug in equationa: it produces huge goals leading to stack overflow if we
don't try reflexivity here. *)
Ltac Equations.Prop.DepElim.solve_equation c ::=
intros; try reflexivity; try Equations.Prop.DepElim.simplify_equation c;
try
match goal with
| |- ImpossibleCall _ => DepElim.find_empty
| _ => try red; try reflexivity || discriminates
end.
Opaque is_erasableb.
#[tactic="idtac"]
Equations? erase (Γ : context) (t : term)
(Ht : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) : E.term
by struct t :=
{ erase Γ t Ht with inspect_bool (is_erasableb X_type X Γ t Ht) :=
{ | left he := E.tBox;
| right he with t := {
| tRel i := E.tRel i
| tVar n := E.tVar n
| tEvar m l := E.tEvar m (erase_terms Γ l _)
| tSort u := !%prg
| tConst kn u := E.tConst kn
| tInd kn u := !%prg
| tConstruct kn k u := E.tConstruct kn k []
| tProd _ _ _ := !%prg
| tLambda na b b' := let t' := erase (vass na b :: Γ) b' _ in
E.tLambda na.(binder_name) t'
| tLetIn na b t0 t1 :=
let b' := erase Γ b _ in
let t1' := erase (vdef na b t0 :: Γ) t1 _ in
E.tLetIn na.(binder_name) b' t1'
| tApp f u :=
let f' := erase Γ f _ in
let l' := erase Γ u _ in
E.tApp f' l'
| tCase ci p c brs :=
let c' := erase Γ c _ in
let brs' := erase_brs Γ p brs _ in
E.tCase (ci.(ci_ind), ci.(ci_npar)) c' brs'
| tProj p c :=
let c' := erase Γ c _ in
E.tProj p c'
| tFix mfix n :=
let Γ' := (fix_context mfix ++ Γ)%list in
let mfix' := erase_fix Γ' mfix _ in
E.tFix mfix' n
| tCoFix mfix n :=
let Γ' := (fix_context mfix ++ Γ)%list in
let mfix' := erase_cofix Γ' mfix _ in
E.tCoFix mfix' n
| tPrim p := E.tPrim (erase_prim_val p) }
} }
where erase_terms (Γ : context) (l : list term) (Hl : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥ All (welltyped Σ Γ) l ∥) : list E.term :=
{ erase_terms Γ [] _ := [];
erase_terms Γ (t :: ts) _ :=
let t' := erase Γ t _ in
let ts' := erase_terms Γ ts _ in
t' :: ts' }
(** We assume that there are no lets in contexts, so nothing has to be expanded.
In particular, note that #|br.(bcontext)| = context_assumptions br.(bcontext) when no lets are present.
*)
where erase_brs (Γ : context) p (brs : list (branch term))
(Ht : forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥ All (fun br => welltyped Σ (Γ ,,, inst_case_branch_context p br) (bbody br)) brs ∥) :
list (list name × E.term) :=
{ erase_brs Γ p [] Ht := [];
erase_brs Γ p (br :: brs) Hbrs :=
let br' := erase (Γ ,,, inst_case_branch_context p br) (bbody br) _ in
let brs' := erase_brs Γ p brs _ in
(erase_context br.(bcontext), br') :: brs' }
where erase_fix (Γ : context) (mfix : mfixpoint term)
(Ht : forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥ All (fun d => isLambda d.(dbody) /\ welltyped Σ Γ d.(dbody)) mfix ∥) : E.mfixpoint E.term :=
{ erase_fix Γ [] _ := [];
erase_fix Γ (d :: mfix) Hmfix :=
let dbody' := erase Γ d.(dbody) _ in
let dbody' := if isBox dbody' then
match d.(dbody) with
(* We ensure that all fixpoint members start with a lambda, even a dummy one if the
recursive definition is erased. *)
| tLambda na _ _ => E.tLambda (binder_name na) E.tBox
| _ => dbody'
end else dbody' in
let d' := {| E.dname := d.(dname).(binder_name); E.rarg := d.(rarg); E.dbody := dbody' |} in
d' :: erase_fix Γ mfix _ }
where erase_cofix (Γ : context) (mfix : mfixpoint term)
(Ht : forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥ All (fun d => welltyped Σ Γ d.(dbody)) mfix ∥) : E.mfixpoint E.term :=
{ erase_cofix Γ [] _ := [];
erase_cofix Γ (d :: mfix) Hmfix :=
let dbody' := erase Γ d.(dbody) _ in
let d' := {| E.dname := d.(dname).(binder_name); E.rarg := d.(rarg); E.dbody := dbody' |} in
d' :: erase_cofix Γ mfix _ }
.
Proof.
all: try clear b'; try clear f';
try clear t';
try clear brs'; try clear c'; try clear br';
try clear d' dbody'; try clear erase; try clear erase_terms; try clear erase_brs; try clear erase_mfix.
all: cbn; intros; subst; lazymatch goal with [ |- False ] => idtac | _ => try clear he end.
all: try pose proof (abstract_env_ext_wf _ H) as [wf];
specialize_Σ H.
all: try destruct Ht as [ty Ht]; try destruct s0; simpl in *.
- now eapply inversion_Evar in Ht.
- discriminate.
- discriminate.
- eapply inversion_Lambda in Ht as (? & ? & ? & ? & ?); auto.
eexists; eauto.
- eapply inversion_LetIn in Ht as (? & ? & ? & ? & ? & ?); auto.
eexists; eauto.
- simpl in *.
eapply inversion_LetIn in Ht as (? & ? & ? & ? & ? & ?); auto.
eexists; eauto.
- eapply inversion_App in Ht as (? & ? & ? & ? & ? & ?); auto.
eexists; eauto.
- eapply inversion_App in Ht as (? & ? & ? & ? & ? & ?); auto.
eexists; eauto.
- move/is_erasableP: he. intro. apply he. intros.
pose proof (abstract_env_ext_wf _ H) as [wf].
specialize_Σ H. destruct Ht as [ty Ht]. sq.
eapply inversion_Ind in Ht as (? & ? & ? & ? & ? & ?) ; auto.
red. eexists. split. econstructor; eauto. left.
eapply isArity_subst_instance.
eapply isArity_ind_type; eauto.
- eapply inversion_Case in Ht as (? & ? & ? & ? & [] & ?); auto.
eexists; eauto.
- now eapply welltyped_brs in Ht as []; tea.
- eapply inversion_Proj in Ht as (? & ? & ? & ? & ? & ? & ? & ? & ?); auto.
eexists; eauto.
- eapply inversion_Fix in Ht as (? & ? & ? & ? & ? & ?); auto.
sq. destruct p. move/andP: i => [wffix _].
solve_all. now eexists.
- eapply inversion_CoFix in Ht as (? & ? & ? & ? & ? & ?); auto.
sq. eapply All_impl; tea. cbn. intros d Ht; now eexists.
- sq. now depelim Hl.
- sq. now depelim Hl.
- sq. now depelim Hbrs.
- sq. now depelim Hbrs.
- sq. now depelim Hmfix.
- clear dbody'0. specialize_Σ H. sq. now depelim Hmfix.
- sq. now depelim Hmfix.
- sq. now depelim Hmfix.
Qed.
End Erase.
Lemma is_erasableb_irrel {X_type X Γ t} wt wt' : is_erasableb X_type X Γ t wt = is_erasableb X_type X Γ t wt'.
Proof.
destruct (@is_erasableP X_type X Γ t wt);
destruct (@is_erasableP X_type X Γ t wt') => //.
Qed.
Ltac iserasableb_irrel :=
match goal with
[ H : context [is_erasableb ?X_type ?X ?Γ ?t ?wt], Heq : inspect_bool _ = _ |- context [ is_erasableb _ _ _ _ ?wt'] ] =>
generalize dependent H; rewrite (is_erasableb_irrel wt wt'); intros; rewrite Heq
end.
Ltac simp_erase := simp erase; rewrite -?erase_equation_1.
Lemma erase_irrel X_type X :
(forall Γ t wt, forall wt', erase X_type X Γ t wt = erase X_type X Γ t wt') ×
(forall Γ l wt, forall wt', erase_terms X_type X Γ l wt = erase_terms X_type X Γ l wt') ×
(forall Γ p l wt, forall wt', erase_brs X_type X Γ p l wt = erase_brs X_type X Γ p l wt') ×
(forall Γ l wt, forall wt', erase_fix X_type X Γ l wt = erase_fix X_type X Γ l wt') ×
(forall Γ l wt, forall wt', erase_cofix X_type X Γ l wt = erase_cofix X_type X Γ l wt').
Proof.
apply: (erase_elim X_type X
(fun Γ t wt e =>
forall wt' : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t, e = erase X_type X Γ t wt')
(fun Γ l awt e => forall wt', e = erase_terms X_type X Γ l wt')
(fun Γ p l awt e => forall wt', e = erase_brs X_type X Γ p l wt')
(fun Γ l awt e => forall wt', e = erase_fix X_type X Γ l wt')
(fun Γ l awt e => forall wt', e = erase_cofix X_type X Γ l wt')); clear.
all:intros *; intros; simp_erase.
all:try simp erase; try iserasableb_irrel; simp_erase => //.
all:try clear he Heq.
all:try bang.
all:try solve [cbn; f_equal; eauto].
all:try solve [cbn; repeat (f_equal; eauto)].
cbn. f_equal. f_equal. now rewrite (H (erase_obligation_19 X_type X Γ d mfix wt')).
now rewrite (H0 (erase_obligation_20 X_type X Γ d mfix wt')).
Qed.
Lemma erase_terms_eq X_type X Γ ts wt :
erase_terms X_type X Γ ts wt = map_All (erase X_type X Γ) ts wt.
Proof.
funelim (map_All (erase X_type X Γ) ts wt); cbn; auto.
f_equal => //. apply erase_irrel.
rewrite -H. eapply erase_irrel.
Qed.
Opaque wf_reduction.
#[global]
Hint Constructors typing erases : core.
Lemma erase_to_box {X_type X} {Γ t} (wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) :
forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
let et := erase X_type X Γ t wt in
if is_box et then ∥ isErasable Σ Γ t ∥
else ~ ∥ isErasable Σ Γ t ∥.
Proof.
cbn. intros.
revert Γ t wt.
apply (erase_elim X_type X
(fun Γ t wt e =>
if is_box e then ∥ isErasable Σ Γ t ∥ else ∥ isErasable Σ Γ t ∥ -> False)
(fun Γ l awt e => True)
(fun Γ p l awt e => True)
(fun Γ l awt e => True)
(fun Γ l awt e => True)); intros.
all:try discriminate; auto.
all:cbn -[isErasable].
all:try solve [ match goal with
[ H : context [ is_erasableb ?X_type ?X ?Γ ?t ?Ht ] |- _ ] =>
destruct (@is_erasableP X_type X Γ t Ht) => //
end; intro;
match goal with n : ~ _ |- _ => apply n end; intros ? HH; now rewrite (abstract_env_ext_irr _ HH H) ].
all:try bang.
- destruct (@is_erasableP X_type X Γ t Ht) => //. apply s; eauto.
- cbn in *. rewrite is_box_tApp.
destruct (@is_erasableP X_type X Γ (tApp f u) Ht) => //.
destruct is_box.
* cbn in *. clear H1.
pose proof (abstract_env_ext_wf _ H) as [wf]. cbn in *.
specialize_Σ H. destruct Ht, H0.
eapply (EArities.Is_type_app _ _ _ [_]); eauto.
eauto using typing_wf_local.
* intro; apply n; intros. now rewrite (abstract_env_ext_irr _ H3 H).
Defined.
Lemma erases_erase {X_type X Γ t}
(wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) :
forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> erases Σ Γ t (erase X_type X Γ t wt).
Proof.
intros. revert Γ t wt.
apply (erase_elim X_type X
(fun Γ t wt e => Σ;;; Γ |- t ⇝ℇ e)
(fun Γ l awt e => All2 (erases Σ Γ) l e)
(fun Γ p l awt e =>
All2 (fun (x : branch term) (x' : list name × E.term) =>
(Σ;;; Γ,,, inst_case_branch_context p x |-
bbody x ⇝ℇ x'.2) *
(erase_context (bcontext x) = x'.1)) l e)
(fun Γ l awt e => All2
(fun (d : def term) (d' : E.def E.term) =>
[× binder_name (dname d) = E.dname d',
rarg d = E.rarg d',
isLambda (dbody d), E.isLambda (E.dbody d') &
Σ;;; Γ |- dbody d ⇝ℇ E.dbody d']) l e)
(fun Γ l awt e => All2
(fun (d : def term) (d' : E.def E.term) =>
(binder_name (dname d) = E.dname d') *
(rarg d = E.rarg d'
× Σ;;; Γ |- dbody d ⇝ℇ E.dbody d')) l e)) ; intros.
all:try discriminate.
all:try bang.
all:try match goal with
[ H : context [is_erasableb ?X_type ?X ?Γ ?t ?Ht ] |- _ ] =>
destruct (@is_erasableP X_type X Γ t Ht) as [[H']|H'] => //; eauto ;
try now eapply erases_box
end.
all: try solve [constructor; eauto].
all:try destruct (abstract_env_ext_wf X H) as [wfΣ].
all: cbn in *; try constructor; auto;
specialize_Σ H.
- clear Heq.
eapply nisErasable_Propositional in Ht; auto.
intro; eapply H'; intros. now rewrite (abstract_env_ext_irr _ H0 H).
- cbn.
destruct (Ht _ H).
destruct (inversion_Case _ _ X1) as [mdecl [idecl []]]; eauto.
eapply elim_restriction_works; eauto.
intros isp. eapply isErasable_Proof in isp.
eapply H'; intros. now rewrite (abstract_env_ext_irr _ H1 H).
- clear Heq.
destruct (Ht _ H) as [? Ht'].
clear H0. eapply inversion_Proj in Ht' as (?&?&?&?&?&?&?&?&?&?); auto.
eapply elim_restriction_works_proj; eauto. exact d.
intros isp. eapply isErasable_Proof in isp.
eapply H'; intros. now rewrite (abstract_env_ext_irr _ H0 H).
- cbn. pose proof (abstract_env_ext_wf _ H) as [wf].
pose proof Hmfix as Hmfix'.
specialize (Hmfix' _ H). destruct Hmfix'.
depelim X1. destruct a.
assert (exists na ty bod, dbody d = tLambda na ty bod).
{ clear -H1. destruct (dbody d) => //. now do 3 eexists. }
destruct H3 as [na [ty [bod eq]]]. rewrite {1 3}eq /= //.
move: H0. rewrite {1}eq.
set (et := erase _ _ _ _ _). clearbody et.
intros He. depelim He. cbn.
split => //. cbn. rewrite eq. now constructor.
split => //. cbn. rewrite eq.
destruct H2.
eapply Is_type_lambda in X2; tea. 2:pcuic. destruct X2.
now constructor.
Qed.
Transparent wf_reduction.
(** We perform erasure up-to the minimal global environment dependencies of the term: i.e.
we don't need to erase entries of the global environment that will not be used by the erased
term.
*)
Program Definition erase_constant_body X_type X
(cb : constant_body)
(Hcb : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥ on_constant_decl (lift_typing typing) Σ cb ∥) : E.constant_body * KernameSet.t :=
let '(body, deps) := match cb.(cst_body) with
| Some b =>
let b' := erase X_type X [] b _ in
(Some b', term_global_deps b')
| None => (None, KernameSet.empty)
end in
({| E.cst_body := body; |}, deps).
Next Obligation.
Proof.
specialize_Σ H. sq. red in Hcb.
rewrite <-Heq_anonymous in Hcb. now eexists.
Qed.
Definition erase_one_inductive_body (oib : one_inductive_body) : E.one_inductive_body :=
(* Projection and constructor types are types, hence always erased *)
let ctors := map (fun cdecl => EAst.mkConstructor cdecl.(cstr_name) cdecl.(cstr_arity)) oib.(ind_ctors) in
let projs := map (fun pdecl => EAst.mkProjection pdecl.(proj_name)) oib.(ind_projs) in
let is_propositional :=
match destArity [] oib.(ind_type) with
| Some (_, u) => is_propositional u
| None => false (* dummy, impossible case *)
end
in
{| E.ind_name := oib.(ind_name);
E.ind_kelim := oib.(ind_kelim);
E.ind_propositional := is_propositional;
E.ind_ctors := ctors;
E.ind_projs := projs |}.
Definition erase_mutual_inductive_body (mib : mutual_inductive_body) : E.mutual_inductive_body :=
let bds := mib.(ind_bodies) in
let arities := arities_context bds in
let bodies := map erase_one_inductive_body bds in
{| E.ind_finite := mib.(ind_finite);
E.ind_npars := mib.(ind_npars);
E.ind_bodies := bodies; |}.
Lemma is_arity_irrel {X_type : abstract_env_impl} {X : X_type.π2.π1}
{X_type' : abstract_env_impl} {X' : X_type'.π2.π1} {Γ h h' t wt wt'} :
Hlookup X_type X X_type' X' ->
is_arity X_type X Γ h t wt = is_arity X_type' X' Γ h' t wt'.
Proof.
intros hl.
funelim (is_arity X_type X _ _ _ _).
- epose proof (reduce_to_sort_irrel hl eq_refl HT wt').
rewrite -rsort in H1.
simp is_arity.
epose proof (reduce_to_sort_irrel hl eq_refl HT wt').
destruct (PCUICSafeReduce.inspect) eqn:hi.
rewrite -e in H1.
destruct x => //.
- epose proof (reduce_to_sort_irrel hl eq_refl HT wt').
rewrite -rsort in H3.
rewrite [is_arity X_type' X' _ _ _ _]is_arity_equation_1.
epose proof (reduce_to_sort_irrel hl eq_refl HT wt').
destruct (PCUICSafeReduce.inspect) eqn:hi.
rewrite -rsort -e in H4.
destruct x => //.
rewrite is_arity_clause_1_equation_2.
destruct (PCUICSafeReduce.inspect (reduce_to_prod _ _ _)) eqn:hi'.
epose proof (reduce_to_prod_irrel hl HT wt').
rewrite -rprod -e0 in H5 => //.
destruct x => //.
destruct a1 as [na' [A' [B' ?]]]. cbn in H5. noconf H5.
rewrite is_arity_clause_1_clause_2_equation_1.
now apply H0.
- epose proof (reduce_to_sort_irrel hl eq_refl HT wt').
rewrite -rsort in H1.
simp is_arity.
destruct (PCUICSafeReduce.inspect) eqn:hi.
rewrite -e0 in H1.
destruct x => //.
simp is_arity.
destruct (PCUICSafeReduce.inspect (reduce_to_prod _ _ _)) eqn:hi'.
epose proof (reduce_to_prod_irrel hl HT wt').
rewrite -rprod -e1 in H2 => //.
destruct x => //.
Qed.
Lemma extends_lookup_env {cf Σ Σ' kn d} : wf Σ' -> extends_decls Σ Σ' ->
lookup_env Σ kn = Some d -> lookup_env Σ' kn = Some d.
Proof.
destruct Σ as [univs Σ].
destruct Σ' as [univs' Σ'].
intros wf [Σ'' []]. cbn in *. subst univs'.
induction x in Σ, Σ', e, wf |- *. cbn in e. now subst Σ'.
intros hl.
rewrite e; cbn.
case: eqb_spec.
intros ->.
eapply lookup_global_Some_fresh in hl.
rewrite e in wf. destruct wf as [_ ond]; depelim ond. destruct o as [f ? ? ? ].
cbn in *. eapply Forall_app in f as []. contradiction.
intros _.
eapply IHx; trea.
rewrite e in wf. destruct wf as [onu ond]; depelim ond.
split => //.
Qed.
Lemma is_erasableb_irrel_global_env {X_type X X_type' X'} {Γ t wt wt'} :
(forall Σ Σ' : global_env_ext, abstract_env_ext_rel X Σ ->
abstract_env_ext_rel X' Σ' -> ∥ extends_decls Σ' Σ ∥ /\ (Σ.2 = Σ'.2)) ->
is_erasableb X_type X Γ t wt = is_erasableb X_type' X' Γ t wt'.
Proof.
intro ext.
(* ext eqext. *)
assert (hl : Hlookup X_type X X_type' X').
{ red. intros. specialize (ext _ _ H H0) as [[?] ?].
split. intros.
rewrite -(abstract_env_lookup_correct _ _ H).
rewrite -(abstract_env_lookup_correct _ _ H0).
rewrite H2 H3. pose proof (abstract_env_ext_wf _ H) as [?].
eapply extends_lookup_env in H3; try apply e; eauto. clear -H2 H3. congruence.
destruct X0.
rewrite -(abstract_env_ext_retroknowledge_correct _ H).
rewrite -(abstract_env_ext_retroknowledge_correct _ H0).
congruence. }
simp is_erasableb.
set (obl := is_erasableb_obligation_2 _ _ _ _). clearbody obl.
set(ty := (type_of_typing X_type' _ _ _ wt')) in *.
set(ty' := (type_of_typing X_type _ _ _ wt)) in *.
assert (ty.π1 = ty'.π1).
{ subst ty ty'. unfold type_of_typing. symmetry.
eapply infer_irrel => //. }
clearbody ty. clearbody ty'.
destruct ty, ty'. cbn in H. subst x0.
cbn -[is_arity] in obl |- *.
set (obl' := is_erasableb_obligation_1 X_type' X' Γ t wt').
set (obl'' := is_erasableb_obligation_2 X_type' X' Γ t _).
clearbody obl'. clearbody obl''.
rewrite (is_arity_irrel (X:=X) (X' := X') (wt' := obl'' (x; s))) => //.
destruct is_arity => //. simp is_erasableb.
set (obl2 := is_erasableb_obligation_3 _ _ _ _ _).
set (obl2' := is_erasableb_obligation_3 _ _ _ _ _).
simpl. f_equal. now apply sort_of_type_irrel.
Qed.
Ltac iserasableb_irrel_env :=
match goal with
[ H : context [is_erasableb ?X_type ?X ?Γ ?t ?wt], Heq : inspect_bool _ = _ |- context [ is_erasableb _ _ _ _ ?wt'] ] =>
generalize dependent H; rewrite (@is_erasableb_irrel_global_env _ _ _ _ _ _ wt wt') //; intros; rewrite Heq
end.
Lemma erase_irrel_global_env {X_type X X_type' X'} {Γ t wt wt'} :
(forall Σ Σ' : global_env_ext, abstract_env_ext_rel X Σ ->
abstract_env_ext_rel X' Σ' -> ∥ extends_decls Σ' Σ ∥ /\ (Σ.2 = Σ'.2)) ->
erase X_type X Γ t wt = erase X_type' X' Γ t wt'.
Proof.
intros ext.
move: wt'.
eapply (erase_elim X_type X
(fun Γ t wt e =>
forall (wt' : forall Σ' : global_env_ext, abstract_env_ext_rel X' Σ' -> welltyped Σ' Γ t),
e = erase X_type' X' Γ t wt')
(fun Γ l awt e => forall wt',
e = erase_terms X_type' X' Γ l wt')
(fun Γ p l awt e => forall wt',
e = erase_brs X_type' X' Γ p l wt')
(fun Γ l awt e => forall wt',
e = erase_fix X_type' X' Γ l wt')
(fun Γ l awt e => forall wt',
e = erase_cofix X_type' X' Γ l wt')).
all:intros *; intros; simp_erase.
simp erase.
all:try simp erase; try iserasableb_irrel_env; simp_erase => //.
all:try clear he Heq.
all:try bang.
all:try solve [cbn; repeat (f_equal; eauto)].
cbn. f_equal. eauto. f_equal.
now rewrite (H (erase_obligation_19 X_type' X' Γ0 d mfix wt')).
now rewrite (H0 (erase_obligation_20 X_type' X' Γ0 d mfix wt')).
Qed.
Lemma erase_constant_body_suffix {X_type X X_type' X'} {cb ondecl ondecl'} :
(forall Σ Σ' : global_env_ext, abstract_env_ext_rel X Σ ->
abstract_env_ext_rel X' Σ' -> ∥ extends_decls Σ' Σ ∥ /\ (Σ.2 = Σ'.2)) ->
erase_constant_body X_type X cb ondecl = erase_constant_body X_type' X' cb ondecl'.
Proof.
intros ext.
destruct cb => //=.
destruct cst_body0 => //=.
unfold erase_constant_body; simpl => /=.
f_equal. f_equal. f_equal.
eapply erase_irrel_global_env; tea.
f_equal.
eapply erase_irrel_global_env; tea.
Qed.
Require Import Morphisms.
From MetaCoq.Template Require Import uGraph.
Global Instance proper_pair_levels_gcs : Proper ((=_lset) ==> GoodConstraintSet.Equal ==> (=_gcs)) (@pair LevelSet.t GoodConstraintSet.t).
Proof.
intros l l' eq gcs gcs' eq'.
split; cbn; auto.
Qed.
Program Fixpoint erase_global_decls {X_type : abstract_env_impl} (deps : KernameSet.t) (X : X_type.π1) (decls : global_declarations)
(prop : forall Σ : global_env, abstract_env_rel X Σ -> Σ.(declarations) = decls) : E.global_declarations :=
match decls with
| [] => []
| (kn, ConstantDecl cb) :: decls =>
let X' := abstract_pop_decls X in
if KernameSet.mem kn deps then
let Xext := abstract_make_wf_env_ext X' (cst_universes cb) _ in
let cb' := erase_constant_body X_type Xext cb _ in
let deps := KernameSet.union deps (snd cb') in
let X'' := erase_global_decls deps X' decls _ in
((kn, E.ConstantDecl (fst cb')) :: X'')
else
erase_global_decls deps X' decls _
| (kn, InductiveDecl mib) :: decls =>
let X' := abstract_pop_decls X in
if KernameSet.mem kn deps then
let mib' := erase_mutual_inductive_body mib in
let X'' := erase_global_decls deps X' decls _ in
((kn, E.InductiveDecl mib') :: X'')
else erase_global_decls deps X' decls _
end.
Next Obligation.
pose proof (abstract_env_wf _ H) as [wf].
pose proof (abstract_env_exists X) as [[? HX]].
pose proof (abstract_env_wf _ HX) as [wfX].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
destruct (abstract_pop_decls_correct X decls prop' _ _ HX H) as [? []].
clear H. specialize (prop _ HX). destruct x, Σ, H0; cbn in *.
subst. sq. destruct wfX. depelim o0. destruct o1. split => //.
Qed.
Next Obligation.
pose proof (abstract_env_ext_wf _ H) as [wf].
pose proof (abstract_env_exists (abstract_pop_decls X)) as [[? HX']].
pose proof (abstract_env_wf _ HX') as [wfX'].
pose proof (abstract_env_exists X) as [[? HX]].
pose proof (abstract_env_wf _ HX) as [wfX].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
pose proof (abstract_pop_decls_correct X decls prop' _ _ HX HX') as [? []].
pose proof (abstract_make_wf_env_ext_correct _ _ _ _ _ HX' H).
clear H HX'. specialize (prop _ HX). destruct x, Σ as [[] u], H0; cbn in *.
subst. sq. inversion H3. subst. clear H3. destruct wfX. cbn in *.
rewrite prop in o0. depelim o0. destruct o1. exact on_global_decl_d.
Qed.
Next Obligation.
pose proof (abstract_env_exists X) as [[? HX]].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
now pose proof (abstract_pop_decls_correct X decls prop' _ _ HX H).
Qed.
Next Obligation.
pose proof (abstract_env_exists X) as [[? HX]].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
now pose proof (abstract_pop_decls_correct X decls prop' _ _ HX H).
Qed.
Next Obligation.
pose proof (abstract_env_exists X) as [[? HX]].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
now pose proof (abstract_pop_decls_correct X decls prop' _ _ HX H).
Qed.
Next Obligation.
pose proof (abstract_env_exists X) as [[? HX]].
assert (prop': forall Σ : global_env, abstract_env_rel X Σ -> exists d, Σ.(declarations) = d :: decls).
{ now eexists. }
now pose proof (abstract_pop_decls_correct X decls prop' _ _ HX H).
Qed.
Lemma erase_global_decls_irr X_type deps (X:X_type.π1) decls prf prf' :
erase_global_decls deps X decls prf =
erase_global_decls deps X decls prf'.
Proof.
revert X deps prf prf'.
induction decls; eauto. intros. destruct a as [kn []]; cbn.
- destruct KernameSet.mem; cbn.
erewrite erase_constant_body_suffix. f_equal.
eapply IHdecls. intros.
pose proof (abstract_env_exists (abstract_pop_decls X)) as [[env wf]].
rewrite (abstract_make_wf_env_ext_correct (abstract_pop_decls X) (cst_universes c) _ _ _ wf H).
now rewrite (abstract_make_wf_env_ext_correct (abstract_pop_decls X) (cst_universes c) _ _ _ wf H0).
apply IHdecls.
- destruct KernameSet.mem; cbn. f_equal. eapply IHdecls.
apply IHdecls.
Qed.
Definition global_erased_with_deps (Σ : global_env) (Σ' : EAst.global_declarations) kn :=
(exists cst, declared_constant Σ kn cst /\
exists cst' : EAst.constant_body,
EGlobalEnv.declared_constant Σ' kn cst' /\
erases_constant_body (Σ, cst_universes cst) cst cst' /\
(forall body : EAst.term,
EAst.cst_body cst' = Some body -> erases_deps Σ Σ' body)) \/
(exists mib mib', declared_minductive Σ kn mib /\
EGlobalEnv.declared_minductive Σ' kn mib' /\
erases_mutual_inductive_body mib mib').
Definition includes_deps (Σ : global_env) (Σ' : EAst.global_declarations) deps :=
forall kn,
KernameSet.In kn deps ->
global_erased_with_deps Σ Σ' kn.
Lemma includes_deps_union (Σ : global_env) (Σ' : EAst.global_declarations) deps deps' :
includes_deps Σ Σ' (KernameSet.union deps deps') ->
includes_deps Σ Σ' deps /\ includes_deps Σ Σ' deps'.
Proof.
intros.
split; intros kn knin; eapply H; rewrite KernameSet.union_spec; eauto.
Qed.
Lemma includes_deps_fold {A} (Σ : global_env) (Σ' : EAst.global_declarations) brs deps (f : A -> EAst.term) :
includes_deps Σ Σ'
(fold_left
(fun (acc : KernameSet.t) (x : A) =>
KernameSet.union (term_global_deps (f x)) acc) brs
deps) ->
includes_deps Σ Σ' deps /\
(forall x, In x brs ->