Changeset 1928 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 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).

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.