source: src/Clight/CexecComplete.ma @ 978

Last change on this file since 978 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 17.4 KB
Line 
1include "Clight/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 #c *;
29] qed.
30
31lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
32#A #a #v' cases a; // #m 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| #m *;
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
81
82theorem the_initial_state:
83  ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
84#p #s cases p; #fns #main #globs #H
85inversion H;
86#b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
87whd in ⊢ (??%?);
88>e1
89whd in ⊢ (??%?);
90>e2
91whd in ⊢ (??%?);
92>e3
93whd in ⊢ (??%?);
94>e4
95whd; @refl
96qed.
97
98lemma cast_complete: ∀m,v,ty,ty',v'.
99  cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'.
100#m #v #ty #ty' #v' #H
101elim H;
102[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
103| #m #f #sz #szi #sg @refl
104| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
105| #m #f #sz #sz' @refl
106| #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
107    elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
108    whd in ⊢ (??%?)
109    [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ]
110    elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
111    #pc' whd in ⊢ (??%?)
112    @(dec_true ? (pointer_compat_dec b sp2) pc') //
113| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
114  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
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 @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @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  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
135    >(eq_bv_false … ne) //
136  | #r #b #pc #i #i0 #s %{ true} % //
137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
138  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
139  | #r #r' #t %{ false} % //;
140  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
141  ]
142qed.
143
144lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
145#v #ty #H elim H;
146  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
147  | #p #b #i #i0 #s //
148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
149  ]
150qed.
151
152lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
153#v #ty #H elim H;
154  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
155  | #r #r' #t //;
156  | #s whd; >(Feq_zero_true …) //;
157  ]
158qed.
159
160lemma expr_lvalue_complete: ∀ge,env,m.
161(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
162(∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)).
163#ge #env #m
164@(combined_expr_lvalue_ind ge env m
165  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
166  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
167[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
168| #f #ty @refl
169| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
170    [ #id | #e' | #e' #id ] #H3
171    whd in ⊢ (??%?)
172    [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)
173    | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)
174    | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)
175    ]
176    >(yields_eq ??? H3)
177    whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉)
178    >H2 @refl
179| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
180    >(yields_eq ??? H2) whd in ⊢ (??%?)
181    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
182    @refl
183| #ty' #sz #sg @refl
184| #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
185    >(yields_eq ??? H3)
186    whd in ⊢ (??%?); >H2 @refl
187| #op #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #e3 #H4 #H5 whd in ⊢ (??%?);
188    >(yields_eq ??? H4) whd in ⊢ (??%?);
189    >(yields_eq ??? H5) whd in ⊢ (??%?);
190    >e3 @refl
191| #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
192    >(yields_eq ??? H4) whd in ⊢ (??%?);
193    >(yields_eq ??? (bool_of_true ?? H2))
194    >(yields_eq ??? H5)
195    @refl
196| #e1 #e2 #e3 #ty #v1 #v2 #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
197    >(yields_eq ??? H4) whd in ⊢ (??%?);
198    >(yields_eq ??? (bool_of_false ?? H2))
199    >(yields_eq ??? H5)
200    @refl
201| #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
202    >(yields_eq ??? H3) whd in ⊢ (??%?);
203    >(yields_eq ??? (bool_of_true ?? H2))
204    @refl
205| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
206    >(yields_eq ??? H5) whd in ⊢ (??%?);
207    >(yields_eq ??? (bool_of_false ?? H2))
208    >(yields_eq ??? H6) whd in ⊢ (??%?);
209    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
210    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
211    @refl
212| #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
213    >(yields_eq ??? H3) whd in ⊢ (??%?);
214    >(yields_eq ??? (bool_of_false ?? H2))
215    @refl
216| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
217    >(yields_eq ??? H5) whd in ⊢ (??%?);
218    >(yields_eq ??? (bool_of_true ?? H2))
219    >(yields_eq ??? H6) whd in ⊢ (??%?);
220    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
221    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
222    @refl
223| #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
224    >(yields_eq ??? H3) whd in ⊢ (??%?);
225    >(yields_eq ??? (cast_complete … H2))
226    @refl
227| #e #ty #v #l #tr #H1 #H2 whd in ⊢ (??%?);
228    >(yields_eq ??? H2) whd in ⊢ (??%?);
229    @refl
230   
231  (* lvalues *)
232| #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl
233| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
234    >e2 @refl
235| #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?);
236    >(yields_eq ??? H2)
237    @refl
238| #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
239    #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?);
240    >(yields_eq ??? H4) whd in ⊢ (??%?);
241    >H3 @refl
242| #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
243    whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?);
244    >(yields_eq ??? H3) @refl
245] qed.
246
247theorem expr_complete:  ∀ge,env,m.
248 ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉).
249#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
250
251theorem exprlist_complete: ∀ge,env,m,es,vs,tr.
252  eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉).
253#ge #env #m #es #vs #tr #H elim H;
254[ @refl
255| #e #et #v #vt #tr #trt #H1 #H2 #H3 whd in ⊢ (??%?);
256    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
257    >(yields_eq ??? H3)
258    @refl
259] qed.
260
261theorem lvalue_complete: ∀ge,env,m.
262 ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉).
263#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
264
265let rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
266match l with
267[ Tnil ⇒ True
268| Tcons h t ⇒ P h ∧ P_typelist P t
269].
270
271let rec type_ind2l
272  (P:type → Prop) (Q:typelist → Prop)
273  (vo:P Tvoid)
274  (it:∀i,s. P (Tint i s))
275  (fl:∀f. P (Tfloat f))
276  (pt:∀s,t. P t → P (Tpointer s t))
277  (ar:∀s,t,n. P t → P (Tarray s t n))
278  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
279  (st:∀i,fl. P (Tstruct i fl))
280  (un:∀i,fl. P (Tunion i fl))
281  (cp:∀r,i. P (Tcomp_ptr r i))
282  (nl:Q Tnil)
283  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
284 (t:type) on t : P t ≝
285  match t return λt'.P t' with
286  [ Tvoid ⇒ vo
287  | Tint i s ⇒ it i s
288  | Tfloat s ⇒ fl s
289  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
290  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
291  | 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')
292  | Tstruct i fs ⇒ st i fs
293  | Tunion i fs ⇒ un i fs
294  | Tcomp_ptr r i ⇒ cp r i
295  ]
296and typelist_ind2l
297  (P:type → Prop) (Q:typelist → Prop)
298  (vo:P Tvoid)
299  (it:∀i,s. P (Tint i s))
300  (fl:∀f. P (Tfloat f))
301  (pt:∀s,t. P t → P (Tpointer s t))
302  (ar:∀s,t,n. P t → P (Tarray s t n))
303  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
304  (st:∀i,fl. P (Tstruct i fl))
305  (un:∀i,fl. P (Tunion i fl))
306  (cp:∀r,i. P (Tcomp_ptr r i))
307  (nl:Q Tnil)
308  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
309  (ts:typelist) on ts : Q ts ≝
310  match ts return λts'.Q ts' with
311  [ Tnil ⇒ nl
312  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
313                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
314  ].
315
316lemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
317#t whd in ⊢ (??(λ_.??%?)); cases (type_eq_dec t t); #E
318[ %{ E} //
319| @False_ind @(absurd ?? E) //
320] qed.
321
322lemma alloc_vars_complete: ∀env,m,l,env',m'.
323  alloc_variables env m l env' m' →
324  exec_alloc_variables env m l = 〈env', m'〉.
325#env #m #l #env' #m' #H elim H;
326[ #env'' #m'' %
327| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
328  < H3 whd in H1:(??%?) ⊢ (??%?)
329    destruct (H1) @refl
330] qed.
331
332lemma bind_params_complete: ∀e,m,params,vs,m2.
333  bind_parameters e m params vs m2 →
334  yields ? (exec_bind_parameters e m params vs) m2.
335#e #m #params #vs #m2 #H elim H;
336[ //;
337| #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4
338    whd in ⊢ (??%?)
339    >H1 whd in ⊢ (??%?);
340    >H2 whd in ⊢ (??%?);
341    @H4
342] qed.
343
344lemma eventval_match_complete': ∀ev,ty,v.
345  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
346#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
347
348lemma eventval_list_match_complete: ∀vs,tys,evs.
349  eventval_list_match evs tys vs → yields ? (check_eventval_list vs tys) evs.
350#vs #tys #evs #H elim H;
351[ //
352| #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?)
353    >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?)
354    >(yields_eq ??? H3) whd in ⊢ (??%?) //
355] qed.
356
357theorem step_complete: ∀ge,s,tr,s'.
358  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
359#ge #s #tr #s' #H elim H;
360[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
361    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?)
362    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?)
363    change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
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 #sz #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; [ #sz #sg #x | #x #sz ] #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
454    change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)
455    #H whd in ⊢ (??%?) >H @refl
456| #f #l #s #k #env #m @refl
457] qed.
458
459lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
460#s0 #r0 * #r #m @refl qed.
461 
Note: See TracBrowser for help on using the repository browser.