From e30e864d61431a0145853fcf90b5f16b781f4a46 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Nov 2018 21:19:05 -0500 Subject: Add `String Notation` vernacular like `Numeral Notation` Users can now register string notations for custom inductives. Much of the code and documentation was copied from numeral notations. I chose to use a 256-constructor inductive for primitive string syntax because (a) it is easy to convert between character codes and constructors, and (b) it is more efficient than the existing `ascii` type. Some choices about proofs of the new `byte` type were made based on efficiency. For example, https://github.com/coq/coq/issues/8517 means that we cannot simply use `Scheme Equality` for this type, and I have taken some care to ensure that the proofs of decidable equality and conversion are fast. (Unfortunately, the `Init/Byte.v` file is the slowest one in the prelude (it takes a couple of seconds to build), and I'm not sure where the slowness is.) In String.v, some uses of `0` as a `nat` were replaced by `O`, because the file initially refused to check interactively otherwise (it complained that `0` could not be interpreted in `string_scope` before loading `Coq.Strings.String`). There is unfortunately a decent amount of code duplication between numeral notations and string notations. I have not put too much thought into chosing names; most names have been chosen to be similar to numeral notations, though I chose the name `byte` from https://github.com/coq/coq/issues/8483#issuecomment-421671785. Unfortunately, this feature does not support declaring string syntax for `list ascii`, unless that type is wrapped in a record or other inductive type. This is not a fundamental limitation; it should be relatively easy for someone who knows the API of the reduction machinery in Coq to extend both this and numeral notations to support any type whose hnf starts with an inductive type. (The reason for needing an inductive type to bottom out at is that this is how the plugin determines what constructors are the entry points for printing the given notation. However, see also https://github.com/coq/coq/issues/8964 for complications that are more likely to arise if inductive type families are supported.) N.B. I generated the long lists of constructors for the `byte` type with short python scripts. Closes #8853 --- theories/Init/Byte.v | 302 ++++++++++ theories/Init/Prelude.v | 5 + theories/Strings/Ascii.v | 59 +- theories/Strings/Byte.v | 1425 +++++++++++++++++++++++++++++++++++++++++++++ theories/Strings/String.v | 86 ++- 5 files changed, 1853 insertions(+), 24 deletions(-) create mode 100644 theories/Init/Byte.v create mode 100644 theories/Strings/Byte.v (limited to 'theories') diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v new file mode 100644 index 0000000000..2d8ee30a43 --- /dev/null +++ b/theories/Init/Byte.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v + | None => x00 (* can't happen *) + end. + +Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. +Proof. + cbv [ascii_of_byte byte_of_ascii]. + pose proof (to_of_N (N_of_ascii x)). + destruct (of_N (N_of_ascii x)) as [x'|] eqn:H1. + { specialize (H x' eq_refl); rewrite H. + apply ascii_N_embedding. } + { exfalso. + rewrite of_N_None_iff in H1. + pose proof (N_ascii_bounded x) as H2. + rewrite N.lt_nge in H1, H2. + destruct (N.le_gt_cases (N_of_ascii x) 255) as [H3|H3]. + { apply H1, H3. } + { rewrite <- N.le_succ_l in H3; apply H2, H3. } } +Qed. + +Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x. +Proof. + cbv [ascii_of_byte byte_of_ascii]. + rewrite N_ascii_embedding, of_to_N; [ reflexivity | ]. + pose proof (to_N_bounded x) as H. + rewrite <- N.lt_succ_r in H; exact H. +Qed. + +Module Export AsciiSyntax. + String Notation ascii ascii_of_byte byte_of_ascii : char_scope. +End AsciiSyntax. Local Open Scope char_scope. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v new file mode 100644 index 0000000000..581094a8b5 --- /dev/null +++ b/theories/Strings/Byte.v @@ -0,0 +1,1425 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Byte.eqb x y = true. +Proof. intro; subst y; destruct x; reflexivity. Defined. + +Definition byte_dec_bl x y (H : Byte.eqb x y = true) : x = y + := match H in (_ = tr) return if tr then x = y else True with + | eq_refl + => match x, y return if Byte.eqb x y then x = y else True with + | x00, x00 => eq_refl + | x01, x01 => eq_refl + | x02, x02 => eq_refl + | x03, x03 => eq_refl + | x04, x04 => eq_refl + | x05, x05 => eq_refl + | x06, x06 => eq_refl + | x07, x07 => eq_refl + | x08, x08 => eq_refl + | x09, x09 => eq_refl + | x0a, x0a => eq_refl + | x0b, x0b => eq_refl + | x0c, x0c => eq_refl + | x0d, x0d => eq_refl + | x0e, x0e => eq_refl + | x0f, x0f => eq_refl + | x10, x10 => eq_refl + | x11, x11 => eq_refl + | x12, x12 => eq_refl + | x13, x13 => eq_refl + | x14, x14 => eq_refl + | x15, x15 => eq_refl + | x16, x16 => eq_refl + | x17, x17 => eq_refl + | x18, x18 => eq_refl + | x19, x19 => eq_refl + | x1a, x1a => eq_refl + | x1b, x1b => eq_refl + | x1c, x1c => eq_refl + | x1d, x1d => eq_refl + | x1e, x1e => eq_refl + | x1f, x1f => eq_refl + | x20, x20 => eq_refl + | x21, x21 => eq_refl + | x22, x22 => eq_refl + | x23, x23 => eq_refl + | x24, x24 => eq_refl + | x25, x25 => eq_refl + | x26, x26 => eq_refl + | x27, x27 => eq_refl + | x28, x28 => eq_refl + | x29, x29 => eq_refl + | x2a, x2a => eq_refl + | x2b, x2b => eq_refl + | x2c, x2c => eq_refl + | x2d, x2d => eq_refl + | x2e, x2e => eq_refl + | x2f, x2f => eq_refl + | x30, x30 => eq_refl + | x31, x31 => eq_refl + | x32, x32 => eq_refl + | x33, x33 => eq_refl + | x34, x34 => eq_refl + | x35, x35 => eq_refl + | x36, x36 => eq_refl + | x37, x37 => eq_refl + | x38, x38 => eq_refl + | x39, x39 => eq_refl + | x3a, x3a => eq_refl + | x3b, x3b => eq_refl + | x3c, x3c => eq_refl + | x3d, x3d => eq_refl + | x3e, x3e => eq_refl + | x3f, x3f => eq_refl + | x40, x40 => eq_refl + | x41, x41 => eq_refl + | x42, x42 => eq_refl + | x43, x43 => eq_refl + | x44, x44 => eq_refl + | x45, x45 => eq_refl + | x46, x46 => eq_refl + | x47, x47 => eq_refl + | x48, x48 => eq_refl + | x49, x49 => eq_refl + | x4a, x4a => eq_refl + | x4b, x4b => eq_refl + | x4c, x4c => eq_refl + | x4d, x4d => eq_refl + | x4e, x4e => eq_refl + | x4f, x4f => eq_refl + | x50, x50 => eq_refl + | x51, x51 => eq_refl + | x52, x52 => eq_refl + | x53, x53 => eq_refl + | x54, x54 => eq_refl + | x55, x55 => eq_refl + | x56, x56 => eq_refl + | x57, x57 => eq_refl + | x58, x58 => eq_refl + | x59, x59 => eq_refl + | x5a, x5a => eq_refl + | x5b, x5b => eq_refl + | x5c, x5c => eq_refl + | x5d, x5d => eq_refl + | x5e, x5e => eq_refl + | x5f, x5f => eq_refl + | x60, x60 => eq_refl + | x61, x61 => eq_refl + | x62, x62 => eq_refl + | x63, x63 => eq_refl + | x64, x64 => eq_refl + | x65, x65 => eq_refl + | x66, x66 => eq_refl + | x67, x67 => eq_refl + | x68, x68 => eq_refl + | x69, x69 => eq_refl + | x6a, x6a => eq_refl + | x6b, x6b => eq_refl + | x6c, x6c => eq_refl + | x6d, x6d => eq_refl + | x6e, x6e => eq_refl + | x6f, x6f => eq_refl + | x70, x70 => eq_refl + | x71, x71 => eq_refl + | x72, x72 => eq_refl + | x73, x73 => eq_refl + | x74, x74 => eq_refl + | x75, x75 => eq_refl + | x76, x76 => eq_refl + | x77, x77 => eq_refl + | x78, x78 => eq_refl + | x79, x79 => eq_refl + | x7a, x7a => eq_refl + | x7b, x7b => eq_refl + | x7c, x7c => eq_refl + | x7d, x7d => eq_refl + | x7e, x7e => eq_refl + | x7f, x7f => eq_refl + | x80, x80 => eq_refl + | x81, x81 => eq_refl + | x82, x82 => eq_refl + | x83, x83 => eq_refl + | x84, x84 => eq_refl + | x85, x85 => eq_refl + | x86, x86 => eq_refl + | x87, x87 => eq_refl + | x88, x88 => eq_refl + | x89, x89 => eq_refl + | x8a, x8a => eq_refl + | x8b, x8b => eq_refl + | x8c, x8c => eq_refl + | x8d, x8d => eq_refl + | x8e, x8e => eq_refl + | x8f, x8f => eq_refl + | x90, x90 => eq_refl + | x91, x91 => eq_refl + | x92, x92 => eq_refl + | x93, x93 => eq_refl + | x94, x94 => eq_refl + | x95, x95 => eq_refl + | x96, x96 => eq_refl + | x97, x97 => eq_refl + | x98, x98 => eq_refl + | x99, x99 => eq_refl + | x9a, x9a => eq_refl + | x9b, x9b => eq_refl + | x9c, x9c => eq_refl + | x9d, x9d => eq_refl + | x9e, x9e => eq_refl + | x9f, x9f => eq_refl + | xa0, xa0 => eq_refl + | xa1, xa1 => eq_refl + | xa2, xa2 => eq_refl + | xa3, xa3 => eq_refl + | xa4, xa4 => eq_refl + | xa5, xa5 => eq_refl + | xa6, xa6 => eq_refl + | xa7, xa7 => eq_refl + | xa8, xa8 => eq_refl + | xa9, xa9 => eq_refl + | xaa, xaa => eq_refl + | xab, xab => eq_refl + | xac, xac => eq_refl + | xad, xad => eq_refl + | xae, xae => eq_refl + | xaf, xaf => eq_refl + | xb0, xb0 => eq_refl + | xb1, xb1 => eq_refl + | xb2, xb2 => eq_refl + | xb3, xb3 => eq_refl + | xb4, xb4 => eq_refl + | xb5, xb5 => eq_refl + | xb6, xb6 => eq_refl + | xb7, xb7 => eq_refl + | xb8, xb8 => eq_refl + | xb9, xb9 => eq_refl + | xba, xba => eq_refl + | xbb, xbb => eq_refl + | xbc, xbc => eq_refl + | xbd, xbd => eq_refl + | xbe, xbe => eq_refl + | xbf, xbf => eq_refl + | xc0, xc0 => eq_refl + | xc1, xc1 => eq_refl + | xc2, xc2 => eq_refl + | xc3, xc3 => eq_refl + | xc4, xc4 => eq_refl + | xc5, xc5 => eq_refl + | xc6, xc6 => eq_refl + | xc7, xc7 => eq_refl + | xc8, xc8 => eq_refl + | xc9, xc9 => eq_refl + | xca, xca => eq_refl + | xcb, xcb => eq_refl + | xcc, xcc => eq_refl + | xcd, xcd => eq_refl + | xce, xce => eq_refl + | xcf, xcf => eq_refl + | xd0, xd0 => eq_refl + | xd1, xd1 => eq_refl + | xd2, xd2 => eq_refl + | xd3, xd3 => eq_refl + | xd4, xd4 => eq_refl + | xd5, xd5 => eq_refl + | xd6, xd6 => eq_refl + | xd7, xd7 => eq_refl + | xd8, xd8 => eq_refl + | xd9, xd9 => eq_refl + | xda, xda => eq_refl + | xdb, xdb => eq_refl + | xdc, xdc => eq_refl + | xdd, xdd => eq_refl + | xde, xde => eq_refl + | xdf, xdf => eq_refl + | xe0, xe0 => eq_refl + | xe1, xe1 => eq_refl + | xe2, xe2 => eq_refl + | xe3, xe3 => eq_refl + | xe4, xe4 => eq_refl + | xe5, xe5 => eq_refl + | xe6, xe6 => eq_refl + | xe7, xe7 => eq_refl + | xe8, xe8 => eq_refl + | xe9, xe9 => eq_refl + | xea, xea => eq_refl + | xeb, xeb => eq_refl + | xec, xec => eq_refl + | xed, xed => eq_refl + | xee, xee => eq_refl + | xef, xef => eq_refl + | xf0, xf0 => eq_refl + | xf1, xf1 => eq_refl + | xf2, xf2 => eq_refl + | xf3, xf3 => eq_refl + | xf4, xf4 => eq_refl + | xf5, xf5 => eq_refl + | xf6, xf6 => eq_refl + | xf7, xf7 => eq_refl + | xf8, xf8 => eq_refl + | xf9, xf9 => eq_refl + | xfa, xfa => eq_refl + | xfb, xfb => eq_refl + | xfc, xfc => eq_refl + | xfd, xfd => eq_refl + | xfe, xfe => eq_refl + | xff, xff => eq_refl + | _, _ => I + end + end. + +Lemma eqb_false x y : Byte.eqb x y = false -> x <> y. +Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed. + +Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y} + := (if Byte.eqb x y as beq return Byte.eqb x y = beq -> _ + then fun pf => left (byte_dec_bl x y pf) + else fun pf => right (eqb_false pf)) + eq_refl. + +Section nat. + Definition to_nat (x : byte) : nat + := match x with + | x00 => 0 + | x01 => 1 + | x02 => 2 + | x03 => 3 + | x04 => 4 + | x05 => 5 + | x06 => 6 + | x07 => 7 + | x08 => 8 + | x09 => 9 + | x0a => 10 + | x0b => 11 + | x0c => 12 + | x0d => 13 + | x0e => 14 + | x0f => 15 + | x10 => 16 + | x11 => 17 + | x12 => 18 + | x13 => 19 + | x14 => 20 + | x15 => 21 + | x16 => 22 + | x17 => 23 + | x18 => 24 + | x19 => 25 + | x1a => 26 + | x1b => 27 + | x1c => 28 + | x1d => 29 + | x1e => 30 + | x1f => 31 + | x20 => 32 + | x21 => 33 + | x22 => 34 + | x23 => 35 + | x24 => 36 + | x25 => 37 + | x26 => 38 + | x27 => 39 + | x28 => 40 + | x29 => 41 + | x2a => 42 + | x2b => 43 + | x2c => 44 + | x2d => 45 + | x2e => 46 + | x2f => 47 + | x30 => 48 + | x31 => 49 + | x32 => 50 + | x33 => 51 + | x34 => 52 + | x35 => 53 + | x36 => 54 + | x37 => 55 + | x38 => 56 + | x39 => 57 + | x3a => 58 + | x3b => 59 + | x3c => 60 + | x3d => 61 + | x3e => 62 + | x3f => 63 + | x40 => 64 + | x41 => 65 + | x42 => 66 + | x43 => 67 + | x44 => 68 + | x45 => 69 + | x46 => 70 + | x47 => 71 + | x48 => 72 + | x49 => 73 + | x4a => 74 + | x4b => 75 + | x4c => 76 + | x4d => 77 + | x4e => 78 + | x4f => 79 + | x50 => 80 + | x51 => 81 + | x52 => 82 + | x53 => 83 + | x54 => 84 + | x55 => 85 + | x56 => 86 + | x57 => 87 + | x58 => 88 + | x59 => 89 + | x5a => 90 + | x5b => 91 + | x5c => 92 + | x5d => 93 + | x5e => 94 + | x5f => 95 + | x60 => 96 + | x61 => 97 + | x62 => 98 + | x63 => 99 + | x64 => 100 + | x65 => 101 + | x66 => 102 + | x67 => 103 + | x68 => 104 + | x69 => 105 + | x6a => 106 + | x6b => 107 + | x6c => 108 + | x6d => 109 + | x6e => 110 + | x6f => 111 + | x70 => 112 + | x71 => 113 + | x72 => 114 + | x73 => 115 + | x74 => 116 + | x75 => 117 + | x76 => 118 + | x77 => 119 + | x78 => 120 + | x79 => 121 + | x7a => 122 + | x7b => 123 + | x7c => 124 + | x7d => 125 + | x7e => 126 + | x7f => 127 + | x80 => 128 + | x81 => 129 + | x82 => 130 + | x83 => 131 + | x84 => 132 + | x85 => 133 + | x86 => 134 + | x87 => 135 + | x88 => 136 + | x89 => 137 + | x8a => 138 + | x8b => 139 + | x8c => 140 + | x8d => 141 + | x8e => 142 + | x8f => 143 + | x90 => 144 + | x91 => 145 + | x92 => 146 + | x93 => 147 + | x94 => 148 + | x95 => 149 + | x96 => 150 + | x97 => 151 + | x98 => 152 + | x99 => 153 + | x9a => 154 + | x9b => 155 + | x9c => 156 + | x9d => 157 + | x9e => 158 + | x9f => 159 + | xa0 => 160 + | xa1 => 161 + | xa2 => 162 + | xa3 => 163 + | xa4 => 164 + | xa5 => 165 + | xa6 => 166 + | xa7 => 167 + | xa8 => 168 + | xa9 => 169 + | xaa => 170 + | xab => 171 + | xac => 172 + | xad => 173 + | xae => 174 + | xaf => 175 + | xb0 => 176 + | xb1 => 177 + | xb2 => 178 + | xb3 => 179 + | xb4 => 180 + | xb5 => 181 + | xb6 => 182 + | xb7 => 183 + | xb8 => 184 + | xb9 => 185 + | xba => 186 + | xbb => 187 + | xbc => 188 + | xbd => 189 + | xbe => 190 + | xbf => 191 + | xc0 => 192 + | xc1 => 193 + | xc2 => 194 + | xc3 => 195 + | xc4 => 196 + | xc5 => 197 + | xc6 => 198 + | xc7 => 199 + | xc8 => 200 + | xc9 => 201 + | xca => 202 + | xcb => 203 + | xcc => 204 + | xcd => 205 + | xce => 206 + | xcf => 207 + | xd0 => 208 + | xd1 => 209 + | xd2 => 210 + | xd3 => 211 + | xd4 => 212 + | xd5 => 213 + | xd6 => 214 + | xd7 => 215 + | xd8 => 216 + | xd9 => 217 + | xda => 218 + | xdb => 219 + | xdc => 220 + | xdd => 221 + | xde => 222 + | xdf => 223 + | xe0 => 224 + | xe1 => 225 + | xe2 => 226 + | xe3 => 227 + | xe4 => 228 + | xe5 => 229 + | xe6 => 230 + | xe7 => 231 + | xe8 => 232 + | xe9 => 233 + | xea => 234 + | xeb => 235 + | xec => 236 + | xed => 237 + | xee => 238 + | xef => 239 + | xf0 => 240 + | xf1 => 241 + | xf2 => 242 + | xf3 => 243 + | xf4 => 244 + | xf5 => 245 + | xf6 => 246 + | xf7 => 247 + | xf8 => 248 + | xf9 => 249 + | xfa => 250 + | xfb => 251 + | xfc => 252 + | xfd => 253 + | xfe => 254 + | xff => 255 + end. + + Definition of_nat (x : nat) : option byte + := match x with + | 0 => Some x00 + | 1 => Some x01 + | 2 => Some x02 + | 3 => Some x03 + | 4 => Some x04 + | 5 => Some x05 + | 6 => Some x06 + | 7 => Some x07 + | 8 => Some x08 + | 9 => Some x09 + | 10 => Some x0a + | 11 => Some x0b + | 12 => Some x0c + | 13 => Some x0d + | 14 => Some x0e + | 15 => Some x0f + | 16 => Some x10 + | 17 => Some x11 + | 18 => Some x12 + | 19 => Some x13 + | 20 => Some x14 + | 21 => Some x15 + | 22 => Some x16 + | 23 => Some x17 + | 24 => Some x18 + | 25 => Some x19 + | 26 => Some x1a + | 27 => Some x1b + | 28 => Some x1c + | 29 => Some x1d + | 30 => Some x1e + | 31 => Some x1f + | 32 => Some x20 + | 33 => Some x21 + | 34 => Some x22 + | 35 => Some x23 + | 36 => Some x24 + | 37 => Some x25 + | 38 => Some x26 + | 39 => Some x27 + | 40 => Some x28 + | 41 => Some x29 + | 42 => Some x2a + | 43 => Some x2b + | 44 => Some x2c + | 45 => Some x2d + | 46 => Some x2e + | 47 => Some x2f + | 48 => Some x30 + | 49 => Some x31 + | 50 => Some x32 + | 51 => Some x33 + | 52 => Some x34 + | 53 => Some x35 + | 54 => Some x36 + | 55 => Some x37 + | 56 => Some x38 + | 57 => Some x39 + | 58 => Some x3a + | 59 => Some x3b + | 60 => Some x3c + | 61 => Some x3d + | 62 => Some x3e + | 63 => Some x3f + | 64 => Some x40 + | 65 => Some x41 + | 66 => Some x42 + | 67 => Some x43 + | 68 => Some x44 + | 69 => Some x45 + | 70 => Some x46 + | 71 => Some x47 + | 72 => Some x48 + | 73 => Some x49 + | 74 => Some x4a + | 75 => Some x4b + | 76 => Some x4c + | 77 => Some x4d + | 78 => Some x4e + | 79 => Some x4f + | 80 => Some x50 + | 81 => Some x51 + | 82 => Some x52 + | 83 => Some x53 + | 84 => Some x54 + | 85 => Some x55 + | 86 => Some x56 + | 87 => Some x57 + | 88 => Some x58 + | 89 => Some x59 + | 90 => Some x5a + | 91 => Some x5b + | 92 => Some x5c + | 93 => Some x5d + | 94 => Some x5e + | 95 => Some x5f + | 96 => Some x60 + | 97 => Some x61 + | 98 => Some x62 + | 99 => Some x63 + | 100 => Some x64 + | 101 => Some x65 + | 102 => Some x66 + | 103 => Some x67 + | 104 => Some x68 + | 105 => Some x69 + | 106 => Some x6a + | 107 => Some x6b + | 108 => Some x6c + | 109 => Some x6d + | 110 => Some x6e + | 111 => Some x6f + | 112 => Some x70 + | 113 => Some x71 + | 114 => Some x72 + | 115 => Some x73 + | 116 => Some x74 + | 117 => Some x75 + | 118 => Some x76 + | 119 => Some x77 + | 120 => Some x78 + | 121 => Some x79 + | 122 => Some x7a + | 123 => Some x7b + | 124 => Some x7c + | 125 => Some x7d + | 126 => Some x7e + | 127 => Some x7f + | 128 => Some x80 + | 129 => Some x81 + | 130 => Some x82 + | 131 => Some x83 + | 132 => Some x84 + | 133 => Some x85 + | 134 => Some x86 + | 135 => Some x87 + | 136 => Some x88 + | 137 => Some x89 + | 138 => Some x8a + | 139 => Some x8b + | 140 => Some x8c + | 141 => Some x8d + | 142 => Some x8e + | 143 => Some x8f + | 144 => Some x90 + | 145 => Some x91 + | 146 => Some x92 + | 147 => Some x93 + | 148 => Some x94 + | 149 => Some x95 + | 150 => Some x96 + | 151 => Some x97 + | 152 => Some x98 + | 153 => Some x99 + | 154 => Some x9a + | 155 => Some x9b + | 156 => Some x9c + | 157 => Some x9d + | 158 => Some x9e + | 159 => Some x9f + | 160 => Some xa0 + | 161 => Some xa1 + | 162 => Some xa2 + | 163 => Some xa3 + | 164 => Some xa4 + | 165 => Some xa5 + | 166 => Some xa6 + | 167 => Some xa7 + | 168 => Some xa8 + | 169 => Some xa9 + | 170 => Some xaa + | 171 => Some xab + | 172 => Some xac + | 173 => Some xad + | 174 => Some xae + | 175 => Some xaf + | 176 => Some xb0 + | 177 => Some xb1 + | 178 => Some xb2 + | 179 => Some xb3 + | 180 => Some xb4 + | 181 => Some xb5 + | 182 => Some xb6 + | 183 => Some xb7 + | 184 => Some xb8 + | 185 => Some xb9 + | 186 => Some xba + | 187 => Some xbb + | 188 => Some xbc + | 189 => Some xbd + | 190 => Some xbe + | 191 => Some xbf + | 192 => Some xc0 + | 193 => Some xc1 + | 194 => Some xc2 + | 195 => Some xc3 + | 196 => Some xc4 + | 197 => Some xc5 + | 198 => Some xc6 + | 199 => Some xc7 + | 200 => Some xc8 + | 201 => Some xc9 + | 202 => Some xca + | 203 => Some xcb + | 204 => Some xcc + | 205 => Some xcd + | 206 => Some xce + | 207 => Some xcf + | 208 => Some xd0 + | 209 => Some xd1 + | 210 => Some xd2 + | 211 => Some xd3 + | 212 => Some xd4 + | 213 => Some xd5 + | 214 => Some xd6 + | 215 => Some xd7 + | 216 => Some xd8 + | 217 => Some xd9 + | 218 => Some xda + | 219 => Some xdb + | 220 => Some xdc + | 221 => Some xdd + | 222 => Some xde + | 223 => Some xdf + | 224 => Some xe0 + | 225 => Some xe1 + | 226 => Some xe2 + | 227 => Some xe3 + | 228 => Some xe4 + | 229 => Some xe5 + | 230 => Some xe6 + | 231 => Some xe7 + | 232 => Some xe8 + | 233 => Some xe9 + | 234 => Some xea + | 235 => Some xeb + | 236 => Some xec + | 237 => Some xed + | 238 => Some xee + | 239 => Some xef + | 240 => Some xf0 + | 241 => Some xf1 + | 242 => Some xf2 + | 243 => Some xf3 + | 244 => Some xf4 + | 245 => Some xf5 + | 246 => Some xf6 + | 247 => Some xf7 + | 248 => Some xf8 + | 249 => Some xf9 + | 250 => Some xfa + | 251 => Some xfb + | 252 => Some xfc + | 253 => Some xfd + | 254 => Some xfe + | 255 => Some xff + | _ => None + end. + + Lemma of_to_nat x : of_nat (to_nat x) = Some x. + Proof. destruct x; reflexivity. Qed. + + Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x. + Proof. + do 256 try destruct x as [|x]; cbv [of_nat]; intro. + all: repeat match goal with + | _ => reflexivity + | _ => progress subst + | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + end. + Qed. + + Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x. + Proof. split; intro; subst; (apply of_to_nat || apply to_of_nat); assumption. Qed. + + Lemma to_of_nat_option_map x : option_map to_nat (of_nat x) = if Nat.leb x 255 then Some x else None. + Proof. do 256 try destruct x as [|x]; reflexivity. Qed. + + Lemma to_nat_bounded x : to_nat x <= 255. + Proof. + generalize (to_of_nat_option_map (to_nat x)). + rewrite of_to_nat; cbn [option_map]. + destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ]. + rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H. + intro; assumption. + Qed. + + Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x. + Proof. + generalize (to_of_nat_option_map x). + destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence. + { rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ]. + rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. } + { rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ]. + rewrite PeanoNat.Nat.lt_nge; intro; assumption. } + Qed. +End nat. + +Section N. + Local Open Scope N_scope. + + Definition to_N (x : byte) : N + := match x with + | x00 => 0 + | x01 => 1 + | x02 => 2 + | x03 => 3 + | x04 => 4 + | x05 => 5 + | x06 => 6 + | x07 => 7 + | x08 => 8 + | x09 => 9 + | x0a => 10 + | x0b => 11 + | x0c => 12 + | x0d => 13 + | x0e => 14 + | x0f => 15 + | x10 => 16 + | x11 => 17 + | x12 => 18 + | x13 => 19 + | x14 => 20 + | x15 => 21 + | x16 => 22 + | x17 => 23 + | x18 => 24 + | x19 => 25 + | x1a => 26 + | x1b => 27 + | x1c => 28 + | x1d => 29 + | x1e => 30 + | x1f => 31 + | x20 => 32 + | x21 => 33 + | x22 => 34 + | x23 => 35 + | x24 => 36 + | x25 => 37 + | x26 => 38 + | x27 => 39 + | x28 => 40 + | x29 => 41 + | x2a => 42 + | x2b => 43 + | x2c => 44 + | x2d => 45 + | x2e => 46 + | x2f => 47 + | x30 => 48 + | x31 => 49 + | x32 => 50 + | x33 => 51 + | x34 => 52 + | x35 => 53 + | x36 => 54 + | x37 => 55 + | x38 => 56 + | x39 => 57 + | x3a => 58 + | x3b => 59 + | x3c => 60 + | x3d => 61 + | x3e => 62 + | x3f => 63 + | x40 => 64 + | x41 => 65 + | x42 => 66 + | x43 => 67 + | x44 => 68 + | x45 => 69 + | x46 => 70 + | x47 => 71 + | x48 => 72 + | x49 => 73 + | x4a => 74 + | x4b => 75 + | x4c => 76 + | x4d => 77 + | x4e => 78 + | x4f => 79 + | x50 => 80 + | x51 => 81 + | x52 => 82 + | x53 => 83 + | x54 => 84 + | x55 => 85 + | x56 => 86 + | x57 => 87 + | x58 => 88 + | x59 => 89 + | x5a => 90 + | x5b => 91 + | x5c => 92 + | x5d => 93 + | x5e => 94 + | x5f => 95 + | x60 => 96 + | x61 => 97 + | x62 => 98 + | x63 => 99 + | x64 => 100 + | x65 => 101 + | x66 => 102 + | x67 => 103 + | x68 => 104 + | x69 => 105 + | x6a => 106 + | x6b => 107 + | x6c => 108 + | x6d => 109 + | x6e => 110 + | x6f => 111 + | x70 => 112 + | x71 => 113 + | x72 => 114 + | x73 => 115 + | x74 => 116 + | x75 => 117 + | x76 => 118 + | x77 => 119 + | x78 => 120 + | x79 => 121 + | x7a => 122 + | x7b => 123 + | x7c => 124 + | x7d => 125 + | x7e => 126 + | x7f => 127 + | x80 => 128 + | x81 => 129 + | x82 => 130 + | x83 => 131 + | x84 => 132 + | x85 => 133 + | x86 => 134 + | x87 => 135 + | x88 => 136 + | x89 => 137 + | x8a => 138 + | x8b => 139 + | x8c => 140 + | x8d => 141 + | x8e => 142 + | x8f => 143 + | x90 => 144 + | x91 => 145 + | x92 => 146 + | x93 => 147 + | x94 => 148 + | x95 => 149 + | x96 => 150 + | x97 => 151 + | x98 => 152 + | x99 => 153 + | x9a => 154 + | x9b => 155 + | x9c => 156 + | x9d => 157 + | x9e => 158 + | x9f => 159 + | xa0 => 160 + | xa1 => 161 + | xa2 => 162 + | xa3 => 163 + | xa4 => 164 + | xa5 => 165 + | xa6 => 166 + | xa7 => 167 + | xa8 => 168 + | xa9 => 169 + | xaa => 170 + | xab => 171 + | xac => 172 + | xad => 173 + | xae => 174 + | xaf => 175 + | xb0 => 176 + | xb1 => 177 + | xb2 => 178 + | xb3 => 179 + | xb4 => 180 + | xb5 => 181 + | xb6 => 182 + | xb7 => 183 + | xb8 => 184 + | xb9 => 185 + | xba => 186 + | xbb => 187 + | xbc => 188 + | xbd => 189 + | xbe => 190 + | xbf => 191 + | xc0 => 192 + | xc1 => 193 + | xc2 => 194 + | xc3 => 195 + | xc4 => 196 + | xc5 => 197 + | xc6 => 198 + | xc7 => 199 + | xc8 => 200 + | xc9 => 201 + | xca => 202 + | xcb => 203 + | xcc => 204 + | xcd => 205 + | xce => 206 + | xcf => 207 + | xd0 => 208 + | xd1 => 209 + | xd2 => 210 + | xd3 => 211 + | xd4 => 212 + | xd5 => 213 + | xd6 => 214 + | xd7 => 215 + | xd8 => 216 + | xd9 => 217 + | xda => 218 + | xdb => 219 + | xdc => 220 + | xdd => 221 + | xde => 222 + | xdf => 223 + | xe0 => 224 + | xe1 => 225 + | xe2 => 226 + | xe3 => 227 + | xe4 => 228 + | xe5 => 229 + | xe6 => 230 + | xe7 => 231 + | xe8 => 232 + | xe9 => 233 + | xea => 234 + | xeb => 235 + | xec => 236 + | xed => 237 + | xee => 238 + | xef => 239 + | xf0 => 240 + | xf1 => 241 + | xf2 => 242 + | xf3 => 243 + | xf4 => 244 + | xf5 => 245 + | xf6 => 246 + | xf7 => 247 + | xf8 => 248 + | xf9 => 249 + | xfa => 250 + | xfb => 251 + | xfc => 252 + | xfd => 253 + | xfe => 254 + | xff => 255 + end. + + Definition of_N (x : N) : option byte + := match x with + | 0 => Some x00 + | 1 => Some x01 + | 2 => Some x02 + | 3 => Some x03 + | 4 => Some x04 + | 5 => Some x05 + | 6 => Some x06 + | 7 => Some x07 + | 8 => Some x08 + | 9 => Some x09 + | 10 => Some x0a + | 11 => Some x0b + | 12 => Some x0c + | 13 => Some x0d + | 14 => Some x0e + | 15 => Some x0f + | 16 => Some x10 + | 17 => Some x11 + | 18 => Some x12 + | 19 => Some x13 + | 20 => Some x14 + | 21 => Some x15 + | 22 => Some x16 + | 23 => Some x17 + | 24 => Some x18 + | 25 => Some x19 + | 26 => Some x1a + | 27 => Some x1b + | 28 => Some x1c + | 29 => Some x1d + | 30 => Some x1e + | 31 => Some x1f + | 32 => Some x20 + | 33 => Some x21 + | 34 => Some x22 + | 35 => Some x23 + | 36 => Some x24 + | 37 => Some x25 + | 38 => Some x26 + | 39 => Some x27 + | 40 => Some x28 + | 41 => Some x29 + | 42 => Some x2a + | 43 => Some x2b + | 44 => Some x2c + | 45 => Some x2d + | 46 => Some x2e + | 47 => Some x2f + | 48 => Some x30 + | 49 => Some x31 + | 50 => Some x32 + | 51 => Some x33 + | 52 => Some x34 + | 53 => Some x35 + | 54 => Some x36 + | 55 => Some x37 + | 56 => Some x38 + | 57 => Some x39 + | 58 => Some x3a + | 59 => Some x3b + | 60 => Some x3c + | 61 => Some x3d + | 62 => Some x3e + | 63 => Some x3f + | 64 => Some x40 + | 65 => Some x41 + | 66 => Some x42 + | 67 => Some x43 + | 68 => Some x44 + | 69 => Some x45 + | 70 => Some x46 + | 71 => Some x47 + | 72 => Some x48 + | 73 => Some x49 + | 74 => Some x4a + | 75 => Some x4b + | 76 => Some x4c + | 77 => Some x4d + | 78 => Some x4e + | 79 => Some x4f + | 80 => Some x50 + | 81 => Some x51 + | 82 => Some x52 + | 83 => Some x53 + | 84 => Some x54 + | 85 => Some x55 + | 86 => Some x56 + | 87 => Some x57 + | 88 => Some x58 + | 89 => Some x59 + | 90 => Some x5a + | 91 => Some x5b + | 92 => Some x5c + | 93 => Some x5d + | 94 => Some x5e + | 95 => Some x5f + | 96 => Some x60 + | 97 => Some x61 + | 98 => Some x62 + | 99 => Some x63 + | 100 => Some x64 + | 101 => Some x65 + | 102 => Some x66 + | 103 => Some x67 + | 104 => Some x68 + | 105 => Some x69 + | 106 => Some x6a + | 107 => Some x6b + | 108 => Some x6c + | 109 => Some x6d + | 110 => Some x6e + | 111 => Some x6f + | 112 => Some x70 + | 113 => Some x71 + | 114 => Some x72 + | 115 => Some x73 + | 116 => Some x74 + | 117 => Some x75 + | 118 => Some x76 + | 119 => Some x77 + | 120 => Some x78 + | 121 => Some x79 + | 122 => Some x7a + | 123 => Some x7b + | 124 => Some x7c + | 125 => Some x7d + | 126 => Some x7e + | 127 => Some x7f + | 128 => Some x80 + | 129 => Some x81 + | 130 => Some x82 + | 131 => Some x83 + | 132 => Some x84 + | 133 => Some x85 + | 134 => Some x86 + | 135 => Some x87 + | 136 => Some x88 + | 137 => Some x89 + | 138 => Some x8a + | 139 => Some x8b + | 140 => Some x8c + | 141 => Some x8d + | 142 => Some x8e + | 143 => Some x8f + | 144 => Some x90 + | 145 => Some x91 + | 146 => Some x92 + | 147 => Some x93 + | 148 => Some x94 + | 149 => Some x95 + | 150 => Some x96 + | 151 => Some x97 + | 152 => Some x98 + | 153 => Some x99 + | 154 => Some x9a + | 155 => Some x9b + | 156 => Some x9c + | 157 => Some x9d + | 158 => Some x9e + | 159 => Some x9f + | 160 => Some xa0 + | 161 => Some xa1 + | 162 => Some xa2 + | 163 => Some xa3 + | 164 => Some xa4 + | 165 => Some xa5 + | 166 => Some xa6 + | 167 => Some xa7 + | 168 => Some xa8 + | 169 => Some xa9 + | 170 => Some xaa + | 171 => Some xab + | 172 => Some xac + | 173 => Some xad + | 174 => Some xae + | 175 => Some xaf + | 176 => Some xb0 + | 177 => Some xb1 + | 178 => Some xb2 + | 179 => Some xb3 + | 180 => Some xb4 + | 181 => Some xb5 + | 182 => Some xb6 + | 183 => Some xb7 + | 184 => Some xb8 + | 185 => Some xb9 + | 186 => Some xba + | 187 => Some xbb + | 188 => Some xbc + | 189 => Some xbd + | 190 => Some xbe + | 191 => Some xbf + | 192 => Some xc0 + | 193 => Some xc1 + | 194 => Some xc2 + | 195 => Some xc3 + | 196 => Some xc4 + | 197 => Some xc5 + | 198 => Some xc6 + | 199 => Some xc7 + | 200 => Some xc8 + | 201 => Some xc9 + | 202 => Some xca + | 203 => Some xcb + | 204 => Some xcc + | 205 => Some xcd + | 206 => Some xce + | 207 => Some xcf + | 208 => Some xd0 + | 209 => Some xd1 + | 210 => Some xd2 + | 211 => Some xd3 + | 212 => Some xd4 + | 213 => Some xd5 + | 214 => Some xd6 + | 215 => Some xd7 + | 216 => Some xd8 + | 217 => Some xd9 + | 218 => Some xda + | 219 => Some xdb + | 220 => Some xdc + | 221 => Some xdd + | 222 => Some xde + | 223 => Some xdf + | 224 => Some xe0 + | 225 => Some xe1 + | 226 => Some xe2 + | 227 => Some xe3 + | 228 => Some xe4 + | 229 => Some xe5 + | 230 => Some xe6 + | 231 => Some xe7 + | 232 => Some xe8 + | 233 => Some xe9 + | 234 => Some xea + | 235 => Some xeb + | 236 => Some xec + | 237 => Some xed + | 238 => Some xee + | 239 => Some xef + | 240 => Some xf0 + | 241 => Some xf1 + | 242 => Some xf2 + | 243 => Some xf3 + | 244 => Some xf4 + | 245 => Some xf5 + | 246 => Some xf6 + | 247 => Some xf7 + | 248 => Some xf8 + | 249 => Some xf9 + | 250 => Some xfa + | 251 => Some xfb + | 252 => Some xfc + | 253 => Some xfd + | 254 => Some xfe + | 255 => Some xff + | _ => None + end. + + Lemma of_to_N x : of_N (to_N x) = Some x. + Proof. destruct x; reflexivity. Qed. + + Lemma to_of_N x y : of_N x = Some y -> to_N y = x. + Proof. + cbv [of_N]; + repeat match goal with + | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x + | _ => intro + | _ => reflexivity + | _ => progress subst + | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + end. + Qed. + + Lemma to_of_N_iff x y : of_N x = Some y <-> to_N y = x. + Proof. split; intro; subst; (apply of_to_N || apply to_of_N); assumption. Qed. + + Lemma to_of_N_option_map x : option_map to_N (of_N x) = if N.leb x 255 then Some x else None. + Proof. + cbv [of_N]; + repeat match goal with + | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x + end; + reflexivity. + Qed. + + Lemma to_N_bounded x : to_N x <= 255. + Proof. + generalize (to_of_N_option_map (to_N x)). + rewrite of_to_N; cbn [option_map]. + destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ]. + rewrite (N.leb_le (to_N x) 255) in H. + intro; assumption. + Qed. + + Lemma of_N_None_iff x : of_N x = None <-> 255 < x. + Proof. + generalize (to_of_N_option_map x). + destruct (of_N x), (N.leb x 255) eqn:H; cbn [option_map]; try congruence. + { rewrite N.leb_le in H; split; [ congruence | ]. + rewrite N.lt_nge; intro H'; exfalso; apply H'; assumption. } + { rewrite N.leb_nle in H; split; [ | reflexivity ]. + rewrite N.lt_nge; intro; assumption. } + Qed. +End N. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a09d518892..08ccfac877 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,6 +15,7 @@ Require Import Arith. Require Import Ascii. Require Import Bool. +Require Import Coq.Strings.Byte. (** *** Definition of strings *) @@ -25,7 +26,6 @@ Inductive string : Set := | String : ascii -> string -> string. Declare Scope string_scope. -Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax. Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. @@ -114,12 +114,12 @@ Theorem get_correct : Proof. intros s1; elim s1; simpl. intros s2; case s2; simpl; split; auto. -intros H; generalize (H 0); intros H1; inversion H1. +intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. intros a s1' Rec s2; case s2; simpl; split; auto. -intros H; generalize (H 0); intros H1; inversion H1. +intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. -intros H; generalize (H 0); simpl; intros H1; inversion H1. +intros H; generalize (H O); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). @@ -150,7 +150,7 @@ Proof. intros s1; elim s1; simpl; auto. intros s2 n; rewrite plus_comm; simpl; auto. intros a s1' Rec s2 n; case n; simpl; auto. -generalize (Rec s2 0); simpl; auto. intros. +generalize (Rec s2 O); simpl; auto. intros. rewrite <- Plus.plus_Snm_nSm; auto. Qed. @@ -162,9 +162,9 @@ Qed. Fixpoint substring (n m : nat) (s : string) : string := match n, m, s with - | 0, 0, _ => EmptyString - | 0, S m', EmptyString => s - | 0, S m', String c s' => String c (substring 0 m' s') + | O, O, _ => EmptyString + | O, S m', EmptyString => s + | O, S m', String c s' => String c (substring 0 m' s') | S n', _, EmptyString => s | S n', _, String c s' => substring n' m s' end. @@ -257,16 +257,16 @@ Qed. Fixpoint index (n : nat) (s1 s2 : string) : option nat := match s2, n with - | EmptyString, 0 => + | EmptyString, O => match s1 with - | EmptyString => Some 0 + | EmptyString => Some O | String a s1' => None end | EmptyString, S n' => None - | String b s2', 0 => - if prefix s1 s2 then Some 0 + | String b s2', O => + if prefix s1 s2 then Some O else - match index 0 s1 s2' with + match index O s1 s2' with | Some n => Some (S n) | None => None end @@ -300,8 +300,8 @@ generalize (prefix_correct s1 (String b s2')); intros H0 H; injection H as <-; auto. case H0; simpl; auto. case m; simpl; auto. -case (index 0 s1 s2'); intros; discriminate. -intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto. +case (index O s1 s2'); intros; discriminate. +intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto. intros x H H0 H1; apply H; injection H1; auto. intros; discriminate. intros n'; case m; simpl; auto. @@ -335,7 +335,7 @@ intros H0 H; injection H as <-; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. -intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto. +intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto. intros x H H0 H1 p; try case p; simpl; auto. intros H2 H3; red; intros H4; case H0. intros H5 H6; absurd (false = true); auto with bool. @@ -383,7 +383,7 @@ intros H4 H5; absurd (false = true); auto with bool. case s1; simpl; auto. intros a s n0 H H0 H1 H2; change (substring n0 (length (String a s)) s2' <> String a s); - apply (Rec 0); auto. + apply (Rec O); auto. generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros; discriminate. apply Le.le_O_n. @@ -423,9 +423,53 @@ Qed. Definition findex n s1 s2 := match index n s1 s2 with | Some n => n - | None => 0 + | None => O end. +(** *** Conversion to/from [list ascii] and [list byte] *) + +Fixpoint string_of_list_ascii (s : list ascii) : string + := match s with + | nil => EmptyString + | cons ch s => String ch (string_of_list_ascii s) + end. + +Fixpoint list_ascii_of_string (s : string) : list ascii + := match s with + | EmptyString => nil + | String ch s => cons ch (list_ascii_of_string s) + end. + +Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s. +Proof. + induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ]. +Defined. + +Lemma list_ascii_of_string_of_list_ascii s : list_ascii_of_string (string_of_list_ascii s) = s. +Proof. + induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ]. +Defined. + +Definition string_of_list_byte (s : list byte) : string + := string_of_list_ascii (List.map ascii_of_byte s). + +Definition list_byte_of_string (s : string) : list byte + := List.map byte_of_ascii (list_ascii_of_string s). + +Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s. +Proof. + cbv [string_of_list_byte list_byte_of_string]. + erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ]. + apply ascii_of_byte_of_ascii. +Qed. + +Lemma list_byte_of_string_of_list_byte s : list_byte_of_string (string_of_list_byte s) = s. +Proof. + cbv [string_of_list_byte list_byte_of_string]. + erewrite list_ascii_of_string_of_list_ascii, List.map_map, List.map_ext, List.map_id; [ reflexivity | intro ]. + apply byte_of_ascii_of_byte. +Qed. + (** *** Concrete syntax *) (** @@ -438,7 +482,11 @@ Definition findex n s1 s2 := part of a valid utf8 sequence of characters are not representable using the Coq string notation (use explicitly the String constructor with the ascii codes of the characters). -*) + *) + +Module Export StringSyntax. + String Notation string string_of_list_byte list_byte_of_string : string_scope. +End StringSyntax. Example HelloWorld := " ""Hello world!"" ". -- cgit v1.2.3 From 732b3550ada0598f56aeed09527d446a1013e353 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 19 Nov 2018 16:58:43 -0500 Subject: Speed up Byte We could move another ~ 1s from Init.Byte to Strings.Byte by moving `of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not worth it. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------- 1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77% ---------------------------------------------------------------------------------- 0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88% 0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35% 0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08% 0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87% 0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00% 0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81% 0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07% 0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64% 0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00% 0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74% 0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49% 0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73% 0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45% 0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08% 0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31% 0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90% 0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92% 0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28% 0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06% 0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16% 0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52% 0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19% 0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00% 0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22% 0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61% 0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00% 0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33% 0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27% 0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92% 0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44% 0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84% 0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00% 0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16% 0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00% 0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16% 0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27% 0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24% 0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99% 0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50% 0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89% 0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76% 0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00% 0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85% 0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26% 0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03% 0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67% 0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00% 0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22% 0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28% 0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44% 0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00% 0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53% 0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00% 0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66% 0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39% 0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84% 0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00% 0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14% 0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33% 0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12% 0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18% 0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33% 0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84% 0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00% 0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11% 0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99% 0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30% 0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29% 0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00% 0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78% 0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34% 0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52% 0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52% 0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04% 0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64% 0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63% 0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00% 0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25% 0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55% 0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72% 0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50% 0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00% 0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78% 0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66% 0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66% 0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66% 0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49% 0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49% 0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77% 0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52% 0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69% 0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00% 0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33% 0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00% 0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00% 0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00% 0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38% 0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33% 0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14% 0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07% 0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00% 0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66% 0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09% 0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00% 0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49% 0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27% 0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33% 0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11% 0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00% 0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00% 0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00% 0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00% 0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44% 0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50% 0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55% 0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00% --- theories/Init/Byte.v | 542 ++++++++++++++++++++++++++++++++++++++++++++++- theories/Strings/Ascii.v | 31 ++- theories/Strings/Byte.v | 294 +++---------------------- 3 files changed, 575 insertions(+), 292 deletions(-) (limited to 'theories') diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 2d8ee30a43..59b5f5ebe3 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -21,7 +21,6 @@ Declare ML Module "string_notation_plugin". which contains all ascii characters. We use 256 constructors for efficiency and ease of conversion. *) -Local Set Boolean Equality Schemes. Declare Scope byte_scope. Delimit Scope byte_scope with byte. @@ -288,15 +287,544 @@ Bind Scope byte_scope with byte. Register byte as core.byte.type. -Notation eqb := byte_beq. +Local Notation "0" := false. +Local Notation "1" := true. + +(** We pick a definition that matches with [Ascii.ascii] *) +Definition of_bits (b : bool * bool * bool * bool * bool * bool * bool * bool) : byte + := match b with + | (0,0,0,0,0,0,0,0) => x00 + | (1,0,0,0,0,0,0,0) => x01 + | (0,1,0,0,0,0,0,0) => x02 + | (1,1,0,0,0,0,0,0) => x03 + | (0,0,1,0,0,0,0,0) => x04 + | (1,0,1,0,0,0,0,0) => x05 + | (0,1,1,0,0,0,0,0) => x06 + | (1,1,1,0,0,0,0,0) => x07 + | (0,0,0,1,0,0,0,0) => x08 + | (1,0,0,1,0,0,0,0) => x09 + | (0,1,0,1,0,0,0,0) => x0a + | (1,1,0,1,0,0,0,0) => x0b + | (0,0,1,1,0,0,0,0) => x0c + | (1,0,1,1,0,0,0,0) => x0d + | (0,1,1,1,0,0,0,0) => x0e + | (1,1,1,1,0,0,0,0) => x0f + | (0,0,0,0,1,0,0,0) => x10 + | (1,0,0,0,1,0,0,0) => x11 + | (0,1,0,0,1,0,0,0) => x12 + | (1,1,0,0,1,0,0,0) => x13 + | (0,0,1,0,1,0,0,0) => x14 + | (1,0,1,0,1,0,0,0) => x15 + | (0,1,1,0,1,0,0,0) => x16 + | (1,1,1,0,1,0,0,0) => x17 + | (0,0,0,1,1,0,0,0) => x18 + | (1,0,0,1,1,0,0,0) => x19 + | (0,1,0,1,1,0,0,0) => x1a + | (1,1,0,1,1,0,0,0) => x1b + | (0,0,1,1,1,0,0,0) => x1c + | (1,0,1,1,1,0,0,0) => x1d + | (0,1,1,1,1,0,0,0) => x1e + | (1,1,1,1,1,0,0,0) => x1f + | (0,0,0,0,0,1,0,0) => x20 + | (1,0,0,0,0,1,0,0) => x21 + | (0,1,0,0,0,1,0,0) => x22 + | (1,1,0,0,0,1,0,0) => x23 + | (0,0,1,0,0,1,0,0) => x24 + | (1,0,1,0,0,1,0,0) => x25 + | (0,1,1,0,0,1,0,0) => x26 + | (1,1,1,0,0,1,0,0) => x27 + | (0,0,0,1,0,1,0,0) => x28 + | (1,0,0,1,0,1,0,0) => x29 + | (0,1,0,1,0,1,0,0) => x2a + | (1,1,0,1,0,1,0,0) => x2b + | (0,0,1,1,0,1,0,0) => x2c + | (1,0,1,1,0,1,0,0) => x2d + | (0,1,1,1,0,1,0,0) => x2e + | (1,1,1,1,0,1,0,0) => x2f + | (0,0,0,0,1,1,0,0) => x30 + | (1,0,0,0,1,1,0,0) => x31 + | (0,1,0,0,1,1,0,0) => x32 + | (1,1,0,0,1,1,0,0) => x33 + | (0,0,1,0,1,1,0,0) => x34 + | (1,0,1,0,1,1,0,0) => x35 + | (0,1,1,0,1,1,0,0) => x36 + | (1,1,1,0,1,1,0,0) => x37 + | (0,0,0,1,1,1,0,0) => x38 + | (1,0,0,1,1,1,0,0) => x39 + | (0,1,0,1,1,1,0,0) => x3a + | (1,1,0,1,1,1,0,0) => x3b + | (0,0,1,1,1,1,0,0) => x3c + | (1,0,1,1,1,1,0,0) => x3d + | (0,1,1,1,1,1,0,0) => x3e + | (1,1,1,1,1,1,0,0) => x3f + | (0,0,0,0,0,0,1,0) => x40 + | (1,0,0,0,0,0,1,0) => x41 + | (0,1,0,0,0,0,1,0) => x42 + | (1,1,0,0,0,0,1,0) => x43 + | (0,0,1,0,0,0,1,0) => x44 + | (1,0,1,0,0,0,1,0) => x45 + | (0,1,1,0,0,0,1,0) => x46 + | (1,1,1,0,0,0,1,0) => x47 + | (0,0,0,1,0,0,1,0) => x48 + | (1,0,0,1,0,0,1,0) => x49 + | (0,1,0,1,0,0,1,0) => x4a + | (1,1,0,1,0,0,1,0) => x4b + | (0,0,1,1,0,0,1,0) => x4c + | (1,0,1,1,0,0,1,0) => x4d + | (0,1,1,1,0,0,1,0) => x4e + | (1,1,1,1,0,0,1,0) => x4f + | (0,0,0,0,1,0,1,0) => x50 + | (1,0,0,0,1,0,1,0) => x51 + | (0,1,0,0,1,0,1,0) => x52 + | (1,1,0,0,1,0,1,0) => x53 + | (0,0,1,0,1,0,1,0) => x54 + | (1,0,1,0,1,0,1,0) => x55 + | (0,1,1,0,1,0,1,0) => x56 + | (1,1,1,0,1,0,1,0) => x57 + | (0,0,0,1,1,0,1,0) => x58 + | (1,0,0,1,1,0,1,0) => x59 + | (0,1,0,1,1,0,1,0) => x5a + | (1,1,0,1,1,0,1,0) => x5b + | (0,0,1,1,1,0,1,0) => x5c + | (1,0,1,1,1,0,1,0) => x5d + | (0,1,1,1,1,0,1,0) => x5e + | (1,1,1,1,1,0,1,0) => x5f + | (0,0,0,0,0,1,1,0) => x60 + | (1,0,0,0,0,1,1,0) => x61 + | (0,1,0,0,0,1,1,0) => x62 + | (1,1,0,0,0,1,1,0) => x63 + | (0,0,1,0,0,1,1,0) => x64 + | (1,0,1,0,0,1,1,0) => x65 + | (0,1,1,0,0,1,1,0) => x66 + | (1,1,1,0,0,1,1,0) => x67 + | (0,0,0,1,0,1,1,0) => x68 + | (1,0,0,1,0,1,1,0) => x69 + | (0,1,0,1,0,1,1,0) => x6a + | (1,1,0,1,0,1,1,0) => x6b + | (0,0,1,1,0,1,1,0) => x6c + | (1,0,1,1,0,1,1,0) => x6d + | (0,1,1,1,0,1,1,0) => x6e + | (1,1,1,1,0,1,1,0) => x6f + | (0,0,0,0,1,1,1,0) => x70 + | (1,0,0,0,1,1,1,0) => x71 + | (0,1,0,0,1,1,1,0) => x72 + | (1,1,0,0,1,1,1,0) => x73 + | (0,0,1,0,1,1,1,0) => x74 + | (1,0,1,0,1,1,1,0) => x75 + | (0,1,1,0,1,1,1,0) => x76 + | (1,1,1,0,1,1,1,0) => x77 + | (0,0,0,1,1,1,1,0) => x78 + | (1,0,0,1,1,1,1,0) => x79 + | (0,1,0,1,1,1,1,0) => x7a + | (1,1,0,1,1,1,1,0) => x7b + | (0,0,1,1,1,1,1,0) => x7c + | (1,0,1,1,1,1,1,0) => x7d + | (0,1,1,1,1,1,1,0) => x7e + | (1,1,1,1,1,1,1,0) => x7f + | (0,0,0,0,0,0,0,1) => x80 + | (1,0,0,0,0,0,0,1) => x81 + | (0,1,0,0,0,0,0,1) => x82 + | (1,1,0,0,0,0,0,1) => x83 + | (0,0,1,0,0,0,0,1) => x84 + | (1,0,1,0,0,0,0,1) => x85 + | (0,1,1,0,0,0,0,1) => x86 + | (1,1,1,0,0,0,0,1) => x87 + | (0,0,0,1,0,0,0,1) => x88 + | (1,0,0,1,0,0,0,1) => x89 + | (0,1,0,1,0,0,0,1) => x8a + | (1,1,0,1,0,0,0,1) => x8b + | (0,0,1,1,0,0,0,1) => x8c + | (1,0,1,1,0,0,0,1) => x8d + | (0,1,1,1,0,0,0,1) => x8e + | (1,1,1,1,0,0,0,1) => x8f + | (0,0,0,0,1,0,0,1) => x90 + | (1,0,0,0,1,0,0,1) => x91 + | (0,1,0,0,1,0,0,1) => x92 + | (1,1,0,0,1,0,0,1) => x93 + | (0,0,1,0,1,0,0,1) => x94 + | (1,0,1,0,1,0,0,1) => x95 + | (0,1,1,0,1,0,0,1) => x96 + | (1,1,1,0,1,0,0,1) => x97 + | (0,0,0,1,1,0,0,1) => x98 + | (1,0,0,1,1,0,0,1) => x99 + | (0,1,0,1,1,0,0,1) => x9a + | (1,1,0,1,1,0,0,1) => x9b + | (0,0,1,1,1,0,0,1) => x9c + | (1,0,1,1,1,0,0,1) => x9d + | (0,1,1,1,1,0,0,1) => x9e + | (1,1,1,1,1,0,0,1) => x9f + | (0,0,0,0,0,1,0,1) => xa0 + | (1,0,0,0,0,1,0,1) => xa1 + | (0,1,0,0,0,1,0,1) => xa2 + | (1,1,0,0,0,1,0,1) => xa3 + | (0,0,1,0,0,1,0,1) => xa4 + | (1,0,1,0,0,1,0,1) => xa5 + | (0,1,1,0,0,1,0,1) => xa6 + | (1,1,1,0,0,1,0,1) => xa7 + | (0,0,0,1,0,1,0,1) => xa8 + | (1,0,0,1,0,1,0,1) => xa9 + | (0,1,0,1,0,1,0,1) => xaa + | (1,1,0,1,0,1,0,1) => xab + | (0,0,1,1,0,1,0,1) => xac + | (1,0,1,1,0,1,0,1) => xad + | (0,1,1,1,0,1,0,1) => xae + | (1,1,1,1,0,1,0,1) => xaf + | (0,0,0,0,1,1,0,1) => xb0 + | (1,0,0,0,1,1,0,1) => xb1 + | (0,1,0,0,1,1,0,1) => xb2 + | (1,1,0,0,1,1,0,1) => xb3 + | (0,0,1,0,1,1,0,1) => xb4 + | (1,0,1,0,1,1,0,1) => xb5 + | (0,1,1,0,1,1,0,1) => xb6 + | (1,1,1,0,1,1,0,1) => xb7 + | (0,0,0,1,1,1,0,1) => xb8 + | (1,0,0,1,1,1,0,1) => xb9 + | (0,1,0,1,1,1,0,1) => xba + | (1,1,0,1,1,1,0,1) => xbb + | (0,0,1,1,1,1,0,1) => xbc + | (1,0,1,1,1,1,0,1) => xbd + | (0,1,1,1,1,1,0,1) => xbe + | (1,1,1,1,1,1,0,1) => xbf + | (0,0,0,0,0,0,1,1) => xc0 + | (1,0,0,0,0,0,1,1) => xc1 + | (0,1,0,0,0,0,1,1) => xc2 + | (1,1,0,0,0,0,1,1) => xc3 + | (0,0,1,0,0,0,1,1) => xc4 + | (1,0,1,0,0,0,1,1) => xc5 + | (0,1,1,0,0,0,1,1) => xc6 + | (1,1,1,0,0,0,1,1) => xc7 + | (0,0,0,1,0,0,1,1) => xc8 + | (1,0,0,1,0,0,1,1) => xc9 + | (0,1,0,1,0,0,1,1) => xca + | (1,1,0,1,0,0,1,1) => xcb + | (0,0,1,1,0,0,1,1) => xcc + | (1,0,1,1,0,0,1,1) => xcd + | (0,1,1,1,0,0,1,1) => xce + | (1,1,1,1,0,0,1,1) => xcf + | (0,0,0,0,1,0,1,1) => xd0 + | (1,0,0,0,1,0,1,1) => xd1 + | (0,1,0,0,1,0,1,1) => xd2 + | (1,1,0,0,1,0,1,1) => xd3 + | (0,0,1,0,1,0,1,1) => xd4 + | (1,0,1,0,1,0,1,1) => xd5 + | (0,1,1,0,1,0,1,1) => xd6 + | (1,1,1,0,1,0,1,1) => xd7 + | (0,0,0,1,1,0,1,1) => xd8 + | (1,0,0,1,1,0,1,1) => xd9 + | (0,1,0,1,1,0,1,1) => xda + | (1,1,0,1,1,0,1,1) => xdb + | (0,0,1,1,1,0,1,1) => xdc + | (1,0,1,1,1,0,1,1) => xdd + | (0,1,1,1,1,0,1,1) => xde + | (1,1,1,1,1,0,1,1) => xdf + | (0,0,0,0,0,1,1,1) => xe0 + | (1,0,0,0,0,1,1,1) => xe1 + | (0,1,0,0,0,1,1,1) => xe2 + | (1,1,0,0,0,1,1,1) => xe3 + | (0,0,1,0,0,1,1,1) => xe4 + | (1,0,1,0,0,1,1,1) => xe5 + | (0,1,1,0,0,1,1,1) => xe6 + | (1,1,1,0,0,1,1,1) => xe7 + | (0,0,0,1,0,1,1,1) => xe8 + | (1,0,0,1,0,1,1,1) => xe9 + | (0,1,0,1,0,1,1,1) => xea + | (1,1,0,1,0,1,1,1) => xeb + | (0,0,1,1,0,1,1,1) => xec + | (1,0,1,1,0,1,1,1) => xed + | (0,1,1,1,0,1,1,1) => xee + | (1,1,1,1,0,1,1,1) => xef + | (0,0,0,0,1,1,1,1) => xf0 + | (1,0,0,0,1,1,1,1) => xf1 + | (0,1,0,0,1,1,1,1) => xf2 + | (1,1,0,0,1,1,1,1) => xf3 + | (0,0,1,0,1,1,1,1) => xf4 + | (1,0,1,0,1,1,1,1) => xf5 + | (0,1,1,0,1,1,1,1) => xf6 + | (1,1,1,0,1,1,1,1) => xf7 + | (0,0,0,1,1,1,1,1) => xf8 + | (1,0,0,1,1,1,1,1) => xf9 + | (0,1,0,1,1,1,1,1) => xfa + | (1,1,0,1,1,1,1,1) => xfb + | (0,0,1,1,1,1,1,1) => xfc + | (1,0,1,1,1,1,1,1) => xfd + | (0,1,1,1,1,1,1,1) => xfe + | (1,1,1,1,1,1,1,1) => xff + end. + +Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool + := match b with + | x00 => (0,0,0,0,0,0,0,0) + | x01 => (1,0,0,0,0,0,0,0) + | x02 => (0,1,0,0,0,0,0,0) + | x03 => (1,1,0,0,0,0,0,0) + | x04 => (0,0,1,0,0,0,0,0) + | x05 => (1,0,1,0,0,0,0,0) + | x06 => (0,1,1,0,0,0,0,0) + | x07 => (1,1,1,0,0,0,0,0) + | x08 => (0,0,0,1,0,0,0,0) + | x09 => (1,0,0,1,0,0,0,0) + | x0a => (0,1,0,1,0,0,0,0) + | x0b => (1,1,0,1,0,0,0,0) + | x0c => (0,0,1,1,0,0,0,0) + | x0d => (1,0,1,1,0,0,0,0) + | x0e => (0,1,1,1,0,0,0,0) + | x0f => (1,1,1,1,0,0,0,0) + | x10 => (0,0,0,0,1,0,0,0) + | x11 => (1,0,0,0,1,0,0,0) + | x12 => (0,1,0,0,1,0,0,0) + | x13 => (1,1,0,0,1,0,0,0) + | x14 => (0,0,1,0,1,0,0,0) + | x15 => (1,0,1,0,1,0,0,0) + | x16 => (0,1,1,0,1,0,0,0) + | x17 => (1,1,1,0,1,0,0,0) + | x18 => (0,0,0,1,1,0,0,0) + | x19 => (1,0,0,1,1,0,0,0) + | x1a => (0,1,0,1,1,0,0,0) + | x1b => (1,1,0,1,1,0,0,0) + | x1c => (0,0,1,1,1,0,0,0) + | x1d => (1,0,1,1,1,0,0,0) + | x1e => (0,1,1,1,1,0,0,0) + | x1f => (1,1,1,1,1,0,0,0) + | x20 => (0,0,0,0,0,1,0,0) + | x21 => (1,0,0,0,0,1,0,0) + | x22 => (0,1,0,0,0,1,0,0) + | x23 => (1,1,0,0,0,1,0,0) + | x24 => (0,0,1,0,0,1,0,0) + | x25 => (1,0,1,0,0,1,0,0) + | x26 => (0,1,1,0,0,1,0,0) + | x27 => (1,1,1,0,0,1,0,0) + | x28 => (0,0,0,1,0,1,0,0) + | x29 => (1,0,0,1,0,1,0,0) + | x2a => (0,1,0,1,0,1,0,0) + | x2b => (1,1,0,1,0,1,0,0) + | x2c => (0,0,1,1,0,1,0,0) + | x2d => (1,0,1,1,0,1,0,0) + | x2e => (0,1,1,1,0,1,0,0) + | x2f => (1,1,1,1,0,1,0,0) + | x30 => (0,0,0,0,1,1,0,0) + | x31 => (1,0,0,0,1,1,0,0) + | x32 => (0,1,0,0,1,1,0,0) + | x33 => (1,1,0,0,1,1,0,0) + | x34 => (0,0,1,0,1,1,0,0) + | x35 => (1,0,1,0,1,1,0,0) + | x36 => (0,1,1,0,1,1,0,0) + | x37 => (1,1,1,0,1,1,0,0) + | x38 => (0,0,0,1,1,1,0,0) + | x39 => (1,0,0,1,1,1,0,0) + | x3a => (0,1,0,1,1,1,0,0) + | x3b => (1,1,0,1,1,1,0,0) + | x3c => (0,0,1,1,1,1,0,0) + | x3d => (1,0,1,1,1,1,0,0) + | x3e => (0,1,1,1,1,1,0,0) + | x3f => (1,1,1,1,1,1,0,0) + | x40 => (0,0,0,0,0,0,1,0) + | x41 => (1,0,0,0,0,0,1,0) + | x42 => (0,1,0,0,0,0,1,0) + | x43 => (1,1,0,0,0,0,1,0) + | x44 => (0,0,1,0,0,0,1,0) + | x45 => (1,0,1,0,0,0,1,0) + | x46 => (0,1,1,0,0,0,1,0) + | x47 => (1,1,1,0,0,0,1,0) + | x48 => (0,0,0,1,0,0,1,0) + | x49 => (1,0,0,1,0,0,1,0) + | x4a => (0,1,0,1,0,0,1,0) + | x4b => (1,1,0,1,0,0,1,0) + | x4c => (0,0,1,1,0,0,1,0) + | x4d => (1,0,1,1,0,0,1,0) + | x4e => (0,1,1,1,0,0,1,0) + | x4f => (1,1,1,1,0,0,1,0) + | x50 => (0,0,0,0,1,0,1,0) + | x51 => (1,0,0,0,1,0,1,0) + | x52 => (0,1,0,0,1,0,1,0) + | x53 => (1,1,0,0,1,0,1,0) + | x54 => (0,0,1,0,1,0,1,0) + | x55 => (1,0,1,0,1,0,1,0) + | x56 => (0,1,1,0,1,0,1,0) + | x57 => (1,1,1,0,1,0,1,0) + | x58 => (0,0,0,1,1,0,1,0) + | x59 => (1,0,0,1,1,0,1,0) + | x5a => (0,1,0,1,1,0,1,0) + | x5b => (1,1,0,1,1,0,1,0) + | x5c => (0,0,1,1,1,0,1,0) + | x5d => (1,0,1,1,1,0,1,0) + | x5e => (0,1,1,1,1,0,1,0) + | x5f => (1,1,1,1,1,0,1,0) + | x60 => (0,0,0,0,0,1,1,0) + | x61 => (1,0,0,0,0,1,1,0) + | x62 => (0,1,0,0,0,1,1,0) + | x63 => (1,1,0,0,0,1,1,0) + | x64 => (0,0,1,0,0,1,1,0) + | x65 => (1,0,1,0,0,1,1,0) + | x66 => (0,1,1,0,0,1,1,0) + | x67 => (1,1,1,0,0,1,1,0) + | x68 => (0,0,0,1,0,1,1,0) + | x69 => (1,0,0,1,0,1,1,0) + | x6a => (0,1,0,1,0,1,1,0) + | x6b => (1,1,0,1,0,1,1,0) + | x6c => (0,0,1,1,0,1,1,0) + | x6d => (1,0,1,1,0,1,1,0) + | x6e => (0,1,1,1,0,1,1,0) + | x6f => (1,1,1,1,0,1,1,0) + | x70 => (0,0,0,0,1,1,1,0) + | x71 => (1,0,0,0,1,1,1,0) + | x72 => (0,1,0,0,1,1,1,0) + | x73 => (1,1,0,0,1,1,1,0) + | x74 => (0,0,1,0,1,1,1,0) + | x75 => (1,0,1,0,1,1,1,0) + | x76 => (0,1,1,0,1,1,1,0) + | x77 => (1,1,1,0,1,1,1,0) + | x78 => (0,0,0,1,1,1,1,0) + | x79 => (1,0,0,1,1,1,1,0) + | x7a => (0,1,0,1,1,1,1,0) + | x7b => (1,1,0,1,1,1,1,0) + | x7c => (0,0,1,1,1,1,1,0) + | x7d => (1,0,1,1,1,1,1,0) + | x7e => (0,1,1,1,1,1,1,0) + | x7f => (1,1,1,1,1,1,1,0) + | x80 => (0,0,0,0,0,0,0,1) + | x81 => (1,0,0,0,0,0,0,1) + | x82 => (0,1,0,0,0,0,0,1) + | x83 => (1,1,0,0,0,0,0,1) + | x84 => (0,0,1,0,0,0,0,1) + | x85 => (1,0,1,0,0,0,0,1) + | x86 => (0,1,1,0,0,0,0,1) + | x87 => (1,1,1,0,0,0,0,1) + | x88 => (0,0,0,1,0,0,0,1) + | x89 => (1,0,0,1,0,0,0,1) + | x8a => (0,1,0,1,0,0,0,1) + | x8b => (1,1,0,1,0,0,0,1) + | x8c => (0,0,1,1,0,0,0,1) + | x8d => (1,0,1,1,0,0,0,1) + | x8e => (0,1,1,1,0,0,0,1) + | x8f => (1,1,1,1,0,0,0,1) + | x90 => (0,0,0,0,1,0,0,1) + | x91 => (1,0,0,0,1,0,0,1) + | x92 => (0,1,0,0,1,0,0,1) + | x93 => (1,1,0,0,1,0,0,1) + | x94 => (0,0,1,0,1,0,0,1) + | x95 => (1,0,1,0,1,0,0,1) + | x96 => (0,1,1,0,1,0,0,1) + | x97 => (1,1,1,0,1,0,0,1) + | x98 => (0,0,0,1,1,0,0,1) + | x99 => (1,0,0,1,1,0,0,1) + | x9a => (0,1,0,1,1,0,0,1) + | x9b => (1,1,0,1,1,0,0,1) + | x9c => (0,0,1,1,1,0,0,1) + | x9d => (1,0,1,1,1,0,0,1) + | x9e => (0,1,1,1,1,0,0,1) + | x9f => (1,1,1,1,1,0,0,1) + | xa0 => (0,0,0,0,0,1,0,1) + | xa1 => (1,0,0,0,0,1,0,1) + | xa2 => (0,1,0,0,0,1,0,1) + | xa3 => (1,1,0,0,0,1,0,1) + | xa4 => (0,0,1,0,0,1,0,1) + | xa5 => (1,0,1,0,0,1,0,1) + | xa6 => (0,1,1,0,0,1,0,1) + | xa7 => (1,1,1,0,0,1,0,1) + | xa8 => (0,0,0,1,0,1,0,1) + | xa9 => (1,0,0,1,0,1,0,1) + | xaa => (0,1,0,1,0,1,0,1) + | xab => (1,1,0,1,0,1,0,1) + | xac => (0,0,1,1,0,1,0,1) + | xad => (1,0,1,1,0,1,0,1) + | xae => (0,1,1,1,0,1,0,1) + | xaf => (1,1,1,1,0,1,0,1) + | xb0 => (0,0,0,0,1,1,0,1) + | xb1 => (1,0,0,0,1,1,0,1) + | xb2 => (0,1,0,0,1,1,0,1) + | xb3 => (1,1,0,0,1,1,0,1) + | xb4 => (0,0,1,0,1,1,0,1) + | xb5 => (1,0,1,0,1,1,0,1) + | xb6 => (0,1,1,0,1,1,0,1) + | xb7 => (1,1,1,0,1,1,0,1) + | xb8 => (0,0,0,1,1,1,0,1) + | xb9 => (1,0,0,1,1,1,0,1) + | xba => (0,1,0,1,1,1,0,1) + | xbb => (1,1,0,1,1,1,0,1) + | xbc => (0,0,1,1,1,1,0,1) + | xbd => (1,0,1,1,1,1,0,1) + | xbe => (0,1,1,1,1,1,0,1) + | xbf => (1,1,1,1,1,1,0,1) + | xc0 => (0,0,0,0,0,0,1,1) + | xc1 => (1,0,0,0,0,0,1,1) + | xc2 => (0,1,0,0,0,0,1,1) + | xc3 => (1,1,0,0,0,0,1,1) + | xc4 => (0,0,1,0,0,0,1,1) + | xc5 => (1,0,1,0,0,0,1,1) + | xc6 => (0,1,1,0,0,0,1,1) + | xc7 => (1,1,1,0,0,0,1,1) + | xc8 => (0,0,0,1,0,0,1,1) + | xc9 => (1,0,0,1,0,0,1,1) + | xca => (0,1,0,1,0,0,1,1) + | xcb => (1,1,0,1,0,0,1,1) + | xcc => (0,0,1,1,0,0,1,1) + | xcd => (1,0,1,1,0,0,1,1) + | xce => (0,1,1,1,0,0,1,1) + | xcf => (1,1,1,1,0,0,1,1) + | xd0 => (0,0,0,0,1,0,1,1) + | xd1 => (1,0,0,0,1,0,1,1) + | xd2 => (0,1,0,0,1,0,1,1) + | xd3 => (1,1,0,0,1,0,1,1) + | xd4 => (0,0,1,0,1,0,1,1) + | xd5 => (1,0,1,0,1,0,1,1) + | xd6 => (0,1,1,0,1,0,1,1) + | xd7 => (1,1,1,0,1,0,1,1) + | xd8 => (0,0,0,1,1,0,1,1) + | xd9 => (1,0,0,1,1,0,1,1) + | xda => (0,1,0,1,1,0,1,1) + | xdb => (1,1,0,1,1,0,1,1) + | xdc => (0,0,1,1,1,0,1,1) + | xdd => (1,0,1,1,1,0,1,1) + | xde => (0,1,1,1,1,0,1,1) + | xdf => (1,1,1,1,1,0,1,1) + | xe0 => (0,0,0,0,0,1,1,1) + | xe1 => (1,0,0,0,0,1,1,1) + | xe2 => (0,1,0,0,0,1,1,1) + | xe3 => (1,1,0,0,0,1,1,1) + | xe4 => (0,0,1,0,0,1,1,1) + | xe5 => (1,0,1,0,0,1,1,1) + | xe6 => (0,1,1,0,0,1,1,1) + | xe7 => (1,1,1,0,0,1,1,1) + | xe8 => (0,0,0,1,0,1,1,1) + | xe9 => (1,0,0,1,0,1,1,1) + | xea => (0,1,0,1,0,1,1,1) + | xeb => (1,1,0,1,0,1,1,1) + | xec => (0,0,1,1,0,1,1,1) + | xed => (1,0,1,1,0,1,1,1) + | xee => (0,1,1,1,0,1,1,1) + | xef => (1,1,1,1,0,1,1,1) + | xf0 => (0,0,0,0,1,1,1,1) + | xf1 => (1,0,0,0,1,1,1,1) + | xf2 => (0,1,0,0,1,1,1,1) + | xf3 => (1,1,0,0,1,1,1,1) + | xf4 => (0,0,1,0,1,1,1,1) + | xf5 => (1,0,1,0,1,1,1,1) + | xf6 => (0,1,1,0,1,1,1,1) + | xf7 => (1,1,1,0,1,1,1,1) + | xf8 => (0,0,0,1,1,1,1,1) + | xf9 => (1,0,0,1,1,1,1,1) + | xfa => (0,1,0,1,1,1,1,1) + | xfb => (1,1,0,1,1,1,1,1) + | xfc => (0,0,1,1,1,1,1,1) + | xfd => (1,0,1,1,1,1,1,1) + | xfe => (0,1,1,1,1,1,1,1) + | xff => (1,1,1,1,1,1,1,1) + end. + +Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. +Proof. destruct b; exact eq_refl. Qed. + +Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b. +Proof. + repeat match goal with + | p : prod _ _ |- _ => destruct p + | b : bool |- _ => destruct b + end; + exact eq_refl. +Qed. Definition byte_of_byte (b : byte) : byte := b. Module Export ByteSyntaxNotations. String Notation byte byte_of_byte byte_of_byte : byte_scope. End ByteSyntaxNotations. - -Module Export ByteNotations. - Export ByteSyntaxNotations. - Infix "=?" := eqb (at level 70) : byte_scope. -End ByteNotations. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 13757c6007..a7bb1732be 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -190,36 +190,29 @@ Qed. *) Definition ascii_of_byte (b : byte) : ascii - := ascii_of_N (Byte.to_N b). + := let '(b7, b6, b5, b4, b3, b2, b1, b0) := Byte.to_bits b in + Ascii b7 b6 b5 b4 b3 b2 b1 b0. Definition byte_of_ascii (a : ascii) : byte - := match Byte.of_N (N_of_ascii a) with - | Some v => v - | None => x00 (* can't happen *) - end. + := let (b7, b6, b5, b4, b3, b2, b1, b0) := a in + Byte.of_bits (b7, b6, b5, b4, b3, b2, b1, b0). Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. Proof. cbv [ascii_of_byte byte_of_ascii]. - pose proof (to_of_N (N_of_ascii x)). - destruct (of_N (N_of_ascii x)) as [x'|] eqn:H1. - { specialize (H x' eq_refl); rewrite H. - apply ascii_N_embedding. } - { exfalso. - rewrite of_N_None_iff in H1. - pose proof (N_ascii_bounded x) as H2. - rewrite N.lt_nge in H1, H2. - destruct (N.le_gt_cases (N_of_ascii x) 255) as [H3|H3]. - { apply H1, H3. } - { rewrite <- N.le_succ_l in H3; apply H2, H3. } } + destruct x; rewrite to_bits_of_bits; reflexivity. Qed. Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x. Proof. cbv [ascii_of_byte byte_of_ascii]. - rewrite N_ascii_embedding, of_to_N; [ reflexivity | ]. - pose proof (to_N_bounded x) as H. - rewrite <- N.lt_succ_r in H; exact H. + repeat match goal with + | [ |- context[match ?x with pair _ _ => _ end] ] + => rewrite (surjective_pairing x) + | [ |- context[(fst ?x, snd ?x)] ] + => rewrite <- (surjective_pairing x) + end. + rewrite of_bits_to_bits; reflexivity. Qed. Module Export AsciiSyntax. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v index 581094a8b5..d4c719bb4c 100644 --- a/theories/Strings/Byte.v +++ b/theories/Strings/Byte.v @@ -14,278 +14,40 @@ Require Export Coq.Init.Byte. Local Set Implicit Arguments. -Lemma byte_dec_lb x y : x = y -> Byte.eqb x y = true. +Definition eqb (a b : byte) : bool + := let '(a7, a6, a5, a4, a3, a2, a1, a0) := to_bits a in + let '(b7, b6, b5, b4, b3, b2, b1, b0) := to_bits b in + (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 && + Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool. + +Module Export ByteNotations. + Export ByteSyntaxNotations. + Infix "=?" := eqb (at level 70) : byte_scope. +End ByteNotations. + +Lemma byte_dec_lb x y : x = y -> eqb x y = true. Proof. intro; subst y; destruct x; reflexivity. Defined. -Definition byte_dec_bl x y (H : Byte.eqb x y = true) : x = y - := match H in (_ = tr) return if tr then x = y else True with - | eq_refl - => match x, y return if Byte.eqb x y then x = y else True with - | x00, x00 => eq_refl - | x01, x01 => eq_refl - | x02, x02 => eq_refl - | x03, x03 => eq_refl - | x04, x04 => eq_refl - | x05, x05 => eq_refl - | x06, x06 => eq_refl - | x07, x07 => eq_refl - | x08, x08 => eq_refl - | x09, x09 => eq_refl - | x0a, x0a => eq_refl - | x0b, x0b => eq_refl - | x0c, x0c => eq_refl - | x0d, x0d => eq_refl - | x0e, x0e => eq_refl - | x0f, x0f => eq_refl - | x10, x10 => eq_refl - | x11, x11 => eq_refl - | x12, x12 => eq_refl - | x13, x13 => eq_refl - | x14, x14 => eq_refl - | x15, x15 => eq_refl - | x16, x16 => eq_refl - | x17, x17 => eq_refl - | x18, x18 => eq_refl - | x19, x19 => eq_refl - | x1a, x1a => eq_refl - | x1b, x1b => eq_refl - | x1c, x1c => eq_refl - | x1d, x1d => eq_refl - | x1e, x1e => eq_refl - | x1f, x1f => eq_refl - | x20, x20 => eq_refl - | x21, x21 => eq_refl - | x22, x22 => eq_refl - | x23, x23 => eq_refl - | x24, x24 => eq_refl - | x25, x25 => eq_refl - | x26, x26 => eq_refl - | x27, x27 => eq_refl - | x28, x28 => eq_refl - | x29, x29 => eq_refl - | x2a, x2a => eq_refl - | x2b, x2b => eq_refl - | x2c, x2c => eq_refl - | x2d, x2d => eq_refl - | x2e, x2e => eq_refl - | x2f, x2f => eq_refl - | x30, x30 => eq_refl - | x31, x31 => eq_refl - | x32, x32 => eq_refl - | x33, x33 => eq_refl - | x34, x34 => eq_refl - | x35, x35 => eq_refl - | x36, x36 => eq_refl - | x37, x37 => eq_refl - | x38, x38 => eq_refl - | x39, x39 => eq_refl - | x3a, x3a => eq_refl - | x3b, x3b => eq_refl - | x3c, x3c => eq_refl - | x3d, x3d => eq_refl - | x3e, x3e => eq_refl - | x3f, x3f => eq_refl - | x40, x40 => eq_refl - | x41, x41 => eq_refl - | x42, x42 => eq_refl - | x43, x43 => eq_refl - | x44, x44 => eq_refl - | x45, x45 => eq_refl - | x46, x46 => eq_refl - | x47, x47 => eq_refl - | x48, x48 => eq_refl - | x49, x49 => eq_refl - | x4a, x4a => eq_refl - | x4b, x4b => eq_refl - | x4c, x4c => eq_refl - | x4d, x4d => eq_refl - | x4e, x4e => eq_refl - | x4f, x4f => eq_refl - | x50, x50 => eq_refl - | x51, x51 => eq_refl - | x52, x52 => eq_refl - | x53, x53 => eq_refl - | x54, x54 => eq_refl - | x55, x55 => eq_refl - | x56, x56 => eq_refl - | x57, x57 => eq_refl - | x58, x58 => eq_refl - | x59, x59 => eq_refl - | x5a, x5a => eq_refl - | x5b, x5b => eq_refl - | x5c, x5c => eq_refl - | x5d, x5d => eq_refl - | x5e, x5e => eq_refl - | x5f, x5f => eq_refl - | x60, x60 => eq_refl - | x61, x61 => eq_refl - | x62, x62 => eq_refl - | x63, x63 => eq_refl - | x64, x64 => eq_refl - | x65, x65 => eq_refl - | x66, x66 => eq_refl - | x67, x67 => eq_refl - | x68, x68 => eq_refl - | x69, x69 => eq_refl - | x6a, x6a => eq_refl - | x6b, x6b => eq_refl - | x6c, x6c => eq_refl - | x6d, x6d => eq_refl - | x6e, x6e => eq_refl - | x6f, x6f => eq_refl - | x70, x70 => eq_refl - | x71, x71 => eq_refl - | x72, x72 => eq_refl - | x73, x73 => eq_refl - | x74, x74 => eq_refl - | x75, x75 => eq_refl - | x76, x76 => eq_refl - | x77, x77 => eq_refl - | x78, x78 => eq_refl - | x79, x79 => eq_refl - | x7a, x7a => eq_refl - | x7b, x7b => eq_refl - | x7c, x7c => eq_refl - | x7d, x7d => eq_refl - | x7e, x7e => eq_refl - | x7f, x7f => eq_refl - | x80, x80 => eq_refl - | x81, x81 => eq_refl - | x82, x82 => eq_refl - | x83, x83 => eq_refl - | x84, x84 => eq_refl - | x85, x85 => eq_refl - | x86, x86 => eq_refl - | x87, x87 => eq_refl - | x88, x88 => eq_refl - | x89, x89 => eq_refl - | x8a, x8a => eq_refl - | x8b, x8b => eq_refl - | x8c, x8c => eq_refl - | x8d, x8d => eq_refl - | x8e, x8e => eq_refl - | x8f, x8f => eq_refl - | x90, x90 => eq_refl - | x91, x91 => eq_refl - | x92, x92 => eq_refl - | x93, x93 => eq_refl - | x94, x94 => eq_refl - | x95, x95 => eq_refl - | x96, x96 => eq_refl - | x97, x97 => eq_refl - | x98, x98 => eq_refl - | x99, x99 => eq_refl - | x9a, x9a => eq_refl - | x9b, x9b => eq_refl - | x9c, x9c => eq_refl - | x9d, x9d => eq_refl - | x9e, x9e => eq_refl - | x9f, x9f => eq_refl - | xa0, xa0 => eq_refl - | xa1, xa1 => eq_refl - | xa2, xa2 => eq_refl - | xa3, xa3 => eq_refl - | xa4, xa4 => eq_refl - | xa5, xa5 => eq_refl - | xa6, xa6 => eq_refl - | xa7, xa7 => eq_refl - | xa8, xa8 => eq_refl - | xa9, xa9 => eq_refl - | xaa, xaa => eq_refl - | xab, xab => eq_refl - | xac, xac => eq_refl - | xad, xad => eq_refl - | xae, xae => eq_refl - | xaf, xaf => eq_refl - | xb0, xb0 => eq_refl - | xb1, xb1 => eq_refl - | xb2, xb2 => eq_refl - | xb3, xb3 => eq_refl - | xb4, xb4 => eq_refl - | xb5, xb5 => eq_refl - | xb6, xb6 => eq_refl - | xb7, xb7 => eq_refl - | xb8, xb8 => eq_refl - | xb9, xb9 => eq_refl - | xba, xba => eq_refl - | xbb, xbb => eq_refl - | xbc, xbc => eq_refl - | xbd, xbd => eq_refl - | xbe, xbe => eq_refl - | xbf, xbf => eq_refl - | xc0, xc0 => eq_refl - | xc1, xc1 => eq_refl - | xc2, xc2 => eq_refl - | xc3, xc3 => eq_refl - | xc4, xc4 => eq_refl - | xc5, xc5 => eq_refl - | xc6, xc6 => eq_refl - | xc7, xc7 => eq_refl - | xc8, xc8 => eq_refl - | xc9, xc9 => eq_refl - | xca, xca => eq_refl - | xcb, xcb => eq_refl - | xcc, xcc => eq_refl - | xcd, xcd => eq_refl - | xce, xce => eq_refl - | xcf, xcf => eq_refl - | xd0, xd0 => eq_refl - | xd1, xd1 => eq_refl - | xd2, xd2 => eq_refl - | xd3, xd3 => eq_refl - | xd4, xd4 => eq_refl - | xd5, xd5 => eq_refl - | xd6, xd6 => eq_refl - | xd7, xd7 => eq_refl - | xd8, xd8 => eq_refl - | xd9, xd9 => eq_refl - | xda, xda => eq_refl - | xdb, xdb => eq_refl - | xdc, xdc => eq_refl - | xdd, xdd => eq_refl - | xde, xde => eq_refl - | xdf, xdf => eq_refl - | xe0, xe0 => eq_refl - | xe1, xe1 => eq_refl - | xe2, xe2 => eq_refl - | xe3, xe3 => eq_refl - | xe4, xe4 => eq_refl - | xe5, xe5 => eq_refl - | xe6, xe6 => eq_refl - | xe7, xe7 => eq_refl - | xe8, xe8 => eq_refl - | xe9, xe9 => eq_refl - | xea, xea => eq_refl - | xeb, xeb => eq_refl - | xec, xec => eq_refl - | xed, xed => eq_refl - | xee, xee => eq_refl - | xef, xef => eq_refl - | xf0, xf0 => eq_refl - | xf1, xf1 => eq_refl - | xf2, xf2 => eq_refl - | xf3, xf3 => eq_refl - | xf4, xf4 => eq_refl - | xf5, xf5 => eq_refl - | xf6, xf6 => eq_refl - | xf7, xf7 => eq_refl - | xf8, xf8 => eq_refl - | xf9, xf9 => eq_refl - | xfa, xfa => eq_refl - | xfb, xfb => eq_refl - | xfc, xfc => eq_refl - | xfd, xfd => eq_refl - | xfe, xfe => eq_refl - | xff, xff => eq_refl - | _, _ => I - end - end. +Lemma byte_dec_bl x y (H : eqb x y = true) : x = y. +Proof. + rewrite <- (of_bits_to_bits x), <- (of_bits_to_bits y). + cbv [eqb] in H; revert H. + generalize (to_bits x) (to_bits y); clear x y; intros x y H. + repeat match goal with + | [ H : and _ _ |- _ ] => destruct H + | [ H : prod _ _ |- _ ] => destruct H + | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H + | [ H : context[Bool.eqb _ _ = true] |- _ ] => rewrite Bool.eqb_true_iff in H + | _ => progress subst + | _ => reflexivity + end. +Qed. -Lemma eqb_false x y : Byte.eqb x y = false -> x <> y. +Lemma eqb_false x y : eqb x y = false -> x <> y. Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed. Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y} - := (if Byte.eqb x y as beq return Byte.eqb x y = beq -> _ + := (if eqb x y as beq return eqb x y = beq -> _ then fun pf => left (byte_dec_bl x y pf) else fun pf => right (eqb_false pf)) eq_refl. -- cgit v1.2.3 From bc6affea2270b1182181c42f3c3f06360bf216e6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Nov 2018 14:59:20 -0500 Subject: Proofs to ensure that conversions round-trip We already have roundtrip proofs for byte<->nat, byte<->N, byte<->ascii, N<->nat, ascii<->N, ascii<->nat, and this commit shows that all roundtrips involving byte commute appropriately. This ensures, e.g., that we don't mess up and reverse the bits in conversion between byte and ascii. --- theories/Strings/Ascii.v | 16 ++++++++++++++++ theories/Strings/Byte.v | 27 +++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) (limited to 'theories') diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index a7bb1732be..131147ff8d 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -215,6 +215,22 @@ Proof. rewrite of_bits_to_bits; reflexivity. Qed. +Lemma ascii_of_byte_via_N x : ascii_of_byte x = ascii_of_N (Byte.to_N x). +Proof. destruct x; reflexivity. Qed. + +Lemma ascii_of_byte_via_nat x : ascii_of_byte x = ascii_of_nat (Byte.to_nat x). +Proof. destruct x; reflexivity. Qed. + +Lemma byte_of_ascii_via_N x : Some (byte_of_ascii x) = Byte.of_N (N_of_ascii x). +Proof. + rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity. +Qed. + +Lemma byte_of_ascii_via_nat x : Some (byte_of_ascii x) = Byte.of_nat (nat_of_ascii x). +Proof. + rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity. +Qed. + Module Export AsciiSyntax. String Notation ascii ascii_of_byte byte_of_ascii : char_scope. End AsciiSyntax. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v index d4c719bb4c..4daa0b196c 100644 --- a/theories/Strings/Byte.v +++ b/theories/Strings/Byte.v @@ -10,6 +10,7 @@ Require Import Coq.Arith.EqNat. Require Import Coq.NArith.BinNat. +Require Import Coq.NArith.Nnat. Require Export Coq.Init.Byte. Local Set Implicit Arguments. @@ -1184,4 +1185,30 @@ Section N. { rewrite N.leb_nle in H; split; [ | reflexivity ]. rewrite N.lt_nge; intro; assumption. } Qed. + + Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x). + Proof. destruct x; reflexivity. Qed. + + Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x). + Proof. destruct x; reflexivity. Qed. + + Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x). + Proof. + destruct (of_N x) as [b|] eqn:H1. + { rewrite to_of_N_iff in H1; subst. + destruct b; reflexivity. } + { rewrite of_N_None_iff, <- N.compare_lt_iff in H1. + symmetry; rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff. + rewrite Nat2N.inj_compare, N2Nat.id; assumption. } + Qed. + + Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x). + Proof. + destruct (of_nat x) as [b|] eqn:H1. + { rewrite to_of_nat_iff in H1; subst. + destruct b; reflexivity. } + { rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1. + symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff. + rewrite N2Nat.inj_compare, Nat2N.id; assumption. } + Qed. End N. -- cgit v1.2.3 From f5e3d9e29f030a86433bb2700e55c4c183593163 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Nov 2018 15:16:31 -0500 Subject: Byte.v: use right-associative tuples in bits We encode the conversion to bits with little-endian right-associative tuples to ensure that the head of the tuple (the `fst` element) is the least significant bit. We still enforce that the ordering of bits matches the order of the `bool`s in the `ascii` inductive type. --- theories/Init/Byte.v | 1028 +++++++++++++++++++++++----------------------- theories/Strings/Ascii.v | 8 +- theories/Strings/Byte.v | 4 +- 3 files changed, 520 insertions(+), 520 deletions(-) (limited to 'theories') diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 59b5f5ebe3..eede9d5028 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -291,524 +291,524 @@ Local Notation "0" := false. Local Notation "1" := true. (** We pick a definition that matches with [Ascii.ascii] *) -Definition of_bits (b : bool * bool * bool * bool * bool * bool * bool * bool) : byte +Definition of_bits (b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))) : byte := match b with - | (0,0,0,0,0,0,0,0) => x00 - | (1,0,0,0,0,0,0,0) => x01 - | (0,1,0,0,0,0,0,0) => x02 - | (1,1,0,0,0,0,0,0) => x03 - | (0,0,1,0,0,0,0,0) => x04 - | (1,0,1,0,0,0,0,0) => x05 - | (0,1,1,0,0,0,0,0) => x06 - | (1,1,1,0,0,0,0,0) => x07 - | (0,0,0,1,0,0,0,0) => x08 - | (1,0,0,1,0,0,0,0) => x09 - | (0,1,0,1,0,0,0,0) => x0a - | (1,1,0,1,0,0,0,0) => x0b - | (0,0,1,1,0,0,0,0) => x0c - | (1,0,1,1,0,0,0,0) => x0d - | (0,1,1,1,0,0,0,0) => x0e - | (1,1,1,1,0,0,0,0) => x0f - | (0,0,0,0,1,0,0,0) => x10 - | (1,0,0,0,1,0,0,0) => x11 - | (0,1,0,0,1,0,0,0) => x12 - | (1,1,0,0,1,0,0,0) => x13 - | (0,0,1,0,1,0,0,0) => x14 - | (1,0,1,0,1,0,0,0) => x15 - | (0,1,1,0,1,0,0,0) => x16 - | (1,1,1,0,1,0,0,0) => x17 - | (0,0,0,1,1,0,0,0) => x18 - | (1,0,0,1,1,0,0,0) => x19 - | (0,1,0,1,1,0,0,0) => x1a - | (1,1,0,1,1,0,0,0) => x1b - | (0,0,1,1,1,0,0,0) => x1c - | (1,0,1,1,1,0,0,0) => x1d - | (0,1,1,1,1,0,0,0) => x1e - | (1,1,1,1,1,0,0,0) => x1f - | (0,0,0,0,0,1,0,0) => x20 - | (1,0,0,0,0,1,0,0) => x21 - | (0,1,0,0,0,1,0,0) => x22 - | (1,1,0,0,0,1,0,0) => x23 - | (0,0,1,0,0,1,0,0) => x24 - | (1,0,1,0,0,1,0,0) => x25 - | (0,1,1,0,0,1,0,0) => x26 - | (1,1,1,0,0,1,0,0) => x27 - | (0,0,0,1,0,1,0,0) => x28 - | (1,0,0,1,0,1,0,0) => x29 - | (0,1,0,1,0,1,0,0) => x2a - | (1,1,0,1,0,1,0,0) => x2b - | (0,0,1,1,0,1,0,0) => x2c - | (1,0,1,1,0,1,0,0) => x2d - | (0,1,1,1,0,1,0,0) => x2e - | (1,1,1,1,0,1,0,0) => x2f - | (0,0,0,0,1,1,0,0) => x30 - | (1,0,0,0,1,1,0,0) => x31 - | (0,1,0,0,1,1,0,0) => x32 - | (1,1,0,0,1,1,0,0) => x33 - | (0,0,1,0,1,1,0,0) => x34 - | (1,0,1,0,1,1,0,0) => x35 - | (0,1,1,0,1,1,0,0) => x36 - | (1,1,1,0,1,1,0,0) => x37 - | (0,0,0,1,1,1,0,0) => x38 - | (1,0,0,1,1,1,0,0) => x39 - | (0,1,0,1,1,1,0,0) => x3a - | (1,1,0,1,1,1,0,0) => x3b - | (0,0,1,1,1,1,0,0) => x3c - | (1,0,1,1,1,1,0,0) => x3d - | (0,1,1,1,1,1,0,0) => x3e - | (1,1,1,1,1,1,0,0) => x3f - | (0,0,0,0,0,0,1,0) => x40 - | (1,0,0,0,0,0,1,0) => x41 - | (0,1,0,0,0,0,1,0) => x42 - | (1,1,0,0,0,0,1,0) => x43 - | (0,0,1,0,0,0,1,0) => x44 - | (1,0,1,0,0,0,1,0) => x45 - | (0,1,1,0,0,0,1,0) => x46 - | (1,1,1,0,0,0,1,0) => x47 - | (0,0,0,1,0,0,1,0) => x48 - | (1,0,0,1,0,0,1,0) => x49 - | (0,1,0,1,0,0,1,0) => x4a - | (1,1,0,1,0,0,1,0) => x4b - | (0,0,1,1,0,0,1,0) => x4c - | (1,0,1,1,0,0,1,0) => x4d - | (0,1,1,1,0,0,1,0) => x4e - | (1,1,1,1,0,0,1,0) => x4f - | (0,0,0,0,1,0,1,0) => x50 - | (1,0,0,0,1,0,1,0) => x51 - | (0,1,0,0,1,0,1,0) => x52 - | (1,1,0,0,1,0,1,0) => x53 - | (0,0,1,0,1,0,1,0) => x54 - | (1,0,1,0,1,0,1,0) => x55 - | (0,1,1,0,1,0,1,0) => x56 - | (1,1,1,0,1,0,1,0) => x57 - | (0,0,0,1,1,0,1,0) => x58 - | (1,0,0,1,1,0,1,0) => x59 - | (0,1,0,1,1,0,1,0) => x5a - | (1,1,0,1,1,0,1,0) => x5b - | (0,0,1,1,1,0,1,0) => x5c - | (1,0,1,1,1,0,1,0) => x5d - | (0,1,1,1,1,0,1,0) => x5e - | (1,1,1,1,1,0,1,0) => x5f - | (0,0,0,0,0,1,1,0) => x60 - | (1,0,0,0,0,1,1,0) => x61 - | (0,1,0,0,0,1,1,0) => x62 - | (1,1,0,0,0,1,1,0) => x63 - | (0,0,1,0,0,1,1,0) => x64 - | (1,0,1,0,0,1,1,0) => x65 - | (0,1,1,0,0,1,1,0) => x66 - | (1,1,1,0,0,1,1,0) => x67 - | (0,0,0,1,0,1,1,0) => x68 - | (1,0,0,1,0,1,1,0) => x69 - | (0,1,0,1,0,1,1,0) => x6a - | (1,1,0,1,0,1,1,0) => x6b - | (0,0,1,1,0,1,1,0) => x6c - | (1,0,1,1,0,1,1,0) => x6d - | (0,1,1,1,0,1,1,0) => x6e - | (1,1,1,1,0,1,1,0) => x6f - | (0,0,0,0,1,1,1,0) => x70 - | (1,0,0,0,1,1,1,0) => x71 - | (0,1,0,0,1,1,1,0) => x72 - | (1,1,0,0,1,1,1,0) => x73 - | (0,0,1,0,1,1,1,0) => x74 - | (1,0,1,0,1,1,1,0) => x75 - | (0,1,1,0,1,1,1,0) => x76 - | (1,1,1,0,1,1,1,0) => x77 - | (0,0,0,1,1,1,1,0) => x78 - | (1,0,0,1,1,1,1,0) => x79 - | (0,1,0,1,1,1,1,0) => x7a - | (1,1,0,1,1,1,1,0) => x7b - | (0,0,1,1,1,1,1,0) => x7c - | (1,0,1,1,1,1,1,0) => x7d - | (0,1,1,1,1,1,1,0) => x7e - | (1,1,1,1,1,1,1,0) => x7f - | (0,0,0,0,0,0,0,1) => x80 - | (1,0,0,0,0,0,0,1) => x81 - | (0,1,0,0,0,0,0,1) => x82 - | (1,1,0,0,0,0,0,1) => x83 - | (0,0,1,0,0,0,0,1) => x84 - | (1,0,1,0,0,0,0,1) => x85 - | (0,1,1,0,0,0,0,1) => x86 - | (1,1,1,0,0,0,0,1) => x87 - | (0,0,0,1,0,0,0,1) => x88 - | (1,0,0,1,0,0,0,1) => x89 - | (0,1,0,1,0,0,0,1) => x8a - | (1,1,0,1,0,0,0,1) => x8b - | (0,0,1,1,0,0,0,1) => x8c - | (1,0,1,1,0,0,0,1) => x8d - | (0,1,1,1,0,0,0,1) => x8e - | (1,1,1,1,0,0,0,1) => x8f - | (0,0,0,0,1,0,0,1) => x90 - | (1,0,0,0,1,0,0,1) => x91 - | (0,1,0,0,1,0,0,1) => x92 - | (1,1,0,0,1,0,0,1) => x93 - | (0,0,1,0,1,0,0,1) => x94 - | (1,0,1,0,1,0,0,1) => x95 - | (0,1,1,0,1,0,0,1) => x96 - | (1,1,1,0,1,0,0,1) => x97 - | (0,0,0,1,1,0,0,1) => x98 - | (1,0,0,1,1,0,0,1) => x99 - | (0,1,0,1,1,0,0,1) => x9a - | (1,1,0,1,1,0,0,1) => x9b - | (0,0,1,1,1,0,0,1) => x9c - | (1,0,1,1,1,0,0,1) => x9d - | (0,1,1,1,1,0,0,1) => x9e - | (1,1,1,1,1,0,0,1) => x9f - | (0,0,0,0,0,1,0,1) => xa0 - | (1,0,0,0,0,1,0,1) => xa1 - | (0,1,0,0,0,1,0,1) => xa2 - | (1,1,0,0,0,1,0,1) => xa3 - | (0,0,1,0,0,1,0,1) => xa4 - | (1,0,1,0,0,1,0,1) => xa5 - | (0,1,1,0,0,1,0,1) => xa6 - | (1,1,1,0,0,1,0,1) => xa7 - | (0,0,0,1,0,1,0,1) => xa8 - | (1,0,0,1,0,1,0,1) => xa9 - | (0,1,0,1,0,1,0,1) => xaa - | (1,1,0,1,0,1,0,1) => xab - | (0,0,1,1,0,1,0,1) => xac - | (1,0,1,1,0,1,0,1) => xad - | (0,1,1,1,0,1,0,1) => xae - | (1,1,1,1,0,1,0,1) => xaf - | (0,0,0,0,1,1,0,1) => xb0 - | (1,0,0,0,1,1,0,1) => xb1 - | (0,1,0,0,1,1,0,1) => xb2 - | (1,1,0,0,1,1,0,1) => xb3 - | (0,0,1,0,1,1,0,1) => xb4 - | (1,0,1,0,1,1,0,1) => xb5 - | (0,1,1,0,1,1,0,1) => xb6 - | (1,1,1,0,1,1,0,1) => xb7 - | (0,0,0,1,1,1,0,1) => xb8 - | (1,0,0,1,1,1,0,1) => xb9 - | (0,1,0,1,1,1,0,1) => xba - | (1,1,0,1,1,1,0,1) => xbb - | (0,0,1,1,1,1,0,1) => xbc - | (1,0,1,1,1,1,0,1) => xbd - | (0,1,1,1,1,1,0,1) => xbe - | (1,1,1,1,1,1,0,1) => xbf - | (0,0,0,0,0,0,1,1) => xc0 - | (1,0,0,0,0,0,1,1) => xc1 - | (0,1,0,0,0,0,1,1) => xc2 - | (1,1,0,0,0,0,1,1) => xc3 - | (0,0,1,0,0,0,1,1) => xc4 - | (1,0,1,0,0,0,1,1) => xc5 - | (0,1,1,0,0,0,1,1) => xc6 - | (1,1,1,0,0,0,1,1) => xc7 - | (0,0,0,1,0,0,1,1) => xc8 - | (1,0,0,1,0,0,1,1) => xc9 - | (0,1,0,1,0,0,1,1) => xca - | (1,1,0,1,0,0,1,1) => xcb - | (0,0,1,1,0,0,1,1) => xcc - | (1,0,1,1,0,0,1,1) => xcd - | (0,1,1,1,0,0,1,1) => xce - | (1,1,1,1,0,0,1,1) => xcf - | (0,0,0,0,1,0,1,1) => xd0 - | (1,0,0,0,1,0,1,1) => xd1 - | (0,1,0,0,1,0,1,1) => xd2 - | (1,1,0,0,1,0,1,1) => xd3 - | (0,0,1,0,1,0,1,1) => xd4 - | (1,0,1,0,1,0,1,1) => xd5 - | (0,1,1,0,1,0,1,1) => xd6 - | (1,1,1,0,1,0,1,1) => xd7 - | (0,0,0,1,1,0,1,1) => xd8 - | (1,0,0,1,1,0,1,1) => xd9 - | (0,1,0,1,1,0,1,1) => xda - | (1,1,0,1,1,0,1,1) => xdb - | (0,0,1,1,1,0,1,1) => xdc - | (1,0,1,1,1,0,1,1) => xdd - | (0,1,1,1,1,0,1,1) => xde - | (1,1,1,1,1,0,1,1) => xdf - | (0,0,0,0,0,1,1,1) => xe0 - | (1,0,0,0,0,1,1,1) => xe1 - | (0,1,0,0,0,1,1,1) => xe2 - | (1,1,0,0,0,1,1,1) => xe3 - | (0,0,1,0,0,1,1,1) => xe4 - | (1,0,1,0,0,1,1,1) => xe5 - | (0,1,1,0,0,1,1,1) => xe6 - | (1,1,1,0,0,1,1,1) => xe7 - | (0,0,0,1,0,1,1,1) => xe8 - | (1,0,0,1,0,1,1,1) => xe9 - | (0,1,0,1,0,1,1,1) => xea - | (1,1,0,1,0,1,1,1) => xeb - | (0,0,1,1,0,1,1,1) => xec - | (1,0,1,1,0,1,1,1) => xed - | (0,1,1,1,0,1,1,1) => xee - | (1,1,1,1,0,1,1,1) => xef - | (0,0,0,0,1,1,1,1) => xf0 - | (1,0,0,0,1,1,1,1) => xf1 - | (0,1,0,0,1,1,1,1) => xf2 - | (1,1,0,0,1,1,1,1) => xf3 - | (0,0,1,0,1,1,1,1) => xf4 - | (1,0,1,0,1,1,1,1) => xf5 - | (0,1,1,0,1,1,1,1) => xf6 - | (1,1,1,0,1,1,1,1) => xf7 - | (0,0,0,1,1,1,1,1) => xf8 - | (1,0,0,1,1,1,1,1) => xf9 - | (0,1,0,1,1,1,1,1) => xfa - | (1,1,0,1,1,1,1,1) => xfb - | (0,0,1,1,1,1,1,1) => xfc - | (1,0,1,1,1,1,1,1) => xfd - | (0,1,1,1,1,1,1,1) => xfe - | (1,1,1,1,1,1,1,1) => xff + | (0,(0,(0,(0,(0,(0,(0,0))))))) => x00 + | (1,(0,(0,(0,(0,(0,(0,0))))))) => x01 + | (0,(1,(0,(0,(0,(0,(0,0))))))) => x02 + | (1,(1,(0,(0,(0,(0,(0,0))))))) => x03 + | (0,(0,(1,(0,(0,(0,(0,0))))))) => x04 + | (1,(0,(1,(0,(0,(0,(0,0))))))) => x05 + | (0,(1,(1,(0,(0,(0,(0,0))))))) => x06 + | (1,(1,(1,(0,(0,(0,(0,0))))))) => x07 + | (0,(0,(0,(1,(0,(0,(0,0))))))) => x08 + | (1,(0,(0,(1,(0,(0,(0,0))))))) => x09 + | (0,(1,(0,(1,(0,(0,(0,0))))))) => x0a + | (1,(1,(0,(1,(0,(0,(0,0))))))) => x0b + | (0,(0,(1,(1,(0,(0,(0,0))))))) => x0c + | (1,(0,(1,(1,(0,(0,(0,0))))))) => x0d + | (0,(1,(1,(1,(0,(0,(0,0))))))) => x0e + | (1,(1,(1,(1,(0,(0,(0,0))))))) => x0f + | (0,(0,(0,(0,(1,(0,(0,0))))))) => x10 + | (1,(0,(0,(0,(1,(0,(0,0))))))) => x11 + | (0,(1,(0,(0,(1,(0,(0,0))))))) => x12 + | (1,(1,(0,(0,(1,(0,(0,0))))))) => x13 + | (0,(0,(1,(0,(1,(0,(0,0))))))) => x14 + | (1,(0,(1,(0,(1,(0,(0,0))))))) => x15 + | (0,(1,(1,(0,(1,(0,(0,0))))))) => x16 + | (1,(1,(1,(0,(1,(0,(0,0))))))) => x17 + | (0,(0,(0,(1,(1,(0,(0,0))))))) => x18 + | (1,(0,(0,(1,(1,(0,(0,0))))))) => x19 + | (0,(1,(0,(1,(1,(0,(0,0))))))) => x1a + | (1,(1,(0,(1,(1,(0,(0,0))))))) => x1b + | (0,(0,(1,(1,(1,(0,(0,0))))))) => x1c + | (1,(0,(1,(1,(1,(0,(0,0))))))) => x1d + | (0,(1,(1,(1,(1,(0,(0,0))))))) => x1e + | (1,(1,(1,(1,(1,(0,(0,0))))))) => x1f + | (0,(0,(0,(0,(0,(1,(0,0))))))) => x20 + | (1,(0,(0,(0,(0,(1,(0,0))))))) => x21 + | (0,(1,(0,(0,(0,(1,(0,0))))))) => x22 + | (1,(1,(0,(0,(0,(1,(0,0))))))) => x23 + | (0,(0,(1,(0,(0,(1,(0,0))))))) => x24 + | (1,(0,(1,(0,(0,(1,(0,0))))))) => x25 + | (0,(1,(1,(0,(0,(1,(0,0))))))) => x26 + | (1,(1,(1,(0,(0,(1,(0,0))))))) => x27 + | (0,(0,(0,(1,(0,(1,(0,0))))))) => x28 + | (1,(0,(0,(1,(0,(1,(0,0))))))) => x29 + | (0,(1,(0,(1,(0,(1,(0,0))))))) => x2a + | (1,(1,(0,(1,(0,(1,(0,0))))))) => x2b + | (0,(0,(1,(1,(0,(1,(0,0))))))) => x2c + | (1,(0,(1,(1,(0,(1,(0,0))))))) => x2d + | (0,(1,(1,(1,(0,(1,(0,0))))))) => x2e + | (1,(1,(1,(1,(0,(1,(0,0))))))) => x2f + | (0,(0,(0,(0,(1,(1,(0,0))))))) => x30 + | (1,(0,(0,(0,(1,(1,(0,0))))))) => x31 + | (0,(1,(0,(0,(1,(1,(0,0))))))) => x32 + | (1,(1,(0,(0,(1,(1,(0,0))))))) => x33 + | (0,(0,(1,(0,(1,(1,(0,0))))))) => x34 + | (1,(0,(1,(0,(1,(1,(0,0))))))) => x35 + | (0,(1,(1,(0,(1,(1,(0,0))))))) => x36 + | (1,(1,(1,(0,(1,(1,(0,0))))))) => x37 + | (0,(0,(0,(1,(1,(1,(0,0))))))) => x38 + | (1,(0,(0,(1,(1,(1,(0,0))))))) => x39 + | (0,(1,(0,(1,(1,(1,(0,0))))))) => x3a + | (1,(1,(0,(1,(1,(1,(0,0))))))) => x3b + | (0,(0,(1,(1,(1,(1,(0,0))))))) => x3c + | (1,(0,(1,(1,(1,(1,(0,0))))))) => x3d + | (0,(1,(1,(1,(1,(1,(0,0))))))) => x3e + | (1,(1,(1,(1,(1,(1,(0,0))))))) => x3f + | (0,(0,(0,(0,(0,(0,(1,0))))))) => x40 + | (1,(0,(0,(0,(0,(0,(1,0))))))) => x41 + | (0,(1,(0,(0,(0,(0,(1,0))))))) => x42 + | (1,(1,(0,(0,(0,(0,(1,0))))))) => x43 + | (0,(0,(1,(0,(0,(0,(1,0))))))) => x44 + | (1,(0,(1,(0,(0,(0,(1,0))))))) => x45 + | (0,(1,(1,(0,(0,(0,(1,0))))))) => x46 + | (1,(1,(1,(0,(0,(0,(1,0))))))) => x47 + | (0,(0,(0,(1,(0,(0,(1,0))))))) => x48 + | (1,(0,(0,(1,(0,(0,(1,0))))))) => x49 + | (0,(1,(0,(1,(0,(0,(1,0))))))) => x4a + | (1,(1,(0,(1,(0,(0,(1,0))))))) => x4b + | (0,(0,(1,(1,(0,(0,(1,0))))))) => x4c + | (1,(0,(1,(1,(0,(0,(1,0))))))) => x4d + | (0,(1,(1,(1,(0,(0,(1,0))))))) => x4e + | (1,(1,(1,(1,(0,(0,(1,0))))))) => x4f + | (0,(0,(0,(0,(1,(0,(1,0))))))) => x50 + | (1,(0,(0,(0,(1,(0,(1,0))))))) => x51 + | (0,(1,(0,(0,(1,(0,(1,0))))))) => x52 + | (1,(1,(0,(0,(1,(0,(1,0))))))) => x53 + | (0,(0,(1,(0,(1,(0,(1,0))))))) => x54 + | (1,(0,(1,(0,(1,(0,(1,0))))))) => x55 + | (0,(1,(1,(0,(1,(0,(1,0))))))) => x56 + | (1,(1,(1,(0,(1,(0,(1,0))))))) => x57 + | (0,(0,(0,(1,(1,(0,(1,0))))))) => x58 + | (1,(0,(0,(1,(1,(0,(1,0))))))) => x59 + | (0,(1,(0,(1,(1,(0,(1,0))))))) => x5a + | (1,(1,(0,(1,(1,(0,(1,0))))))) => x5b + | (0,(0,(1,(1,(1,(0,(1,0))))))) => x5c + | (1,(0,(1,(1,(1,(0,(1,0))))))) => x5d + | (0,(1,(1,(1,(1,(0,(1,0))))))) => x5e + | (1,(1,(1,(1,(1,(0,(1,0))))))) => x5f + | (0,(0,(0,(0,(0,(1,(1,0))))))) => x60 + | (1,(0,(0,(0,(0,(1,(1,0))))))) => x61 + | (0,(1,(0,(0,(0,(1,(1,0))))))) => x62 + | (1,(1,(0,(0,(0,(1,(1,0))))))) => x63 + | (0,(0,(1,(0,(0,(1,(1,0))))))) => x64 + | (1,(0,(1,(0,(0,(1,(1,0))))))) => x65 + | (0,(1,(1,(0,(0,(1,(1,0))))))) => x66 + | (1,(1,(1,(0,(0,(1,(1,0))))))) => x67 + | (0,(0,(0,(1,(0,(1,(1,0))))))) => x68 + | (1,(0,(0,(1,(0,(1,(1,0))))))) => x69 + | (0,(1,(0,(1,(0,(1,(1,0))))))) => x6a + | (1,(1,(0,(1,(0,(1,(1,0))))))) => x6b + | (0,(0,(1,(1,(0,(1,(1,0))))))) => x6c + | (1,(0,(1,(1,(0,(1,(1,0))))))) => x6d + | (0,(1,(1,(1,(0,(1,(1,0))))))) => x6e + | (1,(1,(1,(1,(0,(1,(1,0))))))) => x6f + | (0,(0,(0,(0,(1,(1,(1,0))))))) => x70 + | (1,(0,(0,(0,(1,(1,(1,0))))))) => x71 + | (0,(1,(0,(0,(1,(1,(1,0))))))) => x72 + | (1,(1,(0,(0,(1,(1,(1,0))))))) => x73 + | (0,(0,(1,(0,(1,(1,(1,0))))))) => x74 + | (1,(0,(1,(0,(1,(1,(1,0))))))) => x75 + | (0,(1,(1,(0,(1,(1,(1,0))))))) => x76 + | (1,(1,(1,(0,(1,(1,(1,0))))))) => x77 + | (0,(0,(0,(1,(1,(1,(1,0))))))) => x78 + | (1,(0,(0,(1,(1,(1,(1,0))))))) => x79 + | (0,(1,(0,(1,(1,(1,(1,0))))))) => x7a + | (1,(1,(0,(1,(1,(1,(1,0))))))) => x7b + | (0,(0,(1,(1,(1,(1,(1,0))))))) => x7c + | (1,(0,(1,(1,(1,(1,(1,0))))))) => x7d + | (0,(1,(1,(1,(1,(1,(1,0))))))) => x7e + | (1,(1,(1,(1,(1,(1,(1,0))))))) => x7f + | (0,(0,(0,(0,(0,(0,(0,1))))))) => x80 + | (1,(0,(0,(0,(0,(0,(0,1))))))) => x81 + | (0,(1,(0,(0,(0,(0,(0,1))))))) => x82 + | (1,(1,(0,(0,(0,(0,(0,1))))))) => x83 + | (0,(0,(1,(0,(0,(0,(0,1))))))) => x84 + | (1,(0,(1,(0,(0,(0,(0,1))))))) => x85 + | (0,(1,(1,(0,(0,(0,(0,1))))))) => x86 + | (1,(1,(1,(0,(0,(0,(0,1))))))) => x87 + | (0,(0,(0,(1,(0,(0,(0,1))))))) => x88 + | (1,(0,(0,(1,(0,(0,(0,1))))))) => x89 + | (0,(1,(0,(1,(0,(0,(0,1))))))) => x8a + | (1,(1,(0,(1,(0,(0,(0,1))))))) => x8b + | (0,(0,(1,(1,(0,(0,(0,1))))))) => x8c + | (1,(0,(1,(1,(0,(0,(0,1))))))) => x8d + | (0,(1,(1,(1,(0,(0,(0,1))))))) => x8e + | (1,(1,(1,(1,(0,(0,(0,1))))))) => x8f + | (0,(0,(0,(0,(1,(0,(0,1))))))) => x90 + | (1,(0,(0,(0,(1,(0,(0,1))))))) => x91 + | (0,(1,(0,(0,(1,(0,(0,1))))))) => x92 + | (1,(1,(0,(0,(1,(0,(0,1))))))) => x93 + | (0,(0,(1,(0,(1,(0,(0,1))))))) => x94 + | (1,(0,(1,(0,(1,(0,(0,1))))))) => x95 + | (0,(1,(1,(0,(1,(0,(0,1))))))) => x96 + | (1,(1,(1,(0,(1,(0,(0,1))))))) => x97 + | (0,(0,(0,(1,(1,(0,(0,1))))))) => x98 + | (1,(0,(0,(1,(1,(0,(0,1))))))) => x99 + | (0,(1,(0,(1,(1,(0,(0,1))))))) => x9a + | (1,(1,(0,(1,(1,(0,(0,1))))))) => x9b + | (0,(0,(1,(1,(1,(0,(0,1))))))) => x9c + | (1,(0,(1,(1,(1,(0,(0,1))))))) => x9d + | (0,(1,(1,(1,(1,(0,(0,1))))))) => x9e + | (1,(1,(1,(1,(1,(0,(0,1))))))) => x9f + | (0,(0,(0,(0,(0,(1,(0,1))))))) => xa0 + | (1,(0,(0,(0,(0,(1,(0,1))))))) => xa1 + | (0,(1,(0,(0,(0,(1,(0,1))))))) => xa2 + | (1,(1,(0,(0,(0,(1,(0,1))))))) => xa3 + | (0,(0,(1,(0,(0,(1,(0,1))))))) => xa4 + | (1,(0,(1,(0,(0,(1,(0,1))))))) => xa5 + | (0,(1,(1,(0,(0,(1,(0,1))))))) => xa6 + | (1,(1,(1,(0,(0,(1,(0,1))))))) => xa7 + | (0,(0,(0,(1,(0,(1,(0,1))))))) => xa8 + | (1,(0,(0,(1,(0,(1,(0,1))))))) => xa9 + | (0,(1,(0,(1,(0,(1,(0,1))))))) => xaa + | (1,(1,(0,(1,(0,(1,(0,1))))))) => xab + | (0,(0,(1,(1,(0,(1,(0,1))))))) => xac + | (1,(0,(1,(1,(0,(1,(0,1))))))) => xad + | (0,(1,(1,(1,(0,(1,(0,1))))))) => xae + | (1,(1,(1,(1,(0,(1,(0,1))))))) => xaf + | (0,(0,(0,(0,(1,(1,(0,1))))))) => xb0 + | (1,(0,(0,(0,(1,(1,(0,1))))))) => xb1 + | (0,(1,(0,(0,(1,(1,(0,1))))))) => xb2 + | (1,(1,(0,(0,(1,(1,(0,1))))))) => xb3 + | (0,(0,(1,(0,(1,(1,(0,1))))))) => xb4 + | (1,(0,(1,(0,(1,(1,(0,1))))))) => xb5 + | (0,(1,(1,(0,(1,(1,(0,1))))))) => xb6 + | (1,(1,(1,(0,(1,(1,(0,1))))))) => xb7 + | (0,(0,(0,(1,(1,(1,(0,1))))))) => xb8 + | (1,(0,(0,(1,(1,(1,(0,1))))))) => xb9 + | (0,(1,(0,(1,(1,(1,(0,1))))))) => xba + | (1,(1,(0,(1,(1,(1,(0,1))))))) => xbb + | (0,(0,(1,(1,(1,(1,(0,1))))))) => xbc + | (1,(0,(1,(1,(1,(1,(0,1))))))) => xbd + | (0,(1,(1,(1,(1,(1,(0,1))))))) => xbe + | (1,(1,(1,(1,(1,(1,(0,1))))))) => xbf + | (0,(0,(0,(0,(0,(0,(1,1))))))) => xc0 + | (1,(0,(0,(0,(0,(0,(1,1))))))) => xc1 + | (0,(1,(0,(0,(0,(0,(1,1))))))) => xc2 + | (1,(1,(0,(0,(0,(0,(1,1))))))) => xc3 + | (0,(0,(1,(0,(0,(0,(1,1))))))) => xc4 + | (1,(0,(1,(0,(0,(0,(1,1))))))) => xc5 + | (0,(1,(1,(0,(0,(0,(1,1))))))) => xc6 + | (1,(1,(1,(0,(0,(0,(1,1))))))) => xc7 + | (0,(0,(0,(1,(0,(0,(1,1))))))) => xc8 + | (1,(0,(0,(1,(0,(0,(1,1))))))) => xc9 + | (0,(1,(0,(1,(0,(0,(1,1))))))) => xca + | (1,(1,(0,(1,(0,(0,(1,1))))))) => xcb + | (0,(0,(1,(1,(0,(0,(1,1))))))) => xcc + | (1,(0,(1,(1,(0,(0,(1,1))))))) => xcd + | (0,(1,(1,(1,(0,(0,(1,1))))))) => xce + | (1,(1,(1,(1,(0,(0,(1,1))))))) => xcf + | (0,(0,(0,(0,(1,(0,(1,1))))))) => xd0 + | (1,(0,(0,(0,(1,(0,(1,1))))))) => xd1 + | (0,(1,(0,(0,(1,(0,(1,1))))))) => xd2 + | (1,(1,(0,(0,(1,(0,(1,1))))))) => xd3 + | (0,(0,(1,(0,(1,(0,(1,1))))))) => xd4 + | (1,(0,(1,(0,(1,(0,(1,1))))))) => xd5 + | (0,(1,(1,(0,(1,(0,(1,1))))))) => xd6 + | (1,(1,(1,(0,(1,(0,(1,1))))))) => xd7 + | (0,(0,(0,(1,(1,(0,(1,1))))))) => xd8 + | (1,(0,(0,(1,(1,(0,(1,1))))))) => xd9 + | (0,(1,(0,(1,(1,(0,(1,1))))))) => xda + | (1,(1,(0,(1,(1,(0,(1,1))))))) => xdb + | (0,(0,(1,(1,(1,(0,(1,1))))))) => xdc + | (1,(0,(1,(1,(1,(0,(1,1))))))) => xdd + | (0,(1,(1,(1,(1,(0,(1,1))))))) => xde + | (1,(1,(1,(1,(1,(0,(1,1))))))) => xdf + | (0,(0,(0,(0,(0,(1,(1,1))))))) => xe0 + | (1,(0,(0,(0,(0,(1,(1,1))))))) => xe1 + | (0,(1,(0,(0,(0,(1,(1,1))))))) => xe2 + | (1,(1,(0,(0,(0,(1,(1,1))))))) => xe3 + | (0,(0,(1,(0,(0,(1,(1,1))))))) => xe4 + | (1,(0,(1,(0,(0,(1,(1,1))))))) => xe5 + | (0,(1,(1,(0,(0,(1,(1,1))))))) => xe6 + | (1,(1,(1,(0,(0,(1,(1,1))))))) => xe7 + | (0,(0,(0,(1,(0,(1,(1,1))))))) => xe8 + | (1,(0,(0,(1,(0,(1,(1,1))))))) => xe9 + | (0,(1,(0,(1,(0,(1,(1,1))))))) => xea + | (1,(1,(0,(1,(0,(1,(1,1))))))) => xeb + | (0,(0,(1,(1,(0,(1,(1,1))))))) => xec + | (1,(0,(1,(1,(0,(1,(1,1))))))) => xed + | (0,(1,(1,(1,(0,(1,(1,1))))))) => xee + | (1,(1,(1,(1,(0,(1,(1,1))))))) => xef + | (0,(0,(0,(0,(1,(1,(1,1))))))) => xf0 + | (1,(0,(0,(0,(1,(1,(1,1))))))) => xf1 + | (0,(1,(0,(0,(1,(1,(1,1))))))) => xf2 + | (1,(1,(0,(0,(1,(1,(1,1))))))) => xf3 + | (0,(0,(1,(0,(1,(1,(1,1))))))) => xf4 + | (1,(0,(1,(0,(1,(1,(1,1))))))) => xf5 + | (0,(1,(1,(0,(1,(1,(1,1))))))) => xf6 + | (1,(1,(1,(0,(1,(1,(1,1))))))) => xf7 + | (0,(0,(0,(1,(1,(1,(1,1))))))) => xf8 + | (1,(0,(0,(1,(1,(1,(1,1))))))) => xf9 + | (0,(1,(0,(1,(1,(1,(1,1))))))) => xfa + | (1,(1,(0,(1,(1,(1,(1,1))))))) => xfb + | (0,(0,(1,(1,(1,(1,(1,1))))))) => xfc + | (1,(0,(1,(1,(1,(1,(1,1))))))) => xfd + | (0,(1,(1,(1,(1,(1,(1,1))))))) => xfe + | (1,(1,(1,(1,(1,(1,(1,1))))))) => xff end. -Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool +Definition to_bits (b : byte) : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) := match b with - | x00 => (0,0,0,0,0,0,0,0) - | x01 => (1,0,0,0,0,0,0,0) - | x02 => (0,1,0,0,0,0,0,0) - | x03 => (1,1,0,0,0,0,0,0) - | x04 => (0,0,1,0,0,0,0,0) - | x05 => (1,0,1,0,0,0,0,0) - | x06 => (0,1,1,0,0,0,0,0) - | x07 => (1,1,1,0,0,0,0,0) - | x08 => (0,0,0,1,0,0,0,0) - | x09 => (1,0,0,1,0,0,0,0) - | x0a => (0,1,0,1,0,0,0,0) - | x0b => (1,1,0,1,0,0,0,0) - | x0c => (0,0,1,1,0,0,0,0) - | x0d => (1,0,1,1,0,0,0,0) - | x0e => (0,1,1,1,0,0,0,0) - | x0f => (1,1,1,1,0,0,0,0) - | x10 => (0,0,0,0,1,0,0,0) - | x11 => (1,0,0,0,1,0,0,0) - | x12 => (0,1,0,0,1,0,0,0) - | x13 => (1,1,0,0,1,0,0,0) - | x14 => (0,0,1,0,1,0,0,0) - | x15 => (1,0,1,0,1,0,0,0) - | x16 => (0,1,1,0,1,0,0,0) - | x17 => (1,1,1,0,1,0,0,0) - | x18 => (0,0,0,1,1,0,0,0) - | x19 => (1,0,0,1,1,0,0,0) - | x1a => (0,1,0,1,1,0,0,0) - | x1b => (1,1,0,1,1,0,0,0) - | x1c => (0,0,1,1,1,0,0,0) - | x1d => (1,0,1,1,1,0,0,0) - | x1e => (0,1,1,1,1,0,0,0) - | x1f => (1,1,1,1,1,0,0,0) - | x20 => (0,0,0,0,0,1,0,0) - | x21 => (1,0,0,0,0,1,0,0) - | x22 => (0,1,0,0,0,1,0,0) - | x23 => (1,1,0,0,0,1,0,0) - | x24 => (0,0,1,0,0,1,0,0) - | x25 => (1,0,1,0,0,1,0,0) - | x26 => (0,1,1,0,0,1,0,0) - | x27 => (1,1,1,0,0,1,0,0) - | x28 => (0,0,0,1,0,1,0,0) - | x29 => (1,0,0,1,0,1,0,0) - | x2a => (0,1,0,1,0,1,0,0) - | x2b => (1,1,0,1,0,1,0,0) - | x2c => (0,0,1,1,0,1,0,0) - | x2d => (1,0,1,1,0,1,0,0) - | x2e => (0,1,1,1,0,1,0,0) - | x2f => (1,1,1,1,0,1,0,0) - | x30 => (0,0,0,0,1,1,0,0) - | x31 => (1,0,0,0,1,1,0,0) - | x32 => (0,1,0,0,1,1,0,0) - | x33 => (1,1,0,0,1,1,0,0) - | x34 => (0,0,1,0,1,1,0,0) - | x35 => (1,0,1,0,1,1,0,0) - | x36 => (0,1,1,0,1,1,0,0) - | x37 => (1,1,1,0,1,1,0,0) - | x38 => (0,0,0,1,1,1,0,0) - | x39 => (1,0,0,1,1,1,0,0) - | x3a => (0,1,0,1,1,1,0,0) - | x3b => (1,1,0,1,1,1,0,0) - | x3c => (0,0,1,1,1,1,0,0) - | x3d => (1,0,1,1,1,1,0,0) - | x3e => (0,1,1,1,1,1,0,0) - | x3f => (1,1,1,1,1,1,0,0) - | x40 => (0,0,0,0,0,0,1,0) - | x41 => (1,0,0,0,0,0,1,0) - | x42 => (0,1,0,0,0,0,1,0) - | x43 => (1,1,0,0,0,0,1,0) - | x44 => (0,0,1,0,0,0,1,0) - | x45 => (1,0,1,0,0,0,1,0) - | x46 => (0,1,1,0,0,0,1,0) - | x47 => (1,1,1,0,0,0,1,0) - | x48 => (0,0,0,1,0,0,1,0) - | x49 => (1,0,0,1,0,0,1,0) - | x4a => (0,1,0,1,0,0,1,0) - | x4b => (1,1,0,1,0,0,1,0) - | x4c => (0,0,1,1,0,0,1,0) - | x4d => (1,0,1,1,0,0,1,0) - | x4e => (0,1,1,1,0,0,1,0) - | x4f => (1,1,1,1,0,0,1,0) - | x50 => (0,0,0,0,1,0,1,0) - | x51 => (1,0,0,0,1,0,1,0) - | x52 => (0,1,0,0,1,0,1,0) - | x53 => (1,1,0,0,1,0,1,0) - | x54 => (0,0,1,0,1,0,1,0) - | x55 => (1,0,1,0,1,0,1,0) - | x56 => (0,1,1,0,1,0,1,0) - | x57 => (1,1,1,0,1,0,1,0) - | x58 => (0,0,0,1,1,0,1,0) - | x59 => (1,0,0,1,1,0,1,0) - | x5a => (0,1,0,1,1,0,1,0) - | x5b => (1,1,0,1,1,0,1,0) - | x5c => (0,0,1,1,1,0,1,0) - | x5d => (1,0,1,1,1,0,1,0) - | x5e => (0,1,1,1,1,0,1,0) - | x5f => (1,1,1,1,1,0,1,0) - | x60 => (0,0,0,0,0,1,1,0) - | x61 => (1,0,0,0,0,1,1,0) - | x62 => (0,1,0,0,0,1,1,0) - | x63 => (1,1,0,0,0,1,1,0) - | x64 => (0,0,1,0,0,1,1,0) - | x65 => (1,0,1,0,0,1,1,0) - | x66 => (0,1,1,0,0,1,1,0) - | x67 => (1,1,1,0,0,1,1,0) - | x68 => (0,0,0,1,0,1,1,0) - | x69 => (1,0,0,1,0,1,1,0) - | x6a => (0,1,0,1,0,1,1,0) - | x6b => (1,1,0,1,0,1,1,0) - | x6c => (0,0,1,1,0,1,1,0) - | x6d => (1,0,1,1,0,1,1,0) - | x6e => (0,1,1,1,0,1,1,0) - | x6f => (1,1,1,1,0,1,1,0) - | x70 => (0,0,0,0,1,1,1,0) - | x71 => (1,0,0,0,1,1,1,0) - | x72 => (0,1,0,0,1,1,1,0) - | x73 => (1,1,0,0,1,1,1,0) - | x74 => (0,0,1,0,1,1,1,0) - | x75 => (1,0,1,0,1,1,1,0) - | x76 => (0,1,1,0,1,1,1,0) - | x77 => (1,1,1,0,1,1,1,0) - | x78 => (0,0,0,1,1,1,1,0) - | x79 => (1,0,0,1,1,1,1,0) - | x7a => (0,1,0,1,1,1,1,0) - | x7b => (1,1,0,1,1,1,1,0) - | x7c => (0,0,1,1,1,1,1,0) - | x7d => (1,0,1,1,1,1,1,0) - | x7e => (0,1,1,1,1,1,1,0) - | x7f => (1,1,1,1,1,1,1,0) - | x80 => (0,0,0,0,0,0,0,1) - | x81 => (1,0,0,0,0,0,0,1) - | x82 => (0,1,0,0,0,0,0,1) - | x83 => (1,1,0,0,0,0,0,1) - | x84 => (0,0,1,0,0,0,0,1) - | x85 => (1,0,1,0,0,0,0,1) - | x86 => (0,1,1,0,0,0,0,1) - | x87 => (1,1,1,0,0,0,0,1) - | x88 => (0,0,0,1,0,0,0,1) - | x89 => (1,0,0,1,0,0,0,1) - | x8a => (0,1,0,1,0,0,0,1) - | x8b => (1,1,0,1,0,0,0,1) - | x8c => (0,0,1,1,0,0,0,1) - | x8d => (1,0,1,1,0,0,0,1) - | x8e => (0,1,1,1,0,0,0,1) - | x8f => (1,1,1,1,0,0,0,1) - | x90 => (0,0,0,0,1,0,0,1) - | x91 => (1,0,0,0,1,0,0,1) - | x92 => (0,1,0,0,1,0,0,1) - | x93 => (1,1,0,0,1,0,0,1) - | x94 => (0,0,1,0,1,0,0,1) - | x95 => (1,0,1,0,1,0,0,1) - | x96 => (0,1,1,0,1,0,0,1) - | x97 => (1,1,1,0,1,0,0,1) - | x98 => (0,0,0,1,1,0,0,1) - | x99 => (1,0,0,1,1,0,0,1) - | x9a => (0,1,0,1,1,0,0,1) - | x9b => (1,1,0,1,1,0,0,1) - | x9c => (0,0,1,1,1,0,0,1) - | x9d => (1,0,1,1,1,0,0,1) - | x9e => (0,1,1,1,1,0,0,1) - | x9f => (1,1,1,1,1,0,0,1) - | xa0 => (0,0,0,0,0,1,0,1) - | xa1 => (1,0,0,0,0,1,0,1) - | xa2 => (0,1,0,0,0,1,0,1) - | xa3 => (1,1,0,0,0,1,0,1) - | xa4 => (0,0,1,0,0,1,0,1) - | xa5 => (1,0,1,0,0,1,0,1) - | xa6 => (0,1,1,0,0,1,0,1) - | xa7 => (1,1,1,0,0,1,0,1) - | xa8 => (0,0,0,1,0,1,0,1) - | xa9 => (1,0,0,1,0,1,0,1) - | xaa => (0,1,0,1,0,1,0,1) - | xab => (1,1,0,1,0,1,0,1) - | xac => (0,0,1,1,0,1,0,1) - | xad => (1,0,1,1,0,1,0,1) - | xae => (0,1,1,1,0,1,0,1) - | xaf => (1,1,1,1,0,1,0,1) - | xb0 => (0,0,0,0,1,1,0,1) - | xb1 => (1,0,0,0,1,1,0,1) - | xb2 => (0,1,0,0,1,1,0,1) - | xb3 => (1,1,0,0,1,1,0,1) - | xb4 => (0,0,1,0,1,1,0,1) - | xb5 => (1,0,1,0,1,1,0,1) - | xb6 => (0,1,1,0,1,1,0,1) - | xb7 => (1,1,1,0,1,1,0,1) - | xb8 => (0,0,0,1,1,1,0,1) - | xb9 => (1,0,0,1,1,1,0,1) - | xba => (0,1,0,1,1,1,0,1) - | xbb => (1,1,0,1,1,1,0,1) - | xbc => (0,0,1,1,1,1,0,1) - | xbd => (1,0,1,1,1,1,0,1) - | xbe => (0,1,1,1,1,1,0,1) - | xbf => (1,1,1,1,1,1,0,1) - | xc0 => (0,0,0,0,0,0,1,1) - | xc1 => (1,0,0,0,0,0,1,1) - | xc2 => (0,1,0,0,0,0,1,1) - | xc3 => (1,1,0,0,0,0,1,1) - | xc4 => (0,0,1,0,0,0,1,1) - | xc5 => (1,0,1,0,0,0,1,1) - | xc6 => (0,1,1,0,0,0,1,1) - | xc7 => (1,1,1,0,0,0,1,1) - | xc8 => (0,0,0,1,0,0,1,1) - | xc9 => (1,0,0,1,0,0,1,1) - | xca => (0,1,0,1,0,0,1,1) - | xcb => (1,1,0,1,0,0,1,1) - | xcc => (0,0,1,1,0,0,1,1) - | xcd => (1,0,1,1,0,0,1,1) - | xce => (0,1,1,1,0,0,1,1) - | xcf => (1,1,1,1,0,0,1,1) - | xd0 => (0,0,0,0,1,0,1,1) - | xd1 => (1,0,0,0,1,0,1,1) - | xd2 => (0,1,0,0,1,0,1,1) - | xd3 => (1,1,0,0,1,0,1,1) - | xd4 => (0,0,1,0,1,0,1,1) - | xd5 => (1,0,1,0,1,0,1,1) - | xd6 => (0,1,1,0,1,0,1,1) - | xd7 => (1,1,1,0,1,0,1,1) - | xd8 => (0,0,0,1,1,0,1,1) - | xd9 => (1,0,0,1,1,0,1,1) - | xda => (0,1,0,1,1,0,1,1) - | xdb => (1,1,0,1,1,0,1,1) - | xdc => (0,0,1,1,1,0,1,1) - | xdd => (1,0,1,1,1,0,1,1) - | xde => (0,1,1,1,1,0,1,1) - | xdf => (1,1,1,1,1,0,1,1) - | xe0 => (0,0,0,0,0,1,1,1) - | xe1 => (1,0,0,0,0,1,1,1) - | xe2 => (0,1,0,0,0,1,1,1) - | xe3 => (1,1,0,0,0,1,1,1) - | xe4 => (0,0,1,0,0,1,1,1) - | xe5 => (1,0,1,0,0,1,1,1) - | xe6 => (0,1,1,0,0,1,1,1) - | xe7 => (1,1,1,0,0,1,1,1) - | xe8 => (0,0,0,1,0,1,1,1) - | xe9 => (1,0,0,1,0,1,1,1) - | xea => (0,1,0,1,0,1,1,1) - | xeb => (1,1,0,1,0,1,1,1) - | xec => (0,0,1,1,0,1,1,1) - | xed => (1,0,1,1,0,1,1,1) - | xee => (0,1,1,1,0,1,1,1) - | xef => (1,1,1,1,0,1,1,1) - | xf0 => (0,0,0,0,1,1,1,1) - | xf1 => (1,0,0,0,1,1,1,1) - | xf2 => (0,1,0,0,1,1,1,1) - | xf3 => (1,1,0,0,1,1,1,1) - | xf4 => (0,0,1,0,1,1,1,1) - | xf5 => (1,0,1,0,1,1,1,1) - | xf6 => (0,1,1,0,1,1,1,1) - | xf7 => (1,1,1,0,1,1,1,1) - | xf8 => (0,0,0,1,1,1,1,1) - | xf9 => (1,0,0,1,1,1,1,1) - | xfa => (0,1,0,1,1,1,1,1) - | xfb => (1,1,0,1,1,1,1,1) - | xfc => (0,0,1,1,1,1,1,1) - | xfd => (1,0,1,1,1,1,1,1) - | xfe => (0,1,1,1,1,1,1,1) - | xff => (1,1,1,1,1,1,1,1) + | x00 => (0,(0,(0,(0,(0,(0,(0,0))))))) + | x01 => (1,(0,(0,(0,(0,(0,(0,0))))))) + | x02 => (0,(1,(0,(0,(0,(0,(0,0))))))) + | x03 => (1,(1,(0,(0,(0,(0,(0,0))))))) + | x04 => (0,(0,(1,(0,(0,(0,(0,0))))))) + | x05 => (1,(0,(1,(0,(0,(0,(0,0))))))) + | x06 => (0,(1,(1,(0,(0,(0,(0,0))))))) + | x07 => (1,(1,(1,(0,(0,(0,(0,0))))))) + | x08 => (0,(0,(0,(1,(0,(0,(0,0))))))) + | x09 => (1,(0,(0,(1,(0,(0,(0,0))))))) + | x0a => (0,(1,(0,(1,(0,(0,(0,0))))))) + | x0b => (1,(1,(0,(1,(0,(0,(0,0))))))) + | x0c => (0,(0,(1,(1,(0,(0,(0,0))))))) + | x0d => (1,(0,(1,(1,(0,(0,(0,0))))))) + | x0e => (0,(1,(1,(1,(0,(0,(0,0))))))) + | x0f => (1,(1,(1,(1,(0,(0,(0,0))))))) + | x10 => (0,(0,(0,(0,(1,(0,(0,0))))))) + | x11 => (1,(0,(0,(0,(1,(0,(0,0))))))) + | x12 => (0,(1,(0,(0,(1,(0,(0,0))))))) + | x13 => (1,(1,(0,(0,(1,(0,(0,0))))))) + | x14 => (0,(0,(1,(0,(1,(0,(0,0))))))) + | x15 => (1,(0,(1,(0,(1,(0,(0,0))))))) + | x16 => (0,(1,(1,(0,(1,(0,(0,0))))))) + | x17 => (1,(1,(1,(0,(1,(0,(0,0))))))) + | x18 => (0,(0,(0,(1,(1,(0,(0,0))))))) + | x19 => (1,(0,(0,(1,(1,(0,(0,0))))))) + | x1a => (0,(1,(0,(1,(1,(0,(0,0))))))) + | x1b => (1,(1,(0,(1,(1,(0,(0,0))))))) + | x1c => (0,(0,(1,(1,(1,(0,(0,0))))))) + | x1d => (1,(0,(1,(1,(1,(0,(0,0))))))) + | x1e => (0,(1,(1,(1,(1,(0,(0,0))))))) + | x1f => (1,(1,(1,(1,(1,(0,(0,0))))))) + | x20 => (0,(0,(0,(0,(0,(1,(0,0))))))) + | x21 => (1,(0,(0,(0,(0,(1,(0,0))))))) + | x22 => (0,(1,(0,(0,(0,(1,(0,0))))))) + | x23 => (1,(1,(0,(0,(0,(1,(0,0))))))) + | x24 => (0,(0,(1,(0,(0,(1,(0,0))))))) + | x25 => (1,(0,(1,(0,(0,(1,(0,0))))))) + | x26 => (0,(1,(1,(0,(0,(1,(0,0))))))) + | x27 => (1,(1,(1,(0,(0,(1,(0,0))))))) + | x28 => (0,(0,(0,(1,(0,(1,(0,0))))))) + | x29 => (1,(0,(0,(1,(0,(1,(0,0))))))) + | x2a => (0,(1,(0,(1,(0,(1,(0,0))))))) + | x2b => (1,(1,(0,(1,(0,(1,(0,0))))))) + | x2c => (0,(0,(1,(1,(0,(1,(0,0))))))) + | x2d => (1,(0,(1,(1,(0,(1,(0,0))))))) + | x2e => (0,(1,(1,(1,(0,(1,(0,0))))))) + | x2f => (1,(1,(1,(1,(0,(1,(0,0))))))) + | x30 => (0,(0,(0,(0,(1,(1,(0,0))))))) + | x31 => (1,(0,(0,(0,(1,(1,(0,0))))))) + | x32 => (0,(1,(0,(0,(1,(1,(0,0))))))) + | x33 => (1,(1,(0,(0,(1,(1,(0,0))))))) + | x34 => (0,(0,(1,(0,(1,(1,(0,0))))))) + | x35 => (1,(0,(1,(0,(1,(1,(0,0))))))) + | x36 => (0,(1,(1,(0,(1,(1,(0,0))))))) + | x37 => (1,(1,(1,(0,(1,(1,(0,0))))))) + | x38 => (0,(0,(0,(1,(1,(1,(0,0))))))) + | x39 => (1,(0,(0,(1,(1,(1,(0,0))))))) + | x3a => (0,(1,(0,(1,(1,(1,(0,0))))))) + | x3b => (1,(1,(0,(1,(1,(1,(0,0))))))) + | x3c => (0,(0,(1,(1,(1,(1,(0,0))))))) + | x3d => (1,(0,(1,(1,(1,(1,(0,0))))))) + | x3e => (0,(1,(1,(1,(1,(1,(0,0))))))) + | x3f => (1,(1,(1,(1,(1,(1,(0,0))))))) + | x40 => (0,(0,(0,(0,(0,(0,(1,0))))))) + | x41 => (1,(0,(0,(0,(0,(0,(1,0))))))) + | x42 => (0,(1,(0,(0,(0,(0,(1,0))))))) + | x43 => (1,(1,(0,(0,(0,(0,(1,0))))))) + | x44 => (0,(0,(1,(0,(0,(0,(1,0))))))) + | x45 => (1,(0,(1,(0,(0,(0,(1,0))))))) + | x46 => (0,(1,(1,(0,(0,(0,(1,0))))))) + | x47 => (1,(1,(1,(0,(0,(0,(1,0))))))) + | x48 => (0,(0,(0,(1,(0,(0,(1,0))))))) + | x49 => (1,(0,(0,(1,(0,(0,(1,0))))))) + | x4a => (0,(1,(0,(1,(0,(0,(1,0))))))) + | x4b => (1,(1,(0,(1,(0,(0,(1,0))))))) + | x4c => (0,(0,(1,(1,(0,(0,(1,0))))))) + | x4d => (1,(0,(1,(1,(0,(0,(1,0))))))) + | x4e => (0,(1,(1,(1,(0,(0,(1,0))))))) + | x4f => (1,(1,(1,(1,(0,(0,(1,0))))))) + | x50 => (0,(0,(0,(0,(1,(0,(1,0))))))) + | x51 => (1,(0,(0,(0,(1,(0,(1,0))))))) + | x52 => (0,(1,(0,(0,(1,(0,(1,0))))))) + | x53 => (1,(1,(0,(0,(1,(0,(1,0))))))) + | x54 => (0,(0,(1,(0,(1,(0,(1,0))))))) + | x55 => (1,(0,(1,(0,(1,(0,(1,0))))))) + | x56 => (0,(1,(1,(0,(1,(0,(1,0))))))) + | x57 => (1,(1,(1,(0,(1,(0,(1,0))))))) + | x58 => (0,(0,(0,(1,(1,(0,(1,0))))))) + | x59 => (1,(0,(0,(1,(1,(0,(1,0))))))) + | x5a => (0,(1,(0,(1,(1,(0,(1,0))))))) + | x5b => (1,(1,(0,(1,(1,(0,(1,0))))))) + | x5c => (0,(0,(1,(1,(1,(0,(1,0))))))) + | x5d => (1,(0,(1,(1,(1,(0,(1,0))))))) + | x5e => (0,(1,(1,(1,(1,(0,(1,0))))))) + | x5f => (1,(1,(1,(1,(1,(0,(1,0))))))) + | x60 => (0,(0,(0,(0,(0,(1,(1,0))))))) + | x61 => (1,(0,(0,(0,(0,(1,(1,0))))))) + | x62 => (0,(1,(0,(0,(0,(1,(1,0))))))) + | x63 => (1,(1,(0,(0,(0,(1,(1,0))))))) + | x64 => (0,(0,(1,(0,(0,(1,(1,0))))))) + | x65 => (1,(0,(1,(0,(0,(1,(1,0))))))) + | x66 => (0,(1,(1,(0,(0,(1,(1,0))))))) + | x67 => (1,(1,(1,(0,(0,(1,(1,0))))))) + | x68 => (0,(0,(0,(1,(0,(1,(1,0))))))) + | x69 => (1,(0,(0,(1,(0,(1,(1,0))))))) + | x6a => (0,(1,(0,(1,(0,(1,(1,0))))))) + | x6b => (1,(1,(0,(1,(0,(1,(1,0))))))) + | x6c => (0,(0,(1,(1,(0,(1,(1,0))))))) + | x6d => (1,(0,(1,(1,(0,(1,(1,0))))))) + | x6e => (0,(1,(1,(1,(0,(1,(1,0))))))) + | x6f => (1,(1,(1,(1,(0,(1,(1,0))))))) + | x70 => (0,(0,(0,(0,(1,(1,(1,0))))))) + | x71 => (1,(0,(0,(0,(1,(1,(1,0))))))) + | x72 => (0,(1,(0,(0,(1,(1,(1,0))))))) + | x73 => (1,(1,(0,(0,(1,(1,(1,0))))))) + | x74 => (0,(0,(1,(0,(1,(1,(1,0))))))) + | x75 => (1,(0,(1,(0,(1,(1,(1,0))))))) + | x76 => (0,(1,(1,(0,(1,(1,(1,0))))))) + | x77 => (1,(1,(1,(0,(1,(1,(1,0))))))) + | x78 => (0,(0,(0,(1,(1,(1,(1,0))))))) + | x79 => (1,(0,(0,(1,(1,(1,(1,0))))))) + | x7a => (0,(1,(0,(1,(1,(1,(1,0))))))) + | x7b => (1,(1,(0,(1,(1,(1,(1,0))))))) + | x7c => (0,(0,(1,(1,(1,(1,(1,0))))))) + | x7d => (1,(0,(1,(1,(1,(1,(1,0))))))) + | x7e => (0,(1,(1,(1,(1,(1,(1,0))))))) + | x7f => (1,(1,(1,(1,(1,(1,(1,0))))))) + | x80 => (0,(0,(0,(0,(0,(0,(0,1))))))) + | x81 => (1,(0,(0,(0,(0,(0,(0,1))))))) + | x82 => (0,(1,(0,(0,(0,(0,(0,1))))))) + | x83 => (1,(1,(0,(0,(0,(0,(0,1))))))) + | x84 => (0,(0,(1,(0,(0,(0,(0,1))))))) + | x85 => (1,(0,(1,(0,(0,(0,(0,1))))))) + | x86 => (0,(1,(1,(0,(0,(0,(0,1))))))) + | x87 => (1,(1,(1,(0,(0,(0,(0,1))))))) + | x88 => (0,(0,(0,(1,(0,(0,(0,1))))))) + | x89 => (1,(0,(0,(1,(0,(0,(0,1))))))) + | x8a => (0,(1,(0,(1,(0,(0,(0,1))))))) + | x8b => (1,(1,(0,(1,(0,(0,(0,1))))))) + | x8c => (0,(0,(1,(1,(0,(0,(0,1))))))) + | x8d => (1,(0,(1,(1,(0,(0,(0,1))))))) + | x8e => (0,(1,(1,(1,(0,(0,(0,1))))))) + | x8f => (1,(1,(1,(1,(0,(0,(0,1))))))) + | x90 => (0,(0,(0,(0,(1,(0,(0,1))))))) + | x91 => (1,(0,(0,(0,(1,(0,(0,1))))))) + | x92 => (0,(1,(0,(0,(1,(0,(0,1))))))) + | x93 => (1,(1,(0,(0,(1,(0,(0,1))))))) + | x94 => (0,(0,(1,(0,(1,(0,(0,1))))))) + | x95 => (1,(0,(1,(0,(1,(0,(0,1))))))) + | x96 => (0,(1,(1,(0,(1,(0,(0,1))))))) + | x97 => (1,(1,(1,(0,(1,(0,(0,1))))))) + | x98 => (0,(0,(0,(1,(1,(0,(0,1))))))) + | x99 => (1,(0,(0,(1,(1,(0,(0,1))))))) + | x9a => (0,(1,(0,(1,(1,(0,(0,1))))))) + | x9b => (1,(1,(0,(1,(1,(0,(0,1))))))) + | x9c => (0,(0,(1,(1,(1,(0,(0,1))))))) + | x9d => (1,(0,(1,(1,(1,(0,(0,1))))))) + | x9e => (0,(1,(1,(1,(1,(0,(0,1))))))) + | x9f => (1,(1,(1,(1,(1,(0,(0,1))))))) + | xa0 => (0,(0,(0,(0,(0,(1,(0,1))))))) + | xa1 => (1,(0,(0,(0,(0,(1,(0,1))))))) + | xa2 => (0,(1,(0,(0,(0,(1,(0,1))))))) + | xa3 => (1,(1,(0,(0,(0,(1,(0,1))))))) + | xa4 => (0,(0,(1,(0,(0,(1,(0,1))))))) + | xa5 => (1,(0,(1,(0,(0,(1,(0,1))))))) + | xa6 => (0,(1,(1,(0,(0,(1,(0,1))))))) + | xa7 => (1,(1,(1,(0,(0,(1,(0,1))))))) + | xa8 => (0,(0,(0,(1,(0,(1,(0,1))))))) + | xa9 => (1,(0,(0,(1,(0,(1,(0,1))))))) + | xaa => (0,(1,(0,(1,(0,(1,(0,1))))))) + | xab => (1,(1,(0,(1,(0,(1,(0,1))))))) + | xac => (0,(0,(1,(1,(0,(1,(0,1))))))) + | xad => (1,(0,(1,(1,(0,(1,(0,1))))))) + | xae => (0,(1,(1,(1,(0,(1,(0,1))))))) + | xaf => (1,(1,(1,(1,(0,(1,(0,1))))))) + | xb0 => (0,(0,(0,(0,(1,(1,(0,1))))))) + | xb1 => (1,(0,(0,(0,(1,(1,(0,1))))))) + | xb2 => (0,(1,(0,(0,(1,(1,(0,1))))))) + | xb3 => (1,(1,(0,(0,(1,(1,(0,1))))))) + | xb4 => (0,(0,(1,(0,(1,(1,(0,1))))))) + | xb5 => (1,(0,(1,(0,(1,(1,(0,1))))))) + | xb6 => (0,(1,(1,(0,(1,(1,(0,1))))))) + | xb7 => (1,(1,(1,(0,(1,(1,(0,1))))))) + | xb8 => (0,(0,(0,(1,(1,(1,(0,1))))))) + | xb9 => (1,(0,(0,(1,(1,(1,(0,1))))))) + | xba => (0,(1,(0,(1,(1,(1,(0,1))))))) + | xbb => (1,(1,(0,(1,(1,(1,(0,1))))))) + | xbc => (0,(0,(1,(1,(1,(1,(0,1))))))) + | xbd => (1,(0,(1,(1,(1,(1,(0,1))))))) + | xbe => (0,(1,(1,(1,(1,(1,(0,1))))))) + | xbf => (1,(1,(1,(1,(1,(1,(0,1))))))) + | xc0 => (0,(0,(0,(0,(0,(0,(1,1))))))) + | xc1 => (1,(0,(0,(0,(0,(0,(1,1))))))) + | xc2 => (0,(1,(0,(0,(0,(0,(1,1))))))) + | xc3 => (1,(1,(0,(0,(0,(0,(1,1))))))) + | xc4 => (0,(0,(1,(0,(0,(0,(1,1))))))) + | xc5 => (1,(0,(1,(0,(0,(0,(1,1))))))) + | xc6 => (0,(1,(1,(0,(0,(0,(1,1))))))) + | xc7 => (1,(1,(1,(0,(0,(0,(1,1))))))) + | xc8 => (0,(0,(0,(1,(0,(0,(1,1))))))) + | xc9 => (1,(0,(0,(1,(0,(0,(1,1))))))) + | xca => (0,(1,(0,(1,(0,(0,(1,1))))))) + | xcb => (1,(1,(0,(1,(0,(0,(1,1))))))) + | xcc => (0,(0,(1,(1,(0,(0,(1,1))))))) + | xcd => (1,(0,(1,(1,(0,(0,(1,1))))))) + | xce => (0,(1,(1,(1,(0,(0,(1,1))))))) + | xcf => (1,(1,(1,(1,(0,(0,(1,1))))))) + | xd0 => (0,(0,(0,(0,(1,(0,(1,1))))))) + | xd1 => (1,(0,(0,(0,(1,(0,(1,1))))))) + | xd2 => (0,(1,(0,(0,(1,(0,(1,1))))))) + | xd3 => (1,(1,(0,(0,(1,(0,(1,1))))))) + | xd4 => (0,(0,(1,(0,(1,(0,(1,1))))))) + | xd5 => (1,(0,(1,(0,(1,(0,(1,1))))))) + | xd6 => (0,(1,(1,(0,(1,(0,(1,1))))))) + | xd7 => (1,(1,(1,(0,(1,(0,(1,1))))))) + | xd8 => (0,(0,(0,(1,(1,(0,(1,1))))))) + | xd9 => (1,(0,(0,(1,(1,(0,(1,1))))))) + | xda => (0,(1,(0,(1,(1,(0,(1,1))))))) + | xdb => (1,(1,(0,(1,(1,(0,(1,1))))))) + | xdc => (0,(0,(1,(1,(1,(0,(1,1))))))) + | xdd => (1,(0,(1,(1,(1,(0,(1,1))))))) + | xde => (0,(1,(1,(1,(1,(0,(1,1))))))) + | xdf => (1,(1,(1,(1,(1,(0,(1,1))))))) + | xe0 => (0,(0,(0,(0,(0,(1,(1,1))))))) + | xe1 => (1,(0,(0,(0,(0,(1,(1,1))))))) + | xe2 => (0,(1,(0,(0,(0,(1,(1,1))))))) + | xe3 => (1,(1,(0,(0,(0,(1,(1,1))))))) + | xe4 => (0,(0,(1,(0,(0,(1,(1,1))))))) + | xe5 => (1,(0,(1,(0,(0,(1,(1,1))))))) + | xe6 => (0,(1,(1,(0,(0,(1,(1,1))))))) + | xe7 => (1,(1,(1,(0,(0,(1,(1,1))))))) + | xe8 => (0,(0,(0,(1,(0,(1,(1,1))))))) + | xe9 => (1,(0,(0,(1,(0,(1,(1,1))))))) + | xea => (0,(1,(0,(1,(0,(1,(1,1))))))) + | xeb => (1,(1,(0,(1,(0,(1,(1,1))))))) + | xec => (0,(0,(1,(1,(0,(1,(1,1))))))) + | xed => (1,(0,(1,(1,(0,(1,(1,1))))))) + | xee => (0,(1,(1,(1,(0,(1,(1,1))))))) + | xef => (1,(1,(1,(1,(0,(1,(1,1))))))) + | xf0 => (0,(0,(0,(0,(1,(1,(1,1))))))) + | xf1 => (1,(0,(0,(0,(1,(1,(1,1))))))) + | xf2 => (0,(1,(0,(0,(1,(1,(1,1))))))) + | xf3 => (1,(1,(0,(0,(1,(1,(1,1))))))) + | xf4 => (0,(0,(1,(0,(1,(1,(1,1))))))) + | xf5 => (1,(0,(1,(0,(1,(1,(1,1))))))) + | xf6 => (0,(1,(1,(0,(1,(1,(1,1))))))) + | xf7 => (1,(1,(1,(0,(1,(1,(1,1))))))) + | xf8 => (0,(0,(0,(1,(1,(1,(1,1))))))) + | xf9 => (1,(0,(0,(1,(1,(1,(1,1))))))) + | xfa => (0,(1,(0,(1,(1,(1,(1,1))))))) + | xfb => (1,(1,(0,(1,(1,(1,(1,1))))))) + | xfc => (0,(0,(1,(1,(1,(1,(1,1))))))) + | xfd => (1,(0,(1,(1,(1,(1,(1,1))))))) + | xfe => (0,(1,(1,(1,(1,(1,(1,1))))))) + | xff => (1,(1,(1,(1,(1,(1,(1,1))))))) end. Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 131147ff8d..6a0c5f066e 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -190,12 +190,12 @@ Qed. *) Definition ascii_of_byte (b : byte) : ascii - := let '(b7, b6, b5, b4, b3, b2, b1, b0) := Byte.to_bits b in - Ascii b7 b6 b5 b4 b3 b2 b1 b0. + := let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := Byte.to_bits b in + Ascii b0 b1 b2 b3 b4 b5 b6 b7. Definition byte_of_ascii (a : ascii) : byte - := let (b7, b6, b5, b4, b3, b2, b1, b0) := a in - Byte.of_bits (b7, b6, b5, b4, b3, b2, b1, b0). + := let (b0, b1, b2, b3, b4, b5, b6, b7) := a in + Byte.of_bits (b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))). Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. Proof. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v index 4daa0b196c..2759ea60cb 100644 --- a/theories/Strings/Byte.v +++ b/theories/Strings/Byte.v @@ -16,8 +16,8 @@ Require Export Coq.Init.Byte. Local Set Implicit Arguments. Definition eqb (a b : byte) : bool - := let '(a7, a6, a5, a4, a3, a2, a1, a0) := to_bits a in - let '(b7, b6, b5, b4, b3, b2, b1, b0) := to_bits b in + := let '(a0, (a1, (a2, (a3, (a4, (a5, (a6, a7))))))) := to_bits a in + let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := to_bits b in (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 && Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool. -- cgit v1.2.3