source: Deliverables/D3.1/C-semantics/CexecComplete.ma @ 498

Last change on this file since 498 was 498, checked in by campbell, 9 years ago

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File size: 16.5 KB
Line 
1include "Cexec.ma".
2
3definition yields ≝ λA.λa:res A.λv':A.
4match a with [ OK v ⇒ v' = v | _ ⇒ False ].
5
6(* This tells us that some execution of a results in v'.
7   (There may be many possible executions due to I/O, but we're trying to prove
8   that one particular one exists corresponding to a derivation in the inductive
9   semantics.) *)
10let rec yieldsIO (A:Type[0]) (a:IO io_out io_in A) (v':A) on a : Prop ≝
11match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ].
12
13definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝
14λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ] | _ ⇒ False].
15
16let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝
17match e with
18[ Value v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ]
19| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
20| _ ⇒ False].
21
22lemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
23yieldsIO A a v' →
24yieldsIO_sig A P (io_inject io_out io_in A P (Some ? a) p) v'.
25#A #P #a elim a;
26[ #a #k #IH #v' #p #H whd in H ⊢ %; elim H; #r #H' %{ r} @IH @H'
27| #v #v' #p #H @H
28| #a #b *;
29] qed.
30
31lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
32#A #a #v' cases a; //; whd in ⊢ (% → ?); *;
33qed.
34
35lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (dp … v p).
36#A #P #e #v cases e;
37[ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
38| *;
39] qed.
40
41lemma is_pointer_compat_true: ∀m,b,sp.
42  pointer_compat (block_region m b) sp →
43  is_pointer_compat (block_region m b) sp = true.
44#m #b #sp #H whd in ⊢ (??%?);
45elim (pointer_compat_dec (block_region m b) sp);
46[ //
47| #H' @False_ind @(absurd … H H')
48] qed.
49
50lemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
51[ #s cases s; @refl
52| skip
53] qed.
54
55theorem is_det: ∀p,s,s'.
56initial_state p s → initial_state p s' → s = s'.
57#p #s #s' #H1 #H2
58inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15
59inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25
60>e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
61[ 2: destruct (e1) skip (e11); @refl ]
62#e13 #e14
63
64>e12 in e22 #e2 destruct (e2) skip (e12);
65
66>e13 in e23 #e3 >(?:b1 = b2) in e14
67[ >e24 #e4 >(?:f2 = f1)
68  [ //;
69  | destruct (e4) skip (e24 e25); //;
70  ]
71| destruct (e3) skip (e13); //
72] qed.
73
74lemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
75yields A a v' →
76yields_sig A P (err_inject A P (Some ? a) p) v'.
77#A #P #a cases a;
78[ #v #v' #p #H @H
79| #a #b *;
80] qed.
81
82
83theorem the_initial_state:
84  ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
85#p #s cases p; #fns #main #globs #H
86inversion H;
87#b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
88whd in ⊢ (??%?);
89>e1
90whd in ⊢ (??%?);
91>e2
92whd in ⊢ (??%?);
93>e3
94whd in ⊢ (??%?);
95>e4
96whd; @refl
97qed.
98
99lemma cast_complete: ∀m,v,ty,ty',v'.
100  cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'.
101#m #v #ty #ty' #v' #H
102elim H;
103[ #m #i #sz1 #sz2 #sg1 #sg2 @refl
104| #m #f #sz #szi #sg @refl
105| #m #i #sz #sz' #sg @refl
106| #m #f #sz #sz' @refl
107| #m #sp #sp' #ty #ty' #b #ofs #H1 #H2 #H3
108    elim H1; [ #sp1 #ty1 | #sp1 #ty1 #n1 | #tys1 #ty1 letin sp1 ≝ Code ]
109    whd in ⊢ (??%?);
110    [ 1,2: >(eq_region_dec_true …) whd in ⊢ (??%?); ]
111    elim H2 in H3 ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
112    #H3 whd in ⊢ (??%?);
113    >(is_pointer_compat_true …) //;
114| #m #sz #si #ty'' #r #H cases H; //;
115| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
116    whd in ⊢ (??%?); try @refl >eq_region_dec_true @refl
117] qed.
118
119(* Use to narrow down the choice of expression to just the lvalues. *)
120lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop.
121  eval_lvalue ge env m (Expr e ty) l ofs tr →
122  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
123  P e.
124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
125[ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
126| #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
127| #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
128| #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
129| #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
130] qed.
131
132lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
133#v #ty #r #H elim H; #v #t #H' elim H';
134  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
135  | #p #b #i #i0 #s %{ true} % //
136  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
137  | #i #s %{ false} % //;
138  | #r #r' #t %{ false} % //;
139  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
140  ]
141qed.
142
143lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
144#v #ty #H elim H;
145  [ #i #is #s #ne whd; >(eq_false … ne) //;
146  | #p #b #i #i0 #s //
147  | #f #s #ne whd; >(Feq_zero_false … ne) //;
148  ]
149qed.
150
151lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
152#v #ty #H elim H;
153  [ #i #s //;
154  | #r #r' #t //;
155  | #s whd; >(Feq_zero_true …) //;
156  ]
157qed.
158
159lemma expr_lvalue_complete: ∀ge,env,m.
160(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
161(∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)).
162#ge #env #m
163@(combined_expr_lvalue_ind ge env m
164  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
165  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
166[ #i #ty @refl
167| #f #ty @refl
168| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
169    [ #id | #e' | #e' #id ] #H3
170    whd in ⊢ (??%?);
171    >(yields_eq ??? H3)
172    whd in ⊢ (??%?); >H2 @refl
173| #e #ty #sp #l #off #tr #H1 #H2 whd in ⊢ (??%?);
174    >(yields_eq ??? H2)
175    @refl
176| #ty' #ty @refl
177| #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
178    >(yields_eq ??? H3)
179    whd in ⊢ (??%?); >H2 @refl
180| #op #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #e3 #H4 #H5 whd in ⊢ (??%?);
181    >(yields_eq ??? H4) whd in ⊢ (??%?);
182    >(yields_eq ??? H5) whd in ⊢ (??%?);
183    >e3 @refl
184| #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
185    >(yields_eq ??? H4) whd in ⊢ (??%?);
186    >(yields_eq ??? (bool_of_true ?? H2))
187    >(yields_eq ??? H5)
188    @refl
189| #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
190    >(yields_eq ??? H4) whd in ⊢ (??%?);
191    >(yields_eq ??? (bool_of_false ?? H2))
192    >(yields_eq ??? H5)
193    @refl
194| #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
195    >(yields_eq ??? H3) whd in ⊢ (??%?);
196    >(yields_eq ??? (bool_of_true ?? H2))
197    @refl
198| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
199    >(yields_eq ??? H5) whd in ⊢ (??%?);
200    >(yields_eq ??? (bool_of_false ?? H2))
201    >(yields_eq ??? H6) whd in ⊢ (??%?);
202    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
203    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
204    @refl
205| #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
206    >(yields_eq ??? H3) whd in ⊢ (??%?);
207    >(yields_eq ??? (bool_of_false ?? H2))
208    @refl
209| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
210    >(yields_eq ??? H5) whd in ⊢ (??%?);
211    >(yields_eq ??? (bool_of_true ?? H2))
212    >(yields_eq ??? H6) whd in ⊢ (??%?);
213    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
214    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
215    @refl
216| #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
217    >(yields_eq ??? H3) whd in ⊢ (??%?);
218    >(yields_eq ??? (cast_complete … H2))
219    @refl
220| #e #ty #v #l #tr #H1 #H2 whd in ⊢ (??%?);
221    >(yields_eq ??? H2) whd in ⊢ (??%?);
222    @refl
223   
224  (* lvalues *)
225| #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl
226| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
227    >e2 @refl
228| #e #ty #r #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
229    >(yields_eq ??? H2)
230    @refl
231| #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
232    #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?);
233    >(yields_eq ??? H4) whd in ⊢ (??%?);
234    >H3 @refl
235| #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
236    whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?);
237    >(yields_eq ??? H3) @refl
238] qed.
239
240theorem expr_complete:  ∀ge,env,m.
241 ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉).
242#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
243
244theorem exprlist_complete: ∀ge,env,m,es,vs,tr.
245  eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉).
246#ge #env #m #es #vs #tr #H elim H;
247[ @refl
248| #e #et #v #vt #tr #trt #H1 #H2 #H3 whd in ⊢ (??%?);
249    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
250    >(yields_eq ??? H3)
251    @refl
252] qed.
253
254theorem lvalue_complete: ∀ge,env,m.
255 ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉).
256#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
257
258let rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
259match l with
260[ Tnil ⇒ True
261| Tcons h t ⇒ P h ∧ P_typelist P t
262].
263
264let rec type_ind2l
265  (P:type → Prop) (Q:typelist → Prop)
266  (vo:P Tvoid)
267  (it:∀i,s. P (Tint i s))
268  (fl:∀f. P (Tfloat f))
269  (pt:∀s,t. P t → P (Tpointer s t))
270  (ar:∀s,t,n. P t → P (Tarray s t n))
271  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
272  (st:∀i,fl. P (Tstruct i fl))
273  (un:∀i,fl. P (Tunion i fl))
274  (cp:∀r,i. P (Tcomp_ptr r i))
275  (nl:Q Tnil)
276  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
277 (t:type) on t : P t ≝
278  match t return λt'.P t' with
279  [ Tvoid ⇒ vo
280  | Tint i s ⇒ it i s
281  | Tfloat s ⇒ fl s
282  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
283  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
284  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
285  | Tstruct i fs ⇒ st i fs
286  | Tunion i fs ⇒ un i fs
287  | Tcomp_ptr r i ⇒ cp r i
288  ]
289and typelist_ind2l
290  (P:type → Prop) (Q:typelist → Prop)
291  (vo:P Tvoid)
292  (it:∀i,s. P (Tint i s))
293  (fl:∀f. P (Tfloat f))
294  (pt:∀s,t. P t → P (Tpointer s t))
295  (ar:∀s,t,n. P t → P (Tarray s t n))
296  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
297  (st:∀i,fl. P (Tstruct i fl))
298  (un:∀i,fl. P (Tunion i fl))
299  (cp:∀r,i. P (Tcomp_ptr r i))
300  (nl:Q Tnil)
301  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
302  (ts:typelist) on ts : Q ts ≝
303  match ts return λts'.Q ts' with
304  [ Tnil ⇒ nl
305  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
306                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
307  ].
308
309lemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
310#t whd in ⊢ (??(λ_.??%?)); cases (type_eq_dec t t); #E
311[ %{ E} //
312| @False_ind @(absurd ?? E) //
313] qed.
314
315lemma alloc_vars_complete: ∀env,m,l,env',m'.
316  alloc_variables env m l env' m' →
317  exec_alloc_variables env m l = 〈env', m'〉.
318#env #m #l #env' #m' #H elim H;
319[ #env'' #m'' %
320| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
321  < H3 whd in H1:(??%?) ⊢ (??%?)
322    destruct (H1) //
323] qed.
324
325lemma bind_params_complete: ∀e,m,params,vs,m2.
326  bind_parameters e m params vs m2 →
327  yields ? (exec_bind_parameters e m params vs) m2.
328#e #m #params #vs #m2 #H elim H;
329[ //;
330| #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4
331    whd in ⊢ (??%?)
332    >H1 whd in ⊢ (??%?);
333    >H2 whd in ⊢ (??%?);
334    @H4
335] qed.
336
337lemma eventval_match_complete': ∀ev,ty,v.
338  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
339#ev #ty #v #H elim H; //; qed.
340
341lemma eventval_list_match_complete: ∀vs,tys,evs.
342  eventval_list_match evs tys vs → yields ? (check_eventval_list vs tys) evs.
343#vs #tys #evs #H elim H;
344[ //
345| #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?)
346    >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?)
347    >(yields_eq ??? H3) whd in ⊢ (??%?) //
348] qed.
349
350lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
351#P #f #p #Q #H cases f;
352[ @H
353| #np @False_ind @(absurd ? p np)
354] qed.
355
356lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
357#P #f #p #Q #H cases f;
358[ #np @False_ind @(absurd ? np p)
359| @H
360] qed.
361
362theorem step_complete: ∀ge,s,tr,s'.
363  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
364#ge #s #tr #s' #H elim H;
365[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
366    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
367    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
368    >H3 @refl
369| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
370    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
371    >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?);
372    >H3 whd in ⊢ (??%?);
373    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
374    @refl
375| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
376    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
377    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
378    >H4 whd in ⊢ (??%?);
379    >H5 elim (assert_type_eq_true (fun_typeof ef)); #pty #ety >ety
380    whd in ⊢ (??%?);
381    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
382    @refl
383| #f #s1 #s2 #k #env #m @refl
384| 5,6,7: #f #s #k #env #m @refl
385| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
387    >(yields_eq ??? (bool_of_true ?? H2))
388    @refl
389| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
391    >(yields_eq ??? (bool_of_false ?? H2))
392    @refl
393| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
394    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
395    >(yields_eq ??? (bool_of_false ?? H2))
396    @refl
397| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
398    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
399    >(yields_eq ??? (bool_of_true ?? H2))
400    @refl
401| #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
402| 13,14: #f #e #s #k #env #m @refl
403| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
404    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
405    >(yields_eq ??? (bool_of_false ?? H2))
406    @refl
407| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
408    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
409    >(yields_eq ??? (bool_of_true ?? H2))
410    @refl
411| #f #e #s #k #env #m @refl
412| #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
413    [ #H @False_ind @(absurd ? H nskip)
414    | #H whd in ⊢ (??%?); @refl ]
415| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
416    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
417    >(yields_eq ??? (bool_of_false ?? H2))
418    @refl
419| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
420    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
421    >(yields_eq ??? (bool_of_true ?? H2))
422    @refl
423| #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl
424| 22,23: #f #e #s1 #s2 #k #env #m @refl
425| #f #k #env #m #H whd in ⊢ (??%?); >H @refl
426| #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
427    @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf'
428    whd in ⊢ (??%?);
429    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
430    @refl
431| #f #k #env #m cases k;
432    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
433    | #s' #k' whd in ⊢ (% → ?); *;
434    | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
435    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
436    | #k' whd in ⊢ (% → ?); *;
437    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
438    ]
439| #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
440    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
441    @refl
442| #f #s #k #env #m *; #es >es @refl
443| #f #k #env #m @refl
444| #f #l #s #k #env #m @refl
445| #f #l #k #env #m #s #k' #H1 whd in ⊢ (??%?); >H1 @refl
446| #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?);
447    >(alloc_vars_complete … H1) whd in ⊢ (??%?);
448    >(yields_eq ??? (bind_params_complete … H2))
449    //
450| #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
451    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 <e1 in H1 H2
452    #H1 #H2
453    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
454    whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
455    @refl
456| #v #f #env #k #m @refl
457| #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
458    >H @refl
459| #f #l #s #k #env #m @refl
460] qed.
Note: See TracBrowser for help on using the repository browser.