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
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Wf.
Require Import Crypto.Reflection.SmartMap.
Require Import Crypto.Reflection.ExprInversion.
Require Import Crypto.Reflection.MapCast.
Require Import Crypto.Reflection.Relations.
Require Import Crypto.Reflection.WfProofs.
Require Import Crypto.Reflection.WfInversion.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Tactics.RewriteHyp.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.
Section language.
Context {base_type_code : Type}
{interp_base_type1 : base_type_code -> Type}
{interp_base_type2 : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(interp_op1 : forall src dst, op src dst -> interp_flat_type interp_base_type1 src -> interp_flat_type interp_base_type1 dst)
(interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst)
(failv : forall {var t}, @exprf base_type_code op var (Tbase t)).
Context (transfer_op : forall ovar src1 dst1 src2 dst2
(opc1 : op src1 dst1)
(opc2 : op src2 dst2)
(args1' : @exprf base_type_code op ovar src1)
(args2 : interp_flat_type interp_base_type2 src2),
@exprf base_type_code op ovar dst1).
Context (R' : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop).
Local Notation R x y := (interp_flat_type_rel_pointwise R' x y).
Section gen_Prop.
Context (P : Type) (and : P -> P -> P) (True : P).
Context (bound_is_good : forall t, interp_base_type2 t -> P).
Local Notation bounds_are_good
:= (@interp_flat_type_rel_pointwise1_gen_Prop _ _ P and True bound_is_good _).
Fixpoint bounds_are_recursively_good_gen_Prop {t} (e : exprf base_type_code op t) : P
:= match e with
| LetIn tx ex tC eC
=> and (@bounds_are_recursively_good_gen_Prop tx ex)
(@bounds_are_recursively_good_gen_Prop tC (eC (interpf interp_op2 ex)))
| Op t1 tR opc args as e'
=> and (@bounds_are_recursively_good_gen_Prop _ args)
(bounds_are_good (interpf interp_op2 e'))
| TT => True
| Var t v => bound_is_good _ v
| Pair tx ex ty ey
=> and (@bounds_are_recursively_good_gen_Prop _ ex)
(@bounds_are_recursively_good_gen_Prop _ ey)
end.
End gen_Prop.
Definition bounds_are_recursively_goodb
:= bounds_are_recursively_good_gen_Prop bool andb true.
Global Arguments bounds_are_recursively_goodb _ {_} !_ / .
Definition bounds_are_recursively_good
:= @bounds_are_recursively_good_gen_Prop Prop and True.
Global Arguments bounds_are_recursively_good _ {_} !_ / .
Lemma bounds_are_recursively_good_iff_bool
R t x
: is_true (@bounds_are_recursively_goodb R t x)
<-> @bounds_are_recursively_good (fun t x => is_true (R t x)) t x.
Proof.
unfold is_true.
clear; induction x; simpl in *; rewrite ?Bool.andb_true_iff;
try setoid_rewrite interp_flat_type_rel_pointwise1_gen_Prop_iff_bool;
rewrite_hyp ?*; intuition congruence.
Qed.
Definition bounds_are_recursively_good_gen_Prop_iff_bool
: forall R t x,
is_true (@bounds_are_recursively_good_gen_Prop bool _ _ R t x)
<-> @bounds_are_recursively_good_gen_Prop Prop _ _ (fun t x => is_true (R t x)) t x
:= bounds_are_recursively_good_iff_bool.
Context (bound_is_good : forall t, interp_base_type2 t -> Prop).
Local Notation bounds_are_good
:= (@interp_flat_type_rel_pointwise1 _ _ bound_is_good).
Lemma bounds_are_good_when_recursively_good {t} e
: @bounds_are_recursively_good bound_is_good t e -> bounds_are_good (interpf interp_op2 e).
Proof.
induction e; simpl; unfold LetIn.Let_In; intuition auto.
Qed.
Local Hint Resolve bounds_are_good_when_recursively_good.
Local Notation G_invariant_holds G
:= (forall t x x',
List.In (existT _ t (x, x')%core) G -> R' t x x')
(only parsing).
Context (interpf_transfer_op
: forall G t tR opc ein eout ebounds,
wff G ein ebounds
-> G_invariant_holds G
-> interpf interp_op1 ein = interpf interp_op1 eout
-> bounds_are_recursively_good bound_is_good ebounds
-> bounds_are_good (interp_op2 t tR opc (interpf interp_op2 ebounds))
-> interpf interp_op1 (transfer_op interp_base_type1 t tR t tR opc opc eout (interpf interp_op2 ebounds))
= interpf interp_op1 (Op opc ein)).
Context (R_transfer_op
: forall G t tR opc ein eout ebounds,
wff G ein ebounds
-> G_invariant_holds G
-> interpf interp_op1 ein = interpf interp_op1 eout
-> bounds_are_recursively_good bound_is_good ebounds
-> bounds_are_good (interp_op2 t tR opc (interpf interp_op2 ebounds))
-> R (interpf interp_op1 (transfer_op interp_base_type1 t tR t tR opc opc eout (interpf interp_op2 ebounds)))
(interpf interp_op2 (Op opc ebounds))).
Local Notation mapf_interp_cast
:= (@mapf_interp_cast
base_type_code base_type_code interp_base_type2
op op interp_op2 failv
transfer_op).
Local Notation map_interp_cast
:= (@map_interp_cast
base_type_code base_type_code interp_base_type2
op op interp_op2 failv
transfer_op).
Local Notation MapInterpCast
:= (@MapInterpCast
base_type_code interp_base_type2
op interp_op2 failv
transfer_op).
(* Local *) Hint Resolve <- List.in_app_iff.
Local Hint Resolve (fun t T => @interp_flat_type_rel_pointwise_flatten_binding_list _ _ _ t T R').
Local Ltac break_t
:= first [ progress subst
| progress inversion_wf
| progress invert_expr_subst
| progress inversion_sigma
| progress inversion_prod
| progress destruct_head sig
| progress destruct_head sigT
| progress destruct_head ex
| progress destruct_head and
| progress destruct_head prod
| progress split_and
| progress break_match_hyps ].
Local Ltac fin_False :=
lazymatch goal with
| [ H : False |- _ ] => exfalso; assumption
end.
Local Ltac fin_t0 :=
solve [ constructor; eauto
| eauto
| auto
| hnf; auto ].
Local Ltac handle_list_t :=
match goal with
| _ => progress cbv [LetIn.Let_In duplicate_types] in *
| [ H : List.In _ (_ ++ _) |- _ ] => apply List.in_app_or in H
| [ H : List.In _ (List.map _ _) |- _ ]
=> rewrite List.in_map_iff in H
| _ => rewrite <- flatten_binding_list_flatten_binding_list2
| [ H : appcontext[flatten_binding_list2] |- _ ]
=> rewrite <- flatten_binding_list_flatten_binding_list2 in H
| [ H : context[flatten_binding_list (SmartVarfMap _ _) (SmartVarfMap _ _)] |- _ ]
=> rewrite flatten_binding_list_SmartVarfMap in H
| [ H : context[flatten_binding_list2 (SmartVarfMap _ _) (SmartVarfMap _ _)] |- _ ]
=> rewrite flatten_binding_list2_SmartVarfMap in H
| [ H : context[flatten_binding_list2 (SmartVarfMap _ _) _] |- _ ]
=> rewrite flatten_binding_list2_SmartVarfMap1 in H
| [ H : context[flatten_binding_list2 _ (SmartVarfMap _ _)] |- _ ]
=> rewrite flatten_binding_list2_SmartVarfMap2 in H
| _ => rewrite <- flatten_binding_list_flatten_binding_list2
| _ => rewrite List.in_map_iff
| [ H : context[List.In _ (_ ++ _)] |- _ ]
=> setoid_rewrite List.in_app_iff in H
end.
Local Ltac wff_t :=
match goal with
| [ |- wff _ _ _ ] => constructor
| [ H : _ |- wff _ (mapf_interp_cast _ _ _) (mapf_interp_cast _ _ _) ]
=> eapply H; eauto; []; clear H
| _ => solve [ eauto using wff_in_impl_Proper ]
end.
Local Ltac R_t :=
match goal with
| [ |- R' _ _ _ ] => eapply interp_flat_type_rel_pointwise_flatten_binding_list; eauto
| [ H : forall x y, _ -> R _ _ |- R _ _ ] => apply H; eauto; []
| [ H : forall x y, _ -> _ -> R _ _ |- R _ _ ] => apply H; eauto; []
end.
Local Ltac misc_t :=
match goal with
| _ => progress specialize_by eauto
| [ |- exists _, _ ]
=> eexists (existT _ _ _)
| [ |- _ /\ _ ] => split
| [ H : _ = _ |- _ ] => rewrite H
| [ H : ?x = _, H' : context[?x] |- _ ] => rewrite H in H'
| [ H : forall x y, _ -> _ -> _ = _ |- interpf _ _ = interpf _ _ ]
=> apply H
end.
Local Ltac t_step :=
first [ intro
| fin_False
| progress break_t
| fin_t0
| progress simpl in *
| wff_t
| handle_list_t
| progress destruct_head' or
| misc_t
| R_t ].
Lemma interpf_mapf_interp_cast_and_rel
G
{t1} e1 ebounds
(Hgood : bounds_are_recursively_good bound_is_good ebounds)
(HG : G_invariant_holds G)
(Hwf : wff G e1 ebounds)
: interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds)
= interpf interp_op1 e1
/\ R (interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds))
(interpf interp_op2 ebounds).
Proof. induction Hwf; repeat t_step. Qed.
Local Hint Resolve interpf_mapf_interp_cast_and_rel.
Lemma interpf_mapf_interp_cast
G
{t1} e1 ebounds
(Hgood : bounds_are_recursively_good bound_is_good ebounds)
(HG : G_invariant_holds G)
(Hwf : wff G e1 ebounds)
: interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds)
= interpf interp_op1 e1.
Proof. eapply interpf_mapf_interp_cast_and_rel; eassumption. Qed.
Lemma interp_map_interp_cast_and_rel
{t1} e1 ebounds
args2
(Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2))
(Hwf : wf e1 ebounds)
: forall x,
R x args2
-> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x
= interp interp_op1 e1 x
/\ R (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x)
(interp interp_op2 ebounds args2).
Proof. destruct Hwf; intros; eapply interpf_mapf_interp_cast_and_rel; eauto. Qed.
Lemma interp_map_interp_cast
{t1} e1 ebounds
args2
(Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2))
(Hwf : wf e1 ebounds)
: forall x,
R x args2
-> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x
= interp interp_op1 e1 x.
Proof. intros; eapply interp_map_interp_cast_and_rel; eassumption. Qed.
Lemma InterpMapInterpCastAndRel
{t} e
args
(Hwf : Wf e)
(Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args))
: forall x,
R x args
-> Interp interp_op1 (@MapInterpCast t e args) x
= Interp interp_op1 e x
/\ R (Interp interp_op1 (@MapInterpCast t e args) x)
(Interp interp_op2 e args).
Proof. apply interp_map_interp_cast_and_rel; auto. Qed.
Lemma InterpMapInterpCast
{t} e
args
(Hwf : Wf e)
(Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args))
: forall x,
R x args
-> Interp interp_op1 (@MapInterpCast t e args) x
= Interp interp_op1 e x.
Proof. apply interp_map_interp_cast; auto. Qed.
End language.
|
