Changeset 3535 for LTS/Language.ma


Ignore:
Timestamp:
Mar 16, 2015, 4:30:28 PM (5 years ago)
Author:
piccolo
Message:

final statement of cerco with the first pass integrated in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3531 r3535  
    19591959          ] |1,4:]
    19601960    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    1961     ]
    1962   |*: cases daemon
    1963   ] cases daemon
    1964 qed.
    1965 
    1966 (*
    19671961  |
    19681962   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     
    20122006        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20132007        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2014     ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
    2015       #stack_safety #pre_t' %{abs_top1}
     2008    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen
     2009      #stack_safety #pre_t' #Hsil %{abs_top1}
    20162010    %{s2'} %{(t_ind … t')}
    20172011    [ @hide_prf @(cond_true … EQcode_s1') //
    20182012    |
    2019     ]
     2013    ] % [
    20202014    % [ %
    20212015    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    20302024    ]]
    20312025    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2026    ]
     2027    #h inversion h in ⊢ ?;
     2028    [#H1 #H2 #H3 #H4 #H5 #H6 destruct
     2029    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct
     2030    ]
    20322031  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    20332032    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    20752074        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20762075        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2077     ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
    2078     #pre_t'
     2076    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety
     2077    #pre_t' #Hsil
    20792078    %{abs_top1} %{s2'} %{(t_ind … t')}
    20802079    [ @hide_prf @(cond_false … EQcode_s1') //
    20812080    |
    2082     ]
     2081    ] % [
    20832082    % [ %
    20842083    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    20922091      %{tl1} % // whd in EQk1 : (??%%); destruct //
    20932092    ] ]
    2094     %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2093    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2094    #h inversion h in ⊢ ?;
     2095    [ #H21 #H22 #H23 #H24 #H25 #H26 destruct
     2096    | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
     2097    ]
    20952098 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    20962099   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    21402143       % //
    21412144   ]
    2142    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2143    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2144    [ @hide_prf @(loop_true … EQcode_s1') // |]
     2145   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2146   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2147   [ @hide_prf @(loop_true … EQcode_s1') // |] % [
    21452148   % [ %
    21462149   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    21542157      %{tl1} % // whd in EQk1 : (??%%); destruct //
    21552158   ] ]
    2156    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2159   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2160   #h inversion h in ⊢ ?;
     2161   [ #H41 #H42 #H43 #H44 #H45 #H46 destruct
     2162   | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
     2163   ]
    21572164 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    21582165   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    22002207        % // % // % // % [2: %] //
    22012208   ]
    2202    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2203    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2204    [ @hide_prf @(loop_false … EQcode_s1') // |]
     2209   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2210   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2211   [ @hide_prf @(loop_false … EQcode_s1') // |] % [
    22052212   % [ %
    22062213   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    22112218     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    22122219   ]]
    2213    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2220   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct]
     2221   #h inversion h in ⊢ ?;
     2222   [ #H61 #H62 #H63 #H64 #H65 #H66 destruct
     2223   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct
     2224   ]
    22142225 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    22152226   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     
    22572268       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    22582269   ]
    2259    #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2260    #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    2261    [ @hide_prf @(io_in … EQcode_s1') // |]
     2270   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2271   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
     2272   [ @hide_prf @(io_in … EQcode_s1') // |] % [
    22622273   % [ %
    22632274   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     
    22712282      %{tl1} % // whd in EQk1 : (??%%); destruct //
    22722283   ]]
    2273    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2284   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2285   #h inversion h in ⊢ ?;
     2286   [ #H81 #H82 #H83 #H84 #H85 #H86 destruct
     2287   | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct
     2288   ]
    22742289  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    22752290    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
     
    23412356   #r_t' #EQcode_s1'
    23422357  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    2343   #EQstore11 #EQio_11 #EQ destruct
     2358  #EQstore11 #EQio_111 #EQ destruct
    23442359  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    23452360  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2346   #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2347   #pre_t' %{abs_top1} %{s2'} %{(t_ind … t')}
     2361  #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2362  #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
    23482363  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    2349   | ]
     2364  | ] % [
    23502365  % [ %
    23512366  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     
    23602375    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    23612376  ]]
    2362   %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     2377  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
     2378  #h inversion h in ⊢ ?;
     2379  [ #H101 #H102 #H103 #H104 #H105 #H106 destruct
     2380  | #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct
     2381  ]
    23632382| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    23642383  [1,2,3,4,5,6,7,9:
     
    24372456            ]
    24382457          ]
    2439           #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
    2440           #pre_t' %{abs_top'''}
     2458          #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety
     2459          #pre_t' #Hsil %{abs_top'''}
    24412460          %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    2442           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
     2461          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [
    24432462          % [ %
    24442463          [ % [2: whd in ⊢ (??%%); >EQlen %]
     
    24552474          ]]
    24562475          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
     2476          ]
     2477          #h inversion h in ⊢ ?;
     2478          [ #H121 #H122 #H123 #H124 #H125 #H126 destruct
     2479          | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct
     2480          ]
    24572481        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    24582482        ]
     
    25562580          ]
    25572581     ]
    2558      #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
    2559      #pre_t1'
     2582     #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2583     #pre_t1' #Hsil1
    25602584     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
    25612585     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     
    26202644             abs_tail_cont abs_top'''')
    26212645     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2622      #abs_top_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
    2623      #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2646     #abs_top_1 * #st5' * #t2' ***** #Hst5_st5' #EQcosts'
     2647     #EQlen'  #stack_safety2 #pre_t2' #Hsil2 %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    26242648     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    26252649     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
    26262650     |2,4: skip
    2627      ]
     2651     ] % [
    26282652     % [ %
    26292653     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
     
    26532677       ]
    26542678     ]
    2655 ]
    2656 qed.
    2657 
    2658 *)
     2679  ] #h inversion h in ⊢ ?;
     2680  [ #H141 #H142 #H143 #H144 #H145 #H146 destruct
     2681  |#H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 destruct
     2682  ]
     2683
     2684qed.
     2685
    26592686
    26602687lemma silent_in_silent : ∀p,p',prog.
Note: See TracChangeset for help on using the changeset viewer.