Timings for Byte.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Strings/Byte.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Strings/Byte.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Coq.Arith.EqNat.
Require Import Coq.NArith.BinNat.
Require Import Coq.NArith.Nnat.
Require Export Coq.Init.Byte.
Local Set Implicit Arguments.
Definition eqb (a b : byte) : bool
:= 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.
Module Export ByteNotations.
Export ByteSyntaxNotations.
Infix "=?" := eqb (at level 70) : byte_scope.
Lemma byte_dec_lb x y : x = y -> eqb x y = true.
intro; subst y; destruct x; reflexivity.
Lemma byte_dec_bl x y (H : eqb x y = true) : x = y.
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.
Lemma eqb_false x y : eqb x y = false -> x <> y.
intros H H'; pose proof (byte_dec_lb H'); congruence.
Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y}
:= (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.
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.
Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x.
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.
Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x.
split; intro; subst; (apply of_to_nat || apply to_of_nat); assumption.
Lemma to_of_nat_option_map x : option_map to_nat (of_nat x) = if Nat.leb x 255 then Some x else None.
do 256 try destruct x as [|x]; reflexivity.
Lemma to_nat_bounded x : to_nat x <= 255.
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.
Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x.
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.
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.
Lemma to_of_N x y : of_N x = Some y -> to_N y = x.
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.
Lemma to_of_N_iff x y : of_N x = Some y <-> to_N y = x.
split; intro; subst; (apply of_to_N || apply to_of_N); assumption.
Lemma to_of_N_option_map x : option_map to_N (of_N x) = if N.leb x 255 then Some x else None.
cbv [of_N];
repeat match goal with
| [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x
end;
reflexivity.
Lemma to_N_bounded x : to_N x <= 255.
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.
Lemma of_N_None_iff x : of_N x = None <-> 255 < x.
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.
Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x).
Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x).
Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x).
destruct (of_N x) as [b|] eqn:H1.
rewrite to_of_N_iff in H1; subst.
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.
Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).
destruct (of_nat x) as [b|] eqn:H1.
rewrite to_of_nat_iff in H1; subst.
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.