Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r485 r487  
    11include "Cexec.ma".
    2 include "Plogic/connectives.ma".
    3 
    4 ndefinition yields ≝ λA.λa:res A.λv':A.
     2
     3definition yields ≝ λA.λa:res A.λv':A.
    54match a with [ OK v ⇒ v' = v | _ ⇒ False ].
    65
     
    98   that one particular one exists corresponding to a derivation in the inductive
    109   semantics.) *)
    11 nlet rec yieldsIO (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝
     10let rec yieldsIO (A:Type[0]) (a:IO io_out io_in A) (v':A) on a : Prop ≝
    1211match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ].
    1312
    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_intro v'' _ ⇒ 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 ≝
     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 ≝
    1817match e with
    19 [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
     18[ Value v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ]
    2019| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
    2120| _ ⇒ False].
    2221
    23 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
     22lemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    2423yieldsIO 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.
     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: ∀m,b,sp.
    4342  pointer_compat (block_space m b) sp →
    4443  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 ##| ##skip
    54 ##] nqed.
    55 
    56 ntheorem is_det: ∀p,s,s'.
     44#m #b #sp #H whd in ⊢ (??%?);
     45elim (pointer_compat_dec (block_space m b) sp);
     46[ //
     47| #H' @False_ind @(absurd … H H')
     48] qed.
     49
     50lemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
     51[ #s cases s; @refl
     52| skip
     53] qed.
     54
     55theorem is_det: ∀p,s,s'.
    5756initial_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
     58inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15
     59inversion 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
     74lemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    7675yields 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:
     76yields_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
     83theorem the_initial_state:
    8584  ∀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
     86inversion H;
     87#b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
     88whd in ⊢ (??%?);
     89>e1
     90whd in ⊢ (??%?);
     91>e2
     92whd in ⊢ (??%?);
     93>e3
     94whd in ⊢ (??%?);
     95>e4
     96whd; @refl
     97qed.
     98
     99lemma cast_complete: ∀m,v,ty,ty',v'.
    101100  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
     102elim 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.
    119118
    120119(* 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.
     120lemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
    122121  eval_lvalue ge env m (Expr e ty) sp l ofs tr →
    123122  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
    124123  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
     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  [ #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  ]
     141qed.
     142
     143lemma 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  ]
     149qed.
     150
     151lemma 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  ]
     157qed.
     158
     159lemma expr_lvalue_complete: ∀ge,env,m.
    161160(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
    162161(∀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 m
     162#ge #env #m
     163@(combined_expr_lvalue_ind ge env m
    165164  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    166165  (λ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
    224223   
    225224  (* 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
     240theorem expr_complete:  ∀ge,env,m.
    242241 ∀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
     244theorem exprlist_complete: ∀ge,env,m,es,vs,tr.
    246245  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
     254theorem lvalue_complete: ∀ge,env,m.
    256255 ∀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
     258let rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
    260259match l with
    261260[ Tnil ⇒ True
     
    263262].
    264263
    265 nlet rec type_ind2l
     264let rec type_ind2l
    266265  (P:type → Prop) (Q:typelist → Prop)
    267266  (vo:P Tvoid)
     
    308307  ].
    309308
    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'.
     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'.
    317316  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
     325lemma bind_params_complete: ∀e,m,params,vs,m2.
    328326  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
     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
     350lemma 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
     356lemma 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
     362theorem step_complete: ∀ge,s,tr,s'.
    367363  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; napply refl
    388 ##| ##5,6,7: #f s k env m; napply refl
    389 ##| #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     napply refl
    393 ##| #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     napply refl
    397 ##| #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     napply refl
    401 ##| #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     napply refl
    405 ##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
    406 ##| ##13,14: #f e s k env m; napply refl
    407 ##| #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     napply refl
    411 ##| #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     napply refl
    415 ##| #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; napply refl
    442     ##]
    443 ##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
    444     nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    445     napply refl
    446 ##| #f s k env m; *; #es; nrewrite > es; napply refl;
    447 ##| #f k env m; napply refl
    448 ##| #f l s k env m; napply refl
    449 ##| #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     napply refl
    460 ##| #v f env k m; napply refl
    461 ##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
    462     nrewrite > H; napply refl
    463 ##| #f l s k env m; napply refl
    464 ##] 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.