1 | include "ASM/Util.ma". |
---|

2 | include "ASM/Arithmetic.ma". |
---|

3 | |
---|

4 | definition nat_of_bool: bool → nat ≝ |
---|

5 | λb: bool. |
---|

6 | match b with |
---|

7 | [ true ⇒ 1 |
---|

8 | | false ⇒ 0 |
---|

9 | ]. |
---|

10 | |
---|

11 | lemma blah: |
---|

12 | ∀n: nat. |
---|

13 | ∀bv: BitVector n. |
---|

14 | ∀buffer: nat. |
---|

15 | nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n). |
---|

16 | #n #bv elim bv |
---|

17 | [1: |
---|

18 | #buffer elim buffer try % |
---|

19 | #buffer' #inductive_hypothesis |
---|

20 | normalize <times_n_1 % |
---|

21 | |2: |
---|

22 | #n' #hd #tl #inductive_hypothesis |
---|

23 | #buffer cases hd normalize |
---|

24 | >inductive_hypothesis |
---|

25 | >inductive_hypothesis |
---|

26 | [1: |
---|

27 | change with ( |
---|

28 | ? + (2 * buffer + 1) * ?) in ⊢ (??%?); |
---|

29 | change with ( |
---|

30 | ? + buffer * (2 * 2^n')) in ⊢ (???%); |
---|

31 | cases daemon |
---|

32 | ] |
---|

33 | ] |
---|

34 | cases daemon |
---|

35 | qed. |
---|

36 | |
---|

37 | lemma nat_of_bitvector_aux_hd_tl: |
---|

38 | ∀n: nat. |
---|

39 | ∀tl: BitVector n. |
---|

40 | ∀hd: bool. |
---|

41 | nat_of_bitvector (S n) (hd:::tl) = |
---|

42 | nat_of_bitvector n tl + (nat_of_bool hd * 2^n). |
---|

43 | #n #tl elim tl |
---|

44 | [1: |
---|

45 | #hd cases hd % |
---|

46 | |2: |
---|

47 | #n' #hd' #tl' #inductive_hypothesis #hd |
---|

48 | cases hd whd in ⊢ (??%?); normalize nodelta |
---|

49 | >inductive_hypothesis cases hd' normalize nodelta |
---|

50 | normalize in match (nat_of_bool ?); |
---|

51 | normalize in match (nat_of_bool ?); |
---|

52 | [4: |
---|

53 | normalize in match (2 * ?); |
---|

54 | <plus_n_O <plus_n_O % |
---|

55 | |3: |
---|

56 | normalize in match (2 * ?); |
---|

57 | normalize in match (0 + 1); |
---|

58 | <plus_n_O |
---|

59 | normalize in match (1 * ?); |
---|

60 | <plus_n_O |
---|

61 | cases daemon |
---|

62 | (* XXX: lemma *) |
---|

63 | |*: |
---|

64 | cases daemon |
---|

65 | ] |
---|

66 | ] |
---|

67 | qed. |
---|

68 | |
---|

69 | lemma succ_nat_of_bitvector_aux_half_add_1: |
---|

70 | ∀n: nat. |
---|

71 | ∀bv: BitVector n. |
---|

72 | ∀buffer: nat. |
---|

73 | ∀power_proof: nat_of_bitvector … bv < 2^n - 1. |
---|

74 | S (nat_of_bitvector_aux n buffer bv) = |
---|

75 | nat_of_bitvector … (add n (bitvector_of_nat … 1) bv). |
---|

76 | #n #bv elim bv |
---|

77 | [1: |
---|

78 | #buffer normalize #absurd |
---|

79 | cases (lt_to_not_zero … absurd) |
---|

80 | |2: |
---|

81 | #n' #hd #tl #inductive_hypothesis #buffer |
---|

82 | cases daemon |
---|

83 | ] |
---|

84 | qed. |
---|

85 | |
---|

86 | lemma succ_nat_of_bitvector_half_add_1: |
---|

87 | ∀n: nat. |
---|

88 | ∀bv: BitVector n. |
---|

89 | ∀power_proof: nat_of_bitvector … bv < 2^n - 1. |
---|

90 | S (nat_of_bitvector … bv) = nat_of_bitvector … |
---|

91 | (add n (bitvector_of_nat … 1) bv). |
---|

92 | #n #bv elim bv |
---|

93 | [1: |
---|

94 | normalize #absurd |
---|

95 | cases (lt_to_not_zero … absurd) |
---|

96 | |2: |
---|

97 | #n' #hd #tl #inductive_hypothesis |
---|

98 | cases daemon |
---|

99 | ] |
---|

100 | qed. |
---|