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

Last change on this file since 582 was 500, checked in by campbell, 10 years ago

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

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