Changeset 3446


Ignore:
Timestamp:
Feb 18, 2014, 12:03:54 PM (5 years ago)
Author:
piccolo
Message:

Correctness proof, closed all cases except the big lemma one

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3445 r3446  
    131131
    132132record sem_state_params (p : state_params) : Type[0] ≝
    133 { eval_seq : seq_instr p → state p → option (store_type p)
    134 ; eval_io : io_instr p → state p → option (store_type p)
    135 ; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
    136 ; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
     133{ eval_seq : seq_instr p → (store_type p) → option (store_type p)
     134; eval_io : io_instr p → store_type p → option (store_type p)
     135; eval_cond_cond : cond_instr p → store_type p → option (bool × (store_type p))
     136; eval_loop_cond : loop_instr p → store_type p → option (bool × (store_type p))
    137137; eval_call : signature p p → act_params_type p → store_type p → option (store_type p)
    138138; eval_after_return : return_type p → store_type p → option (store_type p)
     
    159159           (io_info … st = true → is_non_silent_cost_act (\fst hd)) →  (io_info … st') = false → ¬ is_ret_act (\fst hd) →  execute_l … (\fst hd) st st'
    160160| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
    161              eval_seq … p' i st = return s → (code ? st') = cd →
     161             eval_seq … p' i (store … st) = return s → (code ? st') = cd →
    162162             (cont … st) = (cont … st') → (store … st') = s →
    163163             io_info … st = false →  io_info ? st' = false → execute_l … (cost_act opt_l) st st'
    164164| cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
    165    (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈true,new_m〉 →
     165   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈true,new_m〉 →
    166166   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m →
    167167   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st'
    168168| cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m.
    169    (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈false,new_m〉 →
     169   (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈false,new_m〉 →
    170170   cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m →
    171171   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
    172172| loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
    173    code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈true,new_m〉 →
     173   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈true,new_m〉 →
    174174   cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) →
    175175   code … st' = i_true → store … st' = new_m → io_info … st = false →  io_info … st' = false →
    176176   execute_l … (cost_act (Some ? ltrue)) st st'
    177177| loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m.
    178    code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈false,new_m〉 →
    179    cont ? st' = cont … st → code … st' = i_false → store … st = store … st'
     178   code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈false,new_m〉 →
     179   cont ? st' = cont … st → code … st' = i_false → store … st' = new_m
    180180   io_info … st = false →  io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st'
    181181| io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd →
    182     eval_io … p' io st = return mem → code ? st' = EMPTY p →
     182    eval_io … p' io (store … st) = return mem → code ? st' = EMPTY p →
    183183    cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem →
    184184    io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st'
     
    17711771      @is_permutation_cons assumption
    17721772    ]
    1773   |  cases daemon (*TODO*)
    1774 (*     
    1775 |
    1776   #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    1777   #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont
    1778   #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
    1779   #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?);
    1780   inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2
    1781   [ >EQcont in ⊢ (% → ?); | >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta
    1782   *** #HH1 [ >EQcode11 in ⊢ (% → ?); | >EQcode11 in ⊢ (% → ?); ]
    1783   inversion(code … st3)
    1784   [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ]
    1785   #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
    1786   cases daemon *)
    1787   | cases daemon (*TODO*)
    1788   | cases daemon (*TODO*)
    1789   | cases daemon (*TODO*)
    1790   | cases daemon (*TODO*)
    1791   | cases daemon (*TODO*)
     1773  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
     1774    #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11
     1775    #_ #Hpre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
     1776    inversion(check_continuations ?????) normalize nodelta [1,3: #_ *]
     1777    ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
     1778    #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ]
     1779    inversion(code ??) [1,2,4,5,6,7,8,9,11,12,13,14: cases daemon (*assurdi*)]
     1780    #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?);
     1781    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
     1782    * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta
     1783    [2,4: #lab1 ] #EQ destruct(EQ)
     1784    [1,2: inversion(?==?) normalize nodelta #EQget_el ]
     1785    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1786    #EQstore #EQinfo #EQ destruct(EQ)
     1787    cases(IH … (mk_state ? i' (cont … s1') (store … st12) (io_info … s1')) abs_tail_cont ?)
     1788    [3,6: whd
     1789       [ <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
     1790       | <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
     1791       ]
     1792       normalize nodelta % // % // % // % // assumption
     1793    |2,5:
     1794    ]
     1795    #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_top1}
     1796    %{abs_tail1} %{s2'} %{(t_ind … t')}
     1797    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
     1798    |2,5:
     1799    ]
     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
     1804  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     1805    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     1806    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
     1807    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
     1808    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
     1809    [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     1810    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
     1811    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     1812    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
     1813    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     1814    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
     1815    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
     1816    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
     1817    #EQ destruct(EQ)
     1818    cases(IH …
     1819     (mk_state ? i_true1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
     1820     abs_tail_cont gen_lab_i_true')
     1821    [2: whd whd in match (check_continuations ?????);
     1822        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
     1823        change with (check_continuations ?????) in match (foldr2 ???????);
     1824        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
     1825        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
     1826    ] #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcost #EQlen %{abs_top1} %{abs_tail1}
     1827    %{s2'} %{(t_ind … t')}
     1828    [ @hide_prf @(cond_true … EQcode_s1') //
     1829    |
     1830    ]
     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
     1835  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     1836    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     1837    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
     1838    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
     1839    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
     1840    [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     1841    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
     1842    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     1843    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
     1844    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     1845    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
     1846    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
     1847    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
     1848    #EQ destruct(EQ)
     1849    cases(IH …
     1850     (mk_state ? ifalse1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
     1851     abs_tail_cont gen_lab_ifalse1)
     1852    [2: whd whd in match (check_continuations ?????);
     1853        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
     1854        change with (check_continuations ?????) in match (foldr2 ???????);
     1855        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
     1856        >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')}
     1859    [ @hide_prf @(cond_false … EQcode_s1') //
     1860    |
     1861    ]
     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
     1866 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
     1867   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     1868   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
     1869   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
     1870   [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     1871   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
     1872   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     1873   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
     1874   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
     1875   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
     1876   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
     1877   cases(IH …
     1878    (mk_state ? i_true1
     1879     (〈cost_act (None ?),LOOP … cond ltrue i_true1 lfalse i_false1〉 ::
     1880        cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_itrue1)
     1881   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
     1882       whd in match (foldr2 ???????);
     1883       change with (check_continuations ?????) in match (foldr2 ???????);
     1884       >EQcheck normalize nodelta whd in match (call_post_clean ?????);
     1885       >EQi_false2 normalize nodelta >EQi_true2 >m_return_bind >EQget_ltrue1
     1886       >EQget_lfalse1 normalize nodelta % // % // % // % [2: assumption] % //
     1887       % //
     1888   ]
     1889   #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
     1890   %{abs_tail1} %{s2'} %{(t_ind … t')}
     1891   [ @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
     1896 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
     1897   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
     1898   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
     1899   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
     1900   [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     1901   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
     1902   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     1903   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
     1904   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
     1905   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
     1906   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
     1907   cases(IH …
     1908    (mk_state ? i_false1
     1909     (cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_ifalse1)
     1910   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
     1911       whd in match (foldr2 ???????);
     1912       change with (check_continuations ?????) in match (foldr2 ???????);
     1913       >EQcheck normalize nodelta whd in match (call_post_clean ?????);
     1914       >EQi_false2 normalize nodelta >EQi_true2
     1915        % // % // % // % [2: %] //
     1916   ]
     1917   #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
     1918   %{abs_tail1} %{s2'} %{(t_ind … t')}
     1919   [ @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
     1924 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
     1925   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     1926   #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????)
     1927   [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
     1928   #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
     1929   [1,2,3,4,5,6: cases daemon (*ASSURDI*)] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
     1930   whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
     1931   [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta
     1932   [2: #_ #EQ destruct] #EQget_lout1 inversion(?==?) #EQget_lin1 normalize nodelta
     1933   whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1934   #EQstore11 #EQinfo11 #EQ destruct
     1935   cases(IH …
     1936    (mk_state ? (EMPTY p) (〈cost_act (Some ? lout),i1〉::cont … s1') (store … st12) true)
     1937    abs_tail_cont [ ])
     1938   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
     1939       whd in match (foldr2 ???????);
     1940       change with (check_continuations ?????) in match (foldr2 ???????);
     1941       >EQcheck normalize nodelta >EQ_i2 normalize nodelta % // % // % // %
     1942       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
     1943   ]
     1944   #abs_cont1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen %{abs_cont1}
     1945   %{abs_tail1} %{s2'} %{(t_ind … t')}
     1946   [ @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
    17921951  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    17931952    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
    1794   | cases daemon (*TODO absurd as above*)
     1953  | #r_t #mem #con #rb #i #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12
     1954    destruct #t #_ * #nf #EQ destruct
    17951955  ]
    1796 | cases daemon (*TODO*)
     1956| #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,8: cases daemon (*assurdi*)]
     1957  #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ)
     1958  #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6)
     1959  #t * #lbl #EQ destruct(EQ) #pre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
     1960  inversion(check_continuations …) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont
     1961  >EQcont_st11 in ⊢ (% → ?); inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
     1962  * #act_lab #i #cont_s1'' #_ #EQcont_s1' whd in ⊢ (??%% → ?);
     1963  change with (check_continuations ?????) in match (foldr2 ???????);
     1964  inversion(check_continuations ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     1965  ** #H2 #abs_top_cont' #abs_tail_cont' #EQcheck normalize nodelta
     1966  inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****]
     1967  * #gen_labs #i' #EQi' inversion act_lab normalize nodelta
     1968  [ #f #lab | * [| #lbl1 ]| * [| #nf_l] |] #EQ destruct(EQ)
     1969  [1,6: whd in ⊢ (??%% → ?); #EQ destruct *****
     1970  |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct
     1971  ]
     1972  whd in match ret_costed_abs; normalize nodelta
     1973  [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** #EQ destruct(EQ) ]
     1974  inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1975  ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?);
     1976  inversion(code … s1') [1,3,4,5,6,7: cases daemon (*TODO*) ] #r_t' #EQcode_s1'
     1977  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1978  #EQstore11 #EQio_11 #EQ destruct
     1979  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
     1980  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
     1981  #abs_top1 * #abs_tail1 * #s2' * #t' ** #Hst3_s2' #EQcosts #EQlen
     1982  %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     1983  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
     1984  | ]
     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
    17971990| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    17981991  [1,2,3,4,5,6,7,9: cases daemon (*absurd!*)
     
    19472140]
    19482141qed.
    1949    
    1950 
    1951          
    1952  
    1953  
    1954 cases daemon (*TODO*)
    1955 qed.
Note: See TracChangeset for help on using the changeset viewer.