Changeset 1920


Ignore:
Timestamp:
May 8, 2012, 11:16:18 AM (7 years ago)
Author:
campbell
Message:

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r1872 r1920  
    208208  | LSdefault: statement → labeled_statements
    209209  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
     210
     211let rec labeled_statements_ind
     212  (P:labeled_statements → Prop)
     213  (LSd:∀s. P (LSdefault s))
     214  (LSc:∀sz,i,s,tl. P tl → P (LScase sz i s tl))
     215  ls on ls : P ls ≝
     216match ls with
     217[ LSdefault s ⇒ LSd s
     218| LScase sz i s tl ⇒ LSc sz i s tl (labeled_statements_ind P LSd LSc tl)
     219].
    210220
    211221let rec statement_ind2
  • src/Clight/labelSimulation.ma

    r1893 r1920  
    55(* for the induction principle *)
    66include "Clight/CexecSound.ma".
     7
     8(* TODO: make something general that can live in common/Globalenvs.ma. *)
     9record related_globals (ge:genv) (ge':genv) : Prop ≝ {
     10  rg_find_symbol: ∀s.
     11    find_symbol ?? ge s = find_symbol ?? ge' s;
     12  rg_find_funct: ∀v,f.
     13    find_funct ?? ge v = Some ? f →
     14    find_funct ?? ge' v = Some ? (label_fundef f)
     15}.
    716
    817lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D.
     
    1625qed.
    1726
    18 lemma label_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
    19   (∀u'. P (F (\fst (label_expr e u)) u')) →
    20   P (let 〈e',u'〉 ≝ label_expr e u in F e' u').
    21 #e #u #T #F #P
    22 cases (label_expr e u)
    23 #e' #u' #H @H
     27(* lemma to break up label_expr, label_exprs and label_statement in the labelling
     28   functions *)
     29lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
     30  (∀u'. P (F (\fst (L syn u)) u')) →
     31  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
     32#Syn #syn #u #T #L #F #P
     33cases (L syn u)
     34#syn' #u' #H @H
    2435qed.
    2536
     
    5465qed. 
    5566
    56 lemma label_expr_ok : ∀ge,en,m,e,v,tr.
    57   exec_expr ge en m e = OK … 〈v,tr〉 →
    58   ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
    59             trace_with_extra_labels tr tr'.
    60 #ge #en #m #e
    61 @(expr_lvalue_ind ?
    62   (λe,ty. ∀b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
    63           ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
    64                     trace_with_extra_labels tr tr') … e)
     67definition expr_lvalue_ind_combined ≝
     68λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
     69conj ??
     70 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
     71 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     72
     73lemma label_expr_ok : ∀ge,ge',en,m.
     74  related_globals ge ge' →
     75  (∀e,v,tr.
     76   exec_expr ge en m e = OK … 〈v,tr〉 →
     77   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
     78             trace_with_extra_labels tr tr') ∧
     79  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
     80          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
     81                    trace_with_extra_labels tr tr').
     82#ge #ge' #en #m #RG @expr_lvalue_ind_combined
    6583[ 1,2: normalize /3 by ex_intro, conj/
    6684| * //
    67  [ normalize /3 by ex_intro, conj/
     85 [ #id #ty #IH #v #tr #EX #u
     86   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
     87   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
     88   normalize in EX; destruct
     89   cases (IH … EX1 u) #tr1' * #EX1' #T1
     90   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
    6891 | #e1 #ty #IH #v #tr #EX #u
    6992   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
     
    81104   whd in ⊢ (??%?); >EXl @refl
    82105 ]
    83 | #v #ty #b #o #tr #EX #u %{tr} % /2/
     106| #v #ty #b #o #tr #EX #u %{tr} % [
     107    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
     108    [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
     109    | #b // ]
     110  | // ]
    84111| #e1 #ty #IH #b #o #tr #EX #u
    85112  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
     
    106133  %{tr1'} % // >shift_fst
    107134  whd in ⊢ (??(????(?(???%)?))?);
    108   @label_expr_elim #u2
     135  @label_gen_elim #u2
    109136  whd in ⊢ (??%?); >EX1'
    110137  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
     
    117144  >shift_fst
    118145  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    119   @label_expr_elim #u2
     146  @label_gen_elim #u2
    120147  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    121   @label_expr_elim #u3 %{(tr1'⧺tr2')}
     148  @label_gen_elim #u3 %{(tr1'⧺tr2')}
    122149  whd in ⊢ (?(??%?)?); >EX1'
    123150  whd in ⊢ (?(??%?)?); >EX2'
     
    139166  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    140167  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    141   @label_expr_elim #u2
    142   @label_expr_elim #u3
     168  @label_gen_elim #u2
     169  @label_gen_elim #u3
    143170  @add_cost_expr_elim #u4 #l4
    144   @label_expr_elim #u5
     171  @label_gen_elim #u5
    145172  @add_cost_expr_elim #u6 #l6
    146173  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
     
    154181  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
    155182  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    156   @label_expr_elim #u2
    157   @label_expr_elim #u3
     183  @label_gen_elim #u2
     184  @label_gen_elim #u3
    158185  @add_cost_expr_elim #u4 #l4
    159186  @add_cost_expr_elim #u5 #l5
     
    180207  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
    181208  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    182   @label_expr_elim #u2
     209  @label_gen_elim #u2
    183210  @add_cost_expr_elim #u4 #l4
    184   @label_expr_elim #u3
     211  @label_gen_elim #u3
    185212  @add_cost_expr_elim #u5 #l5
    186213  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     
    231258] qed.
    232259
     260lemma label_exprs_ok : ∀ge,ge'.
     261   related_globals ge ge' →
     262   ∀en,m,es,vs,tr.
     263   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
     264   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧
     265             trace_with_extra_labels tr tr'.
     266#ge #ge' #RG #en #m #es elim es
     267[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
     268| #e #tl #IH #vs #tr #EX
     269  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
     270  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
     271  whd in EX:(??%%); destruct
     272  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
     273  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
     274  cases (IH … EX2 u') #tr'' * #EX2' #T2
     275  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     276    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
     277  | /2/ ] | skip ]
     278] qed.
     279
    233280(* Plan:
    234281     - extend labelling functions to continuations and hence states
    235282       NO - this doesn't work because we don't know *which* cost labels to add
    236283       realistically we'll have to define erasure functions
     284       BETTER - use predicate so that we don't need to insist on the absence of
     285       cost labels in the source
    237286     - build a simulation relation linking states to their labelled counterparts
    238287     - write a predicate stating that two traces are the same except for some
     
    246295               cost_related s2 s2'
    247296       using some relationship between ge and ge'.
    248 
    249 WAIT - do I really want functions to erase the labels?  Or a predicate?
    250 
    251 let rec erase_label_expr (e:expr) : expr ≝
    252 match e with
    253 [ Expr ed ty ⇒ Expr (erase_label_expr_descr ed) ty
     297*)
     298
     299inductive cont_with_labels : cont → cont → Prop ≝
     300| cwl_stop : cont_with_labels Kstop Kstop
     301| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
     302| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
     303    cont_with_labels k k' →
     304    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
     305| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
     306    cont_with_labels k k' →
     307    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
     308| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
     309    cont_with_labels k k' →
     310    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
     311| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
     312| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
     313| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
     314| cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
     315| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
     316    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
     317
     318lemma call_cont_with_labels : ∀k,k'.
     319  cont_with_labels k k' →
     320  cont_with_labels (call_cont k) (call_cont k').
     321#k0 #k0' #K elim K /2/
     322qed.
     323
     324inductive state_with_labels : state → state → Prop ≝
     325| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
     326(* Extra matching states that we can reach that don't quite correspond to the
     327   labelling function *)
     328| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     329    state_with_labels (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     330| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     331    state_with_labels (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     332| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     333    state_with_labels (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     334| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
     335    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
     336                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
     337(* and the rest *)
     338| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
     339| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels (Returnstate res k m) (Returnstate res k' m)
     340| swl_finalstate : ∀r. state_with_labels (Finalstate r) (Finalstate r)
     341.
     342
     343inductive plus (ge:genv) : state → trace → state → Prop ≝
     344| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
     345| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
     346
     347definition eplus ≝ λn. repeat n io_out io_in clight_fullexec.
     348
     349inductive hplus (ge:genv) : state → trace → trace → state → Prop ≝
     350| hplus_one : ∀tr,s2,s1',tr1,tr2,s2'.
     351    exec_step ge s1' = OK … 〈tr2,s2'〉 →
     352    trace_with_extra_labels tr (tr1⧺tr2) →
     353    state_with_labels s2 s2' →
     354    hplus ge s1' tr1 tr s2
     355| hplus_succ : ∀s1,tr,s2,tr1,tr2,s3.
     356    exec_step ge s1 = OK … 〈tr2,s2〉 →
     357    hplus ge s2 (tr1⧺tr2) tr s3 →
     358    hplus ge s1 tr1 tr s3.
     359
     360lemma label_function_return : ∀f.
     361  fn_return (label_function f) = fn_return f.
     362* #rty #params #vars #body
     363whd in ⊢ (??(?%)?);
     364cases (label_statement ??) #body' #u'
     365whd in ⊢ (??(?%)?);
     366cases (add_cost_before ??) #body'' #u''
     367//
     368qed.
     369
     370lemma bindIO_inversion: ∀O,I.
     371  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     372  (f »= g = return y) →
     373  ∃x. (f = return x) ∧ (g x = return y).
     374#O #I #A #B #f #g #y cases f normalize
     375[ #o #k #E destruct
     376| #a #e %{a} /2 by conj/
     377| #m #H destruct (H)
     378] qed.
     379
     380lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v.
     381  err_to_io … e = Value O I T v →
     382  e = OK T v.
     383#O #I #T *
     384[ #e #v #E normalize in E; destruct @refl
     385| #m #v #E normalize in E; destruct
    254386]
    255 and erase_label_expr_descr (e:expr_descr) : expr_descr ≝
    256 match e with
    257 [ Ederef e' ⇒ Ederef (erase_label_expr_descr e')
    258 | Eaddrof e' ⇒ Eaddrof (erase_label_expr_descr e')
    259 | Eunop op e'
     387qed.
     388
     389coercion io_eq_from_res :
     390  ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
     391  on _E:eq (IO ???) ?? to eq (res ?) ??.
     392
     393lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
     394  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
     395  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
     396#ge #e #m #a #ty #u
     397whd in ⊢ (??(????(???%))?); >shift_fst @refl
     398qed.
     399
     400lemma label_expr_fun_typeof : ∀a,u.
     401  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
     402#a #u whd in ⊢ (??%?); >label_expr_type @refl
     403qed.
     404
     405lemma label_fundef_typeof_fundef : ∀fd.
     406  type_of_fundef (label_fundef fd) = type_of_fundef fd.
     407* //
     408* #rty #args #vars #body
     409normalize cases (label_statement ??) #body' #u
     410normalize cases (fresh ??) //
     411qed.
     412
     413lemma opt_find_funct : ∀ge,ge',m,vf,fd.
     414  related_globals ge ge' →
     415  opt_to_io io_out io_in … m (find_funct ?? ge vf) = Value … fd →
     416  opt_to_io io_out io_in … m (find_funct ?? ge' vf) = Value … (label_fundef fd).
     417#ge #ge' #m #vf #fd #RG
     418lapply (rg_find_funct … RG … vf fd)
     419cases (find_funct … vf)
     420[ #_ #E normalize in E; destruct
     421| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
     422] qed.
     423
     424(*
     425lemma step_with_labels : ∀ge,s1,s1',tr,s2.
     426  state_with_labels s1 s1' →
     427  exec_step ge s1 = OK … 〈tr,s2〉 →
     428  hplus ge s1' E0 tr s2.
     429#ge #Xs1 #Xs1' #tr #s2 *
     430[ #f #us #s #k #k' #e #m #KL cases s
     431  [ #EX inversion KL
     432    [ #E1 #E2 #_ destruct @hplus_one [3: whd in EX:(??%?) ⊢ (??%?);
     433      >label_function_return >EX in ⊢ (??%?); | 1,2:skip | // | %1
     434      cases f in EX ⊢ %; #rty #params #vars #body #EX whd in ⊢ (??(match ?% with [_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?])?); >EX
     435     whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
     436
     437lemma step_with_labels : ∀ge,s1,s1',tr,s2.
     438  state_with_labels s1 s1' →
     439  exec_step ge s1 = OK … 〈tr,s2〉 →
     440  ∃n,tr',s2'. eplus n ge s1' = OK … 〈tr',s2'〉 ∧
     441            trace_with_extra_labels tr tr' ∧
     442            state_with_labels s2 s2'.
     443#ge #Xs1 #Xs1' #tr #s2 *
     444[ #f #us #s #k #k' #e #m #KL cases s
     445  [ #EX %{1} %{tr} inversion KL
     446    [ #E1 #E2 #_ destruct
     447     whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
     448     whd in EX:(??%?) ⊢ (??(λ_.?(?(??(?????%?)?)?)?));
     449     normalize in EX:(??%?) ⊢ (??(λ_.?(?(??(%??????)?)?)?));
     450      % [2: % [ % [ @plus_one whd in EX:(??%?) ⊢ (??%?); >EX whd in ⊢ (??(??(??%???))?); @EX >EX @refl
    260451*)
     452
     453lemma labelled_not_skip : ∀s,u.
     454  s ≠ Sskip →
     455  (\fst (label_statement s u)) ≠ Sskip.
     456* #u
     457[ * #H cases (H (refl ??))
     458| *: #a try #b try #c try #d try #e
     459     (* Use the state-monad-like structure of the labelling function to break
     460        it up *)
     461     whd in match (label_statement ??);
     462     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
     463     % #E destruct
     464] qed.
     465
     466lemma labelled_is_not_skip : ∀s,u.
     467  s ≠ Sskip →
     468  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
     469#s #u #NE
     470cases (is_Sskip ?)
     471[ #E @⊥ @(absurd ? E) @labelled_not_skip //
     472| /2/
     473] qed.
     474
     475(* TODO: this is from CexecComplete, but should live somewhere else *)
     476lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
     477#P #f #p #Q #H cases f;
     478[ @H
     479| #np cut False [ @(absurd ? p np) | * ]
     480] qed.
     481
     482lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
     483#P #f #p #Q #H cases f;
     484[ #np cut False [ @(absurd ? np p) | * ]
     485| @H
     486] qed.
     487
     488lemma label_select_ls : ∀sz,i,ls,u.
     489  ∃u'.
     490    select_switch sz i (\fst (label_lstatements ls u)) =
     491    \fst (label_lstatements (select_switch sz i ls) u').
     492#sz #i #ls @(labeled_statements_ind … ls)
     493[ #s #u % [2: whd in match (label_lstatements ??);
     494  @label_gen_elim #u1 >shift_fst @refl | skip ]
     495| #sz' #i' #s #tl #IH #u
     496  whd in match (label_lstatements ??);
     497  whd in match (select_switch ?? (LScase ????));
     498  @intsize_eq_elim_elim
     499  [ #NE
     500    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
     501    cases (IH u2)
     502    #u4 #E %{u4} whd in ⊢ (??%?);
     503    >intsize_eq_elim_false //
     504  | #E <E in i' ⊢ %; #i' whd
     505    @eq_bv_elim
     506    [ #Ei >Ei
     507      %{u}
     508      whd in match (label_lstatements (if ? then ? else ?) ?);
     509      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
     510      whd in ⊢ (??%?);
     511      >intsize_eq_elim_true
     512      >eq_bv_true
     513      @refl
     514    | #NEi
     515      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
     516       whd in ⊢ (??(λ_.??%?));
     517       >intsize_eq_elim_true
     518       >eq_bv_false //
     519    ]
     520  ]
     521] qed.
     522
     523lemma blindly_label : ∀u,s. ∀P:statement → Prop.
     524match s with
     525[ Sskip ⇒ P Sskip
     526| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
     527| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3)))
     528| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
     529| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
     530| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
     531| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
     532| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
     533| Sbreak ⇒ P Sbreak
     534| Scontinue ⇒ P Scontinue
     535| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
     536| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
     537| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
     538| Sgoto l ⇒ P (Sgoto l)
     539| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
     540] → P (\fst (label_statement s u)). 
     541#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
     542@label_gen_elim #u1 //
     543@label_gen_elim #u2 //
     544[ 6: >shift_fst //
     545| *: @label_gen_elim #u3 //
     546     @label_gen_elim #u4
     547     [ @label_gen_elim #u5 >shift_fst >shift_fst //
     548     | 2,3: >shift_fst >shift_fst //
     549     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
     550     ]
     551] qed.
     552
     553(* Apply induction hypothesis while getting Matita to infer the continuations
     554   k0 and k0', and the universe u0. *)
     555lemma lfl_IH : ∀s0,lbl.
     556  ∀C:option (statement×cont) → option (statement×cont) → Prop.
     557  ∀IH:cont → cont → universe CostTag → Prop.
     558  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
     559  ∀k0,k0',u0. cont_with_labels k0 k0' →
     560   (IH k0 k0' u0 →
     561    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
     562   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
     563/3/
     564qed.
     565
     566lemma label_find_label : ∀lbl,s,k,k',u.
     567  cont_with_labels k k' →
     568  match find_label lbl s k with
     569  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
     570    ∃u',cs,k1'.
     571    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
     572    cont_with_labels k1 k1'
     573  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
     574  ].
     575#lbl #s @(statement_ind2 ? (λls.
     576  ∀k,k',u.
     577  cont_with_labels k k' →
     578  match find_label_ls lbl ls k with
     579  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
     580    ∃u',cs,k1'.
     581    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
     582    cont_with_labels k1 k1'
     583  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
     584  ])
     585 … s)
     586[ #k #k' #u #F @refl
     587| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
     588| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
     589| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
     590  whd in match (find_label ?? k');
     591  @(lfl_IH sA … IH1) [ /2/ ]
     592  cases (find_label ???)
     593  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
     594    @(lfl_IH … IH2) [ // ]
     595    cases (find_label ???)
     596    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
     597    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
     598      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
     599    ]
     600  | * #sA' #kA' whd in ⊢ (% → %);
     601    * #u1' * #cs * #k1' * #FA' #K'
     602         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
     603  ]
     604| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
     605  whd in match (find_label ?? k); whd in match (find_label ?? k');
     606  whd in match (find_label ?? k');
     607  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
     608  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
     609    lapply (IH2 k k' u3 K) cases (find_label ???)
     610    [ whd in ⊢ (% → %); #FIND2'
     611      whd in match (find_label ???); >FIND1'
     612      whd in match (find_label ???); >FIND2' @refl
     613    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
     614      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
     615      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
     616      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
     617      | // ]|skip]|skip]|skip]
     618    ]
     619  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
     620    % [2: % [2: % [2: % [
     621      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
     622      @refl | // ] |skip ]| skip ]| skip ]
     623  ]
     624| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
     625  whd in match (find_label ?? k); normalize in match (find_label ?? k');
     626  @(lfl_IH s0 … IH) [ /2/ ]
     627  cases (find_label ???)
     628  [ whd in ⊢ (% → %); #FIND1'
     629    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
     630  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
     631    % [2: % [2: % [2: % [
     632      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
     633      @refl | // ]| skip ]| skip ]| skip ]
     634  ]
     635| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
     636  whd in match (find_label ?? k); normalize in match (find_label ?? k');
     637  @(lfl_IH s0 … IH) [ /2/ ]
     638  cases (find_label ???)
     639  [ whd in ⊢ (% → %); #FIND1'
     640    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
     641  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
     642    % [2: % [2: % [2: % [
     643      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
     644      @refl | // ]| skip ]| skip ]| skip ]
     645  ]
     646| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
     647  whd in match (find_label ???); normalize in match (find_label ?? k');
     648  @(lfl_IH s1 … IH1) [ /2/ ]
     649  cases (find_label ???)
     650  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
     651    @(lfl_IH s3 … IH3) [ /2/ ]
     652    cases (find_label ???)
     653    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
     654      @(lfl_IH s2 … IH2) [ /2/ ]
     655      cases (find_label ???)
     656      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
     657      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
     658        % [2: % [2: % [2: % [
     659         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
     660        | // ]| skip ]| skip ]| skip ]
     661      ]
     662    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
     663        % [2: % [2: % [2: % [
     664        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
     665        | // ]| skip ]| skip ]| skip ]
     666    ]
     667  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
     668        % [2: % [2: % [2: % [
     669        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
     670        | // ]| skip ]| skip ]| skip ]
     671  ]
     672| //
     673| //
     674| #eo #k #k' #u @blindly_label #u1 //
     675| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
     676  normalize in match (find_label ???); normalize in match (find_label ???);
     677  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
     678  [ whd in ⊢ (% → %); //
     679  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
     680    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
     681  ]
     682| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
     683  whd in match (find_label ???); whd in match (find_label ?? k');
     684  cases (ident_eq lbl l)
     685  [ #E destruct whd
     686    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
     687  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
     688    normalize in match (find_label ?? k');
     689    @(lfl_IH s0 … IH) [ // ]
     690    cases (find_label ???)
     691    [ //
     692    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
     693      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
     694    ]
     695  ]
     696| //
     697| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
     698| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
     699  @label_gen_elim #u1 >shift_fst >shift_fst
     700  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
     701  @IH
     702| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
     703  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
     704  @label_gen_elim #u3 >shift_fst
     705  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
     706  @(lfl_IH s0 … IH1) [ /2/ ]
     707  cases (find_label ???)
     708  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
     709    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
     710    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
     711    | * #stl #ktl //
     712    ]
     713  | * #s0' #k0' whd in ⊢ (% → %);
     714    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
     715    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
     716  ]
     717] qed.
     718
     719lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
     720  cont_with_labels k k' →
     721  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
     722  ∃u',cs,k1'.
     723    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
     724    cont_with_labels k1 k1'.
     725#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
     726whd in match (label_function ?);
     727@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
     728lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
     729[ /2/ ]
     730>FIND //
     731qed.
     732
     733lemma step_with_labels : ∀ge,ge'.
     734  related_globals ge ge' →
     735  ∀s1,s1',tr,s2.
     736  state_with_labels s1 s1' →
     737  exec_step ge s1 = Value … 〈tr,s2〉 →
     738  ∃tr',s2'. plus ge' s1' tr' s2' ∧
     739            trace_with_extra_labels tr tr' ∧
     740            state_with_labels s2 s2'.
     741#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
     742[ #f #us #s #k #k' #e #m #KL cases s
     743  [ #EX inversion KL
     744    [ #E1 #E2 #_ destruct %{tr}
     745      whd in EX:(??%?);
     746      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
     747      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))}
     748        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
     749        | // ] | /2/ ]
     750      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     751      ]
     752    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
     753      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
     754      whd in EX:(??%%); destruct
     755      % [ % [ @plus_one @refl | // ] | /2/ ]
     756    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
     757      whd in EX:(??%%); destruct
     758      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_whilestate // ] | skip ]
     759    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     760      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
     761      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
     762      normalize in EXbrem; destruct
     763      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
     764      [ % [ 2: % [ 2: % [ % [ @plus_one
     765        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
     766        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
     767        whd in ⊢ (??%?); @refl
     768        | // ]
     769        | @swl_dowhilestate // ] | skip ] | skip ]
     770      | % [ 2: % [ 2: % [ % [ @plus_succ [
     771        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
     772           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
     773           whd in ⊢ (??%?); @refl
     774        | skip | skip
     775        | 5: @plus_succ [ 4: @refl | skip | skip
     776        | 5: @plus_one @refl | skip ] | skip ]
     777        | <(E0_right tr) @twel_app /2/ ]
     778        | /2/ ] | skip ] | skip ]
     779      ]
     780    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     781      whd in EX:(??%?); destruct
     782      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     783    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     784      whd in EX:(??%?); destruct
     785      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     786    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     787      whd in EX:(??%?); destruct
     788      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     789    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     790      whd in EX:(??%?); destruct
     791      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     792    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     793      whd in EX:(??%?);
     794      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
     795      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
     796        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
     797        @refl | // ] | /3/ ] | skip ]
     798      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     799      ]
     800    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     801      % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ]| skip ]| skip ]
     802    ]
     803  | * #a1 #ty1 #a2 #EX
     804    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
     805    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
     806    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
     807    whd in EX:(??%%); destruct
     808    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
     809    whd in match (label_statement ??);
     810    @label_gen_elim #ua1 @label_gen_elim #ua2
     811    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
     812    % [2: % [2: % [ % [
     813      @plus_one whd in ⊢ (??%?);     
     814      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
     815      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
     816      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
     817      @refl
     818    | @twel_app // ] | /2/ ] | skip ] | skip ]
     819  | * [2: * #er #tyr ] #ef #args #EX
     820    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     821    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
     822    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
     823    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
     824    whd in EX:(??%%);
     825    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
     826    destruct
     827    whd in match (label_statement ??);
     828    whd in match (label_opt_expr ??);
     829    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
     830    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
     831    @label_gen_elim #u1
     832    @label_gen_elim #u2
     833    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
     834    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
     835    % [2,4: % [2,4: % [1,3: % [1,3:
     836      @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
     837      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
     838      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
     839      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
     840      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
     841      @refl | *: @twel_app /2/ ] | *: @swl_callstate /2/ ] | *: skip ] | *: skip ]
     842  | #st1 #st2 #EX
     843    whd in EX:(??%%); destruct
     844    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
     845    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_state /2/ ] | skip ]
     846  | #a #st1 #st2 #EX
     847    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     848    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     849    normalize in EX; destruct
     850    whd in match (label_statement ??); @label_gen_elim #u1
     851    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
     852    @label_gen_elim #u5
     853    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
     854    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
     855    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     856    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
     857      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
     858      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
     859      whd in ⊢ (??%?); @refl
     860    | 1,2,6,7: skip
     861    | 5,10: @plus_one @refl
     862    | *: skip
     863    ]
     864    | 2,4: <(E0_right tr) @twel_app /2/
     865    ]| 2,4: /2/ ] | *: skip ] | *: skip ]
     866  | #a #st #EX
     867    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     868    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     869    normalize in EX; destruct
     870    whd in match (label_statement ??); @label_gen_elim #u1
     871    @label_gen_elim #u2
     872    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
     873    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
     874    >shift_fst
     875    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     876    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
     877      | 5,10: @plus_succ [ 4,9:
     878      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
     879      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
     880      whd in ⊢ (??%?); @refl
     881    | 1,2,6,7: skip
     882    | 5: @plus_one @refl
     883    | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     884    | *: skip
     885    ]
     886    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
     887    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
     888  | #a #st #EX
     889    normalize in EX; destruct
     890    whd in match (label_statement ??); @label_gen_elim #u1
     891    @label_gen_elim #u2
     892    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
     893    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
     894    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
     895      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
     896      | /2/ ] | /3/ ] | skip ] | skip ]
     897  | #st1 #a #st2 #st #EX
     898    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
     899    whd in EX:(??%?); >Eskip in EX; #EX
     900    whd in match (label_statement ??); @label_gen_elim #u1
     901    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
     902    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
     903    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
     904    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     905      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     906      normalize in EX; destruct
     907      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     908      % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
     909      | 5,10: @plus_succ [ 4,9:
     910      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
     911      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
     912      whd in ⊢ (??%?); @refl
     913      | 1,2,6,7: skip
     914      | 5: @plus_one @refl
     915      | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     916      | *: skip
     917      ]
     918      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
     919      ]| 2,4: /3/ ] | *: skip ] | *: skip ]
     920    | whd in EX:(??%%); destruct
     921      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
     922        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
     923        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_state /2/ ]
     924      | skip ] | skip ]
     925    ]
     926  | #EX inversion KL
     927    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     928    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     929    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     930    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     931    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     932    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     933    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     934    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     935    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     936    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     937    ]
     938    whd in match (label_statement ??);
     939    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
     940    [1,11,13: @plus_one @refl | 2,12,14: //
     941    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
     942    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
     943    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
     944    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
     945    ]| *: /2/ ]|*: skip]|*: skip ]
     946  | #EX inversion KL
     947    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     948    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     949    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     950    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     951    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     952    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     953    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     954    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     955    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     956    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     957    ]
     958    whd in match (label_statement ??);
     959    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
     960      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
     961      | *: // ] | *: /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
     962    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     963      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     964      normalize in EX; destruct
     965      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
     966      % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
     967        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
     968      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
     969      whd in ⊢ (??%?); @refl
     970      | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     971      | // | <(E0_right tr) @twel_app /2/
     972      ]
     973      | /3/ | /2/ ] | *: skip ] | *: skip ]
     974    ]
     975  | * [2: #a ] #EX
     976    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
     977    #Ety #EX whd in EX:(??%?);
     978    [ destruct
     979    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     980      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     981    | >Ety in EX; #EX
     982    | @⊥ cases (fn_return f) in Ety EX;
     983      [ * #H cases (H (refl ??))
     984      | *: normalize #a #b #c try #d try #e destruct
     985      ]
     986    ]
     987    whd in match (label_statement ??);
     988    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
     989    whd in EX:(??%%); destruct
     990    % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
     991      whd in ⊢ (??%?);
     992      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
     993        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     994      | >label_function_return >Ety in ⊢ (??%?);
     995      ] whd in ⊢ (??%?); @refl
     996      | *: // ]| *: @swl_returnstate /2/ ]|*:skip]|*:skip]
     997  | #a #ls #EX
     998    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     999    cases v1 in EX1 EX;
     1000    [ 2: #sz #i #EX1 #EX
     1001    | *: normalize #A #B try #C destruct
     1002    ]
     1003    whd in EX:(??%%); destruct
     1004    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     1005    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
     1006    % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
     1007      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
     1008      ]|skip ]| skip ]
     1009  | #l #st #EX
     1010    whd in EX:(??%?); destruct
     1011    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
     1012    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
     1013    %[2: %[2: %[ %[ @plus_succ
     1014      [ 4: @refl | 5: @plus_one @refl | *: skip ]
     1015      | /2/ ] | /2/ ] |skip ]| skip ]
     1016  | #l #EX
     1017    whd in EX:(??%?);
     1018    @blindly_label whd
     1019    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
     1020    cases (find_label ???) in ⊢ (???% → ?);
     1021    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
     1022    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
     1023      cases (label_find_label_fn … KL F)
     1024      #u' * #cs * #k1' * #F' #K'
     1025      % [2: %[2: %[ %[ @plus_succ
     1026        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
     1027        | /2/ ] | /2/ ] | skip ] | skip ]
     1028    ]
     1029  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
     1030    % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ] | skip ]| skip ]
     1031  ]
     1032| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     1033  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     1034  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     1035  whd in EX:(??%%); destruct
     1036  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
     1037  [ % [2: % [2: % [ % [
     1038    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     1039                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
     1040               |5: @plus_one @refl | *: skip ]
     1041    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
     1042  | % [2: % [2: % [ % [
     1043    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     1044                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
     1045    | 5: @plus_succ [4: @refl
     1046    | 5: @plus_one @refl | *: skip ] | *: skip ]
     1047    | <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip ]
     1048  ]
     1049| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     1050  whd in EX:(??%%); destruct
     1051  % [2: % [2: % [ % [
     1052    @plus_succ [4: % | 5: @plus_one % | *: skip ]
     1053    | /2/ ]| /3/ ]| skip ]| skip ]
     1054| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
     1055  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     1056  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     1057  whd in EX:(??%%); destruct
     1058  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
     1059  [ % [2: % [2: % [ % [
     1060    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     1061                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
     1062    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
     1063    | *: skip ]| <(E0_right tr) /3/ ] | /3/ ]| skip ]| skip ]
     1064  | % [2: % [2: % [ % [
     1065    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     1066                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
     1067    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
     1068    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip
     1069    ]
     1070  ]
     1071| #f #u * [ #s | #sz #i #s #ls ] #k #k' #e #m #K #EX
     1072  whd in EX:(??(??(??%???))?);
  • src/RTLabs/semantics.ma

    r1882 r1920  
    267267] qed.
    268268
    269 lemma bind_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
    270   (∀a. e = OK A a → f a = OK B v → P v) →
    271   (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
    272 #O #I #A #B *
    273 [ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
    274   [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ]
    275 | #m #f #v #P #H #E whd in E:(??%?); destruct
    276 ] qed.
    277 
    278 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
    279   (∀a. e = Value ??? a → f a = Value ??? v → P v) →
    280   (bindIO O I A B e f = Value ??? v → P v).
    281 #O #I #A #B *
    282 [ #o #k #f #v #P #H #E whd in E:(??%?); destruct
    283 | #a #f #v #P #H #E @H [ @a | @refl | @E ]
    284 | #m #f #v #P #H #E whd in E:(??%?); destruct
    285 ] qed.
    286 
    287269lemma eval_perserves : ∀ge,s,tr,s'.
    288270  eval_statement ge s = Value ??? 〈tr,s'〉 →
     
    296278  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    297279  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    298   | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
    299   | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    300   | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    301   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    302   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    303   | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    304   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     280  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
     281  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     282  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     283  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     284  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     285  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
     286  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    305287(*
    306   | #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    307   | #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     288  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     289  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    308290*)
    309   | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    310   | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
    311   | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
     291  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
     292  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
     293  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
    312294  ]
    313295| * #fn #args #retdst #stk #m #tr #s'
    314296  whd in ⊢ (??%? → ?);
    315   [ @bind_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
     297  [ @bind_res_value #loc #Eloc cases (alloc ? m O ??) #m' #b whd in ⊢ (??%? → ?);
    316298    #E destruct %3
    317299  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     
    319301| #v #r * [2: #f #fs ] #m #tr #s'
    320302  whd in ⊢ (??%? → ?);
    321   [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
     303  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
    322304    %5 cases f #func #locals #next #next_ok #sp #retdst %
    323305  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
  • src/common/AST.ma

    r1882 r1920  
    207207] qed.
    208208
     209lemma intsize_eq_elim_false : ∀A,sz,sz',P,p,f,d.
     210  sz ≠ sz' →
     211  intsize_eq_elim A sz sz' P p f d = d.
     212#A * * // #P #p #f #d * #H cases (H (refl ??))
     213qed.
    209214
    210215(* A type for the integers that appear in the semantics. *)
  • src/common/IOMonad.ma

    r1882 r1920  
    218218] qed.
    219219*)
     220
     221(* Inversion when injecting errors into IO monad. *)
     222lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     223  (∀a. e = OK A a → f a = OK B v → P v) →
     224  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     225#O #I #A #B *
     226[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
     227  [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ]
     228| #m #f #v #P #H #E whd in E:(??%?); destruct
     229] qed.
     230
     231lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     232  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
     233  (bindIO O I A B e f = Value ??? v → P v).
     234#O #I #A #B *
     235[ #o #k #f #v #P #H #E whd in E:(??%?); destruct
     236| #a #f #v #P #H #E @H [ @a | @refl | @E ]
     237| #m #f #v #P #H #E whd in E:(??%?); destruct
     238] qed.
Note: See TracChangeset for help on using the changeset viewer.