Byte.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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.
End ByteNotations.

Lemma byte_dec_lb x y : x = y -> eqb x y = true.x, y:byte
x = y -> (x =? y)%byte = true
Proof.x, y:byte
x = y -> (x =? y)%byte = true intro; subst y; destruct x; reflexivity. Defined.

Lemma byte_dec_bl x y (H : eqb x y = true) : x = y.x, y:byte
H:(x =? y)%byte = true
x = y
Proof.x, y:byte
H:(x =? y)%byte = true
x = y
  rewrite <- (of_bits_to_bits x), <- (of_bits_to_bits y).x, y:byte
H:(x =? y)%byte = true
of_bits (to_bits x) = of_bits (to_bits y)
  cbv [eqb] in H; revert H.x, y:byte
(let
 '(a0, (a1, (a2, (a3, (a4, (a5, (a6, a7))))))) :=
  to_bits x in
  let
  '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) :=
   to_bits y 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) = true ->
of_bits (to_bits x) = of_bits (to_bits y)
  generalize (to_bits x) (to_bits y); clear x y; intros x y H.x, y:(bool *
 (bool *
  (bool * (bool * (bool * (bool * (bool * bool)))))))%type
H:(let
 '(a0, (a1, (a2, (a3, (a4, (a5, (a6, a7))))))) :=
  x in
  let
  '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) :=
   y 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) = true
of_bits x = of_bits y
  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 : eqb x y = false -> x <> y.x, y:byte
(x =? y)%byte = false -> x <> y
Proof.x, y:byte
(x =? y)%byte = false -> x <> y intros H H'; pose proof (byte_dec_lb H'); congruence. Qed.

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.

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.x:byte
of_nat (to_nat x) = Some x
  Proof.x:byte
of_nat (to_nat x) = Some x destruct x; reflexivity. Qed.

  Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x.x:nat
y:byte
of_nat x = Some y -> to_nat y = x
  Proof.x:nat
y:byte
of_nat x = Some y -> to_nat y = x
    do 256 try destruct x as [|x]; cbv [of_nat]; intro.y:byte
H:Some "000"%byte = Some y
to_nat y = 0
y:byte
H:Some "001"%byte = Some y
to_nat y = 1
y:byte
H:Some "002"%byte = Some y
to_nat y = 2
y:byte
H:Some "003"%byte = Some y
to_nat y = 3
y:byte
H:Some "004"%byte = Some y
to_nat y = 4
y:byte
H:Some "005"%byte = Some y
to_nat y = 5
y:byte
H:Some "006"%byte = Some y
to_nat y = 6
y:byte
H:Some "007"%byte = Some y
to_nat y = 7
y:byte
H:Some "008"%byte = Some y
to_nat y = 8
y:byte
H:Some "009"%byte = Some y
to_nat y = 9
y:byte
H:Some "010"%byte = Some y
to_nat y = 10
y:byte
H:Some "011"%byte = Some y
to_nat y = 11
y:byte
H:Some "012"%byte = Some y
to_nat y = 12
y:byte
H:Some "013"%byte = Some y
to_nat y = 13
y:byte
H:Some "014"%byte = Some y
to_nat y = 14
y:byte
H:Some "015"%byte = Some y
to_nat y = 15
y:byte
H:Some "016"%byte = Some y
to_nat y = 16
y:byte
H:Some "017"%byte = Some y
to_nat y = 17
y:byte
H:Some "018"%byte = Some y
to_nat y = 18
y:byte
H:Some "019"%byte = Some y
to_nat y = 19
y:byte
H:Some "020"%byte = Some y
to_nat y = 20
y:byte
H:Some "021"%byte = Some y
to_nat y = 21
y:byte
H:Some "022"%byte = Some y
to_nat y = 22
y:byte
H:Some "023"%byte = Some y
to_nat y = 23
y:byte
H:Some "024"%byte = Some y
to_nat y = 24
y:byte
H:Some "025"%byte = Some y
to_nat y = 25
y:byte
H:Some "026"%byte = Some y
to_nat y = 26
y:byte
H:Some "027"%byte = Some y
to_nat y = 27
y:byte
H:Some "028"%byte = Some y
to_nat y = 28
y:byte
H:Some "029"%byte = Some y
to_nat y = 29
y:byte
H:Some "030"%byte = Some y
to_nat y = 30
y:byte
H:Some "031"%byte = Some y
to_nat y = 31
y:byte
H:Some " "%byte = Some y
to_nat y = 32
y:byte
H:Some "!"%byte = Some y
to_nat y = 33
y:byte
H:Some """"%byte = Some y
to_nat y = 34
y:byte
H:Some "#"%byte = Some y
to_nat y = 35
y:byte
H:Some "$"%byte = Some y
to_nat y = 36
y:byte
H:Some "%"%byte = Some y
to_nat y = 37
y:byte
H:Some "&"%byte = Some y
to_nat y = 38
y:byte
H:Some "'"%byte = Some y
to_nat y = 39
y:byte
H:Some "("%byte = Some y
to_nat y = 40
y:byte
H:Some ")"%byte = Some y
to_nat y = 41
y:byte
H:Some "*"%byte = Some y
to_nat y = 42
y:byte
H:Some "+"%byte = Some y
to_nat y = 43
y:byte
H:Some ","%byte = Some y
to_nat y = 44
y:byte
H:Some "-"%byte = Some y
to_nat y = 45
y:byte
H:Some "."%byte = Some y
to_nat y = 46
y:byte
H:Some "/"%byte = Some y
to_nat y = 47
y:byte
H:Some "0"%byte = Some y
to_nat y = 48
y:byte
H:Some "1"%byte = Some y
to_nat y = 49
y:byte
H:Some "2"%byte = Some y
to_nat y = 50
y:byte
H:Some "3"%byte = Some y
to_nat y = 51
y:byte
H:Some "4"%byte = Some y
to_nat y = 52
y:byte
H:Some "5"%byte = Some y
to_nat y = 53
y:byte
H:Some "6"%byte = Some y
to_nat y = 54
y:byte
H:Some "7"%byte = Some y
to_nat y = 55
y:byte
H:Some "8"%byte = Some y
to_nat y = 56
y:byte
H:Some "9"%byte = Some y
to_nat y = 57
y:byte
H:Some ":"%byte = Some y
to_nat y = 58
y:byte
H:Some ";"%byte = Some y
to_nat y = 59
y:byte
H:Some "<"%byte = Some y
to_nat y = 60
y:byte
H:Some "="%byte = Some y
to_nat y = 61
y:byte
H:Some ">"%byte = Some y
to_nat y = 62
y:byte
H:Some "?"%byte = Some y
to_nat y = 63
y:byte
H:Some "@"%byte = Some y
to_nat y = 64
y:byte
H:Some "A"%byte = Some y
to_nat y = 65
y:byte
H:Some "B"%byte = Some y
to_nat y = 66
y:byte
H:Some "C"%byte = Some y
to_nat y = 67
y:byte
H:Some "D"%byte = Some y
to_nat y = 68
y:byte
H:Some "E"%byte = Some y
to_nat y = 69
y:byte
H:Some "F"%byte = Some y
to_nat y = 70
y:byte
H:Some "G"%byte = Some y
to_nat y = 71
y:byte
H:Some "H"%byte = Some y
to_nat y = 72
y:byte
H:Some "I"%byte = Some y
to_nat y = 73
y:byte
H:Some "J"%byte = Some y
to_nat y = 74
y:byte
H:Some "K"%byte = Some y
to_nat y = 75
y:byte
H:Some "L"%byte = Some y
to_nat y = 76
y:byte
H:Some "M"%byte = Some y
to_nat y = 77
y:byte
H:Some "N"%byte = Some y
to_nat y = 78
y:byte
H:Some "O"%byte = Some y
to_nat y = 79
y:byte
H:Some "P"%byte = Some y
to_nat y = 80
y:byte
H:Some "Q"%byte = Some y
to_nat y = 81
y:byte
H:Some "R"%byte = Some y
to_nat y = 82
y:byte
H:Some "S"%byte = Some y
to_nat y = 83
y:byte
H:Some "T"%byte = Some y
to_nat y = 84
y:byte
H:Some "U"%byte = Some y
to_nat y = 85
y:byte
H:Some "V"%byte = Some y
to_nat y = 86
y:byte
H:Some "W"%byte = Some y
to_nat y = 87
y:byte
H:Some "X"%byte = Some y
to_nat y = 88
y:byte
H:Some "Y"%byte = Some y
to_nat y = 89
y:byte
H:Some "Z"%byte = Some y
to_nat y = 90
y:byte
H:Some "["%byte = Some y
to_nat y = 91
y:byte
H:Some "\"%byte = Some y
to_nat y = 92
y:byte
H:Some "]"%byte = Some y
to_nat y = 93
y:byte
H:Some "^"%byte = Some y
to_nat y = 94
y:byte
H:Some "_"%byte = Some y
to_nat y = 95
y:byte
H:Some "`"%byte = Some y
to_nat y = 96
y:byte
H:Some "a"%byte = Some y
to_nat y = 97
y:byte
H:Some "b"%byte = Some y
to_nat y = 98
y:byte
H:Some "c"%byte = Some y
to_nat y = 99
y:byte
H:Some "d"%byte = Some y
to_nat y = 100
y:byte
H:Some "e"%byte = Some y
to_nat y = 101
y:byte
H:Some "f"%byte = Some y
to_nat y = 102
y:byte
H:Some "g"%byte = Some y
to_nat y = 103
y:byte
H:Some "h"%byte = Some y
to_nat y = 104
y:byte
H:Some "i"%byte = Some y
to_nat y = 105
y:byte
H:Some "j"%byte = Some y
to_nat y = 106
y:byte
H:Some "k"%byte = Some y
to_nat y = 107
y:byte
H:Some "l"%byte = Some y
to_nat y = 108
y:byte
H:Some "m"%byte = Some y
to_nat y = 109
y:byte
H:Some "n"%byte = Some y
to_nat y = 110
y:byte
H:Some "o"%byte = Some y
to_nat y = 111
y:byte
H:Some "p"%byte = Some y
to_nat y = 112
y:byte
H:Some "q"%byte = Some y
to_nat y = 113
y:byte
H:Some "r"%byte = Some y
to_nat y = 114
y:byte
H:Some "s"%byte = Some y
to_nat y = 115
y:byte
H:Some "t"%byte = Some y
to_nat y = 116
y:byte
H:Some "u"%byte = Some y
to_nat y = 117
y:byte
H:Some "v"%byte = Some y
to_nat y = 118
y:byte
H:Some "w"%byte = Some y
to_nat y = 119
y:byte
H:Some "x"%byte = Some y
to_nat y = 120
y:byte
H:Some "y"%byte = Some y
to_nat y = 121
y:byte
H:Some "z"%byte = Some y
to_nat y = 122
y:byte
H:Some "{"%byte = Some y
to_nat y = 123
y:byte
H:Some "|"%byte = Some y
to_nat y = 124
y:byte
H:Some "}"%byte = Some y
to_nat y = 125
y:byte
H:Some "~"%byte = Some y
to_nat y = 126
y:byte
H:Some "127"%byte = Some y
to_nat y = 127
y:byte
H:Some "128"%byte = Some y
to_nat y = 128
y:byte
H:Some "129"%byte = Some y
to_nat y = 129
y:byte
H:Some "130"%byte = Some y
to_nat y = 130
y:byte
H:Some "131"%byte = Some y
to_nat y = 131
y:byte
H:Some "132"%byte = Some y
to_nat y = 132
y:byte
H:Some "133"%byte = Some y
to_nat y = 133
y:byte
H:Some "134"%byte = Some y
to_nat y = 134
y:byte
H:Some "135"%byte = Some y
to_nat y = 135
y:byte
H:Some "136"%byte = Some y
to_nat y = 136
y:byte
H:Some "137"%byte = Some y
to_nat y = 137
y:byte
H:Some "138"%byte = Some y
to_nat y = 138
y:byte
H:Some "139"%byte = Some y
to_nat y = 139
y:byte
H:Some "140"%byte = Some y
to_nat y = 140
y:byte
H:Some "141"%byte = Some y
to_nat y = 141
y:byte
H:Some "142"%byte = Some y
to_nat y = 142
y:byte
H:Some "143"%byte = Some y
to_nat y = 143
y:byte
H:Some "144"%byte = Some y
to_nat y = 144
y:byte
H:Some "145"%byte = Some y
to_nat y = 145
y:byte
H:Some "146"%byte = Some y
to_nat y = 146
y:byte
H:Some "147"%byte = Some y
to_nat y = 147
y:byte
H:Some "148"%byte = Some y
to_nat y = 148
y:byte
H:Some "149"%byte = Some y
to_nat y = 149
y:byte
H:Some "150"%byte = Some y
to_nat y = 150
y:byte
H:Some "151"%byte = Some y
to_nat y = 151
y:byte
H:Some "152"%byte = Some y
to_nat y = 152
y:byte
H:Some "153"%byte = Some y
to_nat y = 153
y:byte
H:Some "154"%byte = Some y
to_nat y = 154
y:byte
H:Some "155"%byte = Some y
to_nat y = 155
y:byte
H:Some "156"%byte = Some y
to_nat y = 156
y:byte
H:Some "157"%byte = Some y
to_nat y = 157
y:byte
H:Some "158"%byte = Some y
to_nat y = 158
y:byte
H:Some "159"%byte = Some y
to_nat y = 159
y:byte
H:Some "160"%byte = Some y
to_nat y = 160
y:byte
H:Some "161"%byte = Some y
to_nat y = 161
y:byte
H:Some "162"%byte = Some y
to_nat y = 162
y:byte
H:Some "163"%byte = Some y
to_nat y = 163
y:byte
H:Some "164"%byte = Some y
to_nat y = 164
y:byte
H:Some "165"%byte = Some y
to_nat y = 165
y:byte
H:Some "166"%byte = Some y
to_nat y = 166
y:byte
H:Some "167"%byte = Some y
to_nat y = 167
y:byte
H:Some "168"%byte = Some y
to_nat y = 168
y:byte
H:Some "169"%byte = Some y
to_nat y = 169
y:byte
H:Some "170"%byte = Some y
to_nat y = 170
y:byte
H:Some "171"%byte = Some y
to_nat y = 171
y:byte
H:Some "172"%byte = Some y
to_nat y = 172
y:byte
H:Some "173"%byte = Some y
to_nat y = 173
y:byte
H:Some "174"%byte = Some y
to_nat y = 174
y:byte
H:Some "175"%byte = Some y
to_nat y = 175
y:byte
H:Some "176"%byte = Some y
to_nat y = 176
y:byte
H:Some "177"%byte = Some y
to_nat y = 177
y:byte
H:Some "178"%byte = Some y
to_nat y = 178
y:byte
H:Some "179"%byte = Some y
to_nat y = 179
y:byte
H:Some "180"%byte = Some y
to_nat y = 180
y:byte
H:Some "181"%byte = Some y
to_nat y = 181
y:byte
H:Some "182"%byte = Some y
to_nat y = 182
y:byte
H:Some "183"%byte = Some y
to_nat y = 183
y:byte
H:Some "184"%byte = Some y
to_nat y = 184
y:byte
H:Some "185"%byte = Some y
to_nat y = 185
y:byte
H:Some "186"%byte = Some y
to_nat y = 186
y:byte
H:Some "187"%byte = Some y
to_nat y = 187
y:byte
H:Some "188"%byte = Some y
to_nat y = 188
y:byte
H:Some "189"%byte = Some y
to_nat y = 189
y:byte
H:Some "190"%byte = Some y
to_nat y = 190
y:byte
H:Some "191"%byte = Some y
to_nat y = 191
y:byte
H:Some "192"%byte = Some y
to_nat y = 192
y:byte
H:Some "193"%byte = Some y
to_nat y = 193
y:byte
H:Some "194"%byte = Some y
to_nat y = 194
y:byte
H:Some "195"%byte = Some y
to_nat y = 195
y:byte
H:Some "196"%byte = Some y
to_nat y = 196
y:byte
H:Some "197"%byte = Some y
to_nat y = 197
y:byte
H:Some "198"%byte = Some y
to_nat y = 198
y:byte
H:Some "199"%byte = Some y
to_nat y = 199
y:byte
H:Some "200"%byte = Some y
to_nat y = 200
y:byte
H:Some "201"%byte = Some y
to_nat y = 201
y:byte
H:Some "202"%byte = Some y
to_nat y = 202
y:byte
H:Some "203"%byte = Some y
to_nat y = 203
y:byte
H:Some "204"%byte = Some y
to_nat y = 204
y:byte
H:Some "205"%byte = Some y
to_nat y = 205
y:byte
H:Some "206"%byte = Some y
to_nat y = 206
y:byte
H:Some "207"%byte = Some y
to_nat y = 207
y:byte
H:Some "208"%byte = Some y
to_nat y = 208
y:byte
H:Some "209"%byte = Some y
to_nat y = 209
y:byte
H:Some "210"%byte = Some y
to_nat y = 210
y:byte
H:Some "211"%byte = Some y
to_nat y = 211
y:byte
H:Some "212"%byte = Some y
to_nat y = 212
y:byte
H:Some "213"%byte = Some y
to_nat y = 213
y:byte
H:Some "214"%byte = Some y
to_nat y = 214
y:byte
H:Some "215"%byte = Some y
to_nat y = 215
y:byte
H:Some "216"%byte = Some y
to_nat y = 216
y:byte
H:Some "217"%byte = Some y
to_nat y = 217
y:byte
H:Some "218"%byte = Some y
to_nat y = 218
y:byte
H:Some "219"%byte = Some y
to_nat y = 219
y:byte
H:Some "220"%byte = Some y
to_nat y = 220
y:byte
H:Some "221"%byte = Some y
to_nat y = 221
y:byte
H:Some "222"%byte = Some y
to_nat y = 222
y:byte
H:Some "223"%byte = Some y
to_nat y = 223
y:byte
H:Some "224"%byte = Some y
to_nat y = 224
y:byte
H:Some "225"%byte = Some y
to_nat y = 225
y:byte
H:Some "226"%byte = Some y
to_nat y = 226
y:byte
H:Some "227"%byte = Some y
to_nat y = 227
y:byte
H:Some "228"%byte = Some y
to_nat y = 228
y:byte
H:Some "229"%byte = Some y
to_nat y = 229
y:byte
H:Some "230"%byte = Some y
to_nat y = 230
y:byte
H:Some "231"%byte = Some y
to_nat y = 231
y:byte
H:Some "232"%byte = Some y
to_nat y = 232
y:byte
H:Some "233"%byte = Some y
to_nat y = 233
y:byte
H:Some "234"%byte = Some y
to_nat y = 234
y:byte
H:Some "235"%byte = Some y
to_nat y = 235
y:byte
H:Some "236"%byte = Some y
to_nat y = 236
y:byte
H:Some "237"%byte = Some y
to_nat y = 237
y:byte
H:Some "238"%byte = Some y
to_nat y = 238
y:byte
H:Some "239"%byte = Some y
to_nat y = 239
y:byte
H:Some "240"%byte = Some y
to_nat y = 240
y:byte
H:Some "241"%byte = Some y
to_nat y = 241
y:byte
H:Some "242"%byte = Some y
to_nat y = 242
y:byte
H:Some "243"%byte = Some y
to_nat y = 243
y:byte
H:Some "244"%byte = Some y
to_nat y = 244
y:byte
H:Some "245"%byte = Some y
to_nat y = 245
y:byte
H:Some "246"%byte = Some y
to_nat y = 246
y:byte
H:Some "247"%byte = Some y
to_nat y = 247
y:byte
H:Some "248"%byte = Some y
to_nat y = 248
y:byte
H:Some "249"%byte = Some y
to_nat y = 249
y:byte
H:Some "250"%byte = Some y
to_nat y = 250
y:byte
H:Some "251"%byte = Some y
to_nat y = 251
y:byte
H:Some "252"%byte = Some y
to_nat y = 252
y:byte
H:Some "253"%byte = Some y
to_nat y = 253
y:byte
H:Some "254"%byte = Some y
to_nat y = 254
y:byte
H:Some "255"%byte = Some y
to_nat y = 255
x:nat
y:byte
H:None = Some y
to_nat y =
S
  (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))
    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.x:nat
y:byte
of_nat x = Some y <-> to_nat y = x
  Proof.x:nat
y:byte
of_nat x = Some y <-> to_nat y = x 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.x:nat
option_map to_nat (of_nat x) =
(if Nat.leb x 255 then Some x else None)
  Proof.x:nat
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. Qed.

  Lemma to_nat_bounded x : to_nat x <= 255.x:byte
to_nat x <= 255
  Proof.x:byte
to_nat x <= 255
    generalize (to_of_nat_option_map (to_nat x)).x:byte
option_map to_nat (of_nat (to_nat x)) =
(if Nat.leb (to_nat x) 255
 then Some (to_nat x)
 else None) -> to_nat x <= 255
    rewrite of_to_nat; cbn [option_map].x:byte
Some (to_nat x) =
(if Nat.leb (to_nat x) 255
 then Some (to_nat x)
 else None) -> to_nat x <= 255
    destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ].x:byte
H:Nat.leb (to_nat x) 255 = true
Some (to_nat x) = Some (to_nat x) -> to_nat x <= 255
    rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H.x:byte
H:to_nat x <= 255
Some (to_nat x) = Some (to_nat x) -> to_nat x <= 255
    intro; assumption.
  Qed.

  Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x.x:nat
of_nat x = None <-> 255 < x
  Proof.x:nat
of_nat x = None <-> 255 < x
    generalize (to_of_nat_option_map x).x:nat
option_map to_nat (of_nat x) =
(if Nat.leb x 255 then Some x else None) ->
of_nat x = None <-> 255 < x
    destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence.x:nat
b:byte
H:Nat.leb x 255 = true
Some (to_nat b) = Some x -> Some b = None <-> 255 < x
x:nat
H:Nat.leb x 255 = false
None = None -> None = None <-> 255 < x
    {x:nat
b:byte
H:Nat.leb x 255 = true
Some (to_nat b) = Some x -> Some b = None <-> 255 < x rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ].x:nat
b:byte
H:x <= 255
H0:Some (to_nat b) = Some x
255 < x -> Some b = None
      rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. }x:nat
H:Nat.leb x 255 = false
None = None -> None = None <-> 255 < x
    {x:nat
H:Nat.leb x 255 = false
None = None -> None = None <-> 255 < x rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ].x:nat
H:~ x <= 255
H0:None = None
None = None -> 255 < x
      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.x:byte
of_N (to_N x) = Some x
  Proof.x:byte
of_N (to_N x) = Some x destruct x; reflexivity. Qed.

  Lemma to_of_N x y : of_N x = Some y -> to_N y = x.x:N
y:byte
of_N x = Some y -> to_N y = x
  Proof.x:N
y:byte
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.
  Qed.

  Lemma to_of_N_iff x y : of_N x = Some y <-> to_N y = x.x:N
y:byte
of_N x = Some y <-> to_N y = x
  Proof.x:N
y:byte
of_N x = Some y <-> to_N y = x 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.x:N
option_map to_N (of_N x) =
(if x <=? 255 then Some x else None)
  Proof.x:N
option_map to_N (of_N x) =
(if 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.
  Qed.

  Lemma to_N_bounded x : to_N x <= 255.x:byte
to_N x <= 255
  Proof.x:byte
to_N x <= 255
    generalize (to_of_N_option_map (to_N x)).x:byte
option_map to_N (of_N (to_N x)) =
(if to_N x <=? 255 then Some (to_N x) else None) ->
to_N x <= 255
    rewrite of_to_N; cbn [option_map].x:byte
Some (to_N x) =
(if to_N x <=? 255 then Some (to_N x) else None) ->
to_N x <= 255
    destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ].x:byte
H:(to_N x <=? 255) = true
Some (to_N x) = Some (to_N x) -> to_N x <= 255
    rewrite (N.leb_le (to_N x) 255) in H.x:byte
H:to_N x <= 255
Some (to_N x) = Some (to_N x) -> to_N x <= 255
    intro; assumption.
  Qed.

  Lemma of_N_None_iff x : of_N x = None <-> 255 < x.x:N
of_N x = None <-> 255 < x
  Proof.x:N
of_N x = None <-> 255 < x
    generalize (to_of_N_option_map x).x:N
option_map to_N (of_N x) =
(if x <=? 255 then Some x else None) ->
of_N x = None <-> 255 < x
    destruct (of_N x), (N.leb x 255) eqn:H; cbn [option_map]; try congruence.x:N
b:byte
H:(x <=? 255) = true
Some (to_N b) = Some x -> Some b = None <-> 255 < x
x:N
H:(x <=? 255) = false
None = None -> None = None <-> 255 < x
    {x:N
b:byte
H:(x <=? 255) = true
Some (to_N b) = Some x -> Some b = None <-> 255 < x rewrite N.leb_le in H; split; [ congruence | ].x:N
b:byte
H:x <= 255
H0:Some (to_N b) = Some x
255 < x -> Some b = None
      rewrite N.lt_nge; intro H'; exfalso; apply H'; assumption. }x:N
H:(x <=? 255) = false
None = None -> None = None <-> 255 < x
    {x:N
H:(x <=? 255) = false
None = None -> None = None <-> 255 < x rewrite N.leb_nle in H; split; [ | reflexivity ].x:N
H:~ x <= 255
H0:None = None
None = None -> 255 < x
      rewrite N.lt_nge; intro; assumption. }
  Qed.

  Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x).x:byte
to_N x = N.of_nat (to_nat x)
  Proof.x:byte
to_N x = N.of_nat (to_nat x) destruct x; reflexivity. Qed.

  Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x).x:byte
to_nat x = N.to_nat (to_N x)
  Proof.x:byte
to_nat x = N.to_nat (to_N x) destruct x; reflexivity. Qed.

  Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x).x:N
of_N x = of_nat (N.to_nat x)
  Proof.x:N
of_N x = of_nat (N.to_nat x)
    destruct (of_N x) as [b|] eqn:H1.x:N
b:byte
H1:of_N x = Some b
Some b = of_nat (N.to_nat x)
x:N
H1:of_N x = None
None = of_nat (N.to_nat x)
    {x:N
b:byte
H1:of_N x = Some b
Some b = of_nat (N.to_nat x) rewrite to_of_N_iff in H1; subst.b:byte
Some b = of_nat (N.to_nat (to_N b))
      destruct b; reflexivity. }x:N
H1:of_N x = None
None = of_nat (N.to_nat x)
    {x:N
H1:of_N x = None
None = of_nat (N.to_nat x) rewrite of_N_None_iff, <- N.compare_lt_iff in H1.x:N
H1:(255 ?= x) = Lt
None = of_nat (N.to_nat x)
      symmetry; rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff.x:N
H1:(255 ?= x) = Lt
PeanoNat.Nat.compare 255 (N.to_nat x) = Lt
      rewrite Nat2N.inj_compare, N2Nat.id; assumption. }
  Qed.

  Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).x:nat
of_nat x = of_N (N.of_nat x)
  Proof.x:nat
of_nat x = of_N (N.of_nat x)
    destruct (of_nat x) as [b|] eqn:H1.x:nat
b:byte
H1:of_nat x = Some b
Some b = of_N (N.of_nat x)
x:nat
H1:of_nat x = None
None = of_N (N.of_nat x)
    {x:nat
b:byte
H1:of_nat x = Some b
Some b = of_N (N.of_nat x) rewrite to_of_nat_iff in H1; subst.b:byte
Some b = of_N (N.of_nat (to_nat b))
      destruct b; reflexivity. }x:nat
H1:of_nat x = None
None = of_N (N.of_nat x)
    {x:nat
H1:of_nat x = None
None = of_N (N.of_nat x) rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1.x:nat
H1:PeanoNat.Nat.compare 255 x = Lt
None = of_N (N.of_nat x)
      symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff.x:nat
H1:PeanoNat.Nat.compare 255 x = Lt
(255 ?= N.of_nat x) = Lt
      rewrite N2Nat.inj_compare, Nat2N.id; assumption. }
  Qed.
End N.