Changeset 1869
 Timestamp:
 Mar 28, 2012, 11:44:40 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1831 r1869 1388 1388 qed. 1389 1389 1390 axiom eqb_true_to_refl: 1390 lemma 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 % 1398 qed. 1399 1400 lemma 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 ] 1411 qed. 1412 1413 lemma 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 1417 qed. 1418 1419 lemma 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 1423 qed. 1424 1425 lemma eqb_true_to_refl: 1391 1426 ∀l, r: nat. 1392 1427 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 ] 1452 qed. 1453 1454 lemma 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 ] 1468 qed. 1469 1470 lemma 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 // 1476 qed. 1477 1478 lemma eqb_false_to_not_refl: 1395 1479 ∀l, r: nat. 1396 1480 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 ] 1505 qed. 1506 1507 lemma 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 ] 1520 qed. 1521 1522 lemma le_neq_to_lt: 1399 1523 ∀m, n: nat. 1400 1524 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 ] 1535 qed. 1401 1536 1402 1537 let rec traverse_code_internal
Note: See TracChangeset
for help on using the changeset viewer.