Changeset 3409 for LTS/Language.ma


Ignore:
Timestamp:
Dec 23, 2013, 1:29:34 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3408 r3409  
    11821182
    11831183
     1184lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A.
     1185no_duplicates … (l1 @ l2) →
     1186no_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
     1190elim 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]
     1208qed.
     1209
     1210
    11841211lemma trans_env_ok : ∀p : state_params.∀ prog.
    11851212no_duplicates_labels … prog →
     
    12141241    [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab
    12151242        >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    ]
    12171273  | 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    ]
    12191303  ]
    12201304| #Hf #Henv_it cases(IH … no_dup_tail … Henv_it)
     
    12711355         ]
    12721356]
    1273 qed.   
     1357qed.
    12741358
    12751359
Note: See TracChangeset for help on using the changeset viewer.