Changeset 3531 for LTS/Language.ma


Ignore:
Timestamp:
Mar 13, 2015, 6:42:58 PM (5 years ago)
Author:
piccolo
Message:

new notion of measurable: some lemmas are still broken

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3527 r3531  
    17041704qed.
    17051705   
    1706 
    17071706lemma correctness_lemma : ∀p,p',prog.
    17081707no_duplicates_labels … prog →
     
    17121711pre_measurable_trace … t →
    17131712state_rel … m keep abs_top abs_tail s1 s1' →
    1714 ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
    1715 state_rel  … m keep abs_top' abs_tail' s2 s2' ∧
     1713∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     1714state_rel  … m keep abs_top' abs_tail s2 s2' ∧
    17161715is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
    1717                  (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
     1716                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail) ∧
    17181717 len … t = len … t' ∧
    17191718 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
    17201719 cont … s1 = k @ cont … s2 →
    17211720∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
    1722 ∧ pre_measurable_trace … t'.
     1721∧ pre_measurable_trace … t' ∧
     1722(pre_silent_trace … t → pre_silent_trace … t').
    17231723#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    17241724#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
    17251725-abs_tail lapply s1' -s1' elim Hpre
    1726 [ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
    1727   %
     1726[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{s1'} %{(t_base …)}
     1727  cut(? : Prop)
     1728  [3: #Hpre' %
    17281729  [ %
     1730   [ %
    17291731    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    17301732      @is_permutation_eq
    17311733    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
    17321734    ]
    1733   | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
     1735  | @Hpre'
     1736  ]
     1737 | #_ %1 /2 by head_of_premeasurable_is_not_io/
     1738 ]
     1739 | skip
     1740 ]
     1741   %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
    17341742    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
    17351743    inversion(code ??) normalize nodelta
     
    17401748    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    17411749    normalize in Hst; <e1 in Hst; normalize nodelta //
    1742   ]   
    17431750| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    17441751  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
     
    17891796         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
    17901797         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1791       #abs_top' * #abs_tail' * #st3' * #t' ****
    1792       #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t'
    1793       %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
     1798      #abs_top' * #st3' * #t' *****
     1799      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' #Hsil
     1800      %{abs_top'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    17941801      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    17951802        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1796       %
     1803      % [ %
    17971804      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
    17981805      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
     
    18021809      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
    18031810      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
    1804       normalize in class_st11; >EQcode11 in class_st11; //
     1811      normalize in class_st11; >EQcode11 in class_st11; // ]
     1812      #H inversion H in ⊢ ?;
     1813      [ #H1 #H2 #H3 #H4 #H5 #H6 destruct ] #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
     1814      destruct %2
     1815      [ % whd in ⊢ (??%% → ?); >EQcodes1' normalize nodelta <EQio11 inversion(io_info … H8)
     1816        normalize nodelta [2: #_ #EQ destruct] #ABS lapply class_st11 whd in match (as_classify ??);
     1817        >EQcode11 normalize nodelta >ABS normalize nodelta * /2/
     1818      ]
     1819      @Hsil //
    18051820    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
    18061821      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     
    18391854           ]
    18401855      ]
    1841       #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
     1856      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore1 #EQio #EQ destruct(EQ)
    18421857      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
    18431858      [2: whd whd in match check_continuations; normalize nodelta
     
    18451860         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
    18461861         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1847       #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety
    1848       #pre_t'
    1849       %{abs_top'} %{abs_tail'} %{st3'}
     1862      #abs_top' * #st3' * #t' ***** #Hst3st3' #EQcost #EQlen #stack_safety
     1863      #pre_t' #Hsil
     1864      %{abs_top'} %{st3'}
    18501865      %{(t_ind … (cost_act (Some ? lbl)) … t')}
    18511866      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    18521867        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1853       %
     1868     cut(? : Prop)
     1869     [3: #Hpre' %
     1870      [ %
    18541871      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
    18551872          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
    18561873          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    1857           @is_permutation_cons assumption
     1874          @is_permutation_cons @EQcost
    18581875        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    18591876          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
     
    18621879          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    18631880        ]]
     1881      @Hpre' ]
     1882      #h inversion h in ⊢ ?; [ #H21 #H22 #H23 #H24 #H25 #H26 destruct]
     1883      #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
     1884      |skip |
    18641885      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
    18651886      normalize in class_st11; >EQcode11 in class_st11; //
    1866     ]
     1887    ]]
    18671888  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
    18681889    #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11
     
    19141935    |2,5:
    19151936    ]
    1916     #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1917     #pre_t' %{abs_top1}
    1918     %{abs_tail1} %{s2'} %{(t_ind … t')}
     1937    #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1938    #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
    19191939    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
    19201940    |2,5:
    19211941    ]
    1922     % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
     1942    cut(? : Prop)
     1943    [3,6: #Hpre'
     1944       %
     1945   
     1946    [1,3: % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f @EQlen ] %{Hst3_s2'} [2: @EQcosts]
    19231947        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
    19241948        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
    1925         assumption
     1949        @EQcosts
    19261950      |*: #k #i #EQcont_st3 >EQcont #EQ
    19271951          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    19281952      ]]
     1953      @Hpre'
     1954      |*: #h inversion h in ⊢ ?;
     1955          [1,3: #H41 #H42 #H43 #H44 #H45 #H46 destruct
     1956          |*: #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
     1957              %2 [ /2 by head_of_premeasurable_is_not_io/ ] @Hsil //
     1958          ]
     1959          ] |1,4:]
    19291960    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    1930   | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     1961    ]
     1962  |*: cases daemon
     1963  ] cases daemon
     1964qed.
     1965
     1966(*
     1967  |
     1968   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    19311969    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
    19321970    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
     
    19742012        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    19752013        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1976     ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
    1977       #stack_safety #pre_t' %{abs_top1} %{abs_tail1}
     2014    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
     2015      #stack_safety #pre_t' %{abs_top1}
    19782016    %{s2'} %{(t_ind … t')}
    19792017    [ @hide_prf @(cond_true … EQcode_s1') //
     
    20372075        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20382076        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2039     ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
     2077    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
    20402078    #pre_t'
    2041     %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2079    %{abs_top1} %{s2'} %{(t_ind … t')}
    20422080    [ @hide_prf @(cond_false … EQcode_s1') //
    20432081    |
     
    21022140       % //
    21032141   ]
    2104    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2105    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2142   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2143   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    21062144   [ @hide_prf @(loop_true … EQcode_s1') // |]
    21072145   % [ %
     
    21622200        % // % // % // % [2: %] //
    21632201   ]
    2164    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2165    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2202   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2203   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    21662204   [ @hide_prf @(loop_false … EQcode_s1') // |]
    21672205   % [ %
     
    22192257       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    22202258   ]
    2221    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2222    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2259   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2260   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    22232261   [ @hide_prf @(io_in … EQcode_s1') // |]
    22242262   % [ %
     
    23062344  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    23072345  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2308   #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2309   #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2346  #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2347  #pre_t' %{abs_top1} %{s2'} %{(t_ind … t')}
    23102348  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    23112349  | ]
     
    23992437            ]
    24002438          ]
    2401           #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
     2439          #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
    24022440          #pre_t' %{abs_top'''}
    2403           %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
     2441          %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    24042442          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
    24052443          % [ %
     
    25182556          ]
    25192557     ]
    2520      #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2558     #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
    25212559     #pre_t1'
    25222560     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
     
    25762614     ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
    25772615     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
    2578      #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
     2616     #EQ1 >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
    25792617     #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ)
    25802618     cases(IH2
     
    25822620             abs_tail_cont abs_top'''')
    25832621     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2584      #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
    2585      #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     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')))}
    25862624     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    25872625     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
     
    26172655]
    26182656qed.
     2657
     2658*)
     2659
     2660lemma silent_in_silent : ∀p,p',prog.
     2661no_duplicates_labels … prog →
     2662let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     2663∀s1,s2,s1' : state p.∀abs_top,abs_tail.
     2664∀t : raw_trace (operational_semantics … p' prog) s1 s2.
     2665silent_trace … t →
     2666state_rel … m keep abs_top abs_tail s1 s1' →
     2667∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     2668state_rel  … m keep abs_top' abs_tail s2 s2' ∧
     2669silent_trace … t'.
     2670#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
     2671#s1 #s2 #s1' #abs_top #abs_tail #t *
     2672[2: cases t -s1 -s2 [2: #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 cases H87 #H cases(H I)]
     2673#st #_ #H %{abs_top} %{s1'} %{(t_base …)} % // %2 % * ]
     2674#H #H1 lapply(correctness_lemma p p' prog no_dup) >EQt_prog normalize nodelta #H2
     2675cases(H2 … (pre_silent_is_premeasurable … H) … H1)  -H2 #abs_top' * #s2' * #t' ***** #REL'
     2676#_ #_ #_ #_ #H2 %{abs_top'} %{s2'} %{t'} %{REL'} % @H2 //
     2677qed.
Note: See TracChangeset for help on using the changeset viewer.