Changeset 1928


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (7 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

Location:
src
Files:
1 added
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1927 r1928  
    6565      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    6666        nat_of_bitvector … program_counter' < total_program_size
    67       (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
    68       [ ADDR16 addr ⇒ λaddr16: True.
    69           reachable_program_counter code_memory total_program_size addr ∧
    70             nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    71               nat_of_bitvector … program_counter' < total_program_size
    72       | _ ⇒ λother: False. ⊥
    73       ] (subaddressing_modein … addr) *)
    7467    | ACALL addr         ⇒
    7568      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    7669        nat_of_bitvector … program_counter' < total_program_size
    77       (* match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
    78       [ ADDR11 addr ⇒ λaddr11: True.
    79         let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
    80         let 〈thr, eig〉 ≝ split … 3 8 addr in
    81         let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
    82         let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
    83           reachable_program_counter code_memory total_program_size new_program_counter ∧
    84             nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
    85               nat_of_bitvector … program_counter' < total_program_size
    86       | _ ⇒ λother: False. ⊥
    87       ] (subaddressing_modein … addr) *)
    8870    | AJMP  addr         ⇒
    8971      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
     
    10284          nat_of_bitvector … program_counter' < total_program_size
    10385    ].
    104 (*  cases other
    105 qed. *)
    10686
    10787definition current_instruction_label ≝
     
    11999    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    120100      program_counter ? code_memory after = program_counter_after.
    121 
    122 lemma eq_bv_true_to_refl:
    123   ∀n: nat.
    124   ∀x: BitVector n.
    125   ∀y: BitVector n.
    126     eq_bv n x y = true → x = y.
    127   #n #x #y
    128   cases daemon (* XXX: !!! *)
    129 qed.
    130 
    131 lemma refl_to_eq_bv_true:
    132   ∀n: nat.
    133   ∀x: BitVector n.
    134   ∀y: BitVector n.
    135     x = y → eq_bv n x y = true.
    136   #n #x #y #refl destruct /2/
    137 qed.
    138 
    139 corollary refl_iff_eq_bv_true:
    140   ∀n: nat.
    141   ∀x: BitVector n.
    142   ∀y: BitVector n.
    143     eq_bv n x y = true ↔ x = y.
    144   #n #x #y whd in match iff; normalize nodelta
    145   @conj /2/
    146 qed.
    147101
    148102definition word_deqset: DeqSet ≝
     
    210164  >inductive_hypothesis %
    211165qed.
    212 
    213 axiom nat_of_bitvector_bitvector_of_nat_inverse:
    214   ∀n: nat.
    215   ∀b: nat.
    216     b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
    217 
    218 axiom bitvector_of_nat_inverse_nat_of_bitvector:
    219   ∀n: nat.
    220   ∀b: BitVector n.
    221     bitvector_of_nat n (nat_of_bitvector n b) = b.
    222166
    223167lemma mem_all_program_counter_list_lt_bound:
     
    374318    try (#assm1 #absurd destruct(absurd) @I)
    375319    try (#absurd destruct(absurd) @I)
    376     (* [1:
    377       #addr #_
    378       @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ]
    379       #w
    380       @pair_elim #lft #rgt @pair_elim #lft' #rgt' @pair_elim #lft'' #rgt''
    381       #_ #_ #_ * * #_
    382     |2:
    383       #addr #_
    384       @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ]
    385       #w * * #_
    386     |3:
    387       #addr #_ *
    388     ] *)
    389320    #_ #_ * #relevant #pc_tps_assm'
    390321    whd cases reachable_program_counter_witness * #n
     
    518449  ].
    519450
    520 include alias "arithmetics/nat.ma".
    521 include alias "basics/logic.ma".
    522 
    523 lemma plus_right_monotone:
    524   ∀m, n, o: nat.
    525     m = n → m + o = n + o.
    526   #m #n #o #refl >refl %
    527 qed.
    528 
    529 lemma plus_left_monotone:
    530   ∀m, n, o: nat.
    531     m = n → o + m = o + n.
    532   #m #n #o #refl destruct %
    533 qed.
    534 
    535 lemma minus_plus_cancel:
    536   ∀m, n : nat.
    537   ∀proof: n ≤ m.
    538     (m - n) + n = m.
    539   #m #n #proof /2 by plus_minus/
    540 qed.
    541 
    542451lemma reachable_program_counter_to_0_lt_total_program_size:
    543452  ∀code_memory: BitVectorTrie Byte 16.
     
    554463    #new_pc @ltn_to_ltO
    555464  ]
    556 qed.
    557 
    558 lemma not_Some_neq_None_to_False:
    559   ∀a: Type[0].
    560   ∀e: a.
    561     ¬ (Some a e ≠ None a) → False.
    562   #a #e #absurd cases absurd -absurd
    563   #absurd @absurd @nmk -absurd
    564   #absurd destruct(absurd)
    565465qed.
    566466
     
    11881088  @hyp @tal_pc_list_length_leq_total_program_size try assumption
    11891089qed.
    1190 
    1191 (* XXX: to be moved into common/Identifiers.ma *)
    1192 lemma lookup_present_add_hit:
    1193   ∀tag, A, map, k, v, k_pres.
    1194     lookup_present tag A (add … map k v) k k_pres = v.
    1195   #tag #a #map #k #v #k_pres
    1196   lapply (lookup_lookup_present … (add … map k v) … k_pres)
    1197   >lookup_add_hit #Some_assm destruct(Some_assm)
    1198   <e0 %
    1199 qed.
    1200 
    1201 lemma lookup_present_add_miss:
    1202   ∀tag, A, map, k, k', v, k_pres', k_pres''.
    1203     k' ≠ k →
    1204       lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
    1205   #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
    1206   lapply (lookup_lookup_present … (add … map k v) ? k_pres')
    1207   >lookup_add_miss try assumption
    1208   #Some_assm
    1209   lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
    1210   lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
    1211 qed.
    1212 
    1213 (* XXX: to be moved into basics/types.ma *)
    1214 lemma not_None_to_Some:
    1215   ∀A: Type[0].
    1216   ∀o: option A.
    1217     o ≠ None A → ∃v: A. o = Some A v.
    1218   #A #o cases o
    1219   [1:
    1220     #absurd cases absurd #absurd' cases (absurd' (refl …))
    1221   |2:
    1222     #v' #ignore /2/
    1223   ]
    1224 qed.
    1225 
    1226 lemma present_add_present:
    1227   ∀tag, a, map, k, k', v.
    1228     k' ≠ k →
    1229       present tag a (add tag a map k v) k' →
    1230         present tag a map k'.
    1231   #tag #a #map #k #k' #v #neq_hyp #present_hyp
    1232   whd in match present; normalize nodelta
    1233   whd in match present in present_hyp; normalize nodelta in present_hyp;
    1234   cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
    1235   lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
    1236   [1:
    1237     * #k_eq_hyp @⊥ /2/
    1238   |2:
    1239     #Some_eq_hyp' /2/
    1240   ]
    1241 qed.
    1242 
    1243 lemma present_add_hit:
    1244   ∀tag, a, map, k, v.
    1245     present tag a (add tag a map k v) k.
    1246   #tag #a #map #k #v
    1247   whd >lookup_add_hit
    1248   % #absurd destruct
    1249 qed.
    1250 
    1251 lemma present_add_miss:
    1252   ∀tag, a, map, k, k', v.
    1253     k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
    1254   #tag #a #map #k #k' #v #neq_assm #present_assm
    1255   whd >lookup_add_miss assumption
    1256 qed.
    1257 
    1258 lemma lt_to_le_to_le:
    1259   ∀n, m, p: nat.
    1260     n < m → m ≤ p → n ≤ p.
    1261   #n #m #p #H #H1
    1262   elim H
    1263   [1:
    1264     @(transitive_le n m p) /2/
    1265   |2:
    1266     /2/
    1267   ]
    1268 qed.
    1269 
    1270 lemma eqb_decidable:
    1271   ∀l, r: nat.
    1272     (eqb l r = true) ∨ (eqb l r = false).
    1273   #l #r //
    1274 qed.
    1275 
    1276 lemma r_Sr_and_l_r_to_Sl_r:
    1277   ∀r, l: nat.
    1278     (∃r': nat. r = S r' ∧ l = r') → S l = r.
    1279   #r #l #exists_hyp
    1280   cases exists_hyp #r'
    1281   #and_hyp cases and_hyp
    1282   #left_hyp #right_hyp
    1283   destruct %
    1284 qed.
    1285 
    1286 lemma eqb_Sn_to_exists_n':
    1287   ∀m, n: nat.
    1288     eqb (S m) n = true → ∃n': nat. n = S n'.
    1289   #m #n
    1290   cases n
    1291   [1:
    1292     normalize #absurd
    1293     destruct(absurd)
    1294   |2:
    1295     #n' #_ %{n'} %
    1296   ]
    1297 qed.
    1298 
    1299 lemma eqb_true_to_eqb_S_S_true:
    1300   ∀m, n: nat.
    1301     eqb m n = true → eqb (S m) (S n) = true.
    1302   #m #n normalize #assm assumption
    1303 qed.
    1304 
    1305 lemma eqb_S_S_true_to_eqb_true:
    1306   ∀m, n: nat.
    1307     eqb (S m) (S n) = true → eqb m n = true.
    1308   #m #n normalize #assm assumption
    1309 qed.
    1310 
    1311 lemma eqb_true_to_refl:
    1312   ∀l, r: nat.
    1313     eqb l r = true → l = r.
    1314   #l
    1315   elim l
    1316   [1:
    1317     #r cases r
    1318     [1:
    1319       #_ %
    1320     |2:
    1321       #l' normalize
    1322       #absurd destruct(absurd)
    1323     ]
    1324   |2:
    1325     #l' #inductive_hypothesis #r
    1326     #eqb_refl @r_Sr_and_l_r_to_Sl_r
    1327     %{(pred r)} @conj
    1328     [1:
    1329       cases (eqb_Sn_to_exists_n' … eqb_refl)
    1330       #r' #S_assm >S_assm %
    1331     |2:
    1332       cases (eqb_Sn_to_exists_n' … eqb_refl)
    1333       #r' #refl_assm destruct normalize
    1334       @inductive_hypothesis
    1335       normalize in eqb_refl; assumption
    1336     ]
    1337   ]
    1338 qed.
    1339 
    1340 lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
    1341   ∀r, l: nat.
    1342     r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
    1343   #r #l #disj_hyp
    1344   cases disj_hyp
    1345   [1:
    1346     #r_O_refl destruct @nmk
    1347     #absurd destruct(absurd)
    1348   |2:
    1349     #exists_hyp cases exists_hyp #r'
    1350     #conj_hyp cases conj_hyp #left_conj #right_conj
    1351     destruct @nmk #S_S_refl_hyp
    1352     elim right_conj #hyp @hyp //
    1353   ]
    1354 qed.
    1355 
    1356 lemma neq_l_r_to_neq_Sl_Sr:
    1357   ∀l, r: nat.
    1358     l ≠ r → S l ≠ S r.
    1359   #l #r #l_neq_r_assm
    1360   @nmk #Sl_Sr_assm cases l_neq_r_assm
    1361   #assm @assm //
    1362 qed.
    1363 
    1364 lemma eqb_false_to_not_refl:
    1365   ∀l, r: nat.
    1366     eqb l r = false → l ≠ r.
    1367   #l
    1368   elim l
    1369   [1:
    1370     #r cases r
    1371     [1:
    1372       normalize #absurd destruct(absurd)
    1373     |2:
    1374       #r' #_ @nmk
    1375       #absurd destruct(absurd)
    1376     ]
    1377   |2:
    1378     #l' #inductive_hypothesis #r
    1379     cases r
    1380     [1:
    1381       #eqb_false_assm
    1382       @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
    1383       @or_introl %
    1384     |2:
    1385       #r' #eqb_false_assm
    1386       @neq_l_r_to_neq_Sl_Sr
    1387       @inductive_hypothesis
    1388       assumption
    1389     ]
    1390   ]
    1391 qed.
    1392 
    1393 lemma le_to_lt_or_eq:
    1394   ∀m, n: nat.
    1395     m ≤ n → m = n ∨ m < n.
    1396   #m #n #le_hyp
    1397   cases le_hyp
    1398   [1:
    1399     @or_introl %
    1400   |2:
    1401     #m' #le_hyp'
    1402     @or_intror
    1403     normalize
    1404     @le_S_S assumption
    1405   ]
    1406 qed.
    1407 
    1408 lemma le_neq_to_lt:
    1409   ∀m, n: nat.
    1410     m ≤ n → m ≠ n → m < n.
    1411   #m #n #le_hyp #neq_hyp
    1412   cases neq_hyp
    1413   #eq_absurd_hyp
    1414   generalize in match (le_to_lt_or_eq m n le_hyp);
    1415   #disj_assm cases disj_assm
    1416   [1:
    1417     #absurd cases (eq_absurd_hyp absurd)
    1418   |2:
    1419     #assm assumption
    1420   ]
    1421 qed.
    1422 
    1423 inverter nat_jmdiscr for nat.
    1424 
    1425 lemma plus_lt_to_lt:
    1426   ∀m, n, o: nat.
    1427     m + n < o → m < o.
    1428   #m #n #o
    1429   elim n
    1430   [1:
    1431     <(plus_n_O m) in ⊢ (% → ?);
    1432     #assumption assumption
    1433   |2:
    1434     #n' #inductive_hypothesis
    1435     <(plus_n_Sm m n') in ⊢ (% → ?);
    1436     #assm @inductive_hypothesis
    1437     normalize in assm; normalize
    1438     /2 by lt_S_to_lt/
    1439   ]
    1440 qed.
    1441 
    1442 include "arithmetics/div_and_mod.ma".
    1443 
    1444 lemma n_plus_1_n_to_False:
    1445   ∀n: nat.
    1446     n + 1 = n → False.
    1447   #n elim n
    1448   [1:
    1449     normalize #absurd destruct(absurd)
    1450   |2:
    1451     #n' #inductive_hypothesis normalize
    1452     #absurd @inductive_hypothesis /2/
    1453   ]
    1454 qed.
    1455 
    1456 lemma one_two_times_n_to_False:
    1457   ∀n: nat.
    1458     1=2*n→False.
    1459   #n cases n
    1460   [1:
    1461     normalize #absurd destruct(absurd)
    1462   |2:
    1463     #n' normalize #absurd
    1464     lapply (injective_S … absurd) -absurd #absurd
    1465     /2/
    1466   ]
    1467 qed.
    1468 
    1469 let rec odd_p
    1470   (n: nat)
    1471     on n ≝
    1472   match n with
    1473   [ O ⇒ False
    1474   | S n' ⇒ even_p n'
    1475   ]
    1476 and even_p
    1477   (n: nat)
    1478     on n ≝
    1479   match n with
    1480   [ O ⇒ True
    1481   | S n' ⇒ odd_p n'
    1482   ].
    1483 
    1484 let rec n_even_p_to_n_plus_2_even_p
    1485   (n: nat)
    1486     on n: even_p n → even_p (n + 2) ≝
    1487   match n with
    1488   [ O ⇒ ?
    1489   | S n' ⇒ ?
    1490   ]
    1491 and n_odd_p_to_n_plus_2_odd_p
    1492   (n: nat)
    1493     on n: odd_p n → odd_p (n + 2) ≝
    1494   match n with
    1495   [ O ⇒ ?
    1496   | S n' ⇒ ?
    1497   ].
    1498   [1,3:
    1499     normalize #assm assumption
    1500   |2:
    1501     normalize @n_odd_p_to_n_plus_2_odd_p
    1502   |4:
    1503     normalize @n_even_p_to_n_plus_2_even_p
    1504   ]
    1505 qed.
    1506 
    1507 let rec two_times_n_even_p
    1508   (n: nat)
    1509     on n: even_p (2 * n) ≝
    1510   match n with
    1511   [ O ⇒ ?
    1512   | S n' ⇒ ?
    1513   ]
    1514 and two_times_n_plus_one_odd_p
    1515   (n: nat)
    1516     on n: odd_p ((2 * n) + 1) ≝
    1517   match n with
    1518   [ O ⇒ ?
    1519   | S n' ⇒ ?
    1520   ].
    1521   [1,3:
    1522     normalize @I
    1523   |2:
    1524     normalize
    1525     >plus_n_Sm
    1526     <(associative_plus n' n' 1)
    1527     >(plus_n_O (n' + n'))
    1528     cut(n' + n' + 0 + 1 = 2 * n' + 1)
    1529     [1:
    1530       //
    1531     |2:
    1532       #refl_assm >refl_assm
    1533       @two_times_n_plus_one_odd_p     
    1534     ]
    1535   |4:
    1536     normalize
    1537     >plus_n_Sm
    1538     cut(n' + (n' + 1) + 1 = (2 * n') + 2)
    1539     [1:
    1540       normalize /2/
    1541     |2:
    1542       #refl_assm >refl_assm
    1543       @n_even_p_to_n_plus_2_even_p
    1544       @two_times_n_even_p
    1545     ]
    1546   ]
    1547 qed.
    1548 
    1549 let rec even_p_to_not_odd_p
    1550   (n: nat)
    1551     on n: even_p n → ¬ odd_p n ≝
    1552   match n with
    1553   [ O ⇒ ?
    1554   | S n' ⇒ ?
    1555   ]
    1556 and odd_p_to_not_even_p
    1557   (n: nat)
    1558     on n: odd_p n → ¬ even_p n ≝
    1559   match n with
    1560   [ O ⇒ ?
    1561   | S n' ⇒ ?
    1562   ].
    1563   [1:
    1564     normalize #_
    1565     @nmk #assm assumption
    1566   |3:
    1567     normalize #absurd
    1568     cases absurd
    1569   |2:
    1570     normalize
    1571     @odd_p_to_not_even_p
    1572   |4:
    1573     normalize
    1574     @even_p_to_not_odd_p
    1575   ]
    1576 qed.
    1577 
    1578 lemma even_p_odd_p_cases:
    1579   ∀n: nat.
    1580     even_p n ∨ odd_p n.
    1581   #n elim n
    1582   [1:
    1583     normalize @or_introl @I
    1584   |2:
    1585     #n' #inductive_hypothesis
    1586     normalize
    1587     cases inductive_hypothesis
    1588     #assm
    1589     try (@or_introl assumption)
    1590     try (@or_intror assumption)
    1591   ]
    1592 qed.
    1593 
    1594 lemma two_times_n_plus_one_refl_two_times_n_to_False:
    1595   ∀m, n: nat.
    1596     2 * m + 1 = 2 * n → False.
    1597   #m #n
    1598   #assm
    1599   cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
    1600   [1:
    1601     >assm
    1602     @conj
    1603     @two_times_n_even_p
    1604   |2:
    1605     * #_ #absurd
    1606     cases (even_p_to_not_odd_p … absurd)
    1607     #assm @assm
    1608     @two_times_n_plus_one_odd_p
    1609   ]
    1610 qed.
    1611 
    1612 lemma nat_of_bitvector_aux_injective:
    1613   ∀n: nat.
    1614   ∀l, r: BitVector n.
    1615   ∀acc_l, acc_r: nat.
    1616     nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
    1617       acc_l = acc_r ∧ l ≃ r.
    1618   #n #l
    1619   elim l #r
    1620   [1:
    1621     #acc_l #acc_r normalize
    1622     >(BitVector_O r) normalize /2/
    1623   |2:
    1624     #hd #tl #inductive_hypothesis #r #acc_l #acc_r
    1625     normalize normalize in inductive_hypothesis;
    1626     cases (BitVector_Sn … r)
    1627     #r_hd * #r_tl #r_refl destruct normalize
    1628     cases hd cases r_hd normalize
    1629     [1:
    1630       #relevant
    1631       cases (inductive_hypothesis … relevant)
    1632       #acc_assm #tl_assm destruct % //
    1633       lapply (injective_plus_l ? ? ? acc_assm)
    1634       -acc_assm #acc_assm
    1635       change with (2 * acc_l = 2 * acc_r) in acc_assm;
    1636       lapply (injective_times_r ? ? ? ? acc_assm) /2/
    1637     |4:
    1638       #relevant
    1639       cases (inductive_hypothesis … relevant)
    1640       #acc_assm #tl_assm destruct % //
    1641       change with (2 * acc_l = 2 * acc_r) in acc_assm;
    1642       lapply(injective_times_r ? ? ? ? acc_assm) /2/
    1643     |2:
    1644       #relevant 
    1645       change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
    1646         (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
    1647       cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
    1648       [1:
    1649         #eqb_true_assm
    1650         lapply (eqb_true_to_refl … eqb_true_assm)
    1651         #refl_assm
    1652         cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
    1653       |2:
    1654         #eqb_false_assm
    1655         lapply (eqb_false_to_not_refl … eqb_false_assm)
    1656         #not_refl_assm cases not_refl_assm #absurd_assm
    1657         cases (inductive_hypothesis … relevant) #absurd
    1658         cases (absurd_assm absurd)
    1659       ]
    1660     |3:
    1661       #relevant 
    1662       change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
    1663         (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
    1664       cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
    1665       [1:
    1666         #eqb_true_assm
    1667         lapply (eqb_true_to_refl … eqb_true_assm)
    1668         #refl_assm
    1669         lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
    1670         -refl_assm #refl_assm
    1671         cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
    1672       |2:
    1673         #eqb_false_assm
    1674         lapply (eqb_false_to_not_refl … eqb_false_assm)
    1675         #not_refl_assm cases not_refl_assm #absurd_assm
    1676         cases (inductive_hypothesis … relevant) #absurd
    1677         cases (absurd_assm absurd)
    1678       ]
    1679     ]
    1680   ]
    1681 qed.
    1682 
    1683 lemma nat_of_bitvector_destruct:
    1684   ∀n: nat.
    1685   ∀l_hd, r_hd: bool.
    1686   ∀l_tl, r_tl: BitVector n.
    1687     nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
    1688       l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
    1689   #n #l_hd #r_hd #l_tl #r_tl
    1690   normalize
    1691   cases l_hd cases r_hd
    1692   normalize
    1693   [4:
    1694     /2/
    1695   |1:
    1696     #relevant
    1697     cases (nat_of_bitvector_aux_injective … relevant)
    1698     #_ #l_r_tl_refl destruct /2/
    1699   |2,3:
    1700     #relevant
    1701     cases (nat_of_bitvector_aux_injective … relevant)
    1702     #absurd destruct(absurd)
    1703   ]
    1704 qed.
    1705 
    1706 lemma BitVector_cons_injective:
    1707   ∀n: nat.
    1708   ∀l_hd, r_hd: bool.
    1709   ∀l_tl, r_tl: BitVector n.
    1710     l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
    1711   #l #l_hd #r_hd #l_tl #r_tl
    1712   #l_refl #r_refl destruct %
    1713 qed.
    1714 
    1715 lemma refl_nat_of_bitvector_to_refl:
    1716   ∀n: nat.
    1717   ∀l, r: BitVector n.
    1718     nat_of_bitvector n l = nat_of_bitvector n r → l = r.
    1719   #n
    1720   elim n
    1721   [1:
    1722     #l #r
    1723     >(BitVector_O l)
    1724     >(BitVector_O r)
    1725     #_ %
    1726   |2:
    1727     #n' #inductive_hypothesis #l #r
    1728     lapply (BitVector_Sn ? l) #l_hypothesis
    1729     lapply (BitVector_Sn ? r) #r_hypothesis
    1730     cases l_hypothesis #l_hd #l_tail_hypothesis
    1731     cases r_hypothesis #r_hd #r_tail_hypothesis
    1732     cases l_tail_hypothesis #l_tl #l_hd_tl_refl
    1733     cases r_tail_hypothesis #r_tl #r_hd_tl_refl
    1734     destruct #cons_refl
    1735     cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
    1736     #hd_refl #tl_refl
    1737     @BitVector_cons_injective try assumption
    1738     @inductive_hypothesis assumption
    1739   ]
    1740 qed.
  • src/ASM/ASMCostsSplit.ma

    r1921 r1928  
    11include "ASM/ASMCosts.ma".
    2 include alias "arithmetics/nat.ma".
    3 include alias "basics/logic.ma".
    4 
    5 
    6 (* Also extracts an equality proof (useful when not using Russell). *)
    7 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
    8  with precedence 10
    9 for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    10         λ${ident E}.$s ] (refl ? $t) }.
    11 
    12 (*
    13 lemma test:
    14   ∀c: nat × nat.
    15     Σx: nat. ∃y: nat. c = 〈x, y〉 ≝
    16   λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left.
    17 *)
    18 
    19 notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
    20  with precedence 10
    21 for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
    22         λ${ident E}.$s ] (refl ? $t) }.
    23 
    24 (*
    25 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    26  with precedence 10
    27 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    28        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    29         λ${ident E}.$s ] ] (refl ? $t) }. *)
    30 
    31 notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    32  with precedence 10
    33 for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    34        match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
    35         λ${ident E}.$s ] ] (refl ? $t) }.
    36 
    37 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
    38  with precedence 10
    39 for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    40        match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    41         λ${ident E}.$s ] ] (refl ? $t) }.
    42 
    43 definition nat_of_bool: bool → nat ≝
    44   λb: bool.
    45   match b with
    46   [ true ⇒ 1
    47   | false ⇒ 0
    48   ].
    49 
    50 lemma blah:
    51   ∀n: nat.
    52   ∀bv: BitVector n.
    53   ∀buffer: nat.
    54     nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
    55   #n #bv elim bv
    56   [1:
    57     #buffer elim buffer try %
    58     #buffer' #inductive_hypothesis
    59     normalize <times_n_1 %
    60   |2:
    61     #n' #hd #tl #inductive_hypothesis
    62     #buffer cases hd normalize
    63     >inductive_hypothesis
    64     >inductive_hypothesis
    65     [1:
    66       change with (
    67         ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
    68       change with (
    69         ? + buffer * (2 * 2^n')) in ⊢ (???%);
    70       cases daemon
    71     ]
    72   ]
    73   cases daemon
    74 qed.
    75 
    76 lemma nat_of_bitvector_aux_hd_tl:
    77   ∀n: nat.
    78   ∀tl: BitVector n.
    79   ∀hd: bool.
    80     nat_of_bitvector (S n) (hd:::tl) =
    81       nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
    82   #n #tl elim tl
    83   [1:
    84     #hd cases hd %
    85   |2:
    86     #n' #hd' #tl' #inductive_hypothesis #hd
    87     cases hd whd in ⊢ (??%?); normalize nodelta
    88     >inductive_hypothesis cases hd' normalize nodelta
    89     normalize in match (nat_of_bool ?);
    90     normalize in match (nat_of_bool ?);
    91     [4:
    92       normalize in match (2 * ?);
    93       <plus_n_O <plus_n_O %
    94     |3:
    95       normalize in match (2 * ?);
    96       normalize in match (0 + 1);
    97       <plus_n_O
    98       normalize in match (1 * ?);
    99       <plus_n_O
    100       cases daemon
    101       (* XXX: lemma *)
    102     |*:
    103       cases daemon
    104     ]
    105   ]
    106 qed.
    107 
    108 lemma succ_nat_of_bitvector_aux_half_add_1:
    109   ∀n: nat.
    110   ∀bv: BitVector n.
    111   ∀buffer: nat.
    112   ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    113     S (nat_of_bitvector_aux n buffer bv) =
    114       nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
    115   #n #bv elim bv
    116   [1:
    117     #buffer normalize #absurd
    118     cases (lt_to_not_zero … absurd)
    119   |2:
    120     #n' #hd #tl #inductive_hypothesis #buffer
    121     cases daemon
    122   ]
    123 qed.
    124    
    125 lemma succ_nat_of_bitvector_half_add_1:
    126   ∀n: nat.
    127   ∀bv: BitVector n.
    128   ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    129     S (nat_of_bitvector … bv) = nat_of_bitvector …
    130       (\snd (half_add n (bitvector_of_nat … 1) bv)).
    131   #n #bv elim bv
    132   [1:
    133     normalize #absurd
    134     cases (lt_to_not_zero … absurd)
    135   |2:
    136     #n' #hd #tl #inductive_hypothesis
    137     cases daemon
    138   ]
    139 qed.
    140    
     2include "ASM/UtilBranch.ma".
    1413include alias "arithmetics/nat.ma".
    1424include alias "basics/logic.ma".
     
    426288qed.
    427289
    428 (*
    429 let rec traverse_code_internal
    430   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    431     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    432       (reachable_program_counter_witness:
    433           ∀lbl: costlabel.
    434           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    435             reachable_program_counter code_memory fixed_program_size program_counter)
    436         (good_program_witness: good_program code_memory fixed_program_size)
    437         (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
    438         (fixed_program_size_limit: fixed_program_size < 2^16)
    439         on program_size:
    440           Σcost_map: identifier_map CostTag nat.
    441             (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    442             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    443               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    444                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    445 *)
    446 
    447290definition traverse_code:
    448291  ∀code_memory: BitVectorTrie Byte 16.
  • src/ASM/Arithmetic.ma

    r1870 r1928  
    178178 | #H / by I/
    179179 ]
     180qed.
     181
     182axiom nat_of_bitvector_bitvector_of_nat_inverse:
     183  ∀n: nat.
     184  ∀b: nat.
     185    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
     186
     187axiom bitvector_of_nat_inverse_nat_of_bitvector:
     188  ∀n: nat.
     189  ∀b: BitVector n.
     190    bitvector_of_nat n (nat_of_bitvector n b) = b.
     191
     192lemma nat_of_bitvector_aux_injective:
     193  ∀n: nat.
     194  ∀l, r: BitVector n.
     195  ∀acc_l, acc_r: nat.
     196    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
     197      acc_l = acc_r ∧ l ≃ r.
     198  #n #l
     199  elim l #r
     200  [1:
     201    #acc_l #acc_r normalize
     202    >(BitVector_O r) normalize /2/
     203  |2:
     204    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
     205    normalize normalize in inductive_hypothesis;
     206    cases (BitVector_Sn … r)
     207    #r_hd * #r_tl #r_refl destruct normalize
     208    cases hd cases r_hd normalize
     209    [1:
     210      #relevant
     211      cases (inductive_hypothesis … relevant)
     212      #acc_assm #tl_assm destruct % //
     213      lapply (injective_plus_l ? ? ? acc_assm)
     214      -acc_assm #acc_assm
     215      change with (2 * acc_l = 2 * acc_r) in acc_assm;
     216      lapply (injective_times_r ? ? ? ? acc_assm) /2/
     217    |4:
     218      #relevant
     219      cases (inductive_hypothesis … relevant)
     220      #acc_assm #tl_assm destruct % //
     221      change with (2 * acc_l = 2 * acc_r) in acc_assm;
     222      lapply(injective_times_r ? ? ? ? acc_assm) /2/
     223    |2:
     224      #relevant 
     225      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
     226        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
     227      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
     228      [1:
     229        #eqb_true_assm
     230        lapply (eqb_true_to_refl … eqb_true_assm)
     231        #refl_assm
     232        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
     233      |2:
     234        #eqb_false_assm
     235        lapply (eqb_false_to_not_refl … eqb_false_assm)
     236        #not_refl_assm cases not_refl_assm #absurd_assm
     237        cases (inductive_hypothesis … relevant) #absurd
     238        cases (absurd_assm absurd)
     239      ]
     240    |3:
     241      #relevant 
     242      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
     243        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
     244      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
     245      [1:
     246        #eqb_true_assm
     247        lapply (eqb_true_to_refl … eqb_true_assm)
     248        #refl_assm
     249        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
     250        -refl_assm #refl_assm
     251        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
     252      |2:
     253        #eqb_false_assm
     254        lapply (eqb_false_to_not_refl … eqb_false_assm)
     255        #not_refl_assm cases not_refl_assm #absurd_assm
     256        cases (inductive_hypothesis … relevant) #absurd
     257        cases (absurd_assm absurd)
     258      ]
     259    ]
     260  ]
     261qed.
     262
     263lemma nat_of_bitvector_destruct:
     264  ∀n: nat.
     265  ∀l_hd, r_hd: bool.
     266  ∀l_tl, r_tl: BitVector n.
     267    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
     268      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
     269  #n #l_hd #r_hd #l_tl #r_tl
     270  normalize
     271  cases l_hd cases r_hd
     272  normalize
     273  [4:
     274    /2/
     275  |1:
     276    #relevant
     277    cases (nat_of_bitvector_aux_injective … relevant)
     278    #_ #l_r_tl_refl destruct /2/
     279  |2,3:
     280    #relevant
     281    cases (nat_of_bitvector_aux_injective … relevant)
     282    #absurd destruct(absurd)
     283  ]
     284qed.
     285
     286lemma BitVector_cons_injective:
     287  ∀n: nat.
     288  ∀l_hd, r_hd: bool.
     289  ∀l_tl, r_tl: BitVector n.
     290    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
     291  #l #l_hd #r_hd #l_tl #r_tl
     292  #l_refl #r_refl destruct %
     293qed.
     294
     295lemma refl_nat_of_bitvector_to_refl:
     296  ∀n: nat.
     297  ∀l, r: BitVector n.
     298    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
     299  #n
     300  elim n
     301  [1:
     302    #l #r
     303    >(BitVector_O l)
     304    >(BitVector_O r)
     305    #_ %
     306  |2:
     307    #n' #inductive_hypothesis #l #r
     308    lapply (BitVector_Sn ? l) #l_hypothesis
     309    lapply (BitVector_Sn ? r) #r_hypothesis
     310    cases l_hypothesis #l_hd #l_tail_hypothesis
     311    cases r_hypothesis #r_hd #r_tail_hypothesis
     312    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
     313    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
     314    destruct #cons_refl
     315    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
     316    #hd_refl #tl_refl
     317    @BitVector_cons_injective try assumption
     318    @inductive_hypothesis assumption
     319  ]
    180320qed.
    181321
  • src/ASM/BitVector.ma

    r1890 r1928  
    209209qed.
    210210
     211corollary refl_iff_eq_bv_true:
     212  ∀n: nat.
     213  ∀x: BitVector n.
     214  ∀y: BitVector n.
     215    eq_bv n x y = true ↔ x = y.
     216  #n #x #y whd in match iff; normalize nodelta
     217  @conj /2/
     218qed.
     219
    211220axiom bitvector_of_string:
    212221  ∀n: nat.
  • src/ASM/CostsProof.ma

    r1927 r1928  
    6262
    6363include alias "arithmetics/nat.ma".
    64 
    65 lemma execute_1_ok_clock:
    66   ∀cm.
    67   ∀s.
    68     clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
    69   #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
    70 qed-.
    7164
    7265let rec compute_max_trace_label_label_cost_is_ok
     
    338331include alias "basics/logic.ma".
    339332
    340 lemma and_intro_right:
    341   ∀a, b: Prop.
    342     a → (a → b) → a ∧ b.
    343   #a #b /3/
    344 qed.
    345 
    346 lemma lt_m_n_to_exists_o_plus_m_n:
    347   ∀m, n: nat.
    348     m < n → ∃o: nat. m + o = n.
    349   #m #n
    350   cases m
    351   [1:
    352     #irrelevant
    353     %{n} %
    354   |2:
    355     #m' #lt_hyp
    356     %{(n - S m')}
    357     >commutative_plus in ⊢ (??%?);
    358     <plus_minus_m_m
    359     [1:
    360       %
    361     |2:
    362       @lt_S_to_lt
    363       assumption
    364     ]
    365   ]
    366 qed.
    367 
    368 lemma lt_O_n_to_S_pred_n_n:
    369   ∀n: nat.
    370     0 < n → S (pred n) = n.
    371   #n
    372   cases n
    373   [1:
    374     #absurd
    375     cases(lt_to_not_zero 0 0 absurd)
    376   |2:
    377     #n' #lt_hyp %
    378   ]
    379 qed.
    380 
    381 lemma exists_plus_m_n_to_exists_Sn:
    382   ∀m, n: nat.
    383     m < n → ∃p: nat. S p = n.
    384   #m #n
    385   cases m
    386   [1:
    387     #lt_hyp %{(pred n)}
    388     @(lt_O_n_to_S_pred_n_n … lt_hyp)
    389   |2:
    390     #m' #lt_hyp %{(pred n)}
    391     @(lt_O_n_to_S_pred_n_n)
    392     @(transitive_le … (S m') …)
    393     [1:
    394       //
    395     |2:
    396       @lt_S_to_lt
    397       assumption
    398     ]
    399   ]
    400 qed.
    401 
    402333include alias "arithmetics/bigops.ma".
    403334
     
    513444qed.
    514445
    515 
    516446definition tech_cost_of_label:
    517447 ∀cost_labels: BitVectorTrie costlabel 16.
     
    595525qed.
    596526   
    597 (* XXX: here *)
    598527let rec compute_trace_label_return_using_paid_ok_with_trace
    599528 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
  • src/ASM/Interpret.ma

    r1910 r1928  
    10891089qed-. (*x Andrea: indexing takes ages here *)
    10901090
     1091lemma execute_1_ok_clock:
     1092  ∀cm.
     1093  ∀s.
     1094    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
     1095  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
     1096qed-.
     1097
    10911098definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
    10921099  λticks,cm,s,instr,pc.
  • src/ASM/Util.ma

    r1908 r1928  
    795795qed.
    796796
     797lemma lt_m_n_to_exists_o_plus_m_n:
     798  ∀m, n: nat.
     799    m < n → ∃o: nat. m + o = n.
     800  #m #n
     801  cases m
     802  [1:
     803    #irrelevant
     804    %{n} %
     805  |2:
     806    #m' #lt_hyp
     807    %{(n - S m')}
     808    >commutative_plus in ⊢ (??%?);
     809    <plus_minus_m_m
     810    [1:
     811      %
     812    |2:
     813      @lt_S_to_lt
     814      assumption
     815    ]
     816  ]
     817qed.
     818
     819lemma lt_O_n_to_S_pred_n_n:
     820  ∀n: nat.
     821    0 < n → S (pred n) = n.
     822  #n
     823  cases n
     824  [1:
     825    #absurd
     826    cases(lt_to_not_zero 0 0 absurd)
     827  |2:
     828    #n' #lt_hyp %
     829  ]
     830qed.
     831
     832lemma exists_plus_m_n_to_exists_Sn:
     833  ∀m, n: nat.
     834    m < n → ∃p: nat. S p = n.
     835  #m #n
     836  cases m
     837  [1:
     838    #lt_hyp %{(pred n)}
     839    @(lt_O_n_to_S_pred_n_n … lt_hyp)
     840  |2:
     841    #m' #lt_hyp %{(pred n)}
     842    @(lt_O_n_to_S_pred_n_n)
     843    @(transitive_le … (S m') …)
     844    [1:
     845      //
     846    |2:
     847      @lt_S_to_lt
     848      assumption
     849    ]
     850  ]
     851qed.
     852
     853lemma plus_right_monotone:
     854  ∀m, n, o: nat.
     855    m = n → m + o = n + o.
     856  #m #n #o #refl >refl %
     857qed.
     858
     859lemma plus_left_monotone:
     860  ∀m, n, o: nat.
     861    m = n → o + m = o + n.
     862  #m #n #o #refl destruct %
     863qed.
     864
     865lemma minus_plus_cancel:
     866  ∀m, n : nat.
     867  ∀proof: n ≤ m.
     868    (m - n) + n = m.
     869  #m #n #proof /2 by plus_minus/
     870qed.
     871
     872lemma lt_to_le_to_le:
     873  ∀n, m, p: nat.
     874    n < m → m ≤ p → n ≤ p.
     875  #n #m #p #H #H1
     876  elim H
     877  [1:
     878    @(transitive_le n m p) /2/
     879  |2:
     880    /2/
     881  ]
     882qed.
     883
     884lemma eqb_decidable:
     885  ∀l, r: nat.
     886    (eqb l r = true) ∨ (eqb l r = false).
     887  #l #r //
     888qed.
     889
     890lemma r_Sr_and_l_r_to_Sl_r:
     891  ∀r, l: nat.
     892    (∃r': nat. r = S r' ∧ l = r') → S l = r.
     893  #r #l #exists_hyp
     894  cases exists_hyp #r'
     895  #and_hyp cases and_hyp
     896  #left_hyp #right_hyp
     897  destruct %
     898qed.
     899
     900lemma eqb_Sn_to_exists_n':
     901  ∀m, n: nat.
     902    eqb (S m) n = true → ∃n': nat. n = S n'.
     903  #m #n
     904  cases n
     905  [1:
     906    normalize #absurd
     907    destruct(absurd)
     908  |2:
     909    #n' #_ %{n'} %
     910  ]
     911qed.
     912
     913lemma eqb_true_to_eqb_S_S_true:
     914  ∀m, n: nat.
     915    eqb m n = true → eqb (S m) (S n) = true.
     916  #m #n normalize #assm assumption
     917qed.
     918
     919lemma eqb_S_S_true_to_eqb_true:
     920  ∀m, n: nat.
     921    eqb (S m) (S n) = true → eqb m n = true.
     922  #m #n normalize #assm assumption
     923qed.
     924
     925lemma eqb_true_to_refl:
     926  ∀l, r: nat.
     927    eqb l r = true → l = r.
     928  #l
     929  elim l
     930  [1:
     931    #r cases r
     932    [1:
     933      #_ %
     934    |2:
     935      #l' normalize
     936      #absurd destruct(absurd)
     937    ]
     938  |2:
     939    #l' #inductive_hypothesis #r
     940    #eqb_refl @r_Sr_and_l_r_to_Sl_r
     941    %{(pred r)} @conj
     942    [1:
     943      cases (eqb_Sn_to_exists_n' … eqb_refl)
     944      #r' #S_assm >S_assm %
     945    |2:
     946      cases (eqb_Sn_to_exists_n' … eqb_refl)
     947      #r' #refl_assm destruct normalize
     948      @inductive_hypothesis
     949      normalize in eqb_refl; assumption
     950    ]
     951  ]
     952qed.
     953
     954lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r:
     955  ∀r, l: nat.
     956    r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r.
     957  #r #l #disj_hyp
     958  cases disj_hyp
     959  [1:
     960    #r_O_refl destruct @nmk
     961    #absurd destruct(absurd)
     962  |2:
     963    #exists_hyp cases exists_hyp #r'
     964    #conj_hyp cases conj_hyp #left_conj #right_conj
     965    destruct @nmk #S_S_refl_hyp
     966    elim right_conj #hyp @hyp //
     967  ]
     968qed.
     969
     970lemma neq_l_r_to_neq_Sl_Sr:
     971  ∀l, r: nat.
     972    l ≠ r → S l ≠ S r.
     973  #l #r #l_neq_r_assm
     974  @nmk #Sl_Sr_assm cases l_neq_r_assm
     975  #assm @assm //
     976qed.
     977
     978lemma eqb_false_to_not_refl:
     979  ∀l, r: nat.
     980    eqb l r = false → l ≠ r.
     981  #l
     982  elim l
     983  [1:
     984    #r cases r
     985    [1:
     986      normalize #absurd destruct(absurd)
     987    |2:
     988      #r' #_ @nmk
     989      #absurd destruct(absurd)
     990    ]
     991  |2:
     992    #l' #inductive_hypothesis #r
     993    cases r
     994    [1:
     995      #eqb_false_assm
     996      @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r
     997      @or_introl %
     998    |2:
     999      #r' #eqb_false_assm
     1000      @neq_l_r_to_neq_Sl_Sr
     1001      @inductive_hypothesis
     1002      assumption
     1003    ]
     1004  ]
     1005qed.
     1006
     1007lemma le_to_lt_or_eq:
     1008  ∀m, n: nat.
     1009    m ≤ n → m = n ∨ m < n.
     1010  #m #n #le_hyp
     1011  cases le_hyp
     1012  [1:
     1013    @or_introl %
     1014  |2:
     1015    #m' #le_hyp'
     1016    @or_intror
     1017    normalize
     1018    @le_S_S assumption
     1019  ]
     1020qed.
     1021
     1022lemma le_neq_to_lt:
     1023  ∀m, n: nat.
     1024    m ≤ n → m ≠ n → m < n.
     1025  #m #n #le_hyp #neq_hyp
     1026  cases neq_hyp
     1027  #eq_absurd_hyp
     1028  generalize in match (le_to_lt_or_eq m n le_hyp);
     1029  #disj_assm cases disj_assm
     1030  [1:
     1031    #absurd cases (eq_absurd_hyp absurd)
     1032  |2:
     1033    #assm assumption
     1034  ]
     1035qed.
     1036
     1037inverter nat_jmdiscr for nat.
     1038
     1039lemma plus_lt_to_lt:
     1040  ∀m, n, o: nat.
     1041    m + n < o → m < o.
     1042  #m #n #o
     1043  elim n
     1044  [1:
     1045    <(plus_n_O m) in ⊢ (% → ?);
     1046    #assumption assumption
     1047  |2:
     1048    #n' #inductive_hypothesis
     1049    <(plus_n_Sm m n') in ⊢ (% → ?);
     1050    #assm @inductive_hypothesis
     1051    normalize in assm; normalize
     1052    /2 by lt_S_to_lt/
     1053  ]
     1054qed.
     1055
     1056include "arithmetics/div_and_mod.ma".
     1057
     1058lemma n_plus_1_n_to_False:
     1059  ∀n: nat.
     1060    n + 1 = n → False.
     1061  #n elim n
     1062  [1:
     1063    normalize #absurd destruct(absurd)
     1064  |2:
     1065    #n' #inductive_hypothesis normalize
     1066    #absurd @inductive_hypothesis /2/
     1067  ]
     1068qed.
     1069
     1070lemma one_two_times_n_to_False:
     1071  ∀n: nat.
     1072    1=2*n→False.
     1073  #n cases n
     1074  [1:
     1075    normalize #absurd destruct(absurd)
     1076  |2:
     1077    #n' normalize #absurd
     1078    lapply (injective_S … absurd) -absurd #absurd
     1079    /2/
     1080  ]
     1081qed.
     1082
     1083let rec odd_p
     1084  (n: nat)
     1085    on n ≝
     1086  match n with
     1087  [ O ⇒ False
     1088  | S n' ⇒ even_p n'
     1089  ]
     1090and even_p
     1091  (n: nat)
     1092    on n ≝
     1093  match n with
     1094  [ O ⇒ True
     1095  | S n' ⇒ odd_p n'
     1096  ].
     1097
     1098let rec n_even_p_to_n_plus_2_even_p
     1099  (n: nat)
     1100    on n: even_p n → even_p (n + 2) ≝
     1101  match n with
     1102  [ O ⇒ ?
     1103  | S n' ⇒ ?
     1104  ]
     1105and n_odd_p_to_n_plus_2_odd_p
     1106  (n: nat)
     1107    on n: odd_p n → odd_p (n + 2) ≝
     1108  match n with
     1109  [ O ⇒ ?
     1110  | S n' ⇒ ?
     1111  ].
     1112  [1,3:
     1113    normalize #assm assumption
     1114  |2:
     1115    normalize @n_odd_p_to_n_plus_2_odd_p
     1116  |4:
     1117    normalize @n_even_p_to_n_plus_2_even_p
     1118  ]
     1119qed.
     1120
     1121let rec two_times_n_even_p
     1122  (n: nat)
     1123    on n: even_p (2 * n) ≝
     1124  match n with
     1125  [ O ⇒ ?
     1126  | S n' ⇒ ?
     1127  ]
     1128and two_times_n_plus_one_odd_p
     1129  (n: nat)
     1130    on n: odd_p ((2 * n) + 1) ≝
     1131  match n with
     1132  [ O ⇒ ?
     1133  | S n' ⇒ ?
     1134  ].
     1135  [1,3:
     1136    normalize @I
     1137  |2:
     1138    normalize
     1139    >plus_n_Sm
     1140    <(associative_plus n' n' 1)
     1141    >(plus_n_O (n' + n'))
     1142    cut(n' + n' + 0 + 1 = 2 * n' + 1)
     1143    [1:
     1144      //
     1145    |2:
     1146      #refl_assm >refl_assm
     1147      @two_times_n_plus_one_odd_p     
     1148    ]
     1149  |4:
     1150    normalize
     1151    >plus_n_Sm
     1152    cut(n' + (n' + 1) + 1 = (2 * n') + 2)
     1153    [1:
     1154      normalize /2/
     1155    |2:
     1156      #refl_assm >refl_assm
     1157      @n_even_p_to_n_plus_2_even_p
     1158      @two_times_n_even_p
     1159    ]
     1160  ]
     1161qed.
     1162
     1163include alias "basics/logic.ma".
     1164
     1165let rec even_p_to_not_odd_p
     1166  (n: nat)
     1167    on n: even_p n → ¬ odd_p n ≝
     1168  match n with
     1169  [ O ⇒ ?
     1170  | S n' ⇒ ?
     1171  ]
     1172and odd_p_to_not_even_p
     1173  (n: nat)
     1174    on n: odd_p n → ¬ even_p n ≝
     1175  match n with
     1176  [ O ⇒ ?
     1177  | S n' ⇒ ?
     1178  ].
     1179  [1:
     1180    normalize #_
     1181    @nmk #assm assumption
     1182  |3:
     1183    normalize #absurd
     1184    cases absurd
     1185  |2:
     1186    normalize
     1187    @odd_p_to_not_even_p
     1188  |4:
     1189    normalize
     1190    @even_p_to_not_odd_p
     1191  ]
     1192qed.
     1193
     1194lemma even_p_odd_p_cases:
     1195  ∀n: nat.
     1196    even_p n ∨ odd_p n.
     1197  #n elim n
     1198  [1:
     1199    normalize @or_introl @I
     1200  |2:
     1201    #n' #inductive_hypothesis
     1202    normalize
     1203    cases inductive_hypothesis
     1204    #assm
     1205    try (@or_introl assumption)
     1206    try (@or_intror assumption)
     1207  ]
     1208qed.
     1209
     1210lemma two_times_n_plus_one_refl_two_times_n_to_False:
     1211  ∀m, n: nat.
     1212    2 * m + 1 = 2 * n → False.
     1213  #m #n
     1214  #assm
     1215  cut (even_p (2 * n) ∧ even_p ((2 * m) + 1))
     1216  [1:
     1217    >assm
     1218    @conj
     1219    @two_times_n_even_p
     1220  |2:
     1221    * #_ #absurd
     1222    cases (even_p_to_not_odd_p … absurd)
     1223    #assm @assm
     1224    @two_times_n_plus_one_odd_p
     1225  ]
     1226qed.
     1227
     1228lemma not_Some_neq_None_to_False:
     1229  ∀a: Type[0].
     1230  ∀e: a.
     1231    ¬ (Some a e ≠ None a) → False.
     1232  #a #e #absurd cases absurd -absurd
     1233  #absurd @absurd @nmk -absurd
     1234  #absurd destruct(absurd)
     1235qed.
     1236
     1237lemma not_None_to_Some:
     1238  ∀A: Type[0].
     1239  ∀o: option A.
     1240    o ≠ None A → ∃v: A. o = Some A v.
     1241  #A #o cases o
     1242  [1:
     1243    #absurd cases absurd #absurd' cases (absurd' (refl …))
     1244  |2:
     1245    #v' #ignore /2/
     1246  ]
     1247qed.
     1248
    7971249lemma inclusive_disjunction_true:
    7981250  ∀b, c: bool.
     
    8341286qed.
    8351287
     1288(* XXX: to be moved into logic/basics.ma *)
     1289lemma and_intro_right:
     1290  ∀a, b: Prop.
     1291    a → (a → b) → a ∧ b.
     1292  #a #b /3/
     1293qed.
     1294
    8361295definition bool_to_Prop ≝
    8371296 λb. match b with [ true ⇒ True | false ⇒ False ].
     
    9241383interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    9251384
     1385(* Also extracts an equality proof (useful when not using Russell). *)
     1386notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
     1387 with precedence 10
     1388for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
     1389        λ${ident E}.$s ] (refl ? $t) }.
     1390
     1391notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
     1392 with precedence 10
     1393for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
     1394        λ${ident E}.$s ] (refl ? $t) }.
     1395
     1396notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
     1397 with precedence 10
     1398for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     1399       match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
     1400        λ${ident E}.$s ] ] (refl ? $t) }.
     1401
     1402notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
     1403 with precedence 10
     1404for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     1405       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
     1406        λ${ident E}.$s ] ] (refl ? $t) }.
     1407
    9261408lemma length_append:
    9271409 ∀A.∀l1,l2:list A.
  • src/common/Identifiers.ma

    r1908 r1928  
    308308  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    309309] qed.
     310
     311lemma lookup_present_add_hit:
     312  ∀tag, A, map, k, v, k_pres.
     313    lookup_present tag A (add … map k v) k k_pres = v.
     314  #tag #a #map #k #v #k_pres
     315  lapply (lookup_lookup_present … (add … map k v) … k_pres)
     316  >lookup_add_hit #Some_assm destruct(Some_assm)
     317  <e0 %
     318qed.
     319
     320lemma lookup_present_add_miss:
     321  ∀tag, A, map, k, k', v, k_pres', k_pres''.
     322    k' ≠ k →
     323      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
     324  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
     325  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
     326  >lookup_add_miss try assumption
     327  #Some_assm
     328  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
     329  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
     330qed.
     331
     332lemma present_add_present:
     333  ∀tag, a, map, k, k', v.
     334    k' ≠ k →
     335      present tag a (add tag a map k v) k' →
     336        present tag a map k'.
     337  #tag #a #map #k #k' #v #neq_hyp #present_hyp
     338  whd in match present; normalize nodelta
     339  whd in match present in present_hyp; normalize nodelta in present_hyp;
     340  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
     341  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
     342  [1:
     343    * #k_eq_hyp @⊥ /2/
     344  |2:
     345    #Some_eq_hyp' /2/
     346  ]
     347qed.
     348
     349lemma present_add_hit:
     350  ∀tag, a, map, k, v.
     351    present tag a (add tag a map k v) k.
     352  #tag #a #map #k #v
     353  whd >lookup_add_hit
     354  % #absurd destruct
     355qed.
     356
     357lemma present_add_miss:
     358  ∀tag, a, map, k, k', v.
     359    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
     360  #tag #a #map #k #k' #v #neq_assm #present_assm
     361  whd >lookup_add_miss assumption
     362qed.
    310363
    311364
Note: See TracChangeset for help on using the changeset viewer.