source: src/Clight/CexecComplete.ma @ 2278

Last change on this file since 2278 was 2176, checked in by campbell, 8 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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