# source:src/ASM/BitVectorZ.ma@916

Last change on this file since 916 was 891, checked in by campbell, 10 years ago

Revise proofs affected by recent matita change.

File size: 4.0 KB
Line
1
2include "utilities/binary/Z.ma".
3include "ASM/BitVector.ma".
4include "ASM/Arithmetic.ma".
5
6let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
7match bv with
8[ VEmpty ⇒ OZ
9| VCons n' h t ⇒
10    if h then pos (fold_left ??? (λacc,b.if b then (p1 acc) else (p0 acc)) one t)
11         else (Z_of_unsigned_bitvector ? t)
12].
13
14definition Z_of_signed_bitvector ≝
15λn.λbv:BitVector n.
16match bv with
17[ VEmpty ⇒ OZ
18| VCons n' h t ⇒
19    if h then - (Zsucc (Z_of_unsigned_bitvector ? (negation_bv ? t)))
20         else (Z_of_unsigned_bitvector n' t)
21].
22
23(* Reverses, so LSB first. *)
24let rec bits_of_pos (p:Pos) : list bool ≝
25match p with
26[ one ⇒ [true]
27| p0 p' ⇒ false::(bits_of_pos p')
28| p1 p' ⇒  true::(bits_of_pos p')
29].
30
31let rec zeroext_reversed (n:nat) (m:nat) (bv:BitVector n) on m : BitVector m ≝
32match m with
33[ O ⇒ [[ ]]
34| S m' ⇒
35    match bv with
36    [ VEmpty ⇒ zero (S m')
37    | VCons n' h t ⇒ VCons ? m' h (zeroext_reversed n' m' t)
38    ]
39].
40
41let rec bitvector_of_Z (n:nat) (z:Z) on z : BitVector n ≝
42match z with
43[ OZ ⇒ zero n
44| pos p ⇒
45  let bits ≝ bits_of_pos p in
46  reverse ?? (zeroext_reversed ? n (vector_of_list … bits))
47| neg p ⇒
48  match p with
49  [ one ⇒ maximum ?
50  | _ ⇒
51    let bits ≝ bits_of_pos (pred p) in
52    let pz ≝ reverse ?? (zeroext_reversed ? n (vector_of_list … bits)) in
53    negation_bv ? pz
54  ]
55].
56
57theorem bv_Z_unsigned_min : ∀n. ∀bv:BitVector n. OZ ≤ Z_of_unsigned_bitvector n bv.
58#n #bv elim bv
59[ //
60| #m * #t #IH whd in ⊢ (??%) //
61] qed.
62
63(* Use bit counting to show the max *)
64
65let rec pos_length (p:Pos) : nat ≝
66match p with
67[ one ⇒ O
68| p0 q ⇒ S (pos_length q)
69| p1 q ⇒ S (pos_length q)
70].
71
72lemma pos_length_lt: ∀p,q. pos_length p < pos_length q → p < q.
73#p elim p
74[ * [ normalize #H elim (absurd ? H (not_le_Sn_n 0))
75    | #q #_ @(lt_one_S (p0 q))
76    | #q #_ >p0_times2 /2/
77    ]
78| #p' #IH
79  * [ normalize #H elim (absurd ? H (not_le_Sn_O ?))
80    | #q #H change with (one+ (p0 p') < one+(p0 q)) @monotonic_lt_plus_r
81      >p0_times2 >(p0_times2 q)
82      @monotonic_lt_times_r @IH
83      @le_S_S_to_le @H
84    | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q))
85      >p0_times2 >(p0_times2 q)
86      change with (succ one * succ p' ≤ succ one * q)
87      @monotonic_le_times_r @IH
88      @le_S_S_to_le @H
89    ]
90| #p' #IH
91  * [ normalize #H elim (absurd ? H (not_le_Sn_O ?))
92    | #q #H change with ((p0 p') < succ (p0 q)) @le_S
93      >p0_times2 >(p0_times2 q)
94      @monotonic_lt_times_r @IH
95      @le_S_S_to_le @H
96    | #q #H
97      >p0_times2 >(p0_times2 q)
98      @monotonic_lt_times_r @IH
99      @le_S_S_to_le @H
100    ]
101] qed.
102
103lemma bvZ_length : ∀n.∀bv:BitVector n. match Z_of_unsigned_bitvector n bv with
104[ OZ ⇒ True | pos p ⇒ pos_length p < n | neg p ⇒ False ].
105#n #bv elim bv
106[ @I
107| #m *
108[ 2: #tl normalize cases (Z_of_unsigned_bitvector m tl) normalize /2/
109| #tl #_ normalize @le_S_S
110  change with (? ≤ pos_length one + m)
111  generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl
112  [ // | #o * #t normalize #IH #p <plus_n_Sm
113    change with (? ≤ pos_length (p1 p) + o)
114    @IH
115  ]
116] qed.
117
118lemma two_power_length : ∀n. pos_length (two_power_nat n) = n.
119#n elim n
120[ @refl
121| #m #IH normalize > IH @refl
122] qed.
123
124theorem bv_Z_unsigned_max : ∀n. ∀bv:BitVector n. Z_of_unsigned_bitvector n bv < Z_two_power_nat n.
125#n #bv normalize
126lapply (bvZ_length n bv) cases (Z_of_unsigned_bitvector n bv) // #p normalize /2/
127qed.
128
129lemma Zopp_le: ∀x,y. x ≤ y → -y ≤ -x.
130* [ 2,3: #p ] * [ 2,3: #q ] //
131qed.
132
133theorem bv_Z_signed_min : ∀n. ∀bv:BitVector n. - Z_two_power_nat n ≤ Z_of_signed_bitvector n bv.
134#n *
135[ //
136| #m *
137  [ #bv @Zopp_le @(transitive_Zle … (Z_two_power_nat m))
138    [ @Zlt_to_Zle @bv_Z_unsigned_max
139    | normalize //
140    ]
141  | #bv @(transitive_Zle … 0) //
142  ]
143] qed.
144
145theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n.
146#n #bv @(vector_inv_n ? (S n) ? bv) *
147[ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))
148  cases (Z_of_unsigned_bitvector n (negation_bv n t)) //
149  #p *
150| #t whd in ⊢ (?%?) //
151] qed.
Note: See TracBrowser for help on using the repository browser.