forked from AU-COBRA/ConCert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPCUICCorrectnessAux.v
2102 lines (1906 loc) · 75 KB
/
PCUICCorrectnessAux.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
(** * Auxiliary lemmas for the soundness proof. *)
From MetaCoq.Utils Require Import MCList.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst.
From MetaCoq.PCUIC Require Import PCUICAstUtils.
From MetaCoq.PCUIC Require Import PCUICLiftSubst.
From MetaCoq.PCUIC Require Import PCUICTyping.
From MetaCoq.PCUIC Require Import PCUICClosed.
From MetaCoq.PCUIC Require Import PCUICLiftSubst.
From MetaCoq.PCUIC Require Import PCUICWcbvEval.
From Coq Require Import PeanoNat.
From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import Basics.
From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Env.
From ConCert.Embedding Require Import Misc.
From ConCert.Embedding Require Import EnvSubst.
From ConCert.Embedding Require Import Ast.
From ConCert.Embedding Require Import EvalE.
From ConCert.Embedding Require Import PCUICFacts.
From ConCert.Embedding Require Import PCUICTranslate.
From ConCert.Embedding Require Import Wf.
From ConCert.Embedding Require Import Utils.
Notation "'eval' ( n , Σ , ρ , e )" := (expr_eval_i Σ n ρ e) (at level 100).
Notation "M { j := N }" := (subst (N :: nil) j M) (at level 10, right associativity).
Import ListNotations Lia ssrbool.
Open Scope list_scope.
Open Scope nat.
Module TCString := bytestring.String.
Definition of_bs (bs : MCString.string) : string := TCString.to_string bs.
Definition to_bs (s : string) : MCString.string := TCString.of_string s.
Coercion to_bs : string >-> MCString.string.
Import NamelessSubst.
Local Set Keyed Unification.
(* [Bool.trans_eq_bool] kills performance, so we remove it *)
#[global] Remove Hints Bool.trans_eq_bool : core.
#[local]
Arguments monad_utils.bind /.
Module P := PCUICAst.
Module PcbvCurr := PCUICWcbvEval.
Notation "Σ |- t1 ⇓ t2 " := (PcbvCurr.eval Σ t1 t2) (at level 50).
(** All constructors of inductives available in the λ-smart environment are available in
the PCUIC environment. *)
(** Eventually, we can translate the whole λ-smart environment, we have a function that
does if for inductives [trans_global_dec] and we use it precisely to unquote
inductives.But it returns [mutual_inductive_entry] and we need
[mutual_inductive_body] *)
Definition genv_sync (Σ1 : list global_dec) (Σ2 : PCUICEnvironment.global_env) :=
forall ind_name c nparams i tys,
resolve_constr Σ1 ind_name c = Some (nparams, i, tys) ->
{ x | let '(mib, oib, cb) := x in
declared_constructor_gen (lookup_env Σ2) (mkInd (kername_of_string ind_name) 0, i) mib oib cb
/\ nparams = ind_npars mib /\ #|tys| = context_assumptions (cstr_args cb) (* same arities *)
}.
Notation "Σ1 ⋈ Σ2 " := (genv_sync Σ1 Σ2) (at level 20).
Tactic Notation "simpl_vars_to_apps" "in" ident(H) :=
simpl in H; try rewrite map_app in H; simpl in H;
rewrite vars_to_apps_unfold in H; simpl in H.
Tactic Notation "simpl_vars_to_apps" :=
simpl; try rewrite map_app; simpl; rewrite vars_to_apps_unfold; simpl.
Section WcbvEvalProp.
Lemma tInd_atom ind i u :
PcbvCurr.atom (tInd (mkInd ind i) u).
Proof. reflexivity. Qed.
Lemma tInd_value_head (Σ : PCUICEnvironment.global_env) ind i u n :
PcbvCurr.value_head Σ n (tInd (mkInd ind i) u).
Proof. constructor. Qed.
Lemma All_eq {A} (l1 l2 : list A) : All2 (fun t1 t2 => t1 = t2) l1 l2 -> l1 = l2.
Proof.
intros H.
induction H; f_equal; auto.
Qed.
Lemma All_All2_impl {A} (l1 l2 : list A) P :
All (fun t1 => forall t2, P t1 t2 -> t1 = t2) l1 ->
All2 P l1 l2 ->
All2 (fun t1 t2 => t1 = t2) l1 l2.
Proof.
intros Hall Hall2.
induction Hall2; auto.
inversion Hall as [a | ty ll HH3 HH4]; subst; clear Hall.
constructor; auto.
Qed.
Lemma mkApps_unfold t1 ts t2 :
mkApps t1 (ts ++ [t2]) = tApp (mkApps t1 ts) t2.
Proof.
apply mkApps_app.
Qed.
Lemma mkApps_eq_false t1 t2 args :
t1 <> t2 -> (forall t1' t2' , t2 <> tApp t1' t2') ->
mkApps t1 args = t2 -> False.
Proof.
intros Hneq Hnapp H.
destruct args using rev_ind; simpl in *; tryfalse.
rewrite mkApps_unfold in H.
destruct t2; tryfalse.
Qed.
Lemma mkApps_tRel_false t args i :
t <> tRel i ->
mkApps t args = tRel i -> False.
Proof.
intros.
eapply mkApps_eq_false; eauto. intros ? ? Hi. tryfalse.
Qed.
Hint Resolve mkApps_tRel_false : facts.
End WcbvEvalProp.
Definition is_app (e : expr) : bool :=
match e with
| eApp _ _ => true
| _ => false
end.
Lemma mkApps_vars_to_apps l : forall (Σ : global_env) e,
P.mkApps (t⟦e⟧Σ) (map (expr_to_term Σ) l) =
t⟦ vars_to_apps e l ⟧ Σ.
Proof.
induction l; intros.
+ reflexivity.
+ simpl. now rewrite <- IHl.
Qed.
Lemma mkApps_vars_to_apps_constr :
forall (Σ1 : global_env) (i0 : Ast.inductive) (n1 : string) (l0 : list val) ci,
resolve_constr Σ1 i0 n1 = Some ci ->
mkApps (tConstruct (mkInd (kername_of_string i0) 0) (ci.1.2) []) (map (fun x => t⟦of_val_i x⟧ Σ1) l0) =
t⟦ vars_to_apps (eConstr i0 n1) (map of_val_i l0) ⟧ Σ1.
Proof.
intros Σ1 i0 n1 l0 ci Hci.
rewrite <- mkApps_vars_to_apps.
simpl. rewrite Hci. apply f_equal. rewrite map_map. reflexivity.
Qed.
Lemma Wcbv_value_vars_to_apps Σ1 Σ2 :
forall (i : inductive) n (l : list val) ci,
Σ1 ⋈ Σ2 ->
resolve_constr Σ1 i n = Some ci ->
#|l| <= ci.1.1 + #|ci.2| -> (* arity, including parameters *)
All (fun v : val => PcbvCurr.value Σ2 (t⟦ of_val_i v ⟧ Σ1)) l ->
PcbvCurr.value Σ2 (t⟦ vars_to_apps (eConstr i n) (map of_val_i l) ⟧ Σ1).
Proof.
intros i n l [[??]?] syncEnv Hres Har Hfa.
destruct (syncEnv _ _ _ _ _ Hres) as [[[??]?][?[??]]].
erewrite <- mkApps_vars_to_apps_constr; eauto.
eapply PcbvCurr.value_app.
+ rewrite length_map. cbn in *.
subst. rewrite H1 in *.
econstructor; eauto.
+ now apply All_map.
Qed.
Open Scope bool.
Fixpoint ge_val_ok Σ v : bool :=
match v with
| vConstr ind ctor args =>
let res :=
match (resolve_constr Σ ind ctor) with
| Some _ => true
| _ => false
end
in res && forallb (ge_val_ok Σ) args
| vClos ρ x0 x1 x2 x3 e => forallb (ge_val_ok Σ ∘ snd) ρ
| vTyClos ρ nm e => forallb (ge_val_ok Σ ∘ snd) ρ
| vTy ty => true
end.
#[export] Hint Constructors PcbvCurr.value : hints.
Lemma decompose_inductive_mkApps ty ind args :
decompose_inductive ty = Some (ind, args) ->
type_to_term ty = mkApps (tInd (mkInd (kername_of_string ind) 0) []) (map type_to_term args).
Proof.
revert args ind.
induction ty; intros args ind Hdi; inversion Hdi; subst.
+ easy.
+ simpl in *. destruct (decompose_inductive ty1) eqn:Heq; tryfalse.
destruct p. inversion Hdi. subst.
rewrite map_app.
cbn.
rewrite mkApps_unfold. now f_equal.
Qed.
Lemma decompose_inductive_value :
forall Σ (t1 : type) (args : list type) ind,
PcbvCurr.value Σ (type_to_term t1) ->
decompose_inductive t1 = Some (ind, args) ->
All (PcbvCurr.value Σ) (map type_to_term args).
Proof.
intros Σ t1.
induction t1; intros args ind Hv Hdi; tryfalse.
+ inversion Hdi; subst. constructor.
+ simpl in *.
destruct (decompose_inductive t1_1) eqn:HH; tryfalse.
destruct p as [ind' tys]. inversion Hdi. subst.
erewrite decompose_inductive_mkApps in Hv by eauto.
rewrite <- mkApps_unfold in Hv.
remember (tInd _ _) as tind.
assert (Hna : ~~ isApp tind) by (subst; auto).
specialize (PcbvCurr.value_mkApps_inv _ _ _ Hna Hv).
intros W. destruct W as [p | p].
* inversion p. destruct tys; tryfalse.
* destruct p as [H1 H2]. now rewrite map_app.
Qed.
Lemma type_value_term_value Σ ty :
iclosed_ty 0 ty ->
ty_val ty ->
PcbvCurr.value Σ (type_to_term ty).
Proof.
intros Hc Hty. induction Hty.
+ simpl. constructor. constructor. apply tInd_atom.
+ simpl. now constructor.
+ simpl. constructor. now constructor.
+ simpl in *. propify. destruct_hyps.
erewrite decompose_inductive_mkApps by eauto.
rewrite <- mkApps_unfold.
eapply PcbvCurr.value_app.
* apply tInd_value_head.
* apply All_app_inv; eauto.
eapply decompose_inductive_value with (t1 := ty1); eauto.
+ do 2 constructor; eauto.
Qed.
#[export] Hint Constructors ty_val : hints.
Lemma env_ok_lookup_ty_val ty i Σ ρ :
env_ok Σ ρ ->
lookup_i ρ i = Some (vTy ty) ->
ty_val ty.
Proof.
intros.
assert (Hok : val_ok Σ (vTy ty)) by now eapply All_lookup_i.
inversion Hok; subst; easy.
Qed.
Lemma env_ok_lookup_closed_ty ty i Σ ρ :
env_ok Σ ρ ->
lookup_i ρ i = Some (vTy ty) ->
iclosed_ty 0 ty.
Proof.
intros.
assert (Hok : val_ok Σ (vTy ty)) by now eapply All_lookup_i.
inversion Hok; subst; easy.
Qed.
Lemma eval_ty_closed Σ ty ty_v ρ n :
env_ok Σ ρ ->
eval_type_i n ρ ty = Some ty_v -> iclosed_ty n ty_v.
Proof.
revert ty_v ρ n.
induction ty; intros ??? Hok He.
+ simpl in *. inversion He. now subst.
+ simpl in *.
destruct (eval_type_i (S n) _ _) eqn:Hty; tryfalse.
inversion He; subst. now simpl.
+ simpl in *.
destruct (eval_type_i _ _ ty2) eqn:Hty2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Hty1; tryfalse.
destruct (decompose_inductive _) eqn:Hind; tryfalse.
inversion He; subst; clear He. simpl.
now propify.
+ tryfalse.
+ simpl in *. destruct (n0 <=? n) eqn:Hn0; tryfalse.
destruct (lookup_i ρ (n - n0)) eqn:Hlook; tryfalse. destruct v; tryfalse.
inversion He. subst. eapply iclosed_ty_0; now eapply env_ok_lookup_closed_ty.
+ simpl in *.
destruct (eval_type_i _ _ ty2) eqn:Hty2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Hty1; tryfalse.
inversion He; subst.
simpl.
now propify.
Qed.
Lemma type_eval_value Σ ρ ty ty_v n :
env_ok Σ ρ ->
eval_type_i n ρ ty = Some ty_v ->
ty_val ty_v.
Proof.
intros Hok He.
generalize dependent ty_v. revert n.
induction ty; intros.
+ simpl in *. inversion He; eauto with hints.
+ simpl in *.
destruct (eval_type_i (S n) _ _) eqn:Hty; tryfalse.
inversion He; subst. now constructor.
+ simpl in *.
simpl in *.
destruct (eval_type_i _ _ ty2) eqn:Hty2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Hty1; tryfalse.
destruct (decompose_inductive _) eqn:Hind; tryfalse.
inversion He; subst; clear He. simpl.
destruct p as [ind0 args].
econstructor; eauto.
+ tryfalse.
+ simpl in *. destruct (n0 <=? n); tryfalse.
destruct (lookup_i ρ (n - n0)) eqn:Hlook; tryfalse. destruct v; tryfalse.
inversion He. subst. now eapply env_ok_lookup_ty_val.
+ simpl in *.
destruct (eval_type_i _ _ ty2) eqn:Hty2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Hty1; tryfalse.
inversion He; subst. now constructor.
Qed.
Lemma type_to_term_eval_value :
forall Σ1 Σ2 (ty ty_v : type) ρ,
env_ok Σ1 ρ ->
eval_type_i 0 ρ ty = Some ty_v ->
PcbvCurr.value Σ2 (type_to_term ty_v).
Proof.
intros.
eapply type_value_term_value; eauto with hints.
eapply eval_ty_closed; eauto.
eapply type_eval_value; eauto.
Qed.
Lemma Wcvb_type_to_term_eval :
forall (Σ1 : PCUICEnvironment.global_env) Σ2 (ty ty_v : type) ρ,
env_ok Σ2 ρ ->
AllEnv (iclosed_n 0) (exprs ρ) ->
eval_type_i 0 ρ ty = Some ty_v ->
Σ1 |- type_to_term ty_v ⇓ type_to_term ty_v.
Proof.
intros.
eapply PcbvCurr.value_final.
eapply type_to_term_eval_value; eauto.
Qed.
Lemma Wcbv_of_value_value v Σ1 Σ2 :
Σ1 ⋈ Σ2 ->
val_ok Σ1 v ->
PcbvCurr.value Σ2 (t⟦ of_val_i v⟧Σ1).
Proof.
intros Hsync Hok.
induction v using val_elim_full.
+ simpl in *.
inversion Hok; subst.
eapply Wcbv_value_vars_to_apps; eauto.
eapply All_impl_inner; eauto.
+ destruct cm. do 2 constructor; auto.
simpl. now do 2 constructor.
+ simpl in *. do 2 constructor; auto.
+ simpl in *.
inversion Hok; subst. now eapply type_value_term_value.
Qed.
Lemma lift_1_closed n t :
closedn n t ->
closedn (S n) ((lift0 1) t) = true.
Proof.
replace (S n) with (n+1) by lia.
now apply closedn_lift with (k := n) (n := 1).
Qed.
#[export] Hint Resolve lift_1_closed : hints.
Lemma type_to_term_closed ty n :
iclosed_ty n ty ->
closedn n (type_to_term ty) = true.
Proof.
revert n.
induction ty; intros n0 H; simpl in *;
propify; destruct_hyps; auto with hints.
Qed.
#[export] Hint Resolve type_to_term_closed : hints.
Lemma type_to_term_subst_par_rec Σ ty k ρ :
ty_env_ok k ρ ty ->
All (fun x : string * expr => iclosed_n 0 (snd x) = true) ρ ->
iclosed_ty (k+#|ρ|) ty ->
subst (map (fun x => expr_to_term Σ (snd x)) ρ) k (type_to_term ty) = type_to_term (subst_env_i_ty k ρ ty).
Proof.
revert k ρ.
induction ty; intros k e0 Hok Hce Hct; simpl in *; propify;
auto with hints; destruct_and_split; auto with all.
+ destruct (k <=? n); auto.
unfold Extras.with_default, lookup_ty.
rewrite lookup_i_nth_error in *.
rewrite nth_error_map.
destruct (nth_error _ _) eqn:Hn; cbn in *.
* destruct p eqn:Hp; cbn in *. destruct e; tryfalse; cbn.
assert (closed T⟦ t ⟧).
{ eapply nth_error_all in Hn; eauto; auto with hints. }
now rewrite lift_closed by auto with hints.
* rewrite length_map. apply f_equal.
apply nth_error_None in Hn; lia.
+ f_equal; auto.
rewrite <- IHty2 by auto.
rewrite commut_lift_subst_rec by lia.
now replace (S k) with (k+1) by lia.
Qed.
Lemma type_to_term_subst Σ ty k e (nm : string) :
ty_env_ok k [(nm,e)] ty ->
iclosed_n 0 e ->
iclosed_ty (1+k) ty ->
(type_to_term ty) {k := t⟦e⟧Σ} = type_to_term (subst_env_i_ty k ([(nm,e)]) ty).
Proof.
intros.
apply type_to_term_subst_par_rec with (ρ := [(nm,e)]); eauto.
cbn; now replace (k+1) with (1+k) by lia.
Qed.
Lemma type_to_term_eval Σ ty k e (nm : string) v:
iclosed_ty k ty ->
eval_type_i k ([(nm,e)]) ty = Some v ->
(type_to_term ty) {k := t⟦of_val_i e⟧Σ} = type_to_term v.
Proof.
revert k e v. induction ty; intros k e0 v Hc H; simpl in *; inversion H; subst; auto; clear H.
+ destruct (eval_type_i _ _ _) eqn:Heq; tryfalse. inversion H1; subst.
simpl. f_equal; eauto.
+ destruct (eval_type_i _ _ ty2) eqn:Heq2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Heq1; tryfalse.
destruct (decompose_inductive t0) eqn:Hde; tryfalse.
inversion H1; subst; clear H1. propify. destruct_hyps.
simpl. f_equal; eauto.
+ destruct (k <=? n) eqn:Hkn.
* destruct (n - k) eqn:Hnk; simpl in *; tryfalse.
unfold is_true in *; propify. lia.
* inversion H1; subst; clear H1; auto.
+ destruct (eval_type_i _ _ ty2) eqn:Heq2; tryfalse.
destruct (eval_type_i _ _ ty1) eqn:Heq1; tryfalse.
inversion H1; subst; clear H1.
propify. destruct_hyps. simpl.
rewrite commut_lift_subst. repeat f_equal; eauto.
Qed.
#[export] Hint Resolve -> length_zero_iff_nil : hints.
#[export] Hint Resolve <- length_zero_iff_nil : hints.
#[export] Hint Resolve type_to_term_subst : hints.
#[export] Hint Resolve type_to_term_closed : hints.
#[export] Hint Unfold compose : hints.
Fixpoint inc_subst (ts : list (string * term)) n (u : term) : list (string * term) :=
match ts with
| [] => []
| (nm, t0) :: ts0 => (nm, t0 {n := u}) :: inc_subst ts0 (1+n) u
end.
Fixpoint nsubst (ts : list term) (n : nat) (t :term) :=
match ts with
| [] => t
| t0 :: ts0 => nsubst ts0 (n-1) (subst [t0] n t)
end.
Lemma nsubst_lam xs b nm ty :
closedn 0 ty ->
nsubst xs (#|xs| - 1) (tLambda nm ty b) = (tLambda nm ty (nsubst xs #|xs| b)).
Proof.
revert b nm ty.
induction xs; intros; auto.
simpl.
assert (closedn (#|xs|) ty) by (eapply closed_upwards; eauto; lia).
replace (S #|xs| - 1) with #|xs| in * by lia.
now rewrite subst_closedn by auto.
Qed.
Lemma map_lift0 xs : map (lift0 0) xs = xs.
Proof.
induction xs; auto.
simpl. now rewrite lift0_p.
Qed.
Lemma simpl_lift_map xs n m p : map ((lift n p) ∘ (lift m p)) xs = map (lift (n+m) p) xs.
Proof.
induction xs; auto.
simpl. unfold compose.
rewrite simpl_lift by lia.
f_equal; eauto.
Qed.
(* TODO : use this lemma in all places where this inversion is needed *)
Lemma eval_lam_inv Σ nm1 nm2 ty1 ty2 b1 b2:
Σ |- tLambda nm1 ty1 b1 ⇓ tLambda nm2 ty2 b2 -> nm1 = nm2 /\ ty1 = ty2 /\ b1 = b2.
Proof.
intros H.
inversion H.
+ now subst.
Qed.
Fixpoint nsubst_alt (ts : list term) (t : term) {struct ts} : term :=
match ts with
| [] => t
| t0 :: ts0 => (nsubst_alt ts0 (t {0 := t0}))
end.
Lemma closed_upwards0 n t :
closed t -> closedn n t.
Proof.
intros; eapply closed_upwards; eauto; lia.
Qed.
#[export] Hint Resolve closed_upwards0 subst_closedn : hints.
Lemma nsubst_app ts t0 t1 :
closed t0 ->
nsubst (ts ++ [t0]) (#|ts|) t1 = nsubst ts (#|ts| - 1) (t1 {0 := t0}).
Proof.
revert t0 t1.
induction ts; intros.
+ simpl. easy.
+ simpl. replace (S #|ts| - 1) with #|ts| by lia. rewrite IHts by assumption.
rewrite distr_subst. simpl. replace (t0 {#|ts| := a}) with t0 by (symmetry; eauto with hints).
reflexivity.
Qed.
Lemma subst_closed_map ts1 ts2 k :
forallb (closedn k) ts2 ->
map (subst ts1 k) ts2 = ts2.
Proof.
intros H. generalize dependent k. revert ts1.
induction ts2; intros; auto.
simpl in *. propify. destruct_hyps.
f_equal; eauto with hints.
Qed.
Ltac destr_args args := let args0 := fresh "args0" in
destruct args as [ | ? args0];
tryfalse; try destruct args0; tryfalse.
Notation "P <--> Q" := (Logic.BiImpl P Q) (at level 100).
Lemma closed_mkApps n t1 t2 :
closedn n (mkApps t1 [t2]) = true <->
closedn n t1 = true /\ closedn n t2 = true.
Proof.
split.
+ intros Hc.
apply Bool.andb_true_iff.
specialize (closedn_mkApps n t1 [t2]) as H. simpl in H.
rewrite Bool.andb_true_r in *. easy.
+ intros Hc.
destruct Hc.
rewrite closedn_mkApps; auto. simpl. rewrite Bool.andb_true_r in *. now rewrite H.
Qed.
#[export] Hint Resolve <- closed_mkApps : hints.
#[export] Hint Resolve -> closed_mkApps : hints.
Lemma genv_ok_constrs_ok Σ ind cs nparam :
genv_ok Σ ->
resolve_inductive Σ ind = Some (nparam, cs) ->
forallb (constr_ok nparam) cs.
Proof.
intros Hgeok Hr. unfold resolve_inductive in *.
destruct (lookup_global Σ ind) eqn:Hlg; tryfalse.
destruct g; tryfalse. inversion Hr; subst; clear Hr.
generalize dependent cs.
induction Σ; intros; tryfalse.
cbn in *. destruct a. cbn in *.
destruct (e0 =? ind)%string; now propify.
Qed.
Lemma constrs_ok_in s c (cs : list constr) nparam :
In (s,c) cs ->
forallb (constr_ok nparam) cs ->
forallb (iclosed_ty nparam) (map snd c).
Proof.
intros Hin Hfa.
assert (constr_ok nparam (s,c)) by (eapply forallb_In; eauto).
easy.
Qed.
Lemma forallb_type_to_term_closed ts n :
forallb (iclosed_ty n) ts ->
forallb (closedn n) (map type_to_term ts).
Proof.
revert n.
induction ts; intros; auto.
cbn in *.
propify.
destruct_hyps.
split; eauto with hints.
Qed.
#[export] Hint Resolve forallb_type_to_term_closed : core.
Lemma closedn_ctx_branches n tys vs :
#|vs| = #|tys| ->
forallb (iclosed_ty n) (map snd tys) ->
closedn_ctx n (map (fun '(nm0, ty) => vass (aRelevant (nNamed (TCString.of_string nm0))) ty)
(combine vs (map (fun x : option ename × type => T⟦ x.2 ⟧) tys))).
Proof.
intros Hlen Htys.
apply forallb_Forall in Htys.
apply Forall_map_inv in Htys.
generalize dependent vs.
induction tys; intros.
- now destruct vs; tryfalse.
- destruct vs; tryfalse; cbn in *.
inversion Hlen as [Hlen0]; subst; clear Hlen.
propify; split.
* inversion Htys; subst; apply IHtys; eauto.
* rewrite length_map, length_combine, length_map.
rewrite Hlen0. replace (Init.Nat.min #|tys| #|tys|) with #|tys| by lia.
inversion Htys; subst; clear Htys.
replace (#|tys| + n) with (n + #|tys|) by lia.
assert (iclosed_ty (n + #|tys|) a.2) by now apply iclosed_ty_m_n.
eauto with hints.
Qed.
Lemma expr_closed_term_closed e n Σ :
genv_ok Σ ->
iclosed_n n e = true -> closedn n (t⟦e⟧Σ) = true.
Proof.
revert n.
induction e using expr_ind_case; intros n1 Hgeok Hc; auto.
+ (* eLambda*)
simpl in *. rewrite Bool.andb_true_iff.
propify. destruct_hyps.
split; auto with hints.
+ (* eTyLam *)
simpl in *. destruct Hc. auto.
+ (* eLetIn *)
simpl in *. repeat rewrite Bool.andb_true_iff in *.
destruct Hc as [[? ?] ?]. repeat split; simpl; eauto with hints.
+ (* eApp *)
simpl in Hc. repeat rewrite Bool.andb_true_iff in *.
cbn -[mkApps]. eauto with hints.
apply <- closed_mkApps. destruct Hc. easy.
+ (* eConstr *)
simpl in *. destruct (resolve_constr Σ i n); auto.
+ (* eCase *)
destruct p. simpl in *. repeat rewrite Bool.andb_true_iff in *.
destruct Hc as [[[? ?] ?] ?].
destruct (resolve_inductive Σ i) eqn:Hres; auto.
destruct ((_ =? _)%nat) eqn:Hnparams; simpl; auto.
propify; repeat split; eauto with hints.
* unfold test_predicate_k; simpl; propify; repeat split; eauto with hints.
** now apply forallb_type_to_term_closed.
** cbn. rewrite closedn_mkApps; eauto. cbn.
replace (#|map type_to_term l0|) with
(#|map (fun x : type => vass (aRelevant nAnon) T⟦ x ⟧) l0|)
by now repeat rewrite length_map.
apply closedn_to_extended_list.
* destruct p as [np cs]. cbn in *.
rewrite forallb_map.
apply forallb_Forall. apply Forall_forall. intros x Hin.
destruct x as [nm tys]. unfold fun_prod,id in *.
unfold test_branch_k; cbn.
remember (etrans_branch _ _ _) as tb.
unfold etrans_branch in Heqtb.
destruct (find (fun x => _)) as [ p0 | ] eqn:Hnm.
2: subst; simpl; auto.
destruct p0 as [pt e1]. cbn in *. rewrite length_map in *.
destruct (#|pVars pt| =? #|tys|)%nat eqn:Hlen; auto.
2: subst; simpl; auto.
apply find_some in Hnm. destruct Hnm as [Hin' Heqs]; cbn in *.
rewrite in_map_iff in Hin'.
destruct Hin' as [x Htmp]. destruct x as [pt1 e2].
destruct Htmp as [He1 Hin'']. inversion He1; subst pt1; subst e1; clear He1.
assert (Hcs : forallb (constr_ok np) cs) by now eapply genv_ok_constrs_ok.
assert (Htys :forallb (iclosed_ty np) (map snd tys)) by now eapply constrs_ok_in.
unfold resolve_inductive in *. destruct (lookup_global _ _); tryfalse. destruct g.
inversion Hres; subst np cs n. clear Hres; cbn in *.
subst; cbn in *.
propify; split.
** rewrite map_map.
now apply closedn_ctx_branches.
** rewrite length_map,length_combine. rewrite_all length_map.
rewrite Hlen. replace (min #|tys| #|tys|) with (#|tys|) by lia.
apply forallb_Forall in H3.
eapply Forall_In in H; eauto; cbn in *.
eapply Forall_In in H3; eauto; cbn in *.
now apply H.
+ simpl in *.
unfold test_def. simpl.
propify.
repeat split; eauto with hints;
try apply type_to_term_closed;
auto with hints solve_subterm.
+ simpl in *. eauto with hints.
Qed.
Lemma closed_exprs_len_iff e n (ρ : env val) :
iclosed_n (n + #|exprs ρ|) e = true <->
iclosed_n (n + #|ρ|) e = true.
Proof.
split.
intros H. rewrite length_map in H. assumption.
intros H. rewrite length_map. assumption.
Qed.
#[export] Hint Resolve
PeanoNat.Nat.compare_eq
Compare_dec.nat_compare_Lt_lt
Compare_dec.nat_compare_Gt_gt
Compare_dec.leb_correct_conv
PeanoNat.Nat.leb_refl : facts.
#[export] Hint Resolve
-> PeanoNat.Nat.ltb_lt : facts.
#[export] Hint Resolve
-> PeanoNat.Nat.leb_le : facts.
#[export] Hint Constructors val_ok Forall : hints.
#[export] Hint Unfold snd env_ok AllEnv compose : hints.
#[export] Hint Resolve subst_env_iclosed_n_inv subst_env_iclosed_0_inv : hints.
#[export] Hint Resolve subst_env_iclosed_n subst_env_iclosed_0 : hints.
Lemma option_to_res_ok {A} (o : option A) s v :
option_to_res o s = Ok v ->
o = Some v.
Proof.
intros H. destruct o. inversion H; auto. tryfalse.
Qed.
Lemma forall_map_spec' :
forall (A B : Type) (P : A -> Prop) (l : list A) (f g : A -> B),
Forall P l -> (forall x : A, In x l -> P x -> f x = g x) -> map f l = map g l.
Proof.
induction l; intros f g Hfa Heq; simpl; auto.
inversion Hfa; subst; clear Hfa.
f_equal.
+ apply Heq; simpl; auto.
+ eapply IHl; intros; try apply Heq; simpl; auto.
Qed.
Lemma forallb_In_snd {A B} (l : list (A * B)) (p : B -> bool) (a : A * B) :
forallb (fun x => p (snd x)) l = true -> In a l -> p (snd a) = true.
Proof.
intros H Hin.
induction l; tryfalse; simpl in *.
propify. now destruct Hin.
Qed.
Lemma forallb_snd {A B} (p : B -> bool) (l1 : list A) (l2 : list B) :
forallb p l2 -> forallb (fun x => p (snd x)) (combine l1 l2).
Proof.
revert l1.
induction l2; intros; destruct l1; auto.
simpl in *; propify. now destruct_and_split.
Qed.
Lemma inc_subst_closed ts t n :
forallb (closedn n) (map snd ts) ->
inc_subst ts n t = ts.
Proof.
revert t n.
induction ts; intros t n H.
+ reflexivity.
+ simpl in *. propify. destruct_hyps. repeat f_equal; eauto with hints.
eapply IHts; eauto. unfold is_true; rewrite forallb_forall in *.
intros. eapply (closed_upwards (k := n)); eauto with hints.
Qed.
Lemma type_to_term_map_par_rec :
forall (ρ : env expr) (Σ : global_env) (n : nat) (args : list type),
forallb (ty_env_ok n ρ) args ->
forallb (fun x : string * expr => iclosed_n 0 (snd x)) ρ ->
forallb (iclosed_ty (n + #|ρ|)) args ->
map (fun x : type => subst (map (expr_to_term Σ ∘ snd) ρ) n (type_to_term x)) args =
map (fun x : type => type_to_term (subst_env_i_ty n ρ x)) args.
Proof.
intros e0 Σ n1 args Hc Hca Hok.
induction args.
+ easy.
+ simpl in *. propify. destruct_hyps. f_equal.
* apply type_to_term_subst_par_rec; eauto using forallb_All.
* eauto.
Qed.
Lemma type_to_term_map :
forall (e0 : expr) (Σ : global_env) (n : nat) (nm : string) (args : list type),
iclosed_n 0 e0 ->
forallb (iclosed_ty (1+n)) args ->
forallb (ty_env_ok n [(nm, e0)]) args ->
map (fun x : type => (type_to_term x) {n := t⟦ e0 ⟧ Σ}) args =
map (fun x : type => type_to_term (subst_env_i_ty n [(nm, e0)] x)) args.
Proof.
intros e0 Σ n1 nm args Hc Hca Hok.
replace (1 + n1) with (n1 + 1) in * by lia.
apply type_to_term_map_par_rec with (ρ := [(nm,e0)]); cbn; propify; eauto.
Qed.
Lemma subst_term_subst_env_rec e e0 :
forall Σ n nm,
genv_ok Σ ->
ty_expr_env_ok (nil # [nm ~> e0]) n e ->
iclosed_n (1+n) e = true ->
iclosed_n 0 e0 = true ->
(t⟦e⟧ Σ) {n := t⟦e0⟧ Σ} =
(t⟦e.[nil # [nm ~> e0]]n⟧ Σ).
Proof.
induction e using expr_ind_case; intros Σ n1 nm Hgeok Hok Hc Hce0.
+ (* eRel *)
cbn.
destruct (Nat.compare n1 n) eqn:Hn.
* assert (n1 = n) by auto with facts.
subst. simpl in *.
assert (Hn0: Nat.leb n n = true) by auto with facts.
rewrite Hn0. replace (n - n) with 0 by lia. simpl.
assert (closed (t⟦ e0 ⟧ Σ) = true) by now apply expr_closed_term_closed.
rewrite lift_closed by assumption.
reflexivity.
* simpl in *.
assert (n1 < n) by auto with facts.
assert (n < S n1) by auto with facts.
exfalso. lia.
* simpl in *.
assert (n < S n1) by auto with facts.
assert (n1 > n) by auto with facts.
assert (Hleb : Nat.leb n1 n = false) by auto with facts.
rewrite Hleb. reflexivity.
+ (* eVar *)
reflexivity.
+ (* eLambda *)
cbn in *. unfold subst1.
propify. destruct_hyps.
erewrite <- type_to_term_subst with (nm := nm); eauto with hints.
f_equal. eapply IHe; eauto.
+ (* eTyLam *)
cbn in *; f_equal; auto.
+ (* eLetIn *)
cbn in *.
unfold is_true in *; propify.
rewrite type_to_term_subst with (nm := nm); auto with all solve_subterm.
+ (* eApp *)
change ((t⟦ eApp e1 e2 ⟧ Σ)) with ((mkApps (t⟦e1⟧Σ) [t⟦e2⟧Σ])) in *.
cbn -[mkApps] in *. unfold is_true in *.
propify. destruct Hc as [Hce1 Hce2].
rewrite subst_mkApps.
change (tApp t⟦e1.[[(nm, e0)]] n1⟧Σ t⟦e2.[[(nm, e0)]] n1⟧ Σ) with
(mkApps t⟦e1.[[(nm, e0)]] n1⟧Σ [t⟦e2.[[(nm, e0)]] n1⟧ Σ]).
f_equal.
eapply IHe1; auto with funelim.
simpl; f_equal; eapply IHe2; auto with funelim.
+ (* eConstr *)
simpl. destruct (resolve_constr Σ i n); auto.
+ (* eConst *)
reflexivity.
+ (* eCase *)
cbn in *. destruct p as [ind tys]. unfold is_true in *; simpl in *.
propify. destruct Hc as [Hce1 Hce2].
destruct (resolve_inductive Σ ind) eqn:Hres; auto.
rewrite length_map. destruct (_ =? _)%nat eqn:Hnparams; auto.
cbn.
repeat f_equal.
* unfold map_predicate_k; cbn.
rewrite_all map_map.
erewrite <- type_to_term_map with (Σ := Σ) by auto with solve_subterm.
rewrite <- map_map with (f := fun x => T⟦ subst_env_i_ty n1 [(nm, e0)] x⟧).
erewrite <- type_to_term_map with (Σ := Σ) by auto with solve_subterm.
rewrite map_map.
f_equal.
** do 3 (apply f_equal2; auto).
unfold to_extended_list, to_extended_list_k.
assert (Hreln : forall ys1 ys2 xs n,
#|ys1| = #|ys2| ->
reln xs n (map (vass (aRelevant nAnon)) ys1) =
reln xs n (map (vass (aRelevant nAnon)) ys2)).
{ induction ys1; intros ys2 xs n Heq; destruct ys2; cbn in *; inversion Heq; cbn; auto. }
rewrite <- map_map. rewrite <- map_map with (f := fun x => T⟦ x ⟧ {n1 := t⟦ e0 ⟧ Σ}).
apply Hreln. now repeat rewrite length_map.
** rewrite commut_lift_subst. auto with all hints solve_subterm.
* apply IHe; auto with solve_subterm.
* rewrite_all map_map. simpl.
unfold on_snd. destruct p as [p cs]; simpl in *.
apply map_ext_in.
intros ctor Hin. destruct ctor as [s l0] eqn:Hconsr. unfold on_snd,etrans_branch.
unfold fun_prod,id. cbn. destruct (find _ _) eqn:Hfnd; simpl.
** eapply find_map with
(p2 := (fun x => pName (fst x) =? s)%string)
(f := fun x => ((fst x), (snd x){#|pVars (fst x)|+n1 := t⟦ e0 ⟧ Σ})) in Hfnd; auto.
rewrite map_map in Hfnd. simpl in Hfnd. unfold fun_prod,id. simpl.
assert (Hmap :
(map (fun x => (id (fst x), (t⟦snd x⟧ Σ) {#|pVars (fst x)|+n1 := t⟦e0⟧ Σ})) l) =
(map (fun x => (fst x, t⟦(snd x) .[[(nm,e0)]](#|pVars (fst x)| + n1) ⟧ Σ)) l)).
{ eapply forall_map_spec'. apply H. intros a Hin' Ha. f_equal.
destruct Hok as [[[? ?] ?] Hty_ok].
assert (iclosed_n (#|pVars (fst a)| + S n1) (snd a) = true) by
now eapply forallb_forall with (x := a) in Hce2.
assert (ty_expr_env_ok [(nm, e0)] (#|pVars a.1| + n1) a.2 = true) by
now eapply forallb_forall with (x := a) in Hty_ok.
apply Ha; auto with hints.
replace (S (#|pVars (fst a)| + n1)) with
(#|pVars (fst a)| + S n1) by lia.
assumption. }
rewrite <- Hmap. unfold id in *. rewrite Hfnd. simpl.
rewrite length_map.
destruct (Nat.eqb #|pVars (fst p0)| #|l0|) eqn:Hlen; simpl; auto.
unfold map_branch_k; cbn. rewrite_all length_map. rewrite length_combine.
rewrite_all length_map. rewrite PeanoNat.Nat.eqb_eq in Hlen.
rewrite Hlen. replace (min _ _) with #|l0| by lia.
f_equal.
** change (fun x : pat * term => pName (fst x) =? s)%string with
((fun x : pat => pName x =? s) ∘ fst (B := term))%string in *.
erewrite find_none_fst with (l1 := (map (fun x : pat × expr => (x.1, t⟦ x.2 ⟧ Σ)) l)); eauto.
now repeat rewrite map_map.
+ (* eFix *)
cbn in *. unfold is_true in *; repeat rewrite Bool.andb_true_iff in *.
unfold map_def. simpl. repeat f_equal; auto with hints solve_subterm.
rewrite commut_lift_subst. auto with all hints solve_subterm.
rewrite commut_lift_subst. auto with all hints solve_subterm.
+ (* eTy *) simpl in *. eauto with hints.
Qed.
Lemma subst_term_subst_env e :
forall v Σ nm,
let ρ := nil # [nm ~> of_val_i v] in
genv_ok Σ ->
ty_expr_env_ok ρ 0 e ->
val_ok Σ v ->
iclosed_n 1 e = true ->
(t⟦e⟧ Σ) {0 := t⟦ of_val_i v ⟧ Σ} =
(t⟦e.[ρ]⟧ Σ).
Proof.
simpl; intros.
assert (iclosed_n 0 (of_val_i v) = true) by now eapply of_value_closed.
now apply subst_term_subst_env_rec.
Qed.
Lemma subst_env_ty_closed_n_eq n m ty ρ :
iclosed_ty n ty ->
subst_env_i_ty (m + n) ρ ty = ty.
Proof.
revert n m ρ.
induction ty; intros; simpl in *; unfold is_true in *; propify; auto with all solve_subterm.
+ f_equal. now replace (S (m + n)) with (m + S n) by lia.
+ destruct (Nat.leb (m + n0)) eqn:Hmn1; propify; try lia; easy.
Qed.
#[export] Hint Resolve subst_env_ty_closed_n_eq : hints.
Lemma map_subst_env_ty_closed n m ρ l0 :
forallb (iclosed_ty n) l0 ->
map (subst_env_i_ty (m + n) ρ) l0 = l0.
Proof.
intros H. generalize dependent n. revert m ρ. induction l0; intros m ρ n Hc; simpl; auto.
simpl in *. propify. destruct_hyps. f_equal; eauto with hints.
Qed.
Lemma subst_env_i_closed_n_eq :
forall (e : expr) (n m : nat) (ρ : env expr),
iclosed_n n e = true ->
e.[ρ](m+n) = e.
Proof.
intros e.
induction e using expr_ind_case; intros n1 m1 ρ Hc; simpl in *;
propify; eauto with hints.
+ simpl in *. destruct (Nat.leb (m1 + n1)) eqn:Hmn1; propify; try lia; easy.
+ simpl in *. f_equal. eapply subst_env_ty_closed_n_eq; auto with solve_subterm.
now replace (S (m1 + n1)) with (m1 + S n1) by lia.
+ simpl in *. f_equal. replace (S (m1 + n1)) with (m1 + S n1) by lia. easy.
+ simpl in *. f_equal; replace (S (m1 + n1)) with (m1 + S n1) by lia; auto with hints solve_subterm.
+ simpl in *. f_equal; replace (S (m1 + n1)) with (m1 + S n1) by lia; easy.
+ simpl in *. destruct p.
assert (map (fun x : pat × expr => (x.1, x.2 .[ ρ] (#|pVars x.1| + (m1 + n1)))) l = l).
{ transitivity (map id l).
eapply forall_map_spec'; eauto.
simpl. intros x Hin Hx. destruct x. unfold id. f_equal. simpl in *.
replace (#|pVars p| + (m1 + n1)) with (m1 + (#|pVars p| + n1)) by lia.
apply Hx. destruct_and_split. rewrite forallb_forall in *.
rewrite Forall_forall in *.
change e0 with (snd (p,e0)).
change p with (fst (p,e0)). easy.
apply map_id. }