Ignore:
Timestamp:
Nov 9, 2012, 4:38:02 PM (8 years ago)
Author:
garnier
Message:

Comitting current state of switch removal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2441 r2448  
    12901290          @lset_eq_concrete_cons >nil_append >nil_append
    12911291          @Hind
    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     ]
     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     ]
    12991299] qed.
    13001300
     
    14171417qed.
    14181418
    1419 
    1420 
     1419(* Additional lemmas on lsets *)
     1420
     1421lemma 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
     1426qed.
     1427
     1428lemma 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
     1431lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
     1432elim 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
     1439lemma 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 ] ] ] ]
     1451qed.
     1452
     1453lemma 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
     1458lemma 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
     1465lemma 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
     1477whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
     1478whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
     1479elim 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
     1499lemma 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 ] ] ]
     1519qed.
     1520
     1521lemma 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/
     1524qed.
     1525
     1526lemma 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                                                       
     1637lemma 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 ]
     1648qed.
Note: See TracChangeset for help on using the changeset viewer.