-
Notifications
You must be signed in to change notification settings - Fork 0
/
Free_algebra.v
1001 lines (947 loc) · 30.5 KB
/
Free_algebra.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 Bintree.
Require Import Env.
Unset Boxed Definitions.
Section with_Denv.
Variable Denv:domain_env.
Record fun_entry : Type :=
mkF{F_arity: arity;
F_result:domain;
F_it: abstract Denv F_arity (interp_domain Denv F_result)}.
Definition signature := Store fun_entry.
Inductive term: Set :=
App : positive -> args -> term
| DB : nat -> term
| Var : positive -> term
with args : Set :=
No_args : args
| More_args : term -> args -> args.
Inductive occ_term :Set :=
Not_here: occ_term
| Here: occ_term
| In_args: occ_args -> occ_term
with occ_args : Set :=
No_occ: occ_args
| Skip_occ : occ_args -> occ_args
| More_occ : occ_term -> occ_args -> occ_args.
Definition mkVar := Var.
Fixpoint term_eq (p q:term) {struct p} :bool :=
match p, q with
App fp argsp,App fq argsq =>
if pos_eq fp fq then args_eq argsp argsq else false
| DB ip, DB iq => nat_eq ip iq
| Var vp, Var vq => pos_eq vp vq
| _, _ => false
end
with args_eq (ap aq:args) {struct ap} : bool :=
match ap, aq with
No_args, No_args => true
| More_args tp aap, More_args tq aaq =>
if term_eq tp tq then args_eq aap aaq else false
| _, _ => false
end.
Lemma refl_term_eq : forall t, term_eq t t =true.
fix 1.
intros [f a |i|n];simpl.
rewrite refl_pos_eq.
induction a;simpl;clean.
rewrite refl_term_eq;auto.
apply refl_nat_eq.
apply refl_pos_eq.
Qed.
Lemma refl_args_eq : forall a, args_eq a a =true.
induction a;simpl;clean.
rewrite refl_term_eq;auto.
Qed.
Fixpoint inst_term (t:term) (n:nat) (s:term) {struct s} :term :=
match s with
App f a => App f (inst_args t n a)
| DB i => if nat_eq i n then t else DB i
| Var v => Var v
end
with inst_args (t:term) (n:nat) (a:args) {struct a} :args :=
match a with
No_args => No_args
| More_args arg more => More_args (inst_term t n arg) (inst_args t n more)
end.
Fixpoint rewrite_term (ta tb:term) (occ:occ_term) (t:term) {struct t} :
option term :=
match occ with Not_here => Some t
| Here => if term_eq t ta then Some tb else None
| In_args aocc =>
match t with
App f a =>
match rewrite_args ta tb aocc a with None => None
| Some rargs => Some (App f rargs)
end
| _ => None
end end
with rewrite_args (ta tb:term) (aocc:occ_args) (a:args) {struct a} :
option args:=
match aocc with
No_occ => Some a
| Skip_occ occq =>
match a with No_args => None
| More_args t q =>
match rewrite_args ta tb occq q with None => None
| Some rq => Some (More_args t rq)
end end
| More_occ occ occq =>
match a with No_args => None
| More_args t q =>
match rewrite_term ta tb occ t,rewrite_args ta tb occq q with
Some rt,Some rq => Some (More_args rt rq)
| _,_ => None
end end end.
Variable Sigma : signature.
Fixpoint check_ground_term (C:var_ctx) (t:term) (expected:domain)
{struct t}: bool :=
match t with
App t a =>
match get t Sigma with PNone => false | PSome TE =>
if pos_eq expected (F_result TE) then
check_ground_args C a (F_arity TE)
else false end
| DB n => false
| Var p =>
match get p C with PSome dom => pos_eq dom expected | _ => false end
end
with check_ground_args (C:var_ctx) (a:args) (rge:list domain) {struct a} : bool :=
match a, rge with
No_args, nil => true
| More_args arg argv, dom::domv =>
if check_ground_term C arg dom then
check_ground_args C argv domv
else false
| _, _ => false end.
Inductive WF_ground_term : var_ctx -> term -> domain -> Prop :=
WF_ground_App :
forall hyps p argv rge dom t,
get p Sigma=PSome (mkF rge dom t) ->
WF_ground_args hyps argv rge ->
WF_ground_term hyps (App p argv) dom
| WF_ground_Var :
forall hyps n dom,
get n hyps = PSome dom ->
WF_ground_term hyps (Var n) dom
with WF_ground_args : var_ctx -> args -> list domain -> Prop :=
WF_ground_No : forall hyps , WF_ground_args hyps No_args nil
| WF_ground_More : forall hyps arg argv dom domv,
WF_ground_term hyps arg dom -> WF_ground_args hyps argv domv ->
WF_ground_args hyps (More_args arg argv) (dom::domv).
Lemma WF_checked_ground_term :
forall vars t expected,
check_ground_term vars t expected = true ->
WF_ground_term vars t expected.
fix 2;intros hyps t expected;destruct t;simpl.
caseq (get p Sigma).
intros FE e;destruct FE;simpl.
caseq (pos_eq expected F_result0).
intro ee;rewrite (pos_eq_refl _ _ ee).
intro Hargs;left with F_arity0 F_it0;auto.
generalize F_arity0 Hargs;clear Hargs.
induction a;intro rge;destruct rge;simpl;try congruence.
left.
intro Hargs;
caseq (check_ground_term hyps t d);intro e0;rewrite e0 in Hargs.
right.
apply WF_checked_ground_term;auto.
apply IHa;auto.
congruence.
congruence.
congruence.
congruence.
caseq (get p hyps).
intro d.
intros e e0;rewrite <-(pos_eq_refl _ _ e0).
right;auto.
congruence.
Qed.
Fixpoint check_term (gamma:var_ctx) (rels:rel_ctx) (t:term) (expected:domain)
{struct t}: bool :=
match t with
App t a =>
match get t Sigma with
PNone => false
| PSome (mkF rge dom _) =>
if pos_eq expected dom then
check_args gamma rels a rge
else false
end
| DB n =>
match Lget n rels with
None => false
| Some dom => pos_eq expected dom
end
| Var p =>
match get p gamma with
PSome dom => pos_eq expected dom
| _ => false
end
end
with check_args (gamma:var_ctx) (rels:list domain) (a:args) (rge:arity)
{struct a} : bool :=
match a,rge with
No_args,nil => true
| More_args arg argv,dom::domv =>
if check_term gamma rels arg dom then
check_args gamma rels argv domv
else false
| _ , _ => false
end.
Inductive WF_term (gamma:var_ctx) (rels:list domain) : term -> domain -> Prop :=
WF_App : forall n a rge dom t,
get n Sigma = PSome (mkF rge dom t) ->
WF_args gamma rels a rge -> WF_term gamma rels (App n a) dom
| WF_DB : forall i dom, Lget i rels = Some dom ->
WF_term gamma rels (DB i) dom
| WF_Var : forall n dom, get n gamma = PSome dom ->
WF_term gamma rels (Var n) dom
with WF_args (gamma:var_ctx) (rels:list domain) : args -> arity -> Prop :=
WF_nil : WF_args gamma rels No_args nil
| WF_cons : forall a rge arg dom,
WF_term gamma rels arg dom -> WF_args gamma rels a rge ->
WF_args gamma rels (More_args arg a) (dom :: rge).
Lemma WF_checked_term : forall vars rels t expected,
check_term vars rels t expected = true ->
WF_term vars rels t expected.
fix 3;intros vars rels t;destruct t;simpl.
caseq (get p Sigma).
intros [rge dom head];intros ep expected.
caseq (pos_eq expected dom).
intros edom Hargs.
rewrite (pos_eq_refl _ _ edom).
constructor 1 with rge head.
assumption.
generalize rge Hargs;clear rge head ep Hargs dom edom;induction a;
intros [ |dom domv];simpl.
left.
congruence.
congruence.
right.
generalize Hargs;clear Hargs.
caseq (check_term vars rels t dom).
intros H _ ;apply WF_checked_term;assumption.
congruence.
generalize Hargs;clear Hargs.
caseq (check_term vars rels t dom).
intros _ H;apply IHa;assumption.
congruence.
congruence.
congruence.
caseq (Lget n rels).
intros dom en expected edom.
rewrite (pos_eq_refl _ _ edom);constructor 2;assumption.
congruence.
caseq (get p vars).
intros dom.
intros en expected edom; rewrite (pos_eq_refl _ _ edom);constructor 3;assumption.
congruence.
Qed.
Lemma WF_checked_args : forall vars rels a rge,
check_args vars rels a rge = true ->
WF_args vars rels a rge.
induction a;intros [ | dom domv].
left.
simpl;congruence.
simpl;congruence.
simpl;caseq (check_term vars rels t dom).
intros et ea;right.
apply WF_checked_term;assumption.
apply IHa;assumption.
congruence.
Qed.
Lemma WF_ground_term_term :
forall hyps rc t dom,
WF_ground_term hyps t dom ->
WF_term hyps rc t dom.
intros hyps rc;fix 1.
intros [ f a | i | n ] dom W; inversion W;subst.
constructor 1 with rge t;trivial.
generalize rge H4;clear rge t H2 H4 W.
induction a;intros rge W;inversion W;subst.
left.
right;trivial.
apply WF_ground_term_term;trivial.
apply IHa;trivial.
constructor 3;trivial.
Qed.
Lemma WF_term_nil_ground_term :
forall hyps t dom,
WF_term hyps nil t dom ->
WF_ground_term hyps t dom.
intros hyps; fix 1.
intros [ f a | i | n ] dom W; inversion W;subst.
constructor 1 with rge t;trivial.
generalize rge H3;clear rge t H1 H3 W.
induction a;intros rge W;inversion W;subst.
left.
right;trivial.
apply WF_term_nil_ground_term;trivial.
apply IHa;trivial.
destruct i;simpl in H0;clean.
constructor 2;trivial.
Qed.
Fixpoint interp_term
(gamma:var_env Denv) (rc:rel_env Denv) (t:term) (expected:domain) {struct t}:
option (interp_domain Denv expected) :=
match t with
App hd a =>
match get hd Sigma with
PNone => None
| PSome (mkF rge dom head) =>
match pos_eq_dec dom expected with
right _ => None
| left e =>
match interp_args gamma rc a rge (interp_domain Denv dom) head with
PNone => None
| PSome it => Some (eq_rec _ (interp_domain Denv) it _ e)
end
end
end
| DB i =>
match Lget i rc with
None => None
| Some (mkE dom it) =>
match pos_eq_dec dom expected with
right _ => None
| left e => Some (eq_rec _ (interp_domain Denv) it _ e)
end
end
| Var n =>
match get n gamma with
PNone => None
| PSome (mkE dom it) =>
match pos_eq_dec dom expected with
right _ => None
| left e => Some (eq_rec _ (interp_domain Denv) it _ e)
end
end
end
with interp_args
(gamma:var_env Denv) (rc:rel_env Denv) (a:args) (rge:arity) (S:Type) {struct a}:
abstract Denv rge S -> Poption S :=
match a,rge return abstract Denv rge S -> Poption S with
No_args,nil => @PSome _
| More_args t argv,dom::domv =>
match interp_term gamma rc t dom with
None => (fun _ => PNone)
| Some arg =>
(fun f => interp_args gamma rc argv domv S (f arg))
end
| _ , _ => (fun _ => PNone)
end.
Lemma EFQ: forall P:Prop, false=true -> P.
congruence.
Qed.
Fixpoint term_eq_id p q {struct p}: term_eq p q = true -> p = q :=
match p , q return term_eq p q = true -> p = q with
App fp argsp, App fq argsq =>
(if pos_eq fp fq as test return
pos_eq fp fq =test -> (if test then args_eq argsp argsq else false) = true ->
App fp argsp = App fq argsq then
(fun testf testargs =>
f_equal2 _ (pos_eq_refl fp fq testf) (args_eq_id argsp argsq testargs))
else (fun _ h => EFQ _ h)) (refl_equal (pos_eq fp fq))
| DB ip,DB iq =>(fun h => f_equal _ (nat_eq_refl _ _ h))
| Var vp,Var vq => (fun h => f_equal _ (pos_eq_refl _ _ h))
| _,_ => EFQ _
end
with args_eq_id ap aq {struct ap}: args_eq ap aq = true -> ap = aq :=
match ap , aq return args_eq ap aq = true -> ap = aq with
More_args tp argsp, More_args tq argsq =>
(if term_eq tp tq as test return
term_eq tp tq = test -> (if test then args_eq argsp argsq else false) =true ->
More_args tp argsp = More_args tq argsq then
(fun testt testargs =>
f_equal2 _ (term_eq_id tp tq testt) (args_eq_id argsp argsq testargs))
else (fun _ h => EFQ _ h)) (refl_equal (term_eq tp tq))
| No_args,No_args => (fun _ => refl_equal No_args)
| _,_ => EFQ _
end.
Lemma term_eq_refl: forall vars rels dom t1 t2,
term_eq t1 t2 = true ->
interp_term vars rels t1 dom =
interp_term vars rels t2 dom.
intros until t2; intro e; generalize (term_eq_id _ _ e).
congruence.
Qed.
Lemma args_eq_refl: forall vars rels doms T hd a1 a2,
args_eq a1 a2 = true ->
interp_args vars rels a1 doms T hd =
interp_args vars rels a2 doms T hd.
intros until a2; intro e; generalize (args_eq_id _ _ e).
congruence.
Qed.
Lemma ground_term_invar :
forall hyps Venv rc t dom,
WF_ground_term hyps t dom ->
interp_term Venv rc t dom =
interp_term Venv nil t dom .
intros hyps Venv rc;fix 1.
intros [ f a | i | n ] dom W; inversion W;subst;simpl.
rewrite H2.
rewrite pos_eq_dec_refl.
replace (interp_args Venv rc a rge (interp_domain Denv dom) t)
with (interp_args Venv nil a rge (interp_domain Denv dom) t).
reflexivity.
generalize rge (interp_domain Denv dom) t H4.
clear rge t H2 H4 W.
induction a;intros rge P head W;inversion W;subst;simpl.
reflexivity.
rewrite ground_term_invar;trivial.
case (interp_term Venv nil t dom0);trivial.
intro i;apply IHa;trivial.
reflexivity.
Qed.
Lemma interp_WF_ground_term_Some :
forall hyps F Venv,
Instanceof Denv hyps F Venv->
forall t dom,
WF_ground_term hyps t dom ->
(exists x, interp_term Venv nil t dom = Some x).
intros hyps F Venv Inst. fix 1.
intros [ f a | i | n ] dom W; inversion W;subst;simpl.
rewrite H2.
rewrite pos_eq_dec_refl;simpl.
cut (ex (fun X =>
interp_args Venv nil a rge (interp_domain Denv dom) t =PSome X)).
intro H;destruct H;rewrite H.
exists x;trivial.
generalize rge (interp_domain Denv dom) t H4; clear rge t H2 H4 W.
induction a;intros rge P T W;inversion W;subst;simpl.
exists T;reflexivity.
elim (interp_WF_ground_term_Some t dom0 );trivial.
intros x ex;rewrite ex;apply IHa;trivial.
elim (get_Instanceof _ _ _ _ _ Inst _ H1);intros x ex.
rewrite ex.
rewrite pos_eq_dec_refl;simpl.
exists x;reflexivity.
Qed.
Lemma WF_term_instx : forall V (F:Full V) rels dom t expected,
WF_term V (rels ++ dom :: nil) t expected ->
WF_term (V \ dom) rels
(inst_term (mkVar (index V)) (length rels) t) expected.
fix 5.
intros hyps F rc dom [ f a | i | n ] expected W;simpl inst_term;inversion W;subst.
constructor 1 with rge t;trivial.
generalize rge H3;clear rge t H1 H3 W.
induction a;intros rge W;inversion W;subst;simpl inst_args.
left.
right.
apply WF_term_instx;trivial.
apply IHa;trivial.
caseq (nat_eq i (length rc));intro ei.
constructor 3.
rewrite get_push_Full;trivial.
rewrite Pcompare_refl.
rewrite Lget_app in H0.
rewrite ei in H0.
congruence.
constructor 2.
rewrite Lget_app in H0.
rewrite ei in H0;assumption.
constructor 3.
apply (Full_push_compat _ _ dom _ F _ H0).
Qed.
Lemma WF_args_instx :forall V (F:Full V) rels dom a doms,
WF_args V (rels ++ dom :: nil) a doms ->
WF_args (V \ dom) rels
(inst_args (mkVar (index V)) (length rels) a) doms.
induction a;intros rge W;inversion W;subst;simpl inst_args.
left.
right.
apply WF_term_instx;trivial.
apply IHa;trivial.
Qed.
Lemma term_instx : forall V F Venv, Instanceof Denv V F Venv ->
forall dom rel rels t expected, WF_term V
(List.map (E_domain Denv) (rels ++ (mkE Denv dom rel) :: nil)) t expected ->
interp_term (Venv\mkE Denv dom rel) rels
(inst_term (mkVar (index V)) (length rels) t) expected =
interp_term Venv (rels ++ (mkE Denv dom rel) :: nil) t expected.
intros hyps F Venv Inst dom rel rc.
fix 1.
intros [f a | i | n] expected W; inversion W;subst;simpl.
rewrite H1.
rewrite pos_eq_dec_refl.
replace
(interp_args (Venv \ mkE Denv dom rel) rc
(inst_args (mkVar (index hyps)) (length rc) a) rge
(interp_domain Denv expected) t)
with
(interp_args Venv (rc ++ mkE Denv dom rel :: nil) a rge
(interp_domain Denv expected) t).
case (interp_args Venv (rc ++ mkE Denv dom rel :: nil) a rge
(interp_domain Denv expected) t);reflexivity.
generalize (interp_domain Denv expected) rge H3 t ; clear rge t H1 H3 W.
induction a; intros P rge W; inversion W;subst;simpl.
reflexivity.
rewrite term_instx;trivial.
case (interp_term Venv (rc ++ (mkE Denv dom rel) :: nil) t dom0);clean.
intros i t0;apply IHa;trivial.
rewrite Lget_app.
caseq (nat_eq i (length rc));simpl.
rewrite get_push_Full;trivial.
rewrite (index_Instanceof Denv hyps F Venv);trivial.
rewrite Pcompare_refl.
reflexivity.
exact (Instanceof_Full _ _ _ _ Inst).
reflexivity.
elim (get_Instanceof _ _ _ _ _ Inst _ H0).
intros var en;simpl.
assert (FF:=Instanceof_Full _ _ _ _ Inst).
rewrite get_push_Full;trivial.
rewrite en.
caseq (n ?= index Venv);intro PCn.
rewrite (Pcompare_Eq_eq _ _ PCn) in en.
rewrite get_Full_Eq in en;trivial;congruence.
reflexivity.
rewrite get_Full_Gt in en;trivial;congruence.
Qed.
Lemma args_instx : forall V F Venv, Instanceof Denv V F Venv ->
forall dom rel rels a doms (T:Type) head, WF_args V
(List.map (E_domain Denv) (rels ++ (mkE Denv dom rel) :: nil)) a doms ->
interp_args (Venv\mkE Denv dom rel) rels
(inst_args (mkVar (index V)) (length rels) a) doms T head =
interp_args Venv (rels ++ (mkE Denv dom rel) :: nil) a doms T
head.
induction a; intros rge T head W;inversion W;subst;simpl;clean.
rewrite (term_instx _ F Venv);trivial.
destruct (interp_term Venv (rels ++ mkE Denv dom rel :: nil) t dom0).
apply IHa;trivial.
reflexivity.
Qed.
Lemma WF_term_inst : forall V t dom,
WF_ground_term V t dom ->
forall rels tt dd,
WF_term V (rels ++ dom :: nil) tt dd ->
WF_term V rels (inst_term t (length rels) tt) dd.
intros hyps t dom Wgt rc; fix 1;intros [ f a | i | n] dd W;inversion W;
subst;simpl inst_term.
constructor 1 with rge t0;trivial.
generalize rge H3;clear W rge t0 H1 H3.
induction a;intros rge W;inversion W;subst;simpl inst_args.
left.
right.
apply WF_term_inst;trivial.
apply IHa;trivial.
rewrite Lget_app in H0.
caseq (nat_eq i (length rc));intro ei;rewrite ei in H0.
apply WF_ground_term_term.
replace dd with dom;[auto|congruence].
constructor 2;trivial.
constructor 3;trivial.
Qed.
Lemma WF_args_inst : forall V t dom,
WF_ground_term V t dom ->
forall rels a doms,
WF_args V (rels ++ dom :: nil) a doms ->
WF_args V rels (inst_args t (length rels) a) doms.
intros hyps t dd Wgt rc;induction a;intros rge W;inversion W;subst;
simpl inst_args.
left.
right.
apply WF_term_inst with dd;trivial.
apply IHa;trivial.
Qed.
Lemma term_inst : forall V F Venv t dom x,
Instanceof Denv V F Venv ->
WF_ground_term V t dom ->
interp_term Venv nil t dom = Some x ->
forall rels tt dd,
WF_term V
(List.map (E_domain Denv) (rels ++ (mkE Denv dom x) :: nil)) tt dd ->
interp_term Venv (rels ++ (mkE Denv dom x) :: nil) tt dd =
interp_term Venv rels (inst_term t (length rels) tt) dd.
intros hyps F Venv t dom x Inst Wgt et rc;fix 1.
intros [ f a | i | n] expected W;inversion W;subst;simpl.
rewrite H1;rewrite pos_eq_dec_refl.
replace (interp_args Venv (rc ++ mkE Denv dom x :: nil) a rge
(interp_domain Denv expected) t0)
with (interp_args Venv rc (inst_args t (length rc) a) rge
(interp_domain Denv expected) t0);trivial.
generalize rge (interp_domain Denv expected) t0 H3;clear rge t0 H1 H3 W.
induction a;intros rge P head W;inversion W;subst;simpl;trivial.
rewrite term_inst;trivial.
case (interp_term Venv rc (inst_term t (length rc) t0) dom0);trivial.
intro i;apply IHa;trivial.
rewrite Lget_app.
generalize H0;clear H0.
rewrite map_app;simpl.
rewrite Lget_app.
rewrite length_map.
caseq (nat_eq i (length rc)).
intros ei edom; injection edom;clear edom;intro edom.
pattern expected;rewrite <- edom.
rewrite pos_eq_dec_refl;
rewrite (ground_term_invar hyps Venv);trivial.
rewrite et;reflexivity.
reflexivity.
reflexivity.
Qed.
Lemma args_inst : forall V F Venv t dom x,
Instanceof Denv V F Venv ->
WF_ground_term V t dom ->
interp_term Venv nil t dom = Some x ->
forall rels a doms T P,
WF_args V
(List.map (E_domain Denv) (rels ++ (mkE Denv dom x) :: nil)) a doms ->
interp_args Venv (rels ++ (mkE Denv dom x) :: nil) a doms T P =
interp_args Venv rels (inst_args t (length rels) a) doms T P.
intros hyps F Venv t dom x Inst Wgt et rc; induction a; intros rge T P W;
inversion W;subst;simpl;trivial.
replace (interp_term Venv (rc ++ (mkE Denv dom x) :: nil) t0 dom0)
with (interp_term Venv rc (inst_term t (length rc) t0) dom0).
case (interp_term Venv rc (inst_term t (length rc) t0) dom0);trivial.
intro i;apply IHa;trivial.
symmetry;apply term_inst with hyps F;trivial.
Qed.
Lemma Weak_WF_term : forall vars dom rels t expected,
Full vars ->
WF_term vars rels t expected ->
WF_term (vars\dom) rels t expected.
fix 4.
intros hyps H rc [f a|n|i] expected F; intro W;inversion W;subst.
constructor 1 with rge t;auto.
generalize rge H4; clear rge H2 H4 t W.
induction a;intros rge W;inversion W.
left.
right.
apply Weak_WF_term;assumption.
apply IHa;assumption.
constructor 2;assumption.
constructor 3.
apply Full_push_compat;assumption.
Qed.
Lemma Weak_WF_args :forall vars dom rels a doms,
Full vars ->
WF_args vars rels a doms ->
WF_args (vars\dom) rels a doms.
induction a;intros rge F W;inversion W;subst.
left.
right.
apply Weak_WF_term;auto.
apply IHa;auto.
Qed.
Lemma Weak_interp_term: forall V F Venv var t rels expected,
Instanceof Denv V F Venv ->
WF_term V (List.map (E_domain Denv) rels) t expected ->
interp_term Venv rels t expected=
interp_term (Venv\var) rels t expected.
fix 5;
intros hyps F Venv var [f a | n | i] rc expected Inst W;inversion_clear W;simpl.
rewrite H.
rewrite pos_eq_dec_refl.
generalize rge t H0.
clear H t H0 rge.
induction a;simpl interp_args.
intros rge head Wa;inversion Wa.
reflexivity.
intros rge head Wa;inversion Wa.
subst.
simpl.
rewrite <- (Weak_interp_term hyps F Venv);auto.
case (interp_term Venv rc t dom);auto.
reflexivity.
assert (FF:=Instanceof_Full _ _ _ _ Inst).
elim (get_Instanceof _ _ _ _ _ Inst _ H);trivial.
rewrite get_push_Full;trivial.
caseq (i ?= index Venv).
intro e;rewrite (Pcompare_Eq_eq _ _ e) in H.
rewrite <- (index_Instanceof _ hyps F Venv) in H;trivial.
rewrite get_Full_Eq in H;trivial;try congruence.
reflexivity.
intro e;rewrite <- (index_Instanceof _ hyps F Venv) in e;trivial.
rewrite get_Full_Gt in H;trivial;congruence.
Qed.
Lemma Weak_interp_args: forall V F Venv var S rels a doms Kont,
Instanceof Denv V F Venv ->
WF_args V (List.map (E_domain Denv) rels) a doms ->
interp_args Venv rels a doms S Kont=
interp_args (Venv\var) rels a doms S Kont.
induction a;intro rge;case rge;simpl;try reflexivity.
intros dom domv Kont Inst Wa.
inversion Wa.
rewrite <- (Weak_interp_term _ F Venv);try assumption.
case (interp_term Venv rels t dom).
intro arg0;apply IHa;assumption.
reflexivity.
Qed.
Lemma Bind_WF_term: forall vars delta rels t expected,
WF_term vars rels t expected ->
WF_term vars (rels ++ delta) t expected.
fix 4;intros hyps delta rc [f a| i|n] dom W;inversion W;subst;try constructor.
constructor 1 with rge t;trivial.
generalize rge H3; clear rge t H1 H3 W.
induction a;intros rge W;inversion W;subst;constructor.
apply Bind_WF_term;trivial.
apply IHa;trivial.
apply Lget_app_Some;trivial.
trivial.
Qed.
Lemma Bind_WF_args : forall vars delta rels a doms,
WF_args vars rels a doms ->
WF_args vars (rels ++ delta) a doms.
induction a;intros rge W;inversion W;subst;try constructor.
apply Bind_WF_term;trivial.
apply IHa;trivial.
Qed.
Lemma Bind_interp_term: forall V F Venv delta rels t expected,
Instanceof Denv V F Venv ->
WF_term V (List.map (E_domain Denv) rels) t expected ->
interp_term Venv rels t expected =
interp_term Venv (rels++delta) t expected.
intros hyps F Venv delta rc; fix 1;
intros [ f a | i | n ] expected Inst W;inversion W; subst;simpl.
rewrite H1;rewrite pos_eq_dec_refl.
replace
(interp_args Venv rc a rge (interp_domain Denv expected) t)
with
(interp_args Venv (rc ++ delta) a rge
(interp_domain Denv expected) t);trivial.
generalize rge (interp_domain Denv expected) t H3;clear rge t H1 H3 W.
induction a;intros rge P head W;inversion W;subst;simpl;trivial.
rewrite Bind_interp_term;trivial.
case (interp_term Venv (rc ++ delta) t dom);trivial.
intro i;apply IHa;trivial.
caseq (Lget i rc);trivial.
intros o ei;rewrite (Lget_app_Some _ _ delta _ _ ei);trivial.
intro ei;assert (HH:=Lget_map _ _ (E_domain Denv) i rc).
rewrite H0 in HH;rewrite ei in HH;congruence.
reflexivity.
Qed.
Lemma Bind_interp_args: forall V F Venv delta S rels a doms Kont,
Instanceof Denv V F Venv ->
WF_args V (List.map (E_domain Denv) rels) a doms ->
interp_args Venv rels a doms S Kont=
interp_args Venv (rels++delta) a doms S Kont.
induction a;intros rge Kont Inst W;inversion W;subst;simpl;trivial.
rewrite (Bind_interp_term _ F Venv delta);trivial.
case (interp_term Venv (rels ++ delta) t dom);trivial.
intro i;apply IHa;trivial.
Qed.
Definition type_of (hyps:var_ctx) (t:term) :
option domain :=
match t with
App f _ =>
match get f Sigma with
PSome (mkF _ dom _ ) => Some dom
| PNone => None
end
| DB i => None
| Var n =>
match get n hyps with
PSome dom => Some dom
| _ => None
end
end.
Lemma type_of_regular : forall hyps dom t,
WF_ground_term hyps t dom ->
type_of hyps t = Some dom.
intros hyps dom [f a | i | n] W;inversion_clear W;simpl;rewrite H;split.
Qed.
Lemma WF_rewrite_term : forall vars dom t1 t2 rels,
WF_ground_term vars t1 dom ->
WF_ground_term vars t2 dom ->
forall t occ rt expected,
rewrite_term t1 t2 occ t = Some rt ->
WF_term vars rels t expected ->
WF_term vars rels rt expected.
intros hyps dom t1 t2 rc Wt1 Wt2.
fix 1;intros [ f a | i | n ] [ | | occa] rt expected;clean;simpl;intros e W.
change ((if term_eq (App f a) t1 then Some t2 else None (A:=term)) =
Some rt) in e.
inversion_clear W;generalize e;clear e.
caseq (term_eq (App f a) t1);clean.
intros ee e;injection e;clear e;intro e;rewrite <- e.
apply WF_ground_term_term.
assert (e' := type_of_regular _ _ _ Wt1).
rewrite <- (term_eq_id _ _ ee) in e'.
simpl in e';rewrite H in e'.
inversion e';trivial.
inversion_clear W;generalize e;clear e.
caseq (rewrite_args t1 t2 occa a);clean.
intros rargs erargs e; injection e;clear e;intro e;rewrite <- e.
constructor 1 with rge t;trivial.
generalize occa rargs rge erargs H0;
clear occa rge t H H0 rargs erargs e;induction a;
intros [ | occa |occt occa] rargs rge;simpl;clean;intros e W.
inversion_clear W;generalize e;clear e.
caseq (rewrite_args t1 t2 occa a);clean.
intros ra ea e;injection e;clear e;intro e;subst.
right;auto.
apply IHa with occa;trivial.
inversion_clear W;generalize e;clear e.
caseq (rewrite_term t1 t2 occt t);clean.
intros rt0 et0.
caseq (rewrite_args t1 t2 occa a);clean.
intros ra ea e;injection e;clear e;intro e;subst.
right.
apply WF_rewrite_term with t occt;trivial.
apply IHa with occa;trivial.
clear WF_rewrite_term.
destruct t1;clean;inversion Wt1.
caseq t1.
intros p a et1;rewrite et1 in e;clean.
intros i et1;rewrite et1 in e;clean.
intros p et1;rewrite et1 in e.
caseq (pos_eq n p);
intros ee;rewrite ee in e;clean; rewrite <- (pos_eq_refl _ _ ee) in et1.
assert (e' := type_of_regular _ _ _ Wt1).
rewrite et1 in e'.
inversion_clear W.
simpl in e';rewrite H in e'.
apply WF_ground_term_term.
congruence.
Qed.
Lemma WF_rewrite_args : forall vars dom t1 t2 rels,
WF_ground_term vars t1 dom ->
WF_ground_term vars t2 dom ->
forall a occ ra doms,
rewrite_args t1 t2 occ a = Some ra ->
WF_args vars rels a doms ->
WF_args vars rels ra doms.
intros hyps dom t1 t2 rc Wt1 Wt2 a.
induction a;intros [ | occa |occt occa] rargs rge;simpl;clean;intros e W.
inversion_clear W;generalize e;clear e.
caseq (rewrite_args t1 t2 occa a);clean.
intros ra ea e;injection e;clear e;intro e;subst.
right;auto.
apply IHa with occa;auto.
inversion_clear W;generalize e;clear e.
caseq (rewrite_term t1 t2 occt t);clean.
intros rt et.
caseq (rewrite_args t1 t2 occa a);clean.
intros ra ea e;injection e;clear e;intro e;subst.
right.
apply WF_rewrite_term with dom t1 t2 t occt;auto.
apply IHa with occa;auto.
Qed.
Lemma term_rewrite : forall V F Venv,
Instanceof Denv V F Venv->
forall dom t1 t2 it1 it2,
WF_ground_term V t1 dom ->
WF_ground_term V t2 dom ->
interp_term Venv nil t1 dom = Some it1 ->
interp_term Venv nil t2 dom = Some it2 ->
it1 = it2 ->
forall rels t occ rt expected,
rewrite_term t1 t2 occ t = Some rt ->
WF_term V (List.map (E_domain Denv) rels) t expected ->
interp_term Venv rels t expected =
interp_term Venv rels rt expected.
intros ctx F Venv Inst dom t1 t2 it1 it2 Wt1 Wt2 et1 et2 eit rels
;fix 1;intros [f a | i | n ] [ | | occa] rt expected; clean.
intro e;simpl rewrite_term in e;congruence.
intro e;change ((if term_eq (App f a) t1 then Some t2 else None) = Some rt) in e.
caseq (term_eq (App f a) t1);intro e';rewrite e' in e;clean.
assert (ee:=(term_eq_id _ _ e'));clear e'.
injection e;clear e;intro e.
intro W;inversion_clear W.
generalize (type_of_regular _ _ _ Wt1).
rewrite <- ee;simpl type_of.
rewrite H.
intro eee;injection eee;clear eee;intro eee.
rewrite ee.
rewrite <- e.
rewrite eee.
rewrite (ground_term_invar _ Venv rels t1 dom Wt1).
rewrite (ground_term_invar _ Venv rels t2 dom Wt2).
congruence.
simpl.
caseq (rewrite_args t1 t2 occa a);clean.
intros ra ea e W;inversion e;inversion W;simpl.
rewrite H2;rewrite pos_eq_dec_refl.
replace
(interp_args Venv rels ra rge (interp_domain Denv expected) t)
with
(interp_args Venv rels a rge (interp_domain Denv expected) t).
reflexivity.
subst.
generalize occa ra rge (interp_domain Denv expected) t ea H4.
clear occa expected ra ea W rge t H2 H4 e.
induction a;intros [ |occq| occa occq ] rargs rge T K;clean;
try solve [intro e;inversion e;split;trivial].
simpl.
caseq (rewrite_args t1 t2 occq a);clean.
intros rq eq e W;inversion e;inversion W;subst.
simpl.
case (interp_term Venv rels t dom0);trivial.
intro i;apply IHa with occq;trivial.
simpl.
caseq (rewrite_term t1 t2 occa t);clean.
intros rt et.
caseq (rewrite_args t1 t2 occq a);clean.
intros rq eq e W;inversion e;inversion W;subst.
simpl.
replace
(interp_term Venv rels rt dom0)
with
(interp_term Venv rels t dom0).
case (interp_term Venv rels t dom0);trivial.
intro i;apply IHa with occq;trivial.
apply term_rewrite with occa;trivial.
simpl rewrite_term;congruence.
intro e;change ((if term_eq (DB i) t1 then Some t2 else None) = Some rt) in e.
generalize e;clear e.
caseq ( term_eq (DB i) t1);clean.
intro e;rewrite <- (term_eq_id _ _ e) in et1;inversion et1.
simpl rewrite_term;congruence.
intro e;change ((if term_eq (Var n) t1 then Some t2 else None) = Some rt) in e.
generalize e;clear e.
caseq (term_eq (Var n) t1);clean.
intro e';assert (e:= term_eq_id _ _ e').
rewrite e.
clear e';intro e';injection e';clear e';intro e'.
rewrite <- e'.
intro W; rewrite <- e in W;inversion_clear W.
generalize (type_of_regular _ _ _ Wt1).
rewrite <- e;simpl type_of;rewrite H.
intro eee;injection eee;clear eee;intro eee.
rewrite e.
rewrite eee.
rewrite (ground_term_invar _ Venv rels t1 dom Wt1).
rewrite (ground_term_invar _ Venv rels t2 dom Wt2).
congruence.
Qed.
Lemma args_rewrite :
forall V F Venv,
Instanceof Denv V F Venv->
forall dom t1 t2 it1 it2,
WF_ground_term V t1 dom ->
WF_ground_term V t2 dom ->
interp_term Venv nil t1 dom = Some it1 ->
interp_term Venv nil t2 dom = Some it2 ->
it1 = it2 ->
forall rels a occ ra doms T K,
rewrite_args t1 t2 occ a = Some ra ->
WF_args V (List.map (E_domain Denv) rels) a doms ->
interp_args Venv rels a doms T K =
interp_args Venv rels ra doms T K.
induction a;intros [ |occq| occa occq ] rargs rge T K;clean;
try solve [intro e;inversion e;split;trivial].
simpl.
caseq (rewrite_args t1 t2 occq a);clean.
intros rq eq e W;inversion e;inversion W.
generalize H3;clear H3;subst;intro H3.
simpl.
case (interp_term Venv rels t dom0);trivial.
intro i.
apply IHa with occq;trivial.
simpl.
caseq (rewrite_term t1 t2 occa t);clean.
intros rt et.
caseq (rewrite_args t1 t2 occq a);clean.
intros rq eq e W;inversion e;inversion W.
generalize H3;clear H3;subst;intro H3.
simpl.
replace
(interp_term Venv rels rt dom0)
with
(interp_term Venv rels t dom0).
case (interp_term Venv rels t dom0);trivial.
intro i.
apply IHa with occq;trivial.
apply term_rewrite with V F dom t1 t2 it2 it2 occa;trivial.
Qed.