source: src/ASM/UtilBranch.ma @ 2168

Last change on this file since 2168 was 1946, checked in by sacerdot, 8 years ago

\snd half_add => add everywhere

File size: 2.2 KB
Line 
1include "ASM/Util.ma".
2include "ASM/Arithmetic.ma".
3
4definition nat_of_bool: bool → nat ≝
5  λb: bool.
6  match b with
7  [ true ⇒ 1
8  | false ⇒ 0
9  ].
10
11lemma 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
35qed.
36
37lemma 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  ]
67qed.
68
69lemma 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  ]
84qed.
85   
86lemma 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  ]
100qed.
Note: See TracBrowser for help on using the repository browser.