Changeset 487 for Deliverables/D3.1/Csemantics/CexecComplete.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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