source: src/joint/semanticsUtils.ma @ 2683

Last change on this file since 2683 was 2683, checked in by tranquil, 7 years ago

proof of properties of b_graph_program_transform (with an open axiom)

File size: 18.2 KB
Line 
1include "joint/joint_semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5include "joint/TranslateUtils.ma".
6include "common/ExtraMonads.ma".
7include "common/extraGlobalenvs.ma".
8
9record hw_register_env : Type[0] ≝
10  { reg_env : BitVectorTrie beval 6
11  ; other_bit : bebit
12  }.
13
14definition empty_hw_register_env: hw_register_env ≝
15  mk_hw_register_env (Stub …) BBundef.
16
17include alias "ASM/BitVectorTrie.ma".
18
19definition hwreg_retrieve: hw_register_env → Register → beval ≝
20 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
21
22definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
23 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
24  (other_bit env).
25
26definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
27λv,env.mk_hw_register_env (reg_env env) v.
28
29definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
30λenv.
31let spl ≝ hwreg_retrieve env RegisterSPL in
32let sph ≝ hwreg_retrieve env RegisterSPH in
33! ptr ← pointer_of_address 〈spl, sph〉 ;
34match ptype ptr return λx.ptype ptr = x → res xpointer with
35[ XData ⇒ λprf.return «ptr, prf»
36| _ ⇒ λ_.Error … [MSG BadPointer]
37] (refl …).
38
39definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
40λenv,sp.
41let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
42hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
43
44(*** Store/retrieve on pseudo-registers ***)
45include alias "common/Identifiers.ma".
46
47record reg_sp : Type[0] ≝
48{ reg_sp_env :> identifier_map RegisterTag beval
49; stackp : xpointer
50}.
51
52definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
53
54definition reg_retrieve : register_env beval → register → res beval ≝
55 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
56
57definition reg_sp_store ≝ λreg,v,locals.
58! locals' ← reg_store reg v (reg_sp_env locals) ;
59return mk_reg_sp locals' (stackp locals).
60
61definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
62
63(*** Store/retrieve on hardware registers ***)
64
65definition init_hw_register_env: xpointer → hw_register_env ≝
66 λsp.hwreg_store_sp empty_hw_register_env sp.
67
68(******************************** GRAPHS **************************************)
69
70record sem_graph_params : Type[1] ≝
71{ sgp_pars : unserialized_params
72; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
73}.
74
75definition sem_graph_params_to_graph_params :
76  ∀pars : sem_graph_params.graph_params ≝
77  λpars.mk_graph_params (sgp_pars pars).
78
79coercion graph_params_from_sem_graph_params nocomposites :
80  ∀pars : sem_graph_params.
81  graph_params ≝ sem_graph_params_to_graph_params
82  on _pars : sem_graph_params to graph_params.
83
84definition sem_graph_params_to_sem_params :
85  ∀pars : sem_graph_params.
86  sem_params ≝
87  λpars.
88  mk_sem_params
89    (pars : graph_params)
90    (sgp_sup pars ?)
91    (word_of_identifier ?)
92    (an_identifier ?)
93    ? (refl …).
94* #p % qed.
95
96coercion sem_params_from_sem_graph_params :
97  ∀pars : sem_graph_params.
98  sem_params ≝ sem_graph_params_to_sem_params
99  on _pars : sem_graph_params to sem_params.
100
101
102(******************************** LINEAR **************************************)
103
104lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
105@pos_elim [%]
106#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
107
108record sem_lin_params : Type[1] ≝
109{ slp_pars : unserialized_params
110; slp_sup : ∀F.sem_unserialized_params slp_pars F
111}.
112
113definition sem_lin_params_to_lin_params :
114  ∀pars : sem_lin_params.lin_params ≝
115  λpars.mk_lin_params (slp_pars pars).
116
117coercion lin_params_from_sem_lin_params nocomposites :
118  ∀pars : sem_lin_params.
119  lin_params ≝ sem_lin_params_to_lin_params
120  on _pars : sem_lin_params to lin_params.
121
122definition sem_lin_params_to_sem_params :
123  ∀pars : sem_lin_params.
124  sem_params ≝
125  λpars.
126  mk_sem_params
127    (pars : lin_params)
128    (slp_sup pars ?)
129    succ_pos_of_nat
130    (λp.pred (nat_of_pos p))
131    ??.
132[ #n >nat_succ_pos %
133| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
134] qed.
135
136coercion sem_params_from_sem_lin_params :
137  ∀pars : sem_lin_params.
138  sem_params ≝ sem_lin_params_to_sem_params
139  on _pars : sem_lin_params to sem_params.
140
141
142lemma fetch_statement_eq : ∀p:sem_params.∀g.
143  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
144  ∀i,fn,s.
145  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
146  let pt ≝ point_of_pc … ptr in
147  stmt_at … (joint_if_code … fn) pt = Some ? s →
148  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
149#p #g #ge #ptr #i #f #s #EQ1 #EQ2
150whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
151>EQ2 %
152qed.
153
154lemma fetch_statement_inv : ∀p:sem_params.∀g.
155  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
156  ∀i,fn,s.
157  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
158  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
159  let pt ≝ point_of_pc p ptr in
160  stmt_at … (joint_if_code … fn) pt = Some ? s.
161#p #g #ge #ptr #i #fn #s #H
162elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
163elim (bind_inversion ????? H) #s' * #H
164lapply (opt_eq_from_res ???? H) -H #EQ2
165whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
166qed.
167
168lemma symbols_match :
169    ∀M:matching.∀initV,initW.
170     (∀v,w. match_var_entry M v w →
171      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
172    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
173    ∀MATCH:match_program … M p p'.
174    symbols … (globalenv … initW p') = symbols … (globalenv … initV p).
175* #A #B #V #W #match_fn #match_var #initV #initW #H
176#p #p' * #Mvars #Mfn #Mmain
177whd in match globalenv in ⊢ (???%); normalize nodelta
178whd in match (globalenv_allocmem ????);
179change with (add_globals ?????) in match (foldl ?????);
180>(proj1 … (add_globals_match … initW … Mvars))
181[ % |*:]
182[ * #idr #v * #idr' #w #MVE %
183  [ inversion MVE
184    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
185  | @(H … MVE)
186  ]
187| @(matching_fns_get_same_blocks … Mfn)
188  #f #g @match_funct_entry_id
189]
190qed.
191
192lemma symbols_transf:
193 ∀A,B,V,init.∀prog_in : program A V.
194 ∀trans : ∀vars.A vars → B vars.
195 let prog_out ≝ transform_program … prog_in trans in
196 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
197#A #B #V #iV #p #tf whd
198@(symbols_match … (transform_program_match … tf ?))
199#v0 #w0 * //
200qed.
201
202definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
203λA,B,P,mA,mB.
204∀p.
205match lookup_opt … p mA with
206[ Some a ⇒
207  match lookup_opt … p mB with
208  [ Some b ⇒ P a b
209  | _ ⇒ False
210  ]
211| _ ⇒ match lookup_opt … p mB with
212  [ Some _ ⇒ False
213  | _ ⇒ True
214  ]
215].
216
217definition match_funct_map :
218  ∀M : matching.
219  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
220  λM,vars.pm_P … (match_fundef M ?).
221
222axiom functions_match:
223    ∀M:matching.∀initV,initW.
224    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
225    ∀MATCH:match_program … M p p'.
226    match_funct_map M ?
227      (functions ? (globalenv ?? initV p))
228      (functions ? (globalenv ?? initW p') ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
229@sym_eq @(matching_vars … (mp_vars … MATCH)) qed.
230
231lemma functions_transf:
232 ∀A,B,V,init.∀prog_in : program A V.
233 ∀trans : ∀vars.A vars → B vars.
234 let prog_out ≝ transform_program … prog_in trans in
235 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
236 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
237#A #B #V #iV #p #tf #n
238lapply(functions_match … (transform_program_match … tf p) n) try @iV
239cases (lookup_opt … n ?) [2: #f] normalize nodelta
240generalize in ⊢ (match (???match % with [ _ ⇒ ?]) with [ _ ⇒ ? | _ ⇒ ? ] → ?);
241#e >(K ?? e) normalize nodelta
242cases (lookup_opt ???) [2,4: #f'] normalize nodelta
243[2,3,4: * % ]
244#EQ destruct %
245qed.
246
247lemma symbol_for_block_transf :
248 ∀A,B,V,init.∀prog_in : program A V.
249 ∀trans : ∀vars.A vars → B vars.
250 let prog_out ≝ transform_program … prog_in trans in
251 ∀bl.
252 symbol_for_block … (globalenv … init prog_out) bl =
253 symbol_for_block … (globalenv … init prog_in) bl.
254#A #B #V #iV #p #tf whd
255#bl
256whd in match symbol_for_block; normalize nodelta
257>(symbols_match … (transform_program_match … tf ?))
258[ % |*:]
259#v #w * //
260qed.
261
262include alias "common/Pointers.ma".
263
264lemma fetch_function_transf :
265 ∀A,B,V,init.∀prog_in : program A V.
266 ∀trans : ∀vars.A vars → B vars.
267 let prog_out ≝ transform_program … prog_in trans in
268 ∀bl.
269 fetch_function … (globalenv … init prog_out) bl =
270 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
271 return 〈i, trans … f〉.
272#A #B #V #init #prog_in #trans #bl
273whd in match fetch_function; normalize nodelta
274>(symbol_for_block_transf A B V init prog_in trans)
275cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
276whd in match find_funct_ptr; normalize nodelta
277whd in match (block_region (pi1 ?? bl));
278cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
279>(functions_transf A B V init prog_in trans p)
280cases (lookup_opt ???) //
281qed.
282
283lemma fetch_internal_function_transf :
284 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
285 ∀trans : ∀vars.A vars → B vars.
286 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
287 ∀bl.
288 fetch_internal_function … (globalenv_noinit … prog_out) bl =
289 ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
290 return 〈i, trans … f〉.
291#A #B #prog #trans #bl
292 whd in match fetch_internal_function; normalize nodelta
293>(fetch_function_transf … prog)
294cases (fetch_function ???)
295[ * #id * #f % | #e % ]
296qed.
297
298include alias "utilities/binary/positive.ma".
299
300lemma pm_map_cases : ∀A.∀P : positive_map A → Prop.∀m : positive_map A.
301((∀p.lookup_opt … p m = None ?) → P m) →
302(∀p,v.lookup_opt … p m = Some ? v → P m) →
303P m.
304#A #P #m lapply P -P elim m -m
305[ #P #H1 #_ @H1 #p % ]
306* [2: #x ] #l #r #IHl #IHr #P #H1 #H2 [ @(H2 one x) % ]
307@IHl [2: #p #v #EQ @(H2 (p0 p) v EQ) ]
308#l_empty
309@IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ]
310#r_empty
311@H1 * normalize //
312qed.
313
314lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
315(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
316(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
317∀m.P m.
318#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
319[ #P #H1 #_ @H1 #p % ]
320#o #l #r #IHl #IHr #P #H1 #H2
321@IHl #l'
322[ #empty_l' @IHr #r'
323  [ #empty_r' cases o [ @H1 * try #p normalize // ]
324    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
325    @H2 [ @H1 * try #p normalize // | % ]
326  ]
327]
328#p #v #H #G
329[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
330| change with (P (insert ? (p0 p) v (pm_node ? ???)))
331] @H2 assumption
332qed.
333
334include alias "basics/logic.ma".
335include alias "common/PositiveMap.ma".
336
337lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
338#A #B #impl * #Bf % #At @Bf @impl @At qed-.
339
340lemma b_graph_transform_program_find_funct_ptr :
341 ∀src,dst:sem_graph_params.
342 ∀data : ∀globals.joint_closed_internal_function src globals →
343  bind_new register (b_graph_translate_data src dst globals).
344 ∀prog_in : joint_program src.
345 let prog_out ≝ b_graph_transform_program … data prog_in in
346 let src_genv ≝ globalenv_noinit ? prog_in in
347 let dst_genv ≝ globalenv_noinit ? prog_out in
348 ∃init_regs : block → list register.
349 ∃f_lbls : block → label → option (list label).
350 ∃f_regs : block → label → option (list register).
351 ∀bl,def_in.
352 find_funct_ptr … src_genv bl = return (Internal ? def_in) →
353 ∃init_data,def_out.
354 find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
355 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
356 b_graph_translate_props src dst ? init_data (init_regs bl)
357    def_in def_out (f_lbls bl) (f_regs bl).
358#src #dst #data #prog_in
359whd
360letin prog_out ≝ (b_graph_transform_program … data prog_in)
361letin src_genv ≝ (globalenv_noinit ? prog_in)
362letin dst_genv ≝ (globalenv_noinit ? prog_out)
363cut (∀p.lookup_opt ? p (functions ? dst_genv) =
364     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
365      (lookup_opt ? p (functions ? src_genv)))
366[ @functions_transf ]
367cases dst_genv #functs2 #nextf2 #symbols2 #H2
368cases src_genv #functs1 #nextf1 #symbols1 #H1
369lapply H2 lapply H1 lapply functs2
370@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
371[ #functs1_empty | #p #f #IH #p_not_in ]
372#functs2 #H1 #H2 #transf
373[ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)}
374  #bl #def_in #ABS @⊥ lapply ABS -ABS
375  whd in match find_funct_ptr;
376  normalize nodelta
377  whd in match (block_region bl);
378  cases (block_id bl) normalize nodelta
379  [2,3: #p [2: >functs1_empty ]]
380  normalize #ABS destruct
381]
382cases (IH (pm_set … p (None ?) functs2) ???)
383[2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
384  [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
385  #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
386|3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
387  [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
388  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
389|4: #b @(eqb_elim b p)
390  [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
391  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
392  >(lookup_opt_insert_miss ? f b p … NEQ) %
393]
394-IH cases f in H1 transf; -f #f #H1 #transf
395#init_regs * #f_lbls * #f_regs #props
396[ (* internal *)
397  letin upd ≝ (λA : Type[0].λf : block → A.
398    λid.λv,id'.
399    if eq_block id id' then v else f id')
400  cases (pi2 ?? (b_graph_translate … (data … f) f))
401  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
402  #inst_loc_data #loc_props
403  letin bl ≝ (mk_block (neg p))
404  %{(upd … init_regs bl loc_init_regs)}
405  %{(upd … f_lbls bl loc_f_lbls)}
406  %{(upd … f_regs bl loc_f_regs)}
407| (* external, nothing changes *)
408  %{init_regs}
409  %{f_lbls}
410  %{f_regs}
411]
412* #p' #def_in
413whd in match find_funct_ptr; normalize nodelta
414whd in match (block_region (mk_block p'));
415cases p' -p' [2,3,5,6: #p' ] normalize nodelta
416[1,3,5,6: #ABS normalize in ABS; destruct]
417@(eqb_elim p' p) #pp' destruct
418[1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
419  %{loc_data} %
420  [2: % [ % ]
421    [ >transf >lookup_opt_insert_hit %
422    |*: >eq_block_b_b assumption
423    ]
424  |]
425|*: >(lookup_opt_insert_miss ???? functs1 … pp')
426  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
427  #EQ lapply (props (mk_block (neg p')) def_in EQ)
428  whd in match find_funct_ptr; normalize nodelta
429  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
430]
431qed.
432
433lemma b_graph_transform_program_fetch_internal_function :
434 ∀src,dst:sem_graph_params.
435 ∀data : ∀globals.joint_closed_internal_function src globals →
436  bind_new register (b_graph_translate_data src dst globals).
437 ∀prog_in : joint_program src.
438 let prog_out ≝ b_graph_transform_program … data prog_in in
439 let src_genv ≝ globalenv_noinit ? prog_in in
440 let dst_genv ≝ globalenv_noinit ? prog_out in
441 let code_block ≝ (Σbl.block_region bl = Code) in
442 ∃init_regs : code_block → list register.
443 ∃f_lbls : code_block → label → option (list label).
444 ∃f_regs : code_block → label → option (list register).
445 ∀bl,id,def_in.
446 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
447 ∃init_data,def_out.
448 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
449 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
450 b_graph_translate_props src dst ? init_data (init_regs bl)
451    def_in def_out (f_lbls bl) (f_regs bl).
452#src #dst #data #prog_in
453cases (b_graph_transform_program_find_funct_ptr src dst data prog_in)
454#init_regs * #f_lbls * #f_regs #props
455%{(λb.init_regs b)}
456%{(λb.f_lbls b)}
457%{(λb.f_regs b)}
458#bl #id #def_in
459#H @('bind_inversion H) * #id' * #def_in' -H
460normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
461@('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
462#H @('bind_inversion H) -H #def_in' #H
463whd in ⊢ (??%%→?); #EQ destruct
464cases (props … H)
465#loc_data * #def_out ** #H1 #H2 #H3
466%{loc_data} %{def_out}
467%{H3} %{H2}
468whd in match fetch_internal_function;
469whd in match fetch_function; normalize nodelta
470>symbol_for_block_transf >EQ1 >m_return_bind
471>H1 %
472qed.
473
474lemma b_graph_transform_program_fetch_statement :
475 ∀src,dst:sem_graph_params.
476 ∀data : ∀globals.joint_closed_internal_function src globals →
477  bind_new register (b_graph_translate_data src dst globals).
478 ∀prog_in : joint_program src.
479 let prog_out ≝ b_graph_transform_program … data prog_in in
480 let src_genv ≝ globalenv_noinit ? prog_in in
481 let dst_genv ≝ globalenv_noinit ? prog_out in
482 let code_block ≝ (Σbl.block_region bl = Code) in
483 ∃init_regs : code_block → list register.
484 ∃f_lbls : code_block → label → option (list label).
485 ∃f_regs : code_block → label → option (list register).
486 ∀pc,id,def_in,s.
487 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
488 ∃init_data,def_out.
489 let bl ≝ pc_block pc in
490 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
491 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
492 b_graph_translate_props src dst ? init_data (init_regs bl)
493    def_in def_out (f_lbls bl) (f_regs bl) ∧
494 let l ≝ point_of_pc dst pc in
495 ∃lbls,regs.
496 f_lbls bl l = Some ? lbls ∧
497 f_regs bl l = Some ? regs ∧
498  match s with
499  [ sequential s' nxt ⇒
500    let block ≝
501      if eq_identifier … (joint_if_entry … def_in) l then
502        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
503      else
504        f_step … init_data l s' in
505    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
506  | final s' ⇒
507    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
508  | FCOND abs _ _ _ ⇒ Ⓧabs
509  ].
510#src #dst #data #prog_in
511cases (b_graph_transform_program_fetch_internal_function src dst data prog_in)
512#init_regs * #f_lbls * #f_regs #props
513%{init_regs}
514%{f_lbls}
515%{f_regs}
516#pc #id #def_in #s
517#H @('bind_inversion H) * #id' #def_in' -H
518#EQfif
519#H @('bind_inversion H) -H #s
520#H lapply (opt_eq_from_res ???? H) -H
521#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
522cases (props … EQfif)
523#a * #b #H %{a} %{b} %{H}
524cases H -H #_ #props'
525@(multi_fetch_ok … props' … EQstmt_at)
526qed.
Note: See TracBrowser for help on using the repository browser.