 Timestamp:
 Dec 23, 2013, 1:29:34 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3408 r3409 1182 1182 1183 1183 1184 lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A. 1185 no_duplicates … (l1 @ l2) → 1186 no_duplicates … (l2 @ l1). 1187 #A #l1 elim l1 1188 [ #l2 >append_nil //] 1189 #x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 H1 IH H2 1190 elim l2 l1 1191 [ >append_nil #H1 #H2 % // ] 1192 #y #ys #IH * #H1 * #H2 #H3 % 1193 [2: @IH 1194 [ % #H4 @H1 cases(memb_append … H4) 1195 [ #H5 >memb_append_l1 // 1196  #H5 >memb_append_l2 // @orb_Prop_r >H5 // 1197 ] 1198  // 1199 ] 1200  % #H4 cases(memb_append … H4) 1201 [ #H5 @(absurd ?? H2) >memb_append_l1 // 1202  whd in match (memb ???); inversion(y==x) 1203 [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 // 1204  #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 // 1205 ] 1206 ] 1207 ] 1208 qed. 1209 1210 1184 1211 lemma trans_env_ok : ∀p : state_params.∀ prog. 1185 1212 no_duplicates_labels … prog → … … 1214 1241 [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab Hhd_lab #Hhd_lab cases Hhd_lab 1215 1242 >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] 1216 normalize nodelta @get_element_append_l1 % #H1 cases daemon (* needs lemma on maps using EQtail *)] 1243 normalize nodelta @get_element_append_l1 % #H1 1244 (* subproof with no nice statement *) 1245 lapply H1 H1 lapply H H lapply Hhd_lab Hhd_lab lapply EQtail EQtail 1246 generalize in match (foldl ?????); lapply env_tail env_tail lapply fresh_tail 1247 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail IH elim tail 1248 normalize nodelta 1249 [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); 1250 #EQ destruct(EQ) whd in match (foldr ?????); 1251 #H1 #H2 * ] 1252 #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); 1253 whd in match (foldr ?????); 1254 @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres 1255 normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); 1256 #H1 #H2 whd in match (memb ???); inversion(x == ?) 1257 [ #H3 #_ <(\P H3) in H2; change with ([?]@?) in match (?::?); #H2 1258 lapply(no_duplicates_append_commute … H2) H2 ** #ABS #_ @ABS 1259 >memb_append_l2 // >Hx % 1260  #H3 normalize nodelta #H4 @(IH … EQres) 1261 [3: >domain_of_associative_list_append in H4; #H4 cases(memb_append … H4) [2: #EQ >EQ %] 1262 #ABS @⊥ @(memb_no_duplicates_append … x … H2) // @orb_Prop_r >memb_append_l1 // 1263 @(lab_map_in_domain … (eq_true_to_b … ABS)) 1264  % #ABS elim H1 H1 #H1 @H1 cases(memb_append … ABS) 1265 [ #H5 >memb_append_l1 // 1266  #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // 1267 ] 1268  lapply(no_duplicates_append_commute … H2) * #_ >associative_append 1269 #h @no_duplicates_append_commute @(no_duplicates_append_r … h) 1270 ] 1271 ] 1272 ] 1217 1273  whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … x … H) 1218 // cases daemon (*using EQtail in a non trivial way*) 1274 // @⊥ 1275 (* subproof with no nice statement *) 1276 lapply ABS ABS lapply H H lapply Hhd_lab Hhd_lab lapply EQtail EQtail 1277 generalize in match (foldl ?????); lapply env_tail env_tail lapply fresh_tail 1278 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail IH elim tail 1279 normalize nodelta 1280 [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); 1281 #EQ destruct(EQ) whd in match (foldr ?????); 1282 #H1 #H2 whd in ⊢ (??%? → ?); #EQ destruct ] 1283 #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); 1284 whd in match (foldr ?????); 1285 @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres 1286 normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); 1287 #H1 #H2 #H3 cases(memb_append … H3) H3 1288 [ #H3 change with ([?]@?) in match (?::?) in H2; 1289 lapply(no_duplicates_append_commute … H2) H2 * #_ #H4 @(memb_no_duplicates_append … x … H4) 1290 [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) % 1291  // 1292 ] 1293  #H3 normalize nodelta @(IH … EQres) 1294 [3: // 1295  % #ABS elim H1 H1 #H1 @H1 cases(memb_append … ABS) 1296 [ #H5 >memb_append_l1 // 1297  #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // 1298 ] 1299  lapply(no_duplicates_append_commute … H2) * #_ >associative_append 1300 #h @no_duplicates_append_commute @(no_duplicates_append_r … h) 1301 ] 1302 ] 1219 1303 ] 1220 1304  #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) … … 1271 1355 ] 1272 1356 ] 1273 qed. 1357 qed. 1274 1358 1275 1359
Note: See TracChangeset
for help on using the changeset viewer.