source: src/Clight/CexecComplete.ma @ 797

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 16.5 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 #i #sz1 #sz2 #sg1 #sg2 @refl
103| #m #f #sz #szi #sg @refl
104| #m #i #sz #sz' #sg @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; //;
114| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
115    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
116] qed.
117
118(* Use to narrow down the choice of expression to just the lvalues. *)
119lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop.
120  eval_lvalue ge env m (Expr e ty) l ofs tr →
121  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
122  P e.
123#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
124[ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
125| #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
126| #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
127| #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
128| #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
129] qed.
130
131lemma 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.
132#v #ty #r #H elim H; #v #t #H' elim H';
133  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
134  | #r #b #pc #i #i0 #s %{ true} % //
135  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
136  | #i #s %{ false} % //;
137  | #r #r' #t %{ false} % //;
138  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
139  ]
140qed.
141
142lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
143#v #ty #H elim H;
144  [ #i #is #s #ne whd; >(eq_false … ne) //;
145  | #p #b #i #i0 #s //
146  | #f #s #ne whd; >(Feq_zero_false … ne) //;
147  ]
148qed.
149
150lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
151#v #ty #H elim H;
152  [ #i #s //;
153  | #r #r' #t //;
154  | #s whd; >(Feq_zero_true …) //;
155  ]
156qed.
157
158lemma expr_lvalue_complete: ∀ge,env,m.
159(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
160(∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)).
161#ge #env #m
162@(combined_expr_lvalue_ind ge env m
163  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
164  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
165[ #i #ty @refl
166| #f #ty @refl
167| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
168    [ #id | #e' | #e' #id ] #H3
169    whd in ⊢ (??%?);
170    >(yields_eq ??? H3)
171    whd in ⊢ (??%?); >H2 @refl
172| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
173    >(yields_eq ??? H2) whd in ⊢ (??%?)
174    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
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 #pc #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) @refl
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
350theorem step_complete: ∀ge,s,tr,s'.
351  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
352#ge #s #tr #s' #H elim H;
353[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
354    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
355    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
356    >H3 @refl
357| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
358    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
359    >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?);
360    >H3 whd in ⊢ (??%?);
361    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
362    @refl
363| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
364    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
365    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
366    >H4 whd in ⊢ (??%?);
367    >H5 elim (assert_type_eq_true (fun_typeof ef)); #pty #ety >ety
368    whd in ⊢ (??%?);
369    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
370    @refl
371| #f #s1 #s2 #k #env #m @refl
372| 5,6,7: #f #s #k #env #m @refl
373| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
374    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
375    >(yields_eq ??? (bool_of_true ?? H2))
376    @refl
377| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
378    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
379    >(yields_eq ??? (bool_of_false ?? H2))
380    @refl
381| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
382    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
383    >(yields_eq ??? (bool_of_false ?? H2))
384    @refl
385| #f #e #s #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 #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
390| 13,14: #f #e #s #k #env #m @refl
391| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
392    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
393    >(yields_eq ??? (bool_of_false ?? H2))
394    @refl
395| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
397    >(yields_eq ??? (bool_of_true ?? H2))
398    @refl
399| #f #e #s #k #env #m @refl
400| #f #s1 #e #s2 #s3 #k #env #m #nskip whd in ⊢ (??%?); cases (is_Sskip s1);
401    [ #H @False_ind @(absurd ? H nskip)
402    | #H whd in ⊢ (??%?); @refl ]
403| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
404    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
405    >(yields_eq ??? (bool_of_false ?? H2))
406    @refl
407| #f #e #s1 #s2 #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
408    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
409    >(yields_eq ??? (bool_of_true ?? H2))
410    @refl
411| #f #s1 #e #s2 #s3 #k #env #m *; #es1 >es1 @refl
412| 22,23: #f #e #s1 #s2 #k #env #m @refl
413| #f #k #env #m #H whd in ⊢ (??%?); >H @refl
414| #f #e #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
415    @(dec_false ? (type_eq_dec (fn_return f) Tvoid) H1) #pf'
416    whd in ⊢ (??%?);
417    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
418    @refl
419| #f #k #env #m cases k;
420    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
421    | #s' #k' whd in ⊢ (% → ?); *;
422    | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
423    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
424    | #k' whd in ⊢ (% → ?); *;
425    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
426    ]
427| #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
428    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
429    @refl
430| #f #s #k #env #m *; #es >es @refl
431| #f #k #env #m @refl
432| #f #l #s #k #env #m @refl
433| #f #l #k #env #m #s #k' #H1 whd in ⊢ (??%?); >H1 @refl
434| #f #args #k #m1 #env #m2 #m3 #H1 #H2 whd in ⊢ (??%?);
435    >(alloc_vars_complete … H1) whd in ⊢ (??%?);
436    >(yields_eq ??? (bind_params_complete … H2))
437    //
438| #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
439    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 <e1 in H1 H2
440    #H1 #H2
441    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
442    whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
443    @refl
444| #v #f #env #k #m @refl
445| #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
446    >H @refl
447| #f #l #s #k #env #m @refl
448] qed.
449
450lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
451#s0 #r0 * #r #m @refl qed.
452 
Note: See TracBrowser for help on using the repository browser.