-
Notifications
You must be signed in to change notification settings - Fork 4
/
terms2.v
2211 lines (1846 loc) · 57.8 KB
/
terms2.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import String.
Require Import bin_rels.
Require Import eq_rel.
Require Import universe.
Require Import LibTactics.
Require Import tactics.
Require Import Coq.Bool.Bool.
Require Import Coq.Program.Tactics.
Require Import Omega.
Require Import Coq.Program.Basics.
Require Import Coq.Lists.List.
Require Import Coq.Init.Notations.
Require Import UsefulTypes.
Require Import Coq.Classes.DecidableClass.
Require Import Coq.Classes.Morphisms.
Require Import list.
Require Import Recdef.
Require Import Eqdep_dec.
Require Import varInterface.
Require Import terms.
Open Scope list_scope.
(** printing # $\times$ #×# *)
(** printing <=> $\Leftrightarrow$ #⇔# *)
(** printing $ $\times$ #×# *)
(** printing & $\times$ #×# *)
(** Here are some handy definitions that will
reduce the verbosity of some of our later definitions
*)
Generalizable Variable Opid.
Section terms2Generic.
Context {NVar VarClass} {deqnvar : Deq NVar} {varcl freshv} {varclass: @VarType NVar VarClass deqnvar varcl freshv}
`{hdeq: Deq Opid} {gts : GenericTermSig Opid}.
Notation NTerm := (@NTerm NVar Opid).
Notation BTerm := (@BTerm NVar Opid).
Definition nobnd (f:NTerm) : BTerm := bterm [] f.
(** %\noindent \\*% We define similar abstractions for other [Opid]s.
This document does not show them. As mentioned before, one can click
at the hyperlinked filename that is closest above to open a
webpage that shows complete contents of this file.
*)
Lemma fold_nobnd :
forall t, bterm [] t = nobnd t.
Proof using.
unfold nobnd; auto.
Qed.
(*
Definition mk_esquash (R : NTerm) :=
oterm (Can NEsquash) [nobnd R].
*)
(* Picks a variable that is not in the set of free variables of a given term *)
Definition newvar (t : NTerm) := fresh_var (free_vars t).
(* Delete. use flat_map instead *)
Fixpoint free_vars_list (terms : list NTerm) :=
match terms with
| [] => []
| t :: ts => free_vars t ++ free_vars_list ts
end.
(* ------ SIMPLE OPERATORS ON TERMS ------ *)
(*
Fixpoint depth (t : NTerm) : nat :=
match t with
| vterm _ => 1
| oterm op bterms => lsum map depth_bterm bterms
end
with depth_bterm (lv : list NVar) (nt : NTerm) :=
match bt with
| bterm lv nt => depth nt
end.
*)
End terms2Generic.
Fixpoint size {NVar:Type} {Opid:Type} (t : @NTerm NVar Opid) : nat :=
match t with
| vterm _ => 1
| oterm op bterms => S (addl (map (@size_bterm NVar _) bterms))
end
with size_bterm {NVar:Type} {Opid:Type} (bt: @BTerm NVar Opid) :nat :=
match bt with
| bterm lv nt => @size NVar Opid nt
end.
Fixpoint wft {NVar:Type} {Opid:Type} {gts : GenericTermSig Opid} (t : @NTerm NVar Opid) : bool :=
match t with
| vterm _ => true
| oterm o bts =>
andb (beq_list deq_nat (map (@num_bvars NVar _) bts) (OpBindings o))
(ball (map wftb bts))
end
with wftb {NVar:Type} {Opid:Type} {gts : GenericTermSig Opid} (bt : @BTerm NVar Opid) : bool :=
match bt with
| bterm vars t => wft t
end.
Scheme Equality for list.
Fixpoint NTerm_beq {NVar:Type} {Opid:Type} `{Deq NVar} `{Deq Opid}
(t1 t2: @NTerm NVar Opid) : bool :=
match (t1, t2) with
| (terms.vterm v1, terms.vterm v2) => decide (v1=v2)
| (terms.oterm o1 lbt1, terms.oterm o2 lbt2)
=> andb (decide (o1=o2)) (list_beq _ (@BTerm_beq NVar Opid _ _) lbt1 lbt2)
|(_,_)=> false
end
with BTerm_beq {NVar:Type} {Opid:Type} `{Deq NVar} `{Deq Opid} (t1 t2:
@BTerm NVar Opid) : bool :=
match (t1, t2) with
| (terms.bterm lv1 t1, terms.bterm lv2 t2) =>
andb (decide (lv1=lv2)) (@NTerm_beq NVar Opid _ _ t1 t2)
end.
(*
Lemma NTerm_beq_correct {NVar:Type} {Opid:Type} `{Deq NVar} `{Deq Opid}
(a b: @terms.NTerm NVar Opid): NTerm_beq a b = true <=> a = b.
Admitted.
*)
Section terms3Generic.
Context {NVar VarClass} {deqnvar : Deq NVar}
{varcl freshv} {varclass: @VarType NVar VarClass deqnvar varcl freshv}
`{hdeq: Deq Opid} {gts : GenericTermSig Opid}.
Notation NTerm := (@NTerm NVar Opid).
Notation BTerm := (@BTerm NVar Opid).
(* ------ INDUCTION ON TERMS ------ *)
Lemma size_subterm2 :
forall (o:Opid) (lb : list BTerm) (b : BTerm) ,
LIn b lb
-> size_bterm b < size (oterm o lb).
Proof using.
simpl. induction lb; intros ? Hin; inverts Hin as; simpl; try omega.
intros Hin. apply IHlb in Hin; omega.
Qed.
Lemma size_subterm3 :
forall (o:Opid) (lb : list BTerm) (nt : NTerm) (lv : list NVar) ,
LIn (bterm lv nt) lb
-> size nt < size (oterm o lb).
Proof using.
introv X.
apply size_subterm2 with (o:=o) in X. auto.
Qed.
Lemma NTerm_better_ind3 :
forall P : NTerm -> Type,
(forall n : NVar, P (vterm n))
-> (forall (o : Opid) (lbt : list BTerm),
(forall (nt: NTerm),
size nt < size (oterm o lbt)
-> P nt
)
-> P (oterm o lbt)
)
-> forall t : NTerm, P t.
Proof using.
intros P Hvar Hbt.
assert (forall n t, size t = n -> P t) as Hass.
Focus 2. intros. apply Hass with (n := size t) ; eauto; fail.
induction n as [n Hind] using comp_ind_type.
intros t Hsz.
destruct t.
apply Hvar.
apply Hbt. introv Hs.
apply Hind with (m := size nt) ; auto.
subst.
assert(size nt < size (oterm o l)); auto.
Qed.
Lemma NTerm_better_ind2 :
forall P : NTerm -> Type,
(forall n : NVar, P (vterm n))
-> (forall (o : Opid) (lbt : list BTerm),
(forall (nt nt': NTerm) (lv: list NVar),
(LIn (bterm lv nt) lbt)
-> size nt' <= size nt
-> P nt'
)
-> P (oterm o lbt)
)
-> forall t : NTerm, P t.
Proof using.
intros P Hvar Hbt.
apply NTerm_better_ind3; eauto.
intros ? ? H.
apply Hbt.
intros ? ? ? Hin Hs. apply H.
eapply le_lt_trans;[apply Hs|].
eapply size_subterm3; eauto.
Qed.
Lemma NTerm_BTerm_ind :
forall (PN : NTerm -> Type) (PB : BTerm -> Type),
(forall n : NVar, PN (vterm n))
-> (forall (o : Opid) (lbt : list BTerm),
(forall b,
(LIn b lbt) -> PB b
)
-> PN (oterm o lbt)
)
-> (forall (lv: list NVar) (nt : NTerm),
PN nt -> PB (bterm lv nt)
)
-> ((forall t : NTerm, PN t) * (forall t : BTerm, PB t)).
Proof using.
introv Hv Hind Hb.
assert (forall A B, A -> (A -> B) -> (A*B)) as H by tauto.
apply H; clear H.
- apply NTerm_better_ind2; auto.
introv Hx. apply Hind. introv Hin. destruct b. eauto.
- intro Hnt. intro b. destruct b. eauto.
Qed.
Lemma NTerm_better_ind :
forall P : NTerm -> Type,
(forall n : NVar, P (vterm n))
-> (forall (o : Opid) (lbt : list BTerm),
(forall (nt : NTerm) (lv: list NVar),
(LIn (bterm lv nt) lbt) -> P nt
)
-> P (oterm o lbt)
)
-> forall t : NTerm, P t.
Proof using.
introv Hv Hind. apply NTerm_better_ind2; auto.
introv Hx. apply Hind. introv Hin. eapply Hx in Hin; eauto.
Qed.
Tactic Notation "nterm_ind" ident(h) ident(c) :=
induction h using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind1" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind1s" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind2;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Lemma num_bvars_on_bterm :
forall (l:list NVar) (n : NTerm),
num_bvars (@bterm NVar Opid l n) = length l.
Proof using.
unfold num_bvars; simpl; sp.
Qed.
Definition wf_term (t : NTerm) := wft t = true.
Definition wf_bterm (bt : BTerm) := wftb bt = true.
Lemma wf_term_proof_irrelevance :
forall t,
forall x y : wf_term t,
x = y.
Proof using.
intros.
apply UIP_dec.
apply bool_dec.
Qed.
Definition wf_term_extract :=
fun (t : NTerm) (x : wf_term t) =>
match x return (x = match x with
| eq_refl => eq_refl (wft t)
end)
with
| eq_refl => eq_refl eq_refl
end.
(*
Definition wf_term_extract1 :=
fun (t : NTerm) (x : wf_term t) =>
match x in _ = b return match b with
| true => x = eq_refl (wft t)
end
with
| eq_refl => eq_refl eq_refl
end.
Lemma wf_term_extract2 :
forall t : NTerm,
forall x : wf_term t,
x = eq_refl (wft t).
*)
(*Lemma yyy : forall A (x : A) (pf : x = x), pf = eq_refl x.
Lemma xxx : forall t (x : wft t = true), x = eq_refl (wft t).*)
Lemma nt_wf_eq :
forall t,
nt_wf t <=> wf_term t.
Proof using.
clear varclass varcl freshv deqnvar VarClass.
unfold wf_term.
nterm_ind t as [|o lbt ind] Case; simpl; intros.
- Case "vterm".
split; sp.
- Case "oterm".
split_iff SCase.
+ SCase "->"; intro w.
inversion w; subst.
allrw.
rewrite beq_list_refl; simpl.
trw ball_true; sp.
alltrewrite in_map_iff; sp; subst.
apply_in_hyp wf; destruct wf; allsimpl.
discover; sp. firstorder.
+ SCase "<-"; sp.
remember (beq_list deq_nat (map num_bvars lbt) (OpBindings o)).
destruct b; allsimpl; sp.
alltrewrite ball_true.
constructor; sp.
destruct l.
apply_in_hyp e.
constructor.
apply e.
apply_hyp.
alltrewrite in_map_iff.
exists (bterm l n); simpl; sp.
remember (OpBindings o).
clear Heql.
revert l Heqb.
Local Opaque deq_nat.
induction lbt; allsimpl.
destruct l; allsimpl; sp.
destruct l; allsimpl; sp.
rewrite decide_decideP in Heqb.
destruct (decideP (num_bvars a = n)); subst; sp.
apply cons_eq.
apply IHlbt; sp.
apply ind with (lv := lv); sp.
Qed.
Lemma nt_wf_implies :
forall t, nt_wf t -> wf_term t.
Proof using.
sp; apply nt_wf_eq; sp.
Qed.
Lemma wf_term_eq :
forall t, wf_term t <=> nt_wf t.
Proof using.
intro; generalize (nt_wf_eq t); sp.
symm; auto.
Qed.
Lemma bt_wf_eq :
forall bt, bt_wf bt <=> wf_bterm bt.
Proof using.
sp; split; intro w.
inversion w; subst; unfold wf_bterm; simpl.
fold (wf_term nt).
apply wf_term_eq; auto.
destruct bt; allunfold wf_bterm; allsimpl.
fold (wf_term n) in w.
constructor.
apply nt_wf_eq; auto.
Qed.
(*
Inductive nt_wfb (t:NTerm) : bool :=
match t with
| vterm _ => true
| bterm _ rt => nt_wfb rt
| oterm o lnt : (eq map (num_bvars) lnt OpBindings o).
*)
Definition closedb (t : NTerm) := nullb (free_vars(t)).
Definition closed_bt (bt : BTerm) := free_vars_bterm bt = [].
Definition isprogram_bt (bt : BTerm) := closed_bt bt # bt_wf bt.
(** Our definition [isprog] below is is logically equivalent to [isprogram],
but unlike [isprogram], it is easy to prove that
for any [t], all members(proofs) of [isprog t] are equal.
An interested reader can look at the lemma
%\coqexternalref{UIP\_dec}
{http://coq.inria.fr/distrib/8.4pl2/stdlib/Coq.Logic.Eqdep\_dec}
{\coqdocdefinition{UIP\_dec}}% from that standard library.
As mentioned before, clicking on the lemma name in
the previous sentence should open
the corresponding webpage of the Coq standard library.
Instead, one can also look at the lemma [isprog_eq] below and
safely ignore these technicalites.
*)
Definition isprog (t : NTerm) := (nullb (free_vars t) && wft t) = true.
Definition isprog_bt (bt : BTerm) :=
(nullb (free_vars_bterm bt) && wftb bt) = true.
Definition isprog_vars (vs : list NVar) (t : NTerm) :=
(sub_vars (free_vars t) vs && wft t) = true.
Lemma closed_nt :
forall op bts,
closed (oterm op bts)
<=>
forall bt, LIn bt bts -> closed_bt bt.
Proof using.
sp; unfold closed, closed_bt; simpl; trw flat_map_empty; split; sp.
Qed.
Lemma closed_nt0 : forall o (nt:NTerm), closed (oterm o [bterm [] nt]) -> closed nt.
Proof using.
intros. unfold closed in H. simpl in H. apply app_eq_nil in H. repnd.
clears_last. unfold closed. assumption.
Qed.
Lemma closed_null_free_vars :
forall (t:NTerm),
closed t <=> null (free_vars t).
Proof using.
unfold closed; sp.
trw null_iff_nil; sp.
Qed.
Lemma isprog_proof_irrelevance :
forall t,
forall x y : isprog t,
x = y.
Proof using.
intros.
apply UIP_dec.
apply bool_dec.
Qed.
Lemma isprog_vars_proof_irrelevance :
forall t vs,
forall x y : isprog_vars vs t,
x = y.
Proof using.
intros.
apply UIP_dec.
apply bool_dec.
Qed.
Require Import tactics.
Lemma isprogram_eq :
forall t,
isprogram t <=> isprog t.
Proof using.
unfold isprog, isprogram.
nterm_ind t Case; simpl; intros.
- Case "vterm".
split; sp. unfold closed in *; allsimpl; sp.
- Case "oterm".
split_iff SCase.
+ SCase "->".
intros i; destruct i as [ cl wf ].
inversion cl; subst.
inversion wf; subst.
repeat (rw andb_eq_true).
rewrite fold_assert.
allrw <- null_iff_nil.
rw ball_map_true.
rw assert_nullb; sp.
rewrite fold_assert.
rw assert_beq_list; auto.
destruct x; allsimpl.
fold (wf_term n).
apply wf_term_eq.
apply_in_hyp p; inversion p; subst; sp.
+ SCase "<-"; intros.
repeat (allrewrite andb_true); repd.
allrw fold_assert.
allrw assert_nullb.
allrw null_iff_nil.
allrw assert_beq_list.
allrw ball_map_true; sp.
constructor; sp.
apply_in_hyp p.
destruct l; allsimpl.
constructor.
allfold (wf_term n).
apply wf_term_eq; auto.
Qed.
Lemma isprogram_implies :
forall t, isprogram t -> isprog t.
Proof using.
sp; apply isprogram_eq; sp.
Qed.
Lemma isprog_implies :
forall t : NTerm, isprog t -> isprogram t.
Proof using.
sp; apply isprogram_eq; sp.
Qed.
Lemma isprog_eq :
forall t, isprog t <=> isprogram t.
Proof using.
intro; symm; apply isprogram_eq; auto.
Qed.
Lemma isprogram_bt_eq :
forall bt,
isprogram_bt bt <=> isprog_bt bt.
Proof using.
intro; unfold isprogram_bt, isprog_bt, closed_bt; split; sp.
allrw; simpl.
fold (wf_bterm bt).
apply bt_wf_eq; auto.
alltrewrite andb_eq_true; sp.
allrewrite fold_assert.
alltrewrite assert_nullb.
alltrewrite null_iff_nil; sp.
destruct bt; constructor.
alltrewrite andb_eq_true; sp; allsimpl.
allfold (wf_term n).
apply nt_wf_eq; auto.
Qed.
Lemma isprog_vars_eq :
forall t vs,
isprog_vars vs t <=> subsetv (free_vars t) vs # nt_wf t.
Proof.
unfold isprog_vars; sp.
rw andb_eq_true.
rewrite fold_assert.
rewrite assert_sub_vars.
rw nt_wf_eq; sp.
Qed.
Lemma isprog_vars_if_isprog :
forall vs t, isprog t -> isprog_vars vs t.
Proof using.
introv ip.
rw isprog_vars_eq.
rw isprog_eq in ip.
destruct ip; sp.
unfold closed in *; allrw; sp.
Qed.
Lemma isprog_vars_app_l :
forall t vs1 vs2,
isprog_vars vs2 t
-> isprog_vars (vs1 ++ vs2) t.
Proof using.
sp; alltrewrite isprog_vars_eq; sp.
unfold subset in *.
apply subset_app_l; sp.
Qed.
Definition areprograms ts := forall t, LIn t ts -> isprogram t.
Lemma areprograms_nil : areprograms [].
Proof using.
unfold areprograms; simpl; sp.
Qed.
Lemma areprograms_snoc :
forall t ts,
areprograms (snoc ts t) <=> areprograms ts # isprogram t.
Proof using.
unfold areprograms; sp; split; sp; try (apply_hyp; rw in_snoc; sp).
alltrewrite in_snoc; sp; subst; sp.
Qed.
Lemma areprograms_cons :
forall t ts, areprograms (t :: ts) <=> isprogram t # areprograms ts.
Proof using.
unfold areprograms; sp; simpl; split; sp; subst; sp.
Qed.
Lemma areprograms_app :
forall ts1 ts2,
areprograms (ts1 ++ ts2) <=> areprograms ts1 # areprograms ts2.
Proof using.
unfold areprograms; sp; split; sp.
apply_hyp; rw in_app_iff; sp.
apply_hyp; rw in_app_iff; sp.
alltrewrite in_app_iff; sp.
Qed.
Lemma isprogram_vterm :
forall v, isprogram (vterm v) <=> False.
Proof using.
unfold isprogram, closed; simpl; sp; split; sp.
Qed.
(*
Ltac repnd :=
repeat match goal with
| [ H : _ # _ |- _ ] =>
let name := fresh H in destruct H as [name H]
| [ H : _ # _ |- _ ] =>
let name := fresh H in destruct H as [name H]
end.
*)
Theorem isprogram_ot_iff :
forall o bts,
isprogram (oterm o bts)
<=>
(map num_bvars bts = OpBindings o
# forall bt, LIn bt bts -> isprogram_bt bt).
Proof using.
intros. sp_iff Case.
- Case "->".
intros Hisp.
unfold isprogram in Hisp. repnd.
inverts Hisp0 as Hflat. inverts Hisp.
split;auto. intros bt Hin.
unfold isprogram_bt.
rw flat_map_empty in Hflat.
apply_in_hyp p; sp.
- Case "<-".
intros eq; destruct eq as [Hmap Hstclose].
unfold isprogram, closed.
split; try (constructor); auto;
try (simpl; apply flat_map_empty);
intros a ain;
apply Hstclose in ain; inversion ain; sp.
Qed.
Theorem nt_wf_ot_implies :
forall lv o (nt1 : NTerm) bts,
nt_wf (oterm o bts)
-> LIn (bterm lv nt1) bts
-> nt_wf nt1.
Proof using. intros ? ? ? ? Hwf Hin. inverts Hwf as Hwf Hmap.
assert (bt_wf (bterm lv nt1)) as Hbf by (apply Hwf; auto).
inverts Hbf. auto.
Qed.
Lemma newvar_prop :
forall (t: NTerm), ! LIn (newvar t) (free_vars t).
Proof using.
unfold newvar; sp.
allapply fresh_var_not_in; sp.
Qed.
(*
Lemma newvar_not_in_free_vars :
forall (t: NTerm),
! LIn nvarx (free_vars t)
-> newvar t = nvarx.
Proof using.
sp.
unfold newvar.
apply fresh_var_nvarx; sp.
Qed.
Lemma newvar_prog :
forall t,
isprog t
-> newvar t = nvarx.
Proof using.
sp.
unfold newvar.
apply isprog_eq in H.
inversion H.
unfold closed in H0.
rewrite H0; sp.
Qed.
*)
(*
(** A value is a program with a canonical operator *)
Inductive isvalue : NTerm -> [univ] :=
| isvl : forall (c : CanonicalOp) (bts : list BTerm ),
isprogram (oterm (Can c) bts)
-> isvalue (oterm (Can c) bts).
Inductive isovalue : NTerm -> Prop :=
| isovl : forall (c : CanonicalOp) (bts : list BTerm),
nt_wf (oterm (Can c) bts)
-> isovalue (oterm (Can c) bts).
Lemma isvalue_closed :
forall t, isvalue t -> closed t.
Proof using.
introv isv; inversion isv.
allunfold isprogram; sp.
unfold isprogram in *.
tauto.
Qed.
Lemma isvalue_program :
forall t, isvalue t -> isprogram t.
Proof using.
introv isv; inversion isv; sp.
Qed.
*)
(* ------ programs ------ *)
Definition WTerm := { t : NTerm | wf_term t }.
Definition WBTerm := { bt : BTerm | wf_bterm bt }.
(*
(* first of all, isprog is NOT a boolean. also, the reader will
be left wondering what UIP_dec is*)
where [isprog] is the Boolean version of [isprogram]
(using a Boolean version of [isprogram] makes it easy to prove that
closed terms are equal by proving that the underlying [NTerm]s are
equals using [UIP_dec]).
*)
(**
The [CTerm] type below is useful in compactly stating definitions
that are only meaningful for closed terms. A [CTerm] is a pair
of an [NTerm] [t] and a proof that [t] is closed.
This [CTerm] type will be handy in compactly
defining the Nuprl type system where types are defined as partial
equivalence relations on closed terms.
*)
Definition CTerm := { t : NTerm | isprog t }.
Definition get_cterm (t : CTerm) := let (a,_) := t in a.
Definition BCTerm := { bt : BTerm | isprog_bt bt }.
(**
We also define a type of terms that specifies what are the possible
free variables of its inhabitants. A term is a [(CVTerm vs)] term
if the set of its free variables is a subset of [vs]. This type is
also useful to define the Nuprl type system. For example, to define
a closed family of types such as a closed function type of the form
$\NUPRLfunction{x}{A}{\NUPRLsuba{B}{z}{x}}$, $A$ has to be closed
and the free variables of $B$ can only be $z$.
*)
Definition CVTerm (vs : list NVar) := { t : NTerm | isprog_vars vs t }.
Definition CVTerm3 := forall a b c, CVTerm [a;b;c].
Definition mk_cvterm (vs : list NVar) (t : NTerm) (p : isprog_vars vs t) :=
exist (isprog_vars vs) t p.
Definition get_wterm (t : WTerm) := let (a,_) := t in a.
Definition get_cvterm (vs : list NVar) (t : CVTerm vs) := let (a,_) := t in a.
Definition get_bcterm (bt : BCTerm) := let (a,_) := bt in a.
Definition selectbt (bts: list BTerm) (n:nat) : BTerm :=
nth n bts (bterm [] (vterm nvarx)).
(*
Definition isnoncan (t: NTerm):=
match t with
| vterm _ => False
| oterm o _ => match o with
| Can _ => False
| NCan _ => True
end
end.
*)
Lemma wf_cterm :
forall t, wf_term (get_cterm t).
Proof.
introv; ( repeat match goal with
| [ H : CTerm |- _ ] => destruct H
| [ H : CVTerm _ |- _ ] => destruct H
end
); simpl.
allrw isprog_eq; unfold isprogram in *; repnd; allrw nt_wf_eq; sp.
Qed.
End terms3Generic.
Ltac irr_step :=
match goal with
| [ H1 : isprog ?a, H2 : isprog ?a |- _ ] =>
assert (H2 = H1) by apply isprog_proof_irrelevance; subst
| [ H1 : isprog_vars ?vs ?a, H2 : isprog_vars ?vs ?a |- _ ] =>
assert (H2 = H1) by apply isprog_vars_proof_irrelevance; subst
end.
Ltac irr := repeat irr_step.
Ltac destruct_cterms :=
repeat match goal with
| [ H : CTerm |- _ ] => destruct H
| [ H : CVTerm _ |- _ ] => destruct H
end.
Ltac dest_cterm H :=
let t := type of H in
match goal with
| [ x : CTerm |- _ ] =>
match t with
| context[x] => destruct x
end
| [ x : CVTerm _ |- _ ] =>
match t with
| context[x] => destruct x
end
end.
(** A faster version of destruct_cterms. We avoid destructing all of them. *)
Ltac dest_cterms H := repeat (dest_cterm H).
Ltac clear_deps h :=
repeat match goal with
| [ H : context[h] |- _ ] => clear H
end.
Tactic Notation "nterm_ind" ident(h) ident(c) :=
induction h using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind1" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Tactic Notation "nterm_ind1s" ident(h) "as" simple_intropattern(I) ident(c) :=
induction h as I using NTerm_better_ind2;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Ltac fold_terms_step :=
match goal with
| [ |- context[bterm [] ?x] ] => fold (nobnd x)
| [ |- context[vterm ?v] ] => fold (mk_var v)
end.
Ltac fold_terms := repeat fold_terms_step.
Ltac boolvar_step :=
match goal with
| [ |- context[beq_var ?v ?v] ] => rw <- beq_var_refl
| [ |- context[memvar ?v ?s] ] =>
let name := fresh "b" in
remember (memvar v s) as name;
match goal with
| [ H : name = memvar v s |- _ ] =>
symmetry in H;
destruct name;
[ rewrite fold_assert in H;
trw_h assert_memvar H;
simpl in H
| trw_h not_of_assert H;
trw_h assert_memvar H;
simpl in H
]
end
| [ |- context[beq_var ?v1 ?v2] ] =>
let name := fresh "b" in
remember (beq_var v1 v2) as name;
match goal with
| [ H : name = beq_var v1 v2 |- _ ] =>
destruct name;
[ apply beq_var_true in H; subst
| apply beq_var_false in H
]
end
| [ H : context[beq_var ?v ?v] |- _ ] => rw <- beq_var_refl in H
end.
Ltac boolvar := repeat boolvar_step.
Ltac unfold_all_mk :=
allunfold mk_var
;allunfold nobnd.
Hint Immediate wf_cterm : wf.
(* Hint Constructors isvalue. *)
Hint Constructors nt_wf bt_wf.
Ltac rwselectbt :=
match goal with
|[ H1: bterm ?lv ?nt = selectbt ?lbt ?n , H2 : context [selectbt ?lbt ?n] |- _ ] => rewrite <- H1 in H2
|[ H1: selectbt ?lbt ?n = bterm ?lv ?nt , H2 : context [selectbt ?lbt ?n] |- _ ] => rewrite H1 in H2
|[ H1: bterm ?lv ?nt = selectbt ?lbt ?n |- context [selectbt ?lbt ?n] ] => rewrite <- H1
|[ H1: selectbt ?lbt ?n = bterm ?lv ?nt |- context [selectbt ?lbt ?n] ] => rewrite H1
end.
Tactic Notation "ntermd" ident(h) "as" simple_intropattern(I) ident(c) :=
destruct h as I;
[ Case_aux c "vterm"
| Case_aux c "oterm"
].
Ltac prove_or :=
try (left;cpx;fail);
try (right;cpx;fail);
try (left;left;cpx;fail);
try (left;right;cpx;fail);
try (right;left;cpx;fail);
try (right;right;cpx;fail).
Ltac fold_selectbt :=
match goal with
[ |- context [nth ?n ?lbt (bterm [] (vterm nvarx))] ] =>
fold (selectbt lbt n)
end.
(*
Ltac d_isnoncan H :=
match type of H with
isnoncan ?t => let tlbt := fresh t "lbt" in let tnc := fresh t "nc" in
let tt := fresh "temp" in
destruct t as [tt|tt tlbt];[inverts H as H; fail|];
destruct tt as [tt|tnc]; [inverts H as H; fail|]
end.
*)
Section terms4Generic.
Context {NVar VarClass} {deqnvar : Deq NVar} {varcl freshv}
{varclass: @VarType NVar VarClass deqnvar varcl freshv}
`{hdeq : Deq Opid} {gts : GenericTermSig Opid}.
Notation NTerm := (@NTerm NVar Opid).
Notation BTerm := (@BTerm NVar Opid).