Changeset 3447 for LTS


Ignore:
Timestamp:
Feb 18, 2014, 5:43:19 PM (6 years ago)
Author:
piccolo
Message:

correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3446 r3447  
    265265
    266266
    267 definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2.
    268 (* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
     267definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2 ∧
    269268 match (code … s1) with
    270269 [ CALL f act_p r_lb i1 ⇒ code … s2 = i1
    271270 | _ ⇒ False
    272271 ].
    273 *)
    274272
    275273definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝
     
    16881686   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
    16891687   (((x ::l4 @y ::l3) @l8) @l9)).
     1688   
    16901689
    16911690lemma correctness : ∀p,p',prog.
     
    17001699is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
    17011700                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
    1702  len … t = len … t'.
     1701 len … t = len … t' ∧
     1702 ∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
     1703 cont … s1 = k @ cont … s2 →
     1704All … (λx.let 〈lab,i〉 ≝ x in ¬ is_unlabelled_ret_act lab) k →
     1705∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|.
    17031706#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    17041707#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
    17051708-abs_tail lapply s1' -s1' elim Hpre
    17061709[ #st #_ #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
    1707   % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    1708   @is_permutation_eq
     1710  %
     1711  [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
     1712    @is_permutation_eq
     1713  | #k #i #_ #EQcont_st #wf %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
     1714  ]
    17091715| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    17101716  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
     
    17391745         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
    17401746         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1741       #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
     1747      #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
    17421748      %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    17431749      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    17441750        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1745       %   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts
     1751      % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
     1752      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
     1753      [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
     1754      destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1755      #EQk1 #EQlength %{(〈cost_act (None ?),new_code'〉::k1)}
     1756      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    17461757    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
    17471758      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     
    17621773         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
    17631774         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1764       #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen
     1775      #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcost #EQlen #stack_safety
    17651776      %{abs_top'} %{abs_tail'} %{st3'}
    17661777      %{(t_ind … (cost_act (Some ? lbl)) … t')}
    17671778      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    17681779        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1769       % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
    1770       whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    1771       @is_permutation_cons assumption
     1780      % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
     1781          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
     1782          @is_permutation_cons assumption
     1783        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
     1784          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
     1785          destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1786          #EQk1 #EQlength %{(〈cost_act (Some ? lbl),new_code'〉::k1)}
     1787          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
     1788        ]
    17721789    ]
    17731790  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
     
    17931810    |2,5:
    17941811    ]
    1795     #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_top1}
     1812    #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1813    %{abs_top1}
    17961814    %{abs_tail1} %{s2'} %{(t_ind … t')}
    17971815    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
    17981816    |2,5:
    17991817    ]
    1800     % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
    1801     whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
    1802     whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
    1803     assumption
     1818    % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
     1819        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
     1820        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
     1821        assumption
     1822      |*: #k #i #EQcont_st3 >EQcont #EQ #H
     1823          cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
     1824      ]
    18041825  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18051826    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18241845        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18251846        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1826     ] #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcost #EQlen %{abs_top1} %{abs_tail1}
     1847    ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen
     1848      #stack_safety %{abs_top1} %{abs_tail1}
    18271849    %{s2'} %{(t_ind … t')}
    18281850    [ @hide_prf @(cond_true … EQcode_s1') //
    18291851    |
    18301852    ]
    1831     % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    1832     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    1833     >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    1834     assumption
     1853    %
     1854    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     1855      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
     1856      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
     1857      assumption
     1858    |  #k #i1 #EQcont_st3 #EQcont_st11 #H
     1859       cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
     1860       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     1861       * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
     1862       %{tl1} % // whd in EQk1 : (??%%); destruct //
     1863    ]
    18351864  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18361865    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18551884        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18561885        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1857     ] #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcost #EQlen %{abs_top1} %{abs_tail1}
    1858     %{s2'} %{(t_ind … t')}
     1886    ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen #stack_safety
     1887    %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    18591888    [ @hide_prf @(cond_false … EQcode_s1') //
    18601889    |
    18611890    ]
    1862     % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    1863     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    1864     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    1865     assumption
     1891    %
     1892    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     1893      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
     1894      >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
     1895      assumption
     1896    | #k #i1 #EQcont_st3 #EQcont_st11 #H
     1897      cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
     1898      [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     1899      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
     1900      %{tl1} % // whd in EQk1 : (??%%); destruct //
     1901    ]
    18661902 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    18671903   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    18871923       % //
    18881924   ]
    1889    #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
    1890    %{abs_tail1} %{s2'} %{(t_ind … t')}
     1925   #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1926   %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    18911927   [ @hide_prf @(loop_true … EQcode_s1') // |]
    1892    % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    1893    whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    1894     >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1895     @is_permutation_cons assumption
     1928   %
     1929   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     1930     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
     1931      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     1932     @is_permutation_cons assumption
     1933   | #k #i1 #EQcont_st3 #EQcont_st11 #H
     1934      cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …)
     1935      [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     1936      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
     1937      %{tl1} % // whd in EQk1 : (??%%); destruct //
     1938   ]
    18961939 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    18971940   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     
    19151958        % // % // % // % [2: %] //
    19161959   ]
    1917    #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
    1918    %{abs_tail1} %{s2'} %{(t_ind … t')}
     1960   #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1961   %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19191962   [ @hide_prf @(loop_false … EQcode_s1') // |]
    1920    % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    1921    whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    1922     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1923     @is_permutation_cons assumption
     1963   %
     1964   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     1965     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
     1966     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     1967     @is_permutation_cons assumption
     1968   | #k #i #EQcont_st3 <EQcont_st12 #EQ #H
     1969     cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
     1970   ]
    19241971 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    19251972   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     
    19421989       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    19431990   ]
    1944    #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
    1945    %{abs_tail1} %{s2'} %{(t_ind … t')}
     1991   #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1992   %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19461993   [ @hide_prf @(io_in … EQcode_s1') // |]
    1947    % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    1948    whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    1949     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1950     @is_permutation_cons assumption
     1994   %
     1995   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
     1996     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
     1997     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     1998     @is_permutation_cons assumption
     1999   | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2000      cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …)
     2001      [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2002      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
     2003      %{tl1} % // whd in EQk1 : (??%%); destruct //
     2004   ]
    19512005  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    19522006    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
     
    19792033  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    19802034  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    1981   #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen
     2035  #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    19822036  %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19832037  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    19842038  | ]
    1985   % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    1986   whd in match (get_costlabels_of_trace ????);
    1987   whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1988   whd in match (map_labels_on_trace ??); >EQget_el @is_permutation_cons
    1989   assumption
     2039  %
     2040  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
     2041    whd in match (get_costlabels_of_trace ????);
     2042    whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     2043    whd in match (map_labels_on_trace ??); >EQget_el @is_permutation_cons
     2044    assumption
     2045  | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%);
     2046    [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
     2047    destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     2048    #EQk1 #EQlength %{(〈ret_act (Some ? lbl1),i〉::k1)}
     2049    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
     2050  ]
    19902051| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    19912052  [1,2,3,4,5,6,7,9: cases daemon (*absurd!*)
     
    20312092            ]
    20322093          ]
    2033           #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
     2094          #abs_top''' * #abs_tail''' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
     2095          %{abs_top'''}
    20342096          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    2035           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
    2036           %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    2037           >EQlab_env_it >associative_append whd in match (append ???); >associative_append
    2038           >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
    2039           whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
    2040           >append_nil whd in match (append ???) in ⊢ (???%); //
     2097          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
     2098          %
     2099          [ % [2: whd in ⊢ (??%%); >EQlen %]
     2100            %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     2101            >EQlab_env_it >associative_append whd in match (append ???); >associative_append
     2102            >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
     2103            whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
     2104            >append_nil whd in match (append ???) in ⊢ (???%); //
     2105          | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2106            cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …)
     2107            [2: >EQcont12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2108            * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
     2109            %{tl1} % // whd in EQk1 : (??%%); destruct //
     2110          ]
    20412111        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    20422112        ]
     
    20542124   #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
    20552125   inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l)
    2056    #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?);
     2126   #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); * #EQcont11_42 >EQcode11 in ⊢ (% → ?);
     2127   normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?);
    20572128   #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail
    20582129    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
     
    20932164          ]
    20942165     ]
    2095      #abs_top''' * #abs_tail''' * #st41' * #t1' ** #Hst41st41' #EQcosts #EQlen
     2166     #abs_top''' * #abs_tail''' * #st41' * #t1' *** #Hst41st41' #EQcosts #EQlen #stack_safety1
    20962167     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
    20972168     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     
    21052176     #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: cases daemon (*assurdi*)]
    21062177     cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i')
    2107      [ cases daemon (*BIG LEMMA!!!*)]
     2178     [ cases(stack_safety1 [ ] …)
     2179       [3: >EQcont41 in ⊢ (??%?); % |4: normalize // |5: % |2:] * [|#x #xs] *
     2180       whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct > EQcont_st41' in EQ1;
     2181       #EQ destruct(EQ) /3 by conj/
     2182     ]
    21082183     ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta
    21092184     >Hlbl_keep' normalize nodelta
     
    21182193             abs_tail_cont abs_top'''')
    21192194     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2120      #abs_top_1 * #abs_tail_1 * #st5' * #t2' ** #Hst5_st5' #EQcosts'
    2121      #EQlen' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2195     #abs_top_1 * #abs_tail_1 * #st5' * #t2' *** #Hst5_st5' #EQcosts'
     2196     #EQlen'  #stack_safety2 %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    21222197     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    21232198     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
    21242199     |2,4: skip
    21252200     ]
    2126      % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
     2201     %
     2202     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
    21272203           whd in ⊢ (??%%); @eq_f // ]
    2128      %{Hst5_st5'} whd in match (map_labels_on_trace ??);
    2129      change with (map_labels_on_trace ??) in match (foldr ?????);
    2130      >map_labels_on_trace_append >get_cost_label_append
    2131      whd in match (get_costlabels_of_trace ??? (t_ind …));
    2132      whd in match (get_costlabels_of_trace ??? (t_ind …));
    2133      >get_cost_label_append
    2134      whd in match (get_costlabels_of_trace ??? (t_ind …));
    2135      >map_labels_on_trace_append >EQlab_env_it >EQgen_labels
    2136      whd in match (map_labels_on_trace ? [ ]);
    2137      whd in match (append ? (nil ?) ?);
    2138      cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
    2139      >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
     2204       %{Hst5_st5'} whd in match (map_labels_on_trace ??);
     2205       change with (map_labels_on_trace ??) in match (foldr ?????);
     2206       >map_labels_on_trace_append >get_cost_label_append
     2207       whd in match (get_costlabels_of_trace ??? (t_ind …));
     2208       whd in match (get_costlabels_of_trace ??? (t_ind …));
     2209       >get_cost_label_append
     2210       whd in match (get_costlabels_of_trace ??? (t_ind …));
     2211       >map_labels_on_trace_append >EQlab_env_it >EQgen_labels
     2212       whd in match (map_labels_on_trace ? [ ]);
     2213       whd in match (append ? (nil ?) ?);
     2214       cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
     2215       >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
     2216     | #k #i #EQcont_st3 #EQ #H
     2217       cases(stack_safety2 … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
     2218     ]
    21402219]
    21412220qed.
Note: See TracChangeset for help on using the changeset viewer.