Changeset 3408 for LTS/Language.ma


Ignore:
Timestamp:
Dec 23, 2013, 11:46:37 AM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3407 r3408  
    10411041  | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on;
    10421042    <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?);
    1043     >associative_append in ⊢ (??%? → ?); #keep_on  @(same_to_keep_on_append … keep_on)
     1043    >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?);
     1044    #keep_on @(same_to_keep_on_append … keep_on) //
     1045    [ >associative_append >append_nil //
     1046    | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/
     1047    ]
     1048  | change with ([?;?]@?@?) in fresh_map : (?%??); <associative_append in fresh_map;
     1049    <(append_nil … (?@?)) change with ([?;?]@?@?) in ⊢ (??%? → ?);
     1050    <associative_append in ⊢ (??%? → ?); <(append_nil … (?@?)) in ⊢ (??%? → ?);
     1051    >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?);
     1052    #fresh_map @(same_fresh_map_on_append … fresh_map) //
     1053    [ >append_nil //
     1054    | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx)
     1055      [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ]
     1056      whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse
     1057      [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse %
     1058      | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue
     1059        [ #_ @orb_Prop_l >Hltrue %
     1060        | whd in match (memb ???); #EQ destruct
     1061        ]
     1062      ]
     1063    ]
     1064  | %
     1065  | cases no_dup #_ * #_ /2 by no_duplicates_append_r/
     1066  |
     1067  ]
     1068|*: cases daemon (*TODO*)
     1069]
    10441070qed.
    10451071
     
    11431169       (foldr  ?? (λx,acc. (f x) @ acc) seed l2).
    11441170#A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/
     1171qed.
     1172
     1173lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l).
     1174//
     1175qed.
     1176
     1177lemma eq_a_call_label :
     1178∀c1,c2.c1 == c2 → a_call c1 == a_call c2.
     1179#c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
     1180#EQ destruct >(\b (refl …)) @I
    11451181qed.
    11461182
     
    11981234        >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 //
    11991235        whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ]
    1200    % [2: #x #Hx <same_fresh_map // (*usare get_element_append_r1 *) cases daemon ]
    1201    % // % // % // <EQ_get_el (*usare get_element_append*) cases daemon
     1236   % [2: #x #Hx <same_fresh_map // >cons_append <associative_append @(get_element_append_r1)
     1237         % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
     1238         [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta
     1239           [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_
     1240               <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it)
     1241               #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
     1242               * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 //
     1243               >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) //
     1244               normalize nodelta >memb_append_l1 // >Hx %
     1245         | #ABS1 @(memb_no_duplicates_append … x … H)
     1246           [ @(lab_map_in_domain … (eq_true_to_b … ABS1))
     1247           | cases(lookup_ok_append … Henv_it)
     1248             #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
     1249             >memb_append_l2 // >memb_append_l1 //
     1250             whd in ⊢ (??%?); cases(x==?) //
     1251             normalize nodelta >memb_append_l1 // >Hx %
     1252           ]
     1253         ]
     1254     ] 
     1255   % // % // % // <EQ_get_el >cons_append <associative_append
     1256   @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
     1257         [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab)
     1258           #EQ_hdlab normalize nodelta
     1259           [2: whd in ⊢ (??%? → ?); #EQ destruct ] 
     1260           #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it)
     1261           #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
     1262           * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 //
     1263           >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) //
     1264         | #ABS1 @(memb_no_duplicates_append … (a_call (f_lab … new_env_it)) … H)
     1265           [ @(lab_map_in_domain … (eq_true_to_b … ABS1))
     1266           | cases(lookup_ok_append … Henv_it)
     1267             #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
     1268             >memb_append_l2 // >memb_append_l1 //
     1269             whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) //
     1270           ]
     1271         ]
    12021272]
    12031273qed.   
Note: See TracChangeset for help on using the changeset viewer.