forked from AbsInt/CompCert
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathReparameterizationproof.v
2269 lines (2119 loc) · 75.8 KB
/
Reparameterizationproof.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
(* Proof of correctness of the Reparameterization pass.
The proof here constructs a forward simulation between a source
program prog and output tprog. In contrast to other simulations,
the parameter values between the prog and tprog executions are
different: the parameter values in tprog are the results of
applying the *unconstrain* transformations to the prog versions.
Moreover, the simulation ensures that the final target value
returned by tprog as the additional Jacobian factor added to it.
This simulation proof is combined with
DenotationalSimulationChange.v to obtain semantic preservation.
Also see Transforms.v which proves many of the mathematical
properties of the constrain/unconstrain mappings that are needed
(e.g. derivatives, monotonicity, continuity of derivatives, etc.)
The proof is very long and is also split across Reparameterizationlemmas.v.
However, conceptually the forward simulation argument is pretty simple:
the simulation relation enforces two key properties:
(1) the expected mapping between parameter variables between the
two programs, and
(2) tprog contains a final Starget statement that adds the
appropriate Jacobian for every parameter (or this statement is on
the continuation stack)
Part of the size of the proof is that we have to prove that the
Stanlight expressions for each of the (a) parameter map/unmap
transforms, and (b) jacobian factors each actually compute the
intended mathematical statements.
*)
From Coq Require Import Reals Psatz ssreflect Utf8.
Require Import Smallstep.
Require Import Errors.
Require Import Linking.
Require Import Globalenvs.
Require Import Stanlight.
Require Import Ssemantics.
Require Import Reparameterization.
Require Import Reparameterizationlemmas.
Require Import DenotationalSimulationChange.
Require Import Coqlib.
Require Import Transforms.
Require Import IteratedRInt.
Require Import Memory.
Require Import ParamMap.
Require Import StanEnv.
Local Open Scope string_scope.
Require Import Clightdefs.
Import Clightdefs.ClightNotations.
Local Open Scope clight_scope.
Require Import RealsExt.
Import Continuity.
(* TODO: it seems to have been annoying to have defined this this way,
probably would have been better to make parameters be a parameter rather than existentially quantifying? *)
Inductive match_fundef (p: program) : fundef -> fundef -> Prop :=
| match_fundef_internal: forall f tf parameters pmap correction,
OK parameters = Errors.mmap (find_parameter p.(pr_defs)) p.(pr_parameters_vars) ->
pmap = u_to_c_rewrite_map parameters ->
correction = collect_corrections parameters ->
transf_function pmap correction f = OK tf ->
match_fundef p (Ctypes.Internal f) (Ctypes.Internal tf)
| match_fundef_external: forall ef args res cc,
match_fundef p (Ctypes.External ef args res cc) (Ctypes.External ef args res cc).
Definition match_varinfo (v: variable) (tv: variable) :=
vd_type v = vd_type tv /\ vd_constraint tv = Cidentity.
Definition match_prog (p: program) (tp: program) : Prop :=
exists parameters,
List.Forall (fun '(id, _, ofun) => ofun = None) p.(pr_parameters_vars) /\
OK parameters = Errors.mmap (find_parameter p.(pr_defs)) p.(pr_parameters_vars) /\
match_program_gen match_fundef match_varinfo p p tp /\
pr_parameters_vars tp = List.map (fun '(id, v, _) =>
(id, vd_type v,
Some (fun x => (unconstrained_to_constrained_fun (vd_constraint v) x))))
parameters /\
pr_data_vars tp = pr_data_vars p /\
Forall (λ '(id, _, _), ¬ In id math_idents) (pr_parameters_vars p) /\
NoDup (pr_parameters_ids p) /\
Forall (λ '(_, b, _), wf_type b) (pr_parameters_vars p).
Lemma transf_program_match:
forall p tp: program, transf_program p = OK tp -> match_prog p tp.
Proof.
unfold transf_program, match_prog; intros p tp Htransf.
eapply bind_inversion in Htransf as (?&Hcheck&Htransf).
eapply bind_inversion in Htransf as (?&Hcheck'&Htransf).
eapply bind_inversion in Htransf as (?&Hcheck_nodup&Htransf).
eapply bind_inversion in Htransf as (?&Hcheck_sizes&Htransf).
eapply bind_inversion in Htransf as (parameters&Heq&Htransf).
eapply bind_inversion in Htransf as (tp'&Heq'&HOK).
assert (program_of_program tp = tp') as ->.
{
unfold AST.transform_partial_program2 in Heq'.
eapply bind_inversion in Heq' as (tp_defs'&Heq''&H').
inversion H'. inversion HOK. subst. simpl. eauto.
}
eexists; split; eauto.
{ apply mmap_inversion in Hcheck.
clear -Hcheck. induction Hcheck => //=.
econstructor; eauto. destruct a1 as ((?&?)&[]); simpl in H; eauto; congruence. }
split; eauto.
split.
{
eapply match_transform_partial_program2; eauto.
- intros. destruct f; inversion H.
{ monadInv H. inv EQ; subst; eauto.
econstructor; eauto. }
{ monadInv H. econstructor. }
- intros. inversion H. subst. econstructor; eauto.
}
split.
{ inversion HOK; subst. simpl. eauto. }
apply mmap_inversion in Hcheck'.
split.
{ inv HOK => //=. }
split.
{
apply Forall_forall. intros ((?&?)&?) Hin.
eapply list_forall2_in_left in Hcheck' as (?&Hin'&Hcheck'); eauto.
eapply param_check_shadow_ok; eauto.
}
split.
{
rewrite /pr_parameters_ids.
exploit check_nodup_params_spec; eauto.
}
{ eapply mmap_inversion in Hcheck_sizes.
clear -Hcheck_sizes.
move: Hcheck_sizes.
generalize x2.
induction (pr_parameters_vars p) => ? Hcheck_sizes.
{ econstructor. }
{ inv Hcheck_sizes; econstructor; eauto.
{ move: H1. destruct a as ((?&[])&?) => //=.
do 3 destruct (Z_lt_ge_dec _ _) => //=.
}
}
}
Qed.
Section PRESERVATION.
Variable prog: Stanlight.program.
Variable tprog: Stanlight.program.
Variable TRANSL: match_prog prog tprog.
Variable prog_genv_has_mathlib :
genv_has_mathlib (globalenv prog).
(* This is really round about and ugly, maybe I should have just made "parameters" an index of
match_prog? But I don't know if that's compatible with the linker machinery *)
Definition found_parameters_aux :
{ x: list (AST.ident * variable * option (expr -> expr)) |
(Errors.mmap (find_parameter prog.(pr_defs)) prog.(pr_parameters_vars)) = OK x}.
Proof.
destruct (Errors.mmap (find_parameter prog.(pr_defs)) prog.(pr_parameters_vars)) as [l|] eqn:Heq.
{ exists l. eauto. }
{ abstract (exfalso; destruct TRANSL; intuition congruence). }
Qed.
Definition found_parameters := proj1_sig found_parameters_aux.
Lemma found_parameters_spec :
Errors.mmap (find_parameter prog.(pr_defs)) prog.(pr_parameters_vars) = OK found_parameters.
Proof. unfold found_parameters. destruct found_parameters_aux; eauto. Qed.
Definition found_constraints :=
map (fun '(id, var, f) => vd_constraint var) found_parameters.
Definition gs :=
map (constrain_fn) (flatten_parameter_constraints prog).
Definition log_dgs :=
map (log_deriv_constrain_fn) (flatten_parameter_constraints prog).
Definition param_map (rs : list R) :=
map (fun '(r, constraint) => constrain_fn constraint r) (combine rs (flatten_parameter_constraints prog)).
Definition param_unmap (rs : list R) :=
map (fun '(r, constraint) => unconstrain_fn constraint r) (combine rs (flatten_parameter_constraints prog)).
Lemma param_map_unmap :
∀ x, in_list_rectangle x (parameter_list_rect prog) ->
param_map (param_unmap x) = x.
Proof.
rewrite /in_list_rectangle/parameter_list_rect/param_map/param_unmap.
remember (flatten_parameter_constraints prog) as constraints eqn:Heq. clear Heq.
intros x Hin.
remember (map constraint_to_interval constraints) as intervals eqn:Heqn.
revert constraints Heqn.
induction Hin.
- rewrite //=.
- intros constraints Heqn. destruct constraints as [|c constraints]; first by (simpl in Heqn; congruence).
simpl in Heqn. inversion Heqn; subst.
rewrite /=. f_equal; eauto.
apply constrain_unconstrain; auto.
Qed.
Lemma find_parameter_ident_match {A} l i' b (e' : A) i v e :
find_parameter l (i', b, e') = OK (i, v, e) ->
i' = i /\ e' = e /\ b = vd_type v.
Proof.
induction l as [| (?&?) l] => //=.
- destruct g; eauto.
destruct (Pos.eq_dec _ _); subst; eauto.
destruct (valid_equiv_param_type _ _) eqn:Heq; inversion 1.
exploit valid_equiv_param_type_spec; eauto.
Qed.
Lemma find_parameter_lookup_def_ident_gen (a : AST.ident * basic * option (expr -> expr)) i v e :
find_parameter (pr_defs prog) a = OK (i, v, e) ->
match List.find (fun '(id', v) => positive_eq_dec i id' && is_gvar v) (pr_defs prog) with
| Some (_, AST.Gvar v') => (i, AST.gvar_info v') = (i, v)
| _ => False
end.
Proof.
induction (pr_defs prog) as [| x l].
- rewrite //=. destruct a as ((?&?)&?). inversion 1.
- rewrite //=. destruct a as ((?&?)&?).
destruct x as (id&def). destruct def.
* rewrite andb_false_r; eauto.
* destruct (Pos.eq_dec id i0).
** destruct (valid_equiv_param_type _ _); inversion 1; subst.
rewrite //=. destruct (Pos.eq_dec i i) => /=; by eauto.
** intros Hfind.
exploit (find_parameter_ident_match l i0 b o); eauto. intros (->&->&?). subst.
destruct (Pos.eq_dec i id).
{ congruence. }
rewrite //=. eapply IHl. eauto.
Qed.
Lemma find_parameter_lookup_def_ident_prog (a : AST.ident * basic * option (expr -> expr)) i v e :
find_parameter (pr_defs prog) a = OK (i, v, e) ->
lookup_def_ident prog i = (i, v).
Proof.
intros Hfind%find_parameter_lookup_def_ident_gen.
rewrite /lookup_def_ident. destruct (find (λ '(id', _), Pos.eq_dec i id' && _) (pr_defs _)) as [p|].
* destruct p as (?&[]); intuition.
* intuition.
Qed.
Lemma find_parameter_lookup_def_ident_tprog (a : AST.ident * basic * option (expr -> expr)) i b' e' v e :
In (i, b', e') (pr_parameters_vars prog) ->
find_parameter (pr_defs prog) a = OK (i, v, e) ->
lookup_def_ident tprog i = (i, mkvariable (v.(vd_type)) Cidentity).
Proof.
intros Hin Hfind. exploit find_parameter_lookup_def_ident_gen; eauto.
rewrite /lookup_def_ident.
intros Hlook.
destruct TRANSL as (x&Hnone&HOK&Hmatch&?).
destruct Hmatch as (Hforall2&?).
edestruct (@list_find_fst_forall2 _ (AST.globdef fundef variable)
((fun '(id', v) => Pos.eq_dec i id' && is_gvar v))) as [Hleft|Hright]; first eauto.
{ intros ?? (?&?); auto. }
{ intros (?&?) (?&?). simpl. intros Hmatch. inversion Hmatch as [Hfst Hglob].
simpl in Hfst, Hglob. inversion Hglob; subst => //=.
}
{ simpl. destruct Hleft as (id'&g1&g2&Heq1&Heq2&Hident).
rewrite Heq2. rewrite Heq1 in Hlook.
inversion Hident as [Hfst_eq Hglob]. simpl in Hglob.
inversion Hglob; auto.
* subst; intuition.
* subst. f_equal. inversion Hlook; subst.
clear -H1.
destruct H1. rewrite /=. destruct H as (H1&H2). rewrite H1. destruct i2. simpl in *. congruence.
}
destruct Hright as (Hnone1&Hnone2). rewrite Hnone1 in Hlook. intuition.
Qed.
Lemma map_repeat {A B} (f: A -> B) (a : A) (i : nat) :
map f (repeat a i) = repeat (f a) i.
Proof.
induction i => //=. congruence.
Qed.
Lemma pr_parameters_vars_found_parameters :
pr_parameters_vars prog = map (λ '(id, v, fe), (id, vd_type v, fe)) found_parameters.
Proof.
specialize (found_parameters_spec) => Hmmap.
remember (pr_parameters_vars prog) as prs eqn:Heqprs.
assert (∀ x, In x prs -> In x (pr_parameters_vars prog)) as Hsub.
{ subst. eauto. }
clear Heqprs.
revert Hmmap. generalize found_parameters.
induction prs.
- rewrite //=. intros fps. inversion 1 => //=.
- destruct a as ((?&?)&?). intros fps Hmmap.
simpl in Hmmap. monadInv Hmmap.
destruct x as ((?&?)&?).
simpl. f_equal; eauto; last first.
{ eapply IHprs; eauto. intros. apply Hsub. by right. }
exploit (@find_parameter_ident_match (option (expr -> expr))); eauto. intros (?&?&?); subst.
auto.
Qed.
Lemma flatten_parameter_variables_tprog:
flatten_parameter_variables tprog = map (λ '(id, vd, f),
(id, mkvariable (vd_type vd) Cidentity,
Some (fun x => (unconstrained_to_constrained_fun (vd_constraint vd) x))))
(flatten_parameter_variables prog).
Proof.
rewrite /flatten_parameter_variables/flatten_ident_variable_list.
rewrite concat_map.
f_equal.
rewrite ?map_map.
destruct TRANSL as (x&Hnone&Heqx&Hmatch&Heq&_).
rewrite Heq.
clear Heq.
revert x Heqx.
remember (pr_parameters_vars prog) as prs eqn:Heqprs.
assert (∀ x, In x prs -> In x (pr_parameters_vars prog)) as Hsub.
{ subst. eauto. }
clear Heqprs Hnone.
induction prs as [| a l].
- intros x Heq. inversion Heq. subst. rewrite //=.
- intros x Heqx.
destruct x as [| a' x'].
{ symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'. }
symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'; subst.
rewrite //=.
f_equal; last first.
{ eapply IHl; eauto. intros. intuition. }
destruct a as ((?&?)&?).
exploit (@find_parameter_ident_match (option (expr -> expr))); eauto. simpl. intros (?&?); subst.
exploit (find_parameter_lookup_def_ident_prog); eauto. intros ->.
exploit (find_parameter_lookup_def_ident_tprog); eauto.
{ eapply Hsub; eauto. left; eauto. }
intros ->. rewrite /=.
destruct (vd_type v) eqn:Hvdt; rewrite /=; rewrite ?Hvdt; eauto.
rewrite map_repeat //=.
Qed.
Lemma parameters_ids_preserved :
pr_parameters_ids tprog = pr_parameters_ids prog.
Proof.
unfold pr_parameters_ids.
destruct TRANSL as (x&Hnone&Heqx&Hmatch&Heq&_).
rewrite Heq.
clear Heq.
revert x Heqx.
remember (pr_parameters_vars prog) as prs eqn:Heqprs.
assert (∀ x, In x prs -> In x (pr_parameters_vars prog)) as Hsub.
{ subst. eauto. }
clear Heqprs Hnone.
induction prs as [| a l].
- intros x Heq. inversion Heq. subst. rewrite //=.
- intros x Heqx.
destruct x as [| a' x'].
{ symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'. }
symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'; subst.
rewrite //=.
f_equal; last first.
{ eapply IHl; eauto. intros. intuition. }
destruct a as ((?&?)&?).
exploit (@find_parameter_ident_match (option (expr -> expr))); eauto. simpl. intros (?&?); subst.
auto.
Qed.
Lemma flatten_parameter_constraints_tprog :
flatten_parameter_constraints tprog =
map (λ x, Cidentity) (flatten_parameter_constraints prog).
Proof.
rewrite /flatten_parameter_constraints. rewrite flatten_parameter_variables_tprog.
rewrite ?map_map.
eapply map_ext. intros ((?&?)&?) => //.
Qed.
Lemma flatten_parameter_list_tprog :
(flatten_parameter_list tprog.(pr_parameters_vars)) =
(flatten_parameter_list prog.(pr_parameters_vars)).
Proof.
rewrite /flatten_parameter_list. f_equal.
destruct TRANSL as (x&Hnone&Heqx&Hmatch&Heq&_).
rewrite Heq.
clear Heq.
revert x Heqx.
remember (pr_parameters_vars prog) as prs eqn:Heqprs.
assert (∀ x, In x prs -> In x (pr_parameters_vars prog)) as Hsub.
{ subst. eauto. }
clear Heqprs Hnone.
induction prs as [| a l].
- intros x Heq. inversion Heq. subst. rewrite //=.
- intros x Heqx.
destruct x as [| a' x'].
{ symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'. }
symmetry in Heqx. inversion Heqx.
apply bind_inversion in H0 as (((?&?)&?)&Hfind&Hbind).
apply bind_inversion in Hbind as (?&Hfind'&Hbind').
inversion Hbind'; subst.
rewrite //=.
f_equal; last first.
{ eapply IHl; eauto. intros. intuition. }
destruct a as ((?&?)&?).
exploit (@find_parameter_ident_match (option (expr -> expr))); eauto. simpl. intros (?&?&?); subst.
eauto.
Qed.
Lemma param_unmap_map :
∀ x, wf_rectangle_list (parameter_list_rect prog) ->
in_list_rectangle x (parameter_list_rect tprog) ->
param_unmap (param_map x) = x.
Proof.
rewrite /in_list_rectangle/parameter_list_rect/param_map/param_unmap.
rewrite flatten_parameter_constraints_tprog.
remember (flatten_parameter_constraints prog) as constraints eqn:Heq. clear Heq.
intros x Hwf Hin.
remember (map constraint_to_interval (map (λ _, Cidentity) constraints)) as intervals eqn:Heqn.
revert constraints Hwf Heqn.
induction Hin.
- rewrite //=.
- intros constraints Hwf Heqn. destruct constraints as [|c constraints]; first by (simpl in Heqn; congruence).
simpl in Heqn. inversion Heqn; subst.
rewrite /=. f_equal; eauto.
* apply unconstrain_constrain; auto.
inversion Hwf; eauto.
* eapply IHHin; eauto. inversion Hwf; eauto.
Qed.
Lemma dimen_preserved: parameter_dimension tprog = parameter_dimension prog.
Proof.
rewrite /parameter_dimension flatten_parameter_constraints_tprog ?map_length //.
Qed.
Lemma wf_paramter_rect_tprog :
wf_rectangle_list (parameter_list_rect prog) ->
wf_rectangle_list (parameter_list_rect tprog).
Proof.
clear 1.
rewrite /parameter_list_rect flatten_parameter_constraints_tprog.
induction (flatten_parameter_constraints prog).
- rewrite //=.
- simpl. econstructor; eauto. split; auto.
Qed.
Lemma param_unmap_in_dom :
∀ x, in_list_rectangle x (parameter_list_rect prog) ->
in_list_rectangle (param_unmap x) (parameter_list_rect tprog).
Proof.
rewrite /parameter_list_rect flatten_parameter_constraints_tprog.
rewrite /param_unmap.
induction (flatten_parameter_constraints prog).
- intros x. inversion 1. subst. econstructor.
- intros x. inversion 1; subst. simpl.
econstructor.
{ split; auto => //=. }
{ eapply IHl. eauto. }
Qed.
Lemma param_map_in_dom :
∀ x,
wf_rectangle_list (parameter_list_rect prog) ->
in_list_rectangle x (parameter_list_rect tprog) ->
in_list_rectangle (param_map x) (parameter_list_rect prog).
Proof.
rewrite /parameter_list_rect flatten_parameter_constraints_tprog.
rewrite /param_map.
induction (flatten_parameter_constraints prog).
- intros x Hwf. inversion 1. subst. econstructor.
- intros x Hwf. inversion 1; subst. simpl.
econstructor.
{ destruct a.
* rewrite /=; split => //=.
* rewrite /=; split => //=.
apply constrain_lb_spec_strict.
* rewrite /=; split => //=.
apply constrain_ub_spec_strict.
* simpl in Hwf. inversion Hwf.
rewrite /=; split => //=; apply constrain_lb_ub_spec_strict; auto.
}
eapply IHl; eauto.
inversion Hwf; eauto.
Qed.
(*
Lemma external_funct_preserved:
match_external_funct (globalenv prog) (globalenv tprog).
Lemma global_env_equiv :
Senv.equiv (globalenv prog) (globalenv tprog).
*)
Lemma Forall_repeat {A: Type} (a : A) (n: nat) (P : A -> Prop) :
P a -> Forall P (repeat a n).
Proof.
intros. induction n; econstructor; eauto.
Qed.
Lemma flatten_parameter_variables_out_none :
List.Forall (fun '(id, _, ofun) => ofun = None) (flatten_parameter_variables prog).
Proof.
rewrite /flatten_parameter_variables. rewrite /flatten_ident_variable_list.
destruct TRANSL as (?&Hnone&_).
induction (pr_parameters_vars).
{ rewrite //=. }
{ rewrite //=. apply Forall_app; split; last first.
{ eapply IHl. inversion Hnone; eauto. }
{ destruct a as ((?&?)&?) => /=.
inversion Hnone; subst.
destruct (lookup_def_ident prog i) as (?&?).
destruct (vd_type _); try (econstructor; eauto; done).
apply Forall_repeat; eauto.
}
}
Qed.
Lemma param_map_gs :
∀ x, in_list_rectangle x (parameter_list_rect tprog) ->
list_apply gs x = param_map x.
Proof.
rewrite /param_map/gs/list_apply//=.
intros x. clear 1. revert x.
induction (flatten_parameter_constraints prog) as [| c l]; intros x.
{ rewrite //=. destruct x => //=. }
{ destruct x => //=. f_equal; auto. }
Qed.
Definition target_map (d p : list Values.val) x := list_plus (list_apply log_dgs (map val2R p)) + x.
Definition target_unmap (d p : list Values.val) x := x - list_plus (list_apply log_dgs (map val2R p)).
Lemma target_map_unmap : ∀ d p x, target_map d p (target_unmap d p x) = x.
Proof. intros d p x. rewrite /target_map/target_unmap. field. Qed.
Lemma target_map_plus:
∀ data x v, in_list_rectangle x (parameter_list_rect tprog) ->
target_map data (map R2val x) v =
list_plus (list_apply log_dgs x) + v.
Proof.
rewrite /target_map. intros. f_equal. f_equal. f_equal.
rewrite map_map. etransitivity; last eapply map_id.
eapply map_ext. intros. rewrite //= IFR_IRF_inv //.
Qed.
Lemma target_map_dgs :
∀ data x, in_list_rectangle x (parameter_list_rect tprog) ->
target_map data (map R2val x) (log_density_of_program prog data (map R2val (param_map x))) =
list_plus (list_apply log_dgs x) + log_density_of_program prog data (map R2val (param_map x)).
Proof. intros. by apply target_map_plus. Qed.
Lemma gs_monotone :
wf_rectangle_list (parameter_list_rect prog) ->
Forall2 strict_monotone_on_interval (parameter_list_rect tprog) gs.
Proof.
rewrite /gs/parameter_list_rect.
intros Hwf.
rewrite flatten_parameter_constraints_tprog.
induction (flatten_parameter_constraints prog) as [| c l].
{ econstructor. }
{ simpl. econstructor; last first.
{ eapply IHl. inversion Hwf; eauto. }
rewrite /strict_monotone_on_interval. intros x y (_&Hlt&_).
destruct c.
- rewrite //=.
- apply constrain_lb_strict_increasing. auto.
- apply constrain_ub_strict_increasing. auto.
- apply constrain_lb_ub_strict_increasing; auto.
inversion Hwf. subst. eauto.
}
Qed.
Lemma gs_image :
wf_rectangle_list (parameter_list_rect prog) ->
Forall3 is_interval_image gs (parameter_list_rect tprog) (parameter_list_rect prog).
Proof.
rewrite /gs/parameter_list_rect.
intros Hwf.
rewrite flatten_parameter_constraints_tprog.
induction (flatten_parameter_constraints prog) as [| c l].
{ econstructor. }
{ simpl. econstructor; last first.
{ eapply IHl. inversion Hwf; eauto. }
rewrite /is_interval_image/=.
destruct c.
- split; auto.
split.
{ simpl. apply is_lim_right_lim; first congruence. apply is_lim_id. }
{ simpl. apply is_lim_left_lim; first congruence. apply is_lim_id. }
- split; auto.
{ simpl. intros. split; auto. apply constrain_lb_spec_strict. }
split.
{ apply constrain_lb_lim_right_correct; congruence. }
{ apply constrain_lb_lim_left_correct; congruence. }
- split; auto.
{ simpl. intros. split; auto. apply constrain_ub_spec_strict. }
split.
{ apply constrain_ub_lim_right_correct; congruence. }
{ apply constrain_ub_lim_left_correct; congruence. }
- split; auto.
{ simpl. intros; apply constrain_lb_ub_spec_strict; inversion Hwf; auto. }
split.
{ apply constrain_lb_ub_lim_right_correct; congruence. }
{ apply constrain_lb_ub_lim_left_correct; congruence. }
}
Qed.
Lemma gs_deriv :
wf_rectangle_list (parameter_list_rect prog) ->
Forall3 continuous_derive_on_interval (parameter_list_rect tprog) gs
(map (λ (f : R → R) (x : R), exp (f x)) log_dgs).
Proof.
rewrite /log_dgs/gs/parameter_list_rect.
intros Hwf.
rewrite flatten_parameter_constraints_tprog.
induction (flatten_parameter_constraints prog) as [| c l].
{ econstructor. }
{ simpl. econstructor; last first.
{ eapply IHl. inversion Hwf; eauto. }
rewrite /continuous_derive_on_interval. intros x (Hlt1&Hlt2).
destruct c.
- rewrite //=. split.
{ rewrite exp_0. apply: Derive.is_derive_id. }
{ apply continuous_const. }
- split.
{ rewrite /=. rewrite exp_ln; last apply deriv_constrain_lb_pos.
apply deriv_constrain_lb_correct. }
rewrite /=.
eapply continuous_ext.
{ intros ?. rewrite exp_ln; last apply deriv_constrain_lb_pos. reflexivity. }
{ eapply deriv_constrain_lb_continuous. }
- split.
{ rewrite /=. rewrite exp_ln; last apply deriv_constrain_ub_pos.
apply deriv_constrain_ub_correct. }
rewrite /=.
eapply continuous_ext.
{ intros ?. rewrite exp_ln; last apply deriv_constrain_ub_pos. reflexivity. }
{ eapply deriv_constrain_ub_continuous. }
- split.
{ rewrite /=. rewrite exp_ln; last apply deriv_constrain_lb_ub_pos.
apply deriv_constrain_lb_ub_correct. inversion Hwf; eauto. }
rewrite /=.
eapply continuous_ext.
{ intros ?. inversion Hwf. rewrite exp_ln; last apply deriv_constrain_lb_ub_pos; auto. }
{ eapply deriv_constrain_lb_ub_continuous. }
}
Qed.
Definition fpmap := u_to_c_rewrite_map found_parameters.
Definition fcorrection := collect_corrections found_parameters.
Inductive match_fundef' (p: program) : fundef -> fundef -> Prop :=
| match_fundef_internal': forall f tf ,
transf_function fpmap fcorrection f = OK tf ->
match_fundef' p (Ctypes.Internal f) (Ctypes.Internal tf)
| match_fundef_external': forall ef args res cc,
match_fundef' p (Ctypes.External ef args res cc) (Ctypes.External ef args res cc).
Definition match_prog' : Prop :=
match_program_gen match_fundef' match_varinfo prog prog tprog /\
pr_parameters_vars tprog = List.map (fun '(id, v, _) =>
(id, vd_type v,
Some (fun x => (unconstrained_to_constrained_fun (vd_constraint v) x))))
found_parameters /\
pr_data_vars tprog = pr_data_vars prog /\
Forall (λ '(id, _, _), ¬ In id math_idents) (pr_parameters_vars prog) /\
NoDup (pr_parameters_ids prog) /\
Forall (λ '(_, b, _), wf_type b) (pr_parameters_vars prog).
Lemma match_fundef_fundef' f tf :
match_fundef prog f tf ->
match_fundef' prog f tf.
Proof.
inversion 1.
- subst. assert (parameters = found_parameters) as ->.
{ specialize (found_parameters_spec) => Heq. congruence. }
econstructor; eauto.
- subst. econstructor; eauto.
Qed.
Lemma TRANSL' : match_prog'.
Proof.
destruct TRANSL as (params'&?&?&?&?&Hcheck).
subst. assert (params' = found_parameters) as ->.
{ specialize (found_parameters_spec) => Heq. congruence. }
split; last by eauto.
inversion H1.
split; eauto.
clear -H3. induction H3.
{ econstructor. }
{ econstructor; last by eauto.
inversion H; econstructor; eauto.
inversion H1; subst; econstructor; eauto.
inversion H5. subst.
eapply match_fundef_fundef'.
eauto.
}
Qed.
Lemma NoDup_pr_parameters_ids_prog : NoDup (pr_parameters_ids prog).
Proof.
specialize (TRANSL'). rewrite /match_prog'. intuition.
Qed.
Lemma wf_type_pr_parameters_ids_prog :
Forall (λ '(_, b, _), wf_type b) (pr_parameters_vars prog).
Proof.
specialize (TRANSL'). rewrite /match_prog'. intuition.
Qed.
Let ge := globalenv prog.
Let tge := globalenv tprog.
Lemma functions_translated:
forall v f,
Genv.find_funct ge v = Some f ->
∃ f', Genv.find_funct tge v = Some f' /\ transf_fundef fpmap fcorrection f = OK f'.
Proof.
intros. destruct TRANSL' as (Hmatch&Hrest&Hdata&Hcheck&Hnodup&Hsizes).
eapply (Genv.find_funct_match) in Hmatch as (?&tfun&Htfun); eauto.
intuition.
eexists; split; eauto.
inversion H2; eauto.
rewrite /=. subst. rewrite H1 => //=.
Qed.
Lemma function_ptr_translated:
forall v f,
Genv.find_funct_ptr ge v = Some f ->
∃ f', Genv.find_funct_ptr tge v = Some f' /\ transf_fundef fpmap fcorrection f = OK f'.
Proof.
intros. destruct TRANSL' as (Hmatch&Hrest&Hdata&Hcheck&Hnodup&Hsizes).
eapply (Genv.find_funct_ptr_match) in Hmatch as (?&tfun&Htfun); eauto.
intuition.
eexists; split; eauto.
inversion H2; eauto.
rewrite /=. subst. rewrite H1 => //=.
Qed.
Lemma ext_functions_preserved:
forall v ef tyargs tyret cconv,
Genv.find_funct ge v = Some (Ctypes.External ef tyargs tyret cconv) ->
Genv.find_funct tge v = Some (Ctypes.External ef tyargs tyret cconv).
Proof.
intros.
exploit (functions_translated); eauto. intros (f'&Hfind&Htrans).
inv Htrans. auto.
Qed.
Lemma symbols_preserved:
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof.
intros. destruct TRANSL'.
eapply Genv.find_symbol_match; intuition eauto.
Qed.
Lemma senv_preserved:
Senv.equiv ge tge.
Proof.
intros. destruct TRANSL'.
eapply Genv.senv_match; eauto.
Qed.
Lemma tprog_genv_has_mathlib :
genv_has_mathlib (globalenv tprog).
Proof.
move: prog_genv_has_mathlib.
destruct 1;
split; rewrite /genv_exp_spec/genv_log_spec/genv_expit_spec/genv_normal_lpdf_spec/genv_normal_lupdf_spec;
rewrite /genv_cauchy_lpdf_spec/genv_cauchy_lupdf_spec;
rewrite ?symbols_preserved.
intuition.
{ destruct GENV_EXP as (loc&?). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_EXPIT as (loc&?). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_LOG as (loc&?). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_NORMAL_LPDF as (loc&Hnor). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_NORMAL_LUPDF as (loc&Hnor). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_CAUCHY_LPDF as (loc&Hnor). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
{ destruct GENV_CAUCHY_LUPDF as (loc&Hnor). exists loc. split; first by intuition.
eapply ext_functions_preserved; intuition eauto. }
Qed.
Lemma eval_expr_fun_const pr v :
eval_expr_fun pr (Econst_float v Breal) = (Values.Vfloat v).
Proof.
apply eval_expr_fun_spec. econstructor.
Qed.
Lemma eval_constrained_fun r c env m pm t :
env_no_shadow_mathlib env ->
param_mem_no_shadow_mathlib pm ->
eval_expr (globalenv tprog) env m pm t
(unconstrained_to_constrained_fun c
(Econst_float (IRF r) Breal)) (Values.Vfloat (IRF (constrain_fn c r))).
Proof.
intros Hnoshadow1 Hnoshadow2.
destruct c.
{ econstructor. }
{ rewrite /unconstrained_to_constrained_fun.
edestruct (tprog_genv_has_mathlib) as [ (expl&?&?)].
simpl.
econstructor.
{ econstructor.
eapply eval_Eglvalue.
eapply eval_Evar_global; eauto.
{
inversion Hnoshadow2 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ rewrite /env_no_shadow_mathlib in Hnoshadow1.
inversion Hnoshadow1 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ eapply deref_loc_reference; eauto. }
{ repeat econstructor. }
{ eauto. }
2:{ eauto. }
rewrite /exp_ef_external; reflexivity.
eapply exp_ext_spec.
}
{ econstructor. }
simpl.
rewrite /Sop.sem_add//=.
rewrite /Sop.sem_binarith//=.
rewrite /constrain_lb.
rewrite -float_add_irf. repeat f_equal. rewrite IRF_IFR_inv //.
}
{
rewrite /unconstrained_to_constrained_fun.
edestruct (tprog_genv_has_mathlib) as [ (expl&?&?)].
simpl.
econstructor.
{ econstructor. }
{
assert ((Floats.Float.sub Floats.Float.zero (IRF r))
= (IRF (- r))) as Heq.
{ rewrite -(IRF_IFR_inv (Floats.Float.zero)).
rewrite float_sub_irf. f_equal. rewrite IFR_zero. nra.
}
econstructor.
eapply eval_Eglvalue.
eapply eval_Evar_global; eauto.
{
inversion Hnoshadow2 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ rewrite /env_no_shadow_mathlib in Hnoshadow1.
inversion Hnoshadow1 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ eapply deref_loc_reference; eauto. }
{ repeat econstructor. }
{ eauto. }
2:{ eauto. }
rewrite /exp_ef_external; reflexivity.
rewrite ?Heq; eapply exp_ext_spec.
}
simpl.
rewrite /Sop.sem_sub//=.
rewrite /Sop.sem_binarith//=.
replace f with (IRF (IFR f)) at 1 by (apply IRF_IFR_inv).
rewrite float_sub_irf. f_equal.
}
{
rewrite /unconstrained_to_constrained_fun.
edestruct (tprog_genv_has_mathlib) as [_ (expl&?&?)].
simpl.
econstructor.
{ econstructor. }
econstructor.
{ repeat econstructor. }
{
econstructor.
eapply eval_Eglvalue.
eapply eval_Evar_global; eauto.
{
inversion Hnoshadow2 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ rewrite /env_no_shadow_mathlib in Hnoshadow1.
inversion Hnoshadow1 as [|??? Hnoshadow'].
inversion Hnoshadow' as [|??? Hnoshadow''].
inversion Hnoshadow'' as [|??? Hnoshadow'''].
eauto.
}
{ eapply deref_loc_reference; eauto. }
{ repeat econstructor. }
{ eauto. }
2:{ eauto. }
rewrite /expit_ef_external; reflexivity.
eapply expit_ext_spec.
}
simpl.
rewrite //=.
rewrite /Sop.sem_binarith//=.
rewrite /Sop.sem_add//=.
rewrite /Sop.sem_binarith//=.
do 2 f_equal.
rewrite /constrain_lb_ub.
rewrite float_add_irf'; repeat f_equal.
rewrite float_mul_irf'.
rewrite float_sub_irf'.
rewrite ?IFR_IRF_inv.
f_equal.
}
Qed.
Lemma eval_constrained_fun' r c env m pm t :
in_interval r (constraint_to_interval c) ->
env_no_shadow_mathlib env ->
param_mem_no_shadow_mathlib pm ->
eval_expr (globalenv tprog) env m pm t
(unconstrained_to_constrained_fun c
(Econst_float (IRF (unconstrain_fn c r)) Breal)) (Values.Vfloat (IRF r)).
Proof.
intros.
assert (r = constrain_fn c (unconstrain_fn c r)) as Heq.
{ rewrite constrain_unconstrain //. }
rewrite {2}Heq.
eapply eval_constrained_fun; auto.
Qed.
Lemma eval_param_map_list_preserved :
∀ x,
in_list_rectangle x (parameter_list_rect tprog) ->
eval_param_map_list tprog x = eval_param_map_list prog (param_map x).
Proof.
rewrite /eval_param_map_list/parameter_list_rect.
intros x.
rewrite /flatten_parameter_out.
rewrite /param_map.
rewrite /flatten_parameter_constraints.
rewrite flatten_parameter_variables_tprog.
specialize (flatten_parameter_variables_out_none) => Hnone.
remember (flatten_parameter_variables prog) as pvars eqn:Heq. clear Heq.
revert pvars Hnone.
induction x => pvars Hnone Hin.
{ rewrite /eval_param_map_list /=//. }
destruct pvars => //=.
f_equal.
{ f_equal.
destruct p as ((?&?)&?). inversion Hnone; subst. rewrite eval_expr_fun_const /=.
apply eval_expr_fun_spec.
apply eval_constrained_fun.
{ repeat (econstructor; first by eauto using Maps.PTree.gempty). econstructor. }
{ repeat (econstructor; first by eauto using gempty). econstructor. }
}
eapply IHx; eauto.
{ inversion Hnone; eauto. }
{ inversion Hin; subst. eauto. }
Qed.
Variable data : list Values.val.
Variable params : list R.
Lemma typeof_fpmap :
∀ i fe efill, fpmap i = Some fe -> typeof efill = Breal -> typeof (fe efill) = Breal.
Proof.
rewrite /fpmap.
induction found_parameters as [| ((?&?)&?)] => //=.
intros i' fe efill.
destruct (Pos.eq_dec _ _).
{ rewrite /unconstrained_to_constrained.
inversion 1. subst. intros Hefill.
destruct (vd_constraint _) => //=.
}
intros. eauto.