Changeset 3445


Ignore:
Timestamp:
Feb 17, 2014, 5:45:26 PM (5 years ago)
Author:
piccolo
Message:

correctness proof finished with a big open lemma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3416 r3445  
    687687include "Simulation.ma".
    688688
    689 let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2)
     689let rec len (s : abstract_status) (st1 : s) (st2 : s) (t : raw_trace s st1 st2)
    690690on t : ℕ ≝
    691691match t with
    692692[ t_base s ⇒ O
    693 | t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1
     693| t_ind s1 s2 s3 l prf lt ⇒ S (len … lt)
    694694].
    695695(*
     
    11621162qed.
    11631163
     1164definition fresh_for_prog_aux : ∀p,p'.Program p p' → ℕ → ℕ ≝
     1165λp,p',prog,n.foldl … (λn,i.max n (compute_max_n … (f_body … i))) n (env … prog).
     1166
     1167include alias "arithmetics/nat.ma".
     1168
     1169lemma max_1 : ∀n,m,k.k ≤ m → k ≤ max m n.
     1170#m #n #k #H normalize @leb_elim // normalize nodelta #H1
     1171/2 by transitive_le/
     1172qed.
     1173
     1174lemma max_2 : ∀n,m,k.k≤ n → k ≤ max m n.
     1175#m #n #k #H normalize @leb_elim // #H1 normalize nodelta
     1176@(transitive_le … H) @(transitive_le … (not_le_to_lt … H1)) //
     1177qed.
     1178
     1179lemma fresh_aux_ok : ∀p,p'.∀prog : Program p p'.∀n,m.n ≤ m →
     1180fresh_for_prog_aux … prog n ≤ fresh_for_prog_aux … prog m.
     1181#p #p' * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (?%%);
     1182@IH whd in ⊢ (?%?); @leb_elim normalize nodelta
     1183[ #H1 @max_2 // | #_ @max_1 // ]
     1184qed.
     1185
    11641186definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝
    1165 λp,p',prog.foldl … (λn,i.max n (compute_max_n … (f_body … i)))
    1166 (compute_max_n … (main … prog)) (env … prog).
     1187λp,p',prog.fresh_for_prog_aux … prog
     1188(compute_max_n … (main … prog)).
    11671189
    11681190definition translate_env ≝
     
    13441366
    13451367definition labels_of_prog : ∀p,p'.Program p p' → ? ≝
    1346 λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) [ ] (env … prog).
     1368λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x)))
     1369 (get_labels_of_code … (main … prog)) (env … prog).
    13471370
    13481371lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) =
    13491372(cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2).
    1350 #l1 #l2 @(sym_eq … (map_append …)) qed.
     1373#l1 #l2 @(sym_eq … (map_append …)) qed.
     1374
     1375include alias "arithmetics/nat.ma".
     1376
     1377
     1378lemma is_fresh_code : ∀p.∀i : Instructions p.
     1379is_fresh_for_return (get_labels_of_code … i) (compute_max_n … i).
     1380#p #main  elim main //
     1381[ #seq * [| * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH)
     1382  inversion(leb ? lbl) // @leb_elim #Hlbl #EQ destruct normalize nodelta
     1383  /2 by le_S/
     1384| #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (?%%);
     1385  @fresh_append
     1386  [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 @max_1 //
     1387  | @fresh_append
     1388    [ @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_1 @max_2 //
     1389    | @(fresh_keep_n_ok … IH3) @le_S @max_1 @max_1 @max_2 //
     1390    ]
     1391  ]
     1392| #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (?%%); @fresh_append
     1393  [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 //
     1394  | @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_2 //
     1395  ]
     1396| #f #act_p * [| * #lbl] #i #IH whd in ⊢ (?%%); //
     1397  change with ([?]@?) in ⊢ (?%?); @fresh_append
     1398  [ whd % // @le_S @max_1 //
     1399  | @(fresh_keep_n_ok … IH) @le_S @max_2 //
     1400  ]
     1401| * #lin #io * #lout #i #IH whd in ⊢ (?%%); @(fresh_keep_n_ok … IH)
     1402  @le_S @max_1 @max_1 //
     1403]
     1404qed.
     1405
     1406lemma is_fresh_fresh_for_prog : ∀p,p'.∀prog : Program p p'.
     1407is_fresh_for_return (labels_of_prog … prog) (fresh_for_prog … prog).
     1408#p #p' * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (?%?);
     1409elim env // * #sig #cost #i #tail #IH  whd in ⊢ (?%?); @fresh_append
     1410[ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 //
     1411| @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta
     1412  whd in ⊢ (??%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(transitive_le …  IH1)
     1413  whd in ⊢ (??%); change with (fresh_for_prog_aux ?? (mk_Program ?? tl1 main) ?) in ⊢ (?%%);
     1414  @fresh_aux_ok @max_1 //
     1415]
     1416qed.
     1417
     1418lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2.
     1419#A #l1 elim l1 // #x #xs #IH #l2 #H %
     1420[ @memb_to_mem >H // >memb_hd //
     1421| @IH #y #H1 @H >memb_cons // >H1 //
     1422]
     1423qed.
     1424
     1425lemma memb_cast_return : ∀keep,x.x ∈ cast_return_to_cost_labels keep →
     1426∃ y.x = a_return_post y ∧ bool_to_Prop (y ∈ keep).
     1427#keep elim keep
     1428[ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels;
     1429whd in match (map ????); whd in match (memb ???); inversion(y==x)
     1430[ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd //
     1431| #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 //
     1432]
     1433qed.
     1434
     1435lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3.
     1436#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/
     1437qed.
     1438
     1439lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2.
     1440#A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y *
     1441[ #EQ destruct // | #H3 @IH // ]
     1442qed.
     1443
     1444lemma transitive_subset : ∀A.transitive … (subset A).
     1445#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 %
     1446[ @(subset_def_inv … H3) // | @IH // ]
     1447qed.
     1448
     1449lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2).
     1450#A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ]
     1451qed.
     1452
     1453lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3).
     1454#A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 %
     1455[ @mem_append_l2 // | @IH // ]
     1456qed.
     1457
     1458lemma lab_to_keep_in_prog : ∀p,p'.∀prog : Program p p'.
     1459∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 →
     1460(cast_return_to_cost_labels keep) ⊆ (labels_of_prog p p' prog).
     1461#p #p' * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta
     1462@pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct
     1463lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh
     1464lapply env1 -env1 generalize in match (fresh_for_prog ???); elim env
     1465[ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???);
     1466  @subset_def #x #H whd in match (labels_of_prog); normalize nodelta
     1467  whd in match (foldr ?????); cases(memb_cast_return … H) -H #x1 * #EQ1 #H destruct
     1468  @(lab_to_keep_in_domain … H)
     1469| #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim
     1470  * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail
     1471  change with (translate_env ????) in match (foldr ?????); #EQt_env_tail
     1472  normalize nodelta #EQ1 destruct >cast_return_append @subset_append
     1473  [ >cast_return_append @subset_append
     1474    [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
     1475      @subset_def #y #H cases(memb_cast_return … H) -H #y1 * #EQ destruct #H
     1476      >memb_append_l2 // @(lab_to_keep_in_domain … H)
     1477    | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
     1478      change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????);
     1479      @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
     1480      >cast_return_append @subset_append_h1 //
     1481    ]
     1482  | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
     1483    change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????);
     1484    @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
     1485     >cast_return_append @subset_append_h2 //
     1486  ]
     1487]
     1488qed.
     1489
     1490lemma fresh_call_post_trans_ok : ∀p.∀i : Instructions p.∀n,l.
     1491n ≤ fresh … (call_post_trans … i n l).
     1492#p #i elim i //
     1493qed.
     1494
     1495lemma fresh_translate_env_ok : ∀p,p'.∀env,t_env : list (env_item p p').∀n,n1,m,keep.
     1496translate_env … env n = 〈t_env,n1,m,keep〉 → n ≤ n1.
     1497#p #p' #env elim env
     1498[ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ]
     1499#x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?);
     1500change with (translate_env ????) in match (foldr ?????); @pair_elim
     1501* #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta
     1502#EQ destruct @(transitive_le … (IH … EQt_env_tail)) @fresh_call_post_trans_ok
     1503qed.
     1504 
    13511505
    13521506lemma trans_env_ok : ∀p : state_params.∀ prog.
     
    13881542      [ @(fresh_keep_n_ok … Hfresh1)
    13891543        @(fresh_for_subset … (labels_of_prog … prog))
    1390         cases daemon (*TODO*)
    1391        | cases daemon (*TODO*)
     1544        [ @(lab_to_keep_in_prog … EQkeep1) | @is_fresh_fresh_for_prog ]
     1545       | @(transitive_le … (fresh_translate_env_ok … EQtail)) //
    13921546      ]
    13931547    | whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta
     
    15221676qed.
    15231677
    1524 
     1678lemma len_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     1679∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
     1680len … (t1 @ t2) = len … t1 + len …  t2.
     1681#S #st1 #st2 #st3 #t1 elim t1 normalize //
     1682qed.
     1683
     1684axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y.
     1685  (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7)
     1686 →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9)
     1687 →is_permutation A
     1688   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
     1689   (((x ::l4 @y ::l3) @l8) @l9)).
    15251690
    15261691lemma correctness : ∀p,p',prog.
     
    16931858  [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ]
    16941859   #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
    1695    #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #_ #_
    1696    #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
    1697    inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l *
    1698    #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?); #EQ destruct
    1699    #IH1 #IH2 #st1' #abs_top #abs_tail
     1860   #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio
     1861   #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
     1862   inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l)
     1863   #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?);
     1864   #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail
    17001865    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
    17011866    #abs_top_cont #abs_tail_cont #EQcheck
     
    17041869    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    17051870    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
    1706     cases(H … EQenv_it) -H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans
     1871    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans
    17071872    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
    17081873    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
    17091874    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
    17101875    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
    1711     [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] cases(memb ???) normalize nodelta
     1876    [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l')
     1877    inversion(memb ???) normalize nodelta #Hlbl_keep'
    17121878    [ cases(?==?) normalize nodelta ]
    17131879     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    1714      xxxxxxx
    1715      
    1716      
    1717      
    1718           cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
    1719           [2: whd >EQcont12
    1720               change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
    1721               >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
    1722             whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
    1723             % // % // % // % [/5 by conj/] >EQcode12 <EQtrans
    1724             @(inverse_call_post_trans … fresh')
    1725             [2: % |*: [2,3: /2 by / ]
    1726                 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
    1727                 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
    1728                 #no_dup lapply(no_duplicates_append_r … no_dup) #H1
    1729                 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
    1730                 change with ([?]@?) in match (?::?); #H1
    1731                 lapply(no_duplicates_append_r … H1) >append_nil //
    1732             ]
     1880     cases(IH1
     1881            (mk_state ?
     1882              (f_body … env_it')
     1883              (〈ret_act (Some ? lbl'),i'〉 :: (cont … st1'))
     1884              (store ? st12) false)
     1885            (abs_top''@abs_tail_cont)
     1886            (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
     1887     [2: whd >EQcont12
     1888         change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
     1889          >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
     1890          whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta
     1891          % // % // % // % [/5 by conj/] >EQcode12 <EQtrans
     1892          @(inverse_call_post_trans … fresh')
     1893          [2: % |*: [2,3: /2 by / ]
     1894              cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
     1895              whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
     1896              #no_dup lapply(no_duplicates_append_r … no_dup) #H1
     1897              lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
     1898              change with ([?]@?) in match (?::?); #H1
     1899              lapply(no_duplicates_append_r … H1) >append_nil //
    17331900          ]
    1734           #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
    1735           %{abs_top'''}
    1736           %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    1737           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
    1738           %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1739           >EQlab_env_it >associative_append >associative_append
    1740           >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
    1741           >EQopt_l' in t'; #t'
    1742           whd in match (map_labels_on_trace ??); >EQgen_labels
    1743           whd in match (foldr ?????); >append_nil
    1744           whd in match (get_costlabels_of_trace ????);
    1745            @is_permutation_cons
    1746           >append_nil whd in match (append ???) in ⊢ (???%); //
    1747        
    1748 
    1749         ]
    1750     | whd in ⊢ (???% → ?); #EQ destruct
    1751     ]
    1752 |       
     1901     ]
     1902     #abs_top''' * #abs_tail''' * #st41' * #t1' ** #Hst41st41' #EQcosts #EQlen
     1903     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
     1904     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     1905     whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta
     1906     [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41'
     1907     change with (check_continuations ?????) in match (foldr2 ???????);
     1908     inversion(check_continuations ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     1909     ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind
     1910     normalize nodelta inversion(call_post_clean ?????) normalize nodelta
     1911     [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i'''
     1912     #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: cases daemon (*assurdi*)]
     1913     cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i')
     1914     [ cases daemon (*BIG LEMMA!!!*)]
     1915     ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta
     1916     >Hlbl_keep' normalize nodelta
     1917     whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ)
     1918     >EQcode41 in ⊢ (% → ?); inversion(code … st41')
     1919     [1,3,4,5,6,7: cases daemon (*ASSURDI*) ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
     1920     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
     1921     #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
     1922     #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ)
     1923     cases(IH2
     1924             (mk_state ? i' (cont … st1') (store … st42) (io_info … st42))
     1925             abs_tail_cont abs_top'''')
     1926     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
     1927     #abs_top_1 * #abs_tail_1 * #st5' * #t2' ** #Hst5_st5' #EQcosts'
     1928     #EQlen' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     1929     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
     1930     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
     1931     |2,4: skip
     1932     ]
     1933     % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
     1934           whd in ⊢ (??%%); @eq_f // ]
     1935     %{Hst5_st5'} whd in match (map_labels_on_trace ??);
     1936     change with (map_labels_on_trace ??) in match (foldr ?????);
     1937     >map_labels_on_trace_append >get_cost_label_append
     1938     whd in match (get_costlabels_of_trace ??? (t_ind …));
     1939     whd in match (get_costlabels_of_trace ??? (t_ind …));
     1940     >get_cost_label_append
     1941     whd in match (get_costlabels_of_trace ??? (t_ind …));
     1942     >map_labels_on_trace_append >EQlab_env_it >EQgen_labels
     1943     whd in match (map_labels_on_trace ? [ ]);
     1944     whd in match (append ? (nil ?) ?);
     1945     cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
     1946     >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
     1947]
     1948qed.
    17531949   
    17541950
Note: See TracChangeset for help on using the changeset viewer.