Changeset 2448 for src/Clight/frontend_misc.ma
 Timestamp:
 Nov 9, 2012, 4:38:02 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2441 r2448 1290 1290 @lset_eq_concrete_cons >nil_append >nil_append 1291 1291 @Hind 1292  1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta1293 >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%));1294 @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl'))1295 [ 1: @Hind1296  2: %21297  3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ]1298 ]1292  1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta 1293 >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%)); 1294 @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl')) 1295 [ 1: @Hind 1296  2: %2 1297  3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ] 1298 ] 1299 1299 ] qed. 1300 1300 … … 1417 1417 qed. 1418 1418 1419 1420 1419 (* Additional lemmas on lsets *) 1420 1421 lemma lset_difference_empty : 1422 ∀A : DeqSet. 1423 ∀s1. lset_difference A s1 [ ] = s1. 1424 #A #s1 elim s1 try // 1425 #hd #tl #Hind >lset_difference_unfold >Hind @refl 1426 qed. 1427 1428 lemma lset_not_mem_difference : 1429 ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3). 1430 #A #s1 #s2 #s3 #Hincl #x #Hmem 1431 lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3 1432 elim s1 in Hincl Hmem; 1433 [ 1: #_ * 1434  2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall * 1435 [ 2: #Hmem_x_tl @Hind assumption 1436  1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ] 1437 ] qed. 1438 1439 lemma lset_mem_inclusion_mem : 1440 ∀A,s1,s2,elt. 1441 mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2. 1442 #A #s1 elim s1 1443 [ 1: #s2 #elt * 1444  2: #hd #tl #Hind #s2 #elt * 1445 [ 1: #Heq destruct * // 1446  2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl; 1447 [ 1: #_ * 1448  2: #hd' #tl' #Hind * #Hmem' #Hall * 1449 [ 1: #Heq destruct @Hmem' 1450  2: #Hmem'' @Hind assumption ] ] ] ] 1451 qed. 1452 1453 lemma lset_remove_inclusion : 1454 ∀A : DeqSet. ∀s,elt. 1455 lset_inclusion A (lset_remove ? s elt) s. 1456 #A #s elim s try // qed. 1457 1458 lemma lset_difference_remove_inclusion : 1459 ∀A : DeqSet. ∀s1,s2,elt. 1460 lset_inclusion A 1461 (lset_difference ? (lset_remove ? s1 elt) s2) 1462 (lset_difference ? s1 s2). 1463 #A #s elim s try // qed. 1464 1465 lemma lset_difference_permute : 1466 ∀A : DeqSet. ∀s1,s2,s3. 1467 lset_difference A s1 (s2 @ s3) = 1468 lset_difference A s1 (s3 @ s2). 1469 #A #s1 #s2 elim s2 try // 1470 #hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute 1471 >Hind elim s3 try // 1472 #hd' #tl' #Hind' >cons_to_append >associative_append 1473 >associative_append >(cons_to_append … hd tl) 1474 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1475 >lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append 1476 <Hind' generalize in match (lset_difference ???); #foo 1477 whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?); 1478 whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%)); 1479 elim foo 1480 [ 1: normalize @refl 1481  2: #hd'' #tl'' #Hind normalize 1482 @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with 1483 [ true ⇒ λH. ? 1484  false ⇒ λH. ? 1485 ] (refl ? (hd''==hd'))) 1486 @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with 1487 [ true ⇒ λH'. ? 1488  false ⇒ λH'. ? 1489 ] (refl ? (hd''==hd))) 1490 normalize nodelta 1491 try @Hind 1492 [ 1: normalize >H normalize nodelta @Hind 1493  2: normalize >H' normalize nodelta @Hind 1494  3: normalize >H >H' normalize nodelta >Hind @refl 1495 ] qed. 1496 1497 1498 1499 lemma lset_disjoint_dec : 1500 ∀A : DeqSet. 1501 ∀s1,elt,s2. 1502 mem ? elt s1 ∨ mem ? elt (lset_difference A (elt :: s2) s1). 1503 #A #s1 #elt #s2 1504 @(match elt ∈ s1 return λx. ((elt ∈ s1) = x) → ? 1505 with 1506 [ false ⇒ λHA. ? 1507  true ⇒ λHA. ? ] (refl ? (elt ∈ s1))) 1508 [ 1: lapply (memb_to_mem … HA) #Hmem 1509 %1 @Hmem 1510  2: %2 elim s1 in HA; 1511 [ 1: #_ whd %1 @refl 1512  2: #hd1 #tl1 #Hind normalize in ⊢ (% → ?); 1513 >lset_difference_unfold 1514 >lset_difference_unfold2 1515 lapply (eqb_true ? elt hd1) whd in match (memb ???) in ⊢ (? → ? → %); 1516 cases (elt==hd1) normalize nodelta 1517 [ 1: #_ #Habsurd destruct 1518  2: #HA #HB >HB normalize nodelta %1 @refl ] ] ] 1519 qed. 1520 1521 lemma mem_filter : ∀A : DeqSet. ∀l,elt1,elt2. 1522 mem A elt1 (filter A (λx:A.¬x==elt2) l) → mem A elt1 l. 1523 #A #l elim l try // #hd #tl #Hind #elt1 #elt2 /2 by lset_mem_inclusion_mem/ 1524 qed. 1525 1526 lemma lset_inclusion_difference_aux : 1527 ∀A : DeqSet. ∀s1,s2. 1528 lset_inclusion A s1 s2 → 1529 (lset_eq A s2 (s1@lset_difference A s2 s1)). 1530 #A #s1 1531 @(WF_ind ????? (filtered_list_wf A s1)) 1532 * 1533 [ 1: #_ #_ #s2 #_ >nil_append >lset_difference_empty @reflexive_lset_eq 1534  2: #hd1 #tl1 #Hwf #Hind #s2 * #Hmem #Hincl 1535 lapply (Hind (filter ? (λx.¬x==hd1) tl1) ?) 1536 [ 1: whd normalize 1537 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta @refl ] 1538 #Hind_wf 1539 elim (list_mem_split ??? Hmem) #s2A * #s2B #Heq >Heq 1540 >cons_to_append in ⊢ (???%); >associative_append 1541 >lset_difference_unfold2 1542 >nil_append 1543 >lset_remove_split >lset_remove_split 1544 normalize in match (lset_remove ? [hd1] hd1); 1545 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1546 >nil_append <lset_remove_split >lset_difference_lset_remove_commute 1547 lapply (Hind_wf (lset_remove A (s2A@s2B) hd1) ?) 1548 [ 1: lapply (lset_inclusion_remove … Hincl hd1) 1549 >Heq @lset_inclusion_eq2 1550 >lset_remove_split >lset_remove_split >lset_remove_split 1551 normalize in match (lset_remove ? [hd1] hd1); 1552 >(proj2 … (eqb_true ? hd1 hd1) (refl ??)) normalize nodelta 1553 >nil_append @reflexive_lset_eq ] 1554 #Hind >lset_difference_lset_remove_commute in Hind; <lset_remove_split #Hind 1555 @lset_eq_concrete_to_lset_eq 1556 lapply (lset_eq_to_lset_eq_concrete … (cons_monotonic_eq … Hind hd1)) #Hindc 1557 @(square_lset_eq_concrete ????? Hindc) Hindc Hind 1558 [ 1: @(transitive_lset_eq_concrete ?? ([hd1]@s2A@s2B) (s2A@[hd1]@s2B)) 1559 [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete 1560  1: @lset_eq_to_lset_eq_concrete @lset_eq_filter ] 1561  2: @lset_eq_to_lset_eq_concrete @(transitive_lset_eq A … (lset_eq_filter ? ? hd1 …)) 1562 elim (s2A@s2B) 1563 [ 1: normalize in match (lset_difference ???); @reflexive_lset_eq 1564  2: #hd2 #tl2 #Hind >lset_difference_unfold >lset_difference_unfold 1565 @(match (hd2∈filter A (λx:A.¬x==hd1) tl1) 1566 return λx. ((hd2∈filter A (λx:A.¬x==hd1) tl1) = x) → ? 1567 with 1568 [ false ⇒ λH. ? 1569  true ⇒ λH. ? 1570 ] (refl ? (hd2∈filter A (λx:A.¬x==hd1) tl1))) normalize nodelta 1571 [ 1: lapply (memb_to_mem … H) #Hfilter >(mem_to_memb … (mem_filter … Hfilter)) 1572 normalize nodelta @Hind 1573  2: @(match (hd2∈tl1) 1574 return λx. ((hd2∈tl1) = x) → ? 1575 with 1576 [ false ⇒ λH'. ? 1577  true ⇒ λH'. ? 1578 ] (refl ? (hd2∈tl1))) normalize nodelta 1579 [ 1: (* We have hd2 = hd1 *) 1580 cut (hd2 = hd1) 1581 [ elim tl1 in H H'; 1582 [ 1: normalize #_ #Habsurd destruct (Habsurd) 1583  2: #hdtl1 #tltl1 #Hind normalize in ⊢ (% → % → ?); 1584 lapply (eqb_true ? hdtl1 hd1) 1585 cases (hdtl1==hd1) normalize nodelta 1586 [ 1: * #H >(H (refl ??)) #_ 1587 lapply (eqb_true ? hd2 hd1) 1588 cases (hd2==hd1) normalize nodelta * 1589 [ 1: #H' >(H' (refl ??)) #_ #_ #_ @refl 1590  2: #_ #_ @Hind ] 1591  2: #_ normalize lapply (eqb_true ? hd2 hdtl1) 1592 cases (hd2 == hdtl1) normalize nodelta * 1593 [ 1: #_ #_ #Habsurd destruct (Habsurd) 1594  2: #_ #_ @Hind ] ] ] ] 1595 #Heq_hd2hd1 destruct (Heq_hd2hd1) 1596 @lset_eq_concrete_to_lset_eq lapply (lset_eq_to_lset_eq_concrete … Hind) 1597 #Hind' @(square_lset_eq_concrete … Hind') 1598 [ 2: @lset_refl 1599  1: >cons_to_append >cons_to_append in ⊢ (???%); 1600 @(transitive_lset_eq_concrete … ([hd1]@[hd1]@tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1601 [ 1: @lset_eq_to_lset_eq_concrete @symmetric_lset_eq @lset_eq_contract 1602  2: >(cons_to_append … hd1 (lset_difference ???)) 1603 @lset_eq_concrete_cons >nil_append >nil_append 1604 @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] ] 1605  2: @(match hd2 == hd1 1606 return λx. ((hd2 == hd1) = x) → ? 1607 with 1608 [ true ⇒ λH''. ? 1609  false ⇒ λH''. ? 1610 ] (refl ? (hd2 == hd1))) 1611 [ 1: whd in match (lset_remove ???) in ⊢ (???%); 1612 >H'' normalize nodelta >((proj1 … (eqb_true …)) H'') 1613 @(transitive_lset_eq … Hind) 1614 @(transitive_lset_eq … (hd1::hd1::tl1@lset_difference A tl2 (filter A (λx:A.¬x==hd1) tl1))) 1615 [ 2: @lset_eq_contract ] 1616 @lset_eq_concrete_to_lset_eq @lset_eq_concrete_cons 1617 @switch_lset_eq_concrete 1618  2: whd in match (lset_remove ???) in ⊢ (???%); 1619 >H'' >notb_false normalize nodelta 1620 @lset_eq_concrete_to_lset_eq 1621 lapply (lset_eq_to_lset_eq_concrete … Hind) #Hindc 1622 lapply (lset_eq_concrete_cons … Hindc hd2) #Hindc' Hindc 1623 @(square_lset_eq_concrete … Hindc') 1624 [ 1: @symmetric_lset_eq_concrete 1625 >cons_to_append >cons_to_append in ⊢ (???%); 1626 >(cons_to_append … hd2) >(cons_to_append … hd1) in ⊢ (???%); 1627 @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1628  2: @symmetric_lset_eq_concrete @(switch_lset_eq_concrete ? ([hd1]@tl1) hd2 ?) 1629 ] 1630 ] 1631 ] 1632 ] 1633 ] 1634 ] 1635 ] qed. 1636 1637 lemma lset_inclusion_difference : 1638 ∀A : DeqSet. 1639 ∀s1,s2 : lset (carr A). 1640 lset_inclusion ? s1 s2 → 1641 ∃s2'. lset_eq ? s2 (s1 @ s2') ∧ 1642 lset_disjoint ? s1 s2' ∧ 1643 lset_eq ? s2' (lset_difference ? s2 s1). 1644 #A #s1 #s2 #Hincl %{(lset_difference A s2 s1)} @conj try @conj 1645 [ 1: @lset_inclusion_difference_aux @Hincl 1646  2: /2 by lset_difference_disjoint/ 1647  3,4: @reflexive_lset_inclusion ] 1648 qed.
Note: See TracChangeset
for help on using the changeset viewer.