Changeset 2124 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (7 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2123 r2124  
    14781478qed.
    14791479
     1480(*CSC: just a synonim, get rid of it!*)
     1481lemma Some_eq:
     1482 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y ≝ option_destruct_Some.
     1483
    14801484lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
    14811485  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
     
    14831487qed.
    14841488
    1485 lemma Some_eq:
    1486  ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
    1487  #T #x #y #H @option_destruct_Some @H
    1488 qed.
    1489 
    14901489lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?.
    14911490#A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS')
     
    14941493coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
    14951494  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
     1495
     1496lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
     1497 #P #A #a #abs destruct
     1498qed.
     1499
     1500discriminator Prod.
     1501
     1502lemma pair_replace:
     1503 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
     1504  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
     1505 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
     1506qed.
     1507
     1508lemma jmpair_as_replace:
     1509 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
     1510  ∀EQ:c ≃ 〈a,b〉.
     1511  P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
     1512  [2:
     1513    >EQc @EQ
     1514  |1:
     1515    #A #B #T #P #a #b
     1516    #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
     1517    letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
     1518    change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
     1519    @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
     1520    -EQ cases c in f; normalize //
     1521  ]
     1522qed.
     1523
     1524lemma if_then_else_replace:
     1525  ∀T: Type[0].
     1526  ∀P: T → Prop.
     1527  ∀t1, t2: T.
     1528  ∀c, c', c'': bool.
     1529    c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
     1530  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
     1531  assumption
     1532qed.
     1533
     1534lemma refl_to_jmrefl:
     1535  ∀a: Type[0].
     1536  ∀l, r: a.
     1537    l = r → l ≃ r.
     1538  #a #l #r #refl destruct %
     1539qed.
     1540
     1541lemma prod_eq_left:
     1542  ∀A: Type[0].
     1543  ∀p, q, r: A.
     1544    p = q → 〈p, r〉 = 〈q, r〉.
     1545  #A #p #q #r #hyp
     1546  destruct %
     1547qed.
     1548
     1549lemma prod_eq_right:
     1550  ∀A: Type[0].
     1551  ∀p, q, r: A.
     1552    p = q → 〈r, p〉 = 〈r, q〉.
     1553  #A #p #q #r #hyp
     1554  destruct %
     1555qed.
     1556
     1557lemma destruct_bug_fix_1:
     1558  ∀n: nat.
     1559    S n = 0 → False.
     1560  #n #absurd destruct(absurd)
     1561qed.
     1562
     1563lemma destruct_bug_fix_2:
     1564  ∀m, n: nat.
     1565    S m = S n → m = n.
     1566  #m #n #refl destruct %
     1567qed.
     1568
     1569lemma eq_rect_Type1_r:
     1570  ∀A: Type[1].
     1571  ∀a: A.
     1572  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     1573  #A #a #P #H #x #p
     1574  generalize in match H;
     1575  generalize in match P;
     1576  cases p //
     1577qed.
     1578
     1579lemma Some_Some_elim:
     1580 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
     1581 #T #x #y #P #H #K @H @option_destruct_Some //
     1582qed.
     1583
     1584lemma pair_destruct_right:
     1585  ∀A: Type[0].
     1586  ∀B: Type[0].
     1587  ∀a, c: A.
     1588  ∀b, d: B.
     1589    〈a, b〉 = 〈c, d〉 → b = d.
     1590  #A #B #a #b #c #d //
     1591qed.
     1592
     1593lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
     1594  /2/
     1595qed.
     1596
     1597definition eq_sum:
     1598    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
     1599  λlt, rt, leq, req, left, right.
     1600    match left with
     1601    [ inl l ⇒
     1602      match right with
     1603      [ inl l' ⇒ leq l l'
     1604      | _ ⇒ false
     1605      ]
     1606    | inr r ⇒
     1607      match right with
     1608      [ inr r' ⇒ req r r'
     1609      | _ ⇒ false
     1610      ]
     1611    ].
     1612
     1613lemma eq_sum_refl:
     1614  ∀A, B: Type[0].
     1615  ∀leq, req.
     1616  ∀s.
     1617  ∀leq_refl: (∀t. leq t t = true).
     1618  ∀req_refl: (∀u. req u u = true).
     1619    eq_sum A B leq req s s = true.
     1620  #A #B #leq #req #s #leq_refl #req_refl
     1621  cases s assumption
     1622qed.
     1623
     1624definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
     1625  λlt, rt, leq, req, left, right.
     1626    let 〈l, r〉 ≝ left in
     1627    let 〈l', r'〉 ≝ right in
     1628      leq l l' ∧ req r r'.
     1629
     1630lemma eq_prod_refl:
     1631  ∀A, B: Type[0].
     1632  ∀leq, req.
     1633  ∀s.
     1634  ∀leq_refl: (∀t. leq t t = true).
     1635  ∀req_refl: (∀u. req u u = true).
     1636    eq_prod A B leq req s s = true.
     1637  #A #B #leq #req #s #leq_refl #req_refl
     1638  cases s
     1639  whd in ⊢ (? → ? → ??%?);
     1640  #l #r
     1641  >leq_refl @req_refl
     1642qed.
    14961643 
    14971644lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
Note: See TracChangeset for help on using the changeset viewer.