Require Import Arith.
Require Import Cheerios.Types.
Require Import StructTact.StructTactics.

Definition byte_to_nat (b : byte) : nat :=
  match b 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 nat_to_byte (n : nat) : option byte :=
  match n 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 pcancel_byte_nat : forall b : byte, nat_to_byte (byte_to_nat b) = Some b.
Proof.
(* Goal: forall b : byte, @eq (option byte) (nat_to_byte (byte_to_nat b)) (@Some byte b) *)
  destruct b; auto.
Qed.

Definition byte_eq_dec : forall (a b : byte), {a = b} + {a <> b}.
refine
  (fun a b =>
     match Nat.eq_dec (byte_to_nat a) (byte_to_nat b) with
     | left H_dec => left _
     | right H_dec => right _
     end).
- pose proof (pcancel_byte_nat a) as H_a.
(* Goal: @eq byte a b *)
  pose proof (pcancel_byte_nat b) as H_b.
(* Goal: @eq byte a b *)
  rewrite H_dec in H_a.
(* Goal: @eq byte a b *)
  rewrite H_a in H_b.
(* Goal: @eq byte a b *)
  find_injection.
(* Goal: @eq byte b b *)
  reflexivity.
- intro H_eq.
(* Goal: False *)
  rewrite H_eq in H_dec.
(* Goal: False *)
  auto.
Defined.
