Changeset 1869 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 28, 2012, 11:44:40 AM (8 years ago)
Author:
mulligan
Message:

a load of axioms closed in ASMCosts file

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1831 r1869  
    13881388qed.
    13891389
    1390 axiom eqb_true_to_refl:
     1390lemma r_Sr_and_l_r_to_Sl_r:
     1391  ∀r, l: nat.
     1392    (∃r': nat. r = S r' ∧ l = r') → S l = r.
     1393  #r #l #exists_hyp
     1394  cases exists_hyp #r'
     1395  #and_hyp cases and_hyp
     1396  #left_hyp #right_hyp
     1397  destruct %
     1398qed.
     1399
     1400lemma eqb_Sn_to_exists_n':
     1401  ∀m, n: nat.
     1402    eqb (S m) n = true → ∃n': nat. n = S n'.
     1403  #m #n
     1404  cases n
     1405  [1:
     1406    normalize #absurd
     1407    destruct(absurd)
     1408  |2:
     1409    #n' #_ %{n'} %
     1410  ]
     1411qed.
     1412
     1413lemma eqb_true_to_eqb_S_S_true:
     1414  ∀m, n: nat.
     1415    eqb m n = true → eqb (S m) (S n) = true.
     1416  #m #n normalize #assm assumption
     1417qed.
     1418
     1419lemma eqb_S_S_true_to_eqb_true:
     1420  ∀m, n: nat.
     1421    eqb (S m) (S n) = true → eqb m n = true.
     1422  #m #n normalize #assm assumption
     1423qed.
     1424
     1425lemma eqb_true_to_refl:
    13911426  ∀l, r: nat.
    13921427    eqb l r = true → l = r.
    1393 
    1394 axiom eqb_false_to_not_refl:
     1428  #l
     1429  elim l
     1430  [1:
     1431    #r cases r
     1432    [1:
     1433      #_ %
     1434    |2:
     1435      #l' normalize
     1436      #absurd destruct(absurd)
     1437    ]
     1438  |2:
     1439    #l' #inductive_hypothesis #r
     1440    #eqb_refl @r_Sr_and_l_r_to_Sl_r
     1441    %{(pred r)} @conj
     1442    [1:
     1443      cases (eqb_Sn_to_exists_n' … eqb_refl)
     1444      #r' #S_assm >S_assm %
     1445    |2:
     1446      cases (eqb_Sn_to_exists_n' … eqb_refl)
     1447      #r' #refl_assm destruct normalize
     1448      @inductive_hypothesis
     1449      normalize in eqb_refl; assumption
     1450    ]
     1451  ]
     1452qed.
     1453
     1454lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
     1455  ∀r, l: nat.
     1456    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
     1457  #r #l #disj_hyp
     1458  cases disj_hyp
     1459  [1:
     1460    #r_O_refl destruct @nmk
     1461    #absurd destruct(absurd)
     1462  |2:
     1463    #exists_hyp cases exists_hyp #r'
     1464    #conj_hyp cases conj_hyp #left_conj #right_conj
     1465    destruct @nmk #S_S_refl_hyp
     1466    elim right_conj #hyp @hyp //
     1467  ]
     1468qed.
     1469
     1470lemma neq_l_r_to_neq_Sl_Sr:
     1471  ∀l, r: nat.
     1472    l ≠ r → S l ≠ S r.
     1473  #l #r #l_neq_r_assm
     1474  @nmk #Sl_Sr_assm cases l_neq_r_assm
     1475  #assm @assm //
     1476qed.
     1477
     1478lemma eqb_false_to_not_refl:
    13951479  ∀l, r: nat.
    13961480    eqb l r = false → l ≠ r.
    1397 
    1398 axiom le_neq_to_lt:
     1481  #l
     1482  elim l
     1483  [1:
     1484    #r cases r
     1485    [1:
     1486      normalize #absurd destruct(absurd)
     1487    |2:
     1488      #r' #_ @nmk
     1489      #absurd destruct(absurd)
     1490    ]
     1491  |2:
     1492    #l' #inductive_hypothesis #r
     1493    cases r
     1494    [1:
     1495      #eqb_false_assm
     1496      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
     1497      @or_introl %
     1498    |2:
     1499      #r' #eqb_false_assm
     1500      @neq_l_r_to_neq_Sl_Sr
     1501      @inductive_hypothesis
     1502      assumption
     1503    ]
     1504  ]
     1505qed.
     1506
     1507lemma le_to_lt_or_eq:
     1508  ∀m, n: nat.
     1509    m ≤ n → m = n ∨ m < n.
     1510  #m #n #le_hyp
     1511  cases le_hyp
     1512  [1:
     1513    @or_introl %
     1514  |2:
     1515    #m' #le_hyp'
     1516    @or_intror
     1517    normalize
     1518    @le_S_S assumption
     1519  ]
     1520qed.
     1521
     1522lemma le_neq_to_lt:
    13991523  ∀m, n: nat.
    14001524    m ≤ n → m ≠ n → m < n.
     1525  #m #n #le_hyp #neq_hyp
     1526  cases neq_hyp
     1527  #eq_absurd_hyp
     1528  generalize in match (le_to_lt_or_eq m n le_hyp);
     1529  #disj_assm cases disj_assm
     1530  [1:
     1531    #absurd cases (eq_absurd_hyp absurd)
     1532  |2:
     1533    #assm assumption
     1534  ]
     1535qed.
    14011536
    14021537let rec traverse_code_internal
Note: See TracChangeset for help on using the changeset viewer.