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/Strings/Byte.v | 1425 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1425 insertions(+) create mode 100644 theories/Strings/Byte.v (limited to 'theories/Strings/Byte.v') 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. -- 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/Strings/Byte.v | 294 +++++------------------------------------------- 1 file changed, 28 insertions(+), 266 deletions(-) (limited to 'theories/Strings/Byte.v') 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/Byte.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'theories/Strings/Byte.v') 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/Strings/Byte.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Strings/Byte.v') 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