diff options
| author | Jason Gross | 2018-11-28 15:16:31 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:16:31 -0500 |
| commit | f5e3d9e29f030a86433bb2700e55c4c183593163 (patch) | |
| tree | 519a8de15016906348e69a03560c0d8393215d7e | |
| parent | 5537151575195addd3e1e0003025384a85d957f7 (diff) | |
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.
| -rw-r--r-- | test-suite/output/Search.out | 9 | ||||
| -rw-r--r-- | theories/Init/Byte.v | 1028 | ||||
| -rw-r--r-- | theories/Strings/Ascii.v | 8 | ||||
| -rw-r--r-- | theories/Strings/Byte.v | 4 |
4 files changed, 526 insertions, 523 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 20b154b5d0..f4544a0df3 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -46,9 +46,11 @@ eq_true_ind: eq_true_ind_r: forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true Byte.to_bits: - Byte.byte -> bool * bool * bool * bool * bool * bool * bool * bool + Byte.byte -> + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) Byte.of_bits: - bool * bool * bool * bool * bool * bool * bool * bool -> Byte.byte + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> + Byte.byte andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true @@ -57,7 +59,8 @@ BoolSpec_ind: (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: - forall b : bool * bool * bool * bool * bool * bool * bool * bool, + forall + b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: forall (S : Set) (R1 R2 : S -> Prop), diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 59b5f5ebe3..eede9d5028 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -291,524 +291,524 @@ Local Notation "0" := false. Local Notation "1" := true. (** We pick a definition that matches with [Ascii.ascii] *) -Definition of_bits (b : bool * bool * bool * bool * bool * bool * bool * bool) : byte +Definition of_bits (b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))) : byte := match b with - | (0,0,0,0,0,0,0,0) => x00 - | (1,0,0,0,0,0,0,0) => x01 - | (0,1,0,0,0,0,0,0) => x02 - | (1,1,0,0,0,0,0,0) => x03 - | (0,0,1,0,0,0,0,0) => x04 - | (1,0,1,0,0,0,0,0) => x05 - | (0,1,1,0,0,0,0,0) => x06 - | (1,1,1,0,0,0,0,0) => x07 - | (0,0,0,1,0,0,0,0) => x08 - | (1,0,0,1,0,0,0,0) => x09 - | (0,1,0,1,0,0,0,0) => x0a - | (1,1,0,1,0,0,0,0) => x0b - | (0,0,1,1,0,0,0,0) => x0c - | (1,0,1,1,0,0,0,0) => x0d - | (0,1,1,1,0,0,0,0) => x0e - | (1,1,1,1,0,0,0,0) => x0f - | (0,0,0,0,1,0,0,0) => x10 - | (1,0,0,0,1,0,0,0) => x11 - | (0,1,0,0,1,0,0,0) => x12 - | (1,1,0,0,1,0,0,0) => x13 - | (0,0,1,0,1,0,0,0) => x14 - | (1,0,1,0,1,0,0,0) => x15 - | (0,1,1,0,1,0,0,0) => x16 - | (1,1,1,0,1,0,0,0) => x17 - | (0,0,0,1,1,0,0,0) => x18 - | (1,0,0,1,1,0,0,0) => x19 - | (0,1,0,1,1,0,0,0) => x1a - | (1,1,0,1,1,0,0,0) => x1b - | (0,0,1,1,1,0,0,0) => x1c - | (1,0,1,1,1,0,0,0) => x1d - | (0,1,1,1,1,0,0,0) => x1e - | (1,1,1,1,1,0,0,0) => x1f - | (0,0,0,0,0,1,0,0) => x20 - | (1,0,0,0,0,1,0,0) => x21 - | (0,1,0,0,0,1,0,0) => x22 - | (1,1,0,0,0,1,0,0) => x23 - | (0,0,1,0,0,1,0,0) => x24 - | (1,0,1,0,0,1,0,0) => x25 - | (0,1,1,0,0,1,0,0) => x26 - | (1,1,1,0,0,1,0,0) => x27 - | (0,0,0,1,0,1,0,0) => x28 - | (1,0,0,1,0,1,0,0) => x29 - | (0,1,0,1,0,1,0,0) => x2a - | (1,1,0,1,0,1,0,0) => x2b - | (0,0,1,1,0,1,0,0) => x2c - | (1,0,1,1,0,1,0,0) => x2d - | (0,1,1,1,0,1,0,0) => x2e - | (1,1,1,1,0,1,0,0) => x2f - | (0,0,0,0,1,1,0,0) => x30 - | (1,0,0,0,1,1,0,0) => x31 - | (0,1,0,0,1,1,0,0) => x32 - | (1,1,0,0,1,1,0,0) => x33 - | (0,0,1,0,1,1,0,0) => x34 - | (1,0,1,0,1,1,0,0) => x35 - | (0,1,1,0,1,1,0,0) => x36 - | (1,1,1,0,1,1,0,0) => x37 - | (0,0,0,1,1,1,0,0) => x38 - | (1,0,0,1,1,1,0,0) => x39 - | (0,1,0,1,1,1,0,0) => x3a - | (1,1,0,1,1,1,0,0) => x3b - | (0,0,1,1,1,1,0,0) => x3c - | (1,0,1,1,1,1,0,0) => x3d - | (0,1,1,1,1,1,0,0) => x3e - | (1,1,1,1,1,1,0,0) => x3f - | (0,0,0,0,0,0,1,0) => x40 - | (1,0,0,0,0,0,1,0) => x41 - | (0,1,0,0,0,0,1,0) => x42 - | (1,1,0,0,0,0,1,0) => x43 - | (0,0,1,0,0,0,1,0) => x44 - | (1,0,1,0,0,0,1,0) => x45 - | (0,1,1,0,0,0,1,0) => x46 - | (1,1,1,0,0,0,1,0) => x47 - | (0,0,0,1,0,0,1,0) => x48 - | (1,0,0,1,0,0,1,0) => x49 - | (0,1,0,1,0,0,1,0) => x4a - | (1,1,0,1,0,0,1,0) => x4b - | (0,0,1,1,0,0,1,0) => x4c - | (1,0,1,1,0,0,1,0) => x4d - | (0,1,1,1,0,0,1,0) => x4e - | (1,1,1,1,0,0,1,0) => x4f - | (0,0,0,0,1,0,1,0) => x50 - | (1,0,0,0,1,0,1,0) => x51 - | (0,1,0,0,1,0,1,0) => x52 - | (1,1,0,0,1,0,1,0) => x53 - | (0,0,1,0,1,0,1,0) => x54 - | (1,0,1,0,1,0,1,0) => x55 - | (0,1,1,0,1,0,1,0) => x56 - | (1,1,1,0,1,0,1,0) => x57 - | (0,0,0,1,1,0,1,0) => x58 - | (1,0,0,1,1,0,1,0) => x59 - | (0,1,0,1,1,0,1,0) => x5a - | (1,1,0,1,1,0,1,0) => x5b - | (0,0,1,1,1,0,1,0) => x5c - | (1,0,1,1,1,0,1,0) => x5d - | (0,1,1,1,1,0,1,0) => x5e - | (1,1,1,1,1,0,1,0) => x5f - | (0,0,0,0,0,1,1,0) => x60 - | (1,0,0,0,0,1,1,0) => x61 - | (0,1,0,0,0,1,1,0) => x62 - | (1,1,0,0,0,1,1,0) => x63 - | (0,0,1,0,0,1,1,0) => x64 - | (1,0,1,0,0,1,1,0) => x65 - | (0,1,1,0,0,1,1,0) => x66 - | (1,1,1,0,0,1,1,0) => x67 - | (0,0,0,1,0,1,1,0) => x68 - | (1,0,0,1,0,1,1,0) => x69 - | (0,1,0,1,0,1,1,0) => x6a - | (1,1,0,1,0,1,1,0) => x6b - | (0,0,1,1,0,1,1,0) => x6c - | (1,0,1,1,0,1,1,0) => x6d - | (0,1,1,1,0,1,1,0) => x6e - | (1,1,1,1,0,1,1,0) => x6f - | (0,0,0,0,1,1,1,0) => x70 - | (1,0,0,0,1,1,1,0) => x71 - | (0,1,0,0,1,1,1,0) => x72 - | (1,1,0,0,1,1,1,0) => x73 - | (0,0,1,0,1,1,1,0) => x74 - | (1,0,1,0,1,1,1,0) => x75 - | (0,1,1,0,1,1,1,0) => x76 - | (1,1,1,0,1,1,1,0) => x77 - | (0,0,0,1,1,1,1,0) => x78 - | (1,0,0,1,1,1,1,0) => x79 - | (0,1,0,1,1,1,1,0) => x7a - | (1,1,0,1,1,1,1,0) => x7b - | (0,0,1,1,1,1,1,0) => x7c - | (1,0,1,1,1,1,1,0) => x7d - | (0,1,1,1,1,1,1,0) => x7e - | (1,1,1,1,1,1,1,0) => x7f - | (0,0,0,0,0,0,0,1) => x80 - | (1,0,0,0,0,0,0,1) => x81 - | (0,1,0,0,0,0,0,1) => x82 - | (1,1,0,0,0,0,0,1) => x83 - | (0,0,1,0,0,0,0,1) => x84 - | (1,0,1,0,0,0,0,1) => x85 - | (0,1,1,0,0,0,0,1) => x86 - | (1,1,1,0,0,0,0,1) => x87 - | (0,0,0,1,0,0,0,1) => x88 - | (1,0,0,1,0,0,0,1) => x89 - | (0,1,0,1,0,0,0,1) => x8a - | (1,1,0,1,0,0,0,1) => x8b - | (0,0,1,1,0,0,0,1) => x8c - | (1,0,1,1,0,0,0,1) => x8d - | (0,1,1,1,0,0,0,1) => x8e - | (1,1,1,1,0,0,0,1) => x8f - | (0,0,0,0,1,0,0,1) => x90 - | (1,0,0,0,1,0,0,1) => x91 - | (0,1,0,0,1,0,0,1) => x92 - | (1,1,0,0,1,0,0,1) => x93 - | (0,0,1,0,1,0,0,1) => x94 - | (1,0,1,0,1,0,0,1) => x95 - | (0,1,1,0,1,0,0,1) => x96 - | (1,1,1,0,1,0,0,1) => x97 - | (0,0,0,1,1,0,0,1) => x98 - | (1,0,0,1,1,0,0,1) => x99 - | (0,1,0,1,1,0,0,1) => x9a - | (1,1,0,1,1,0,0,1) => x9b - | (0,0,1,1,1,0,0,1) => x9c - | (1,0,1,1,1,0,0,1) => x9d - | (0,1,1,1,1,0,0,1) => x9e - | (1,1,1,1,1,0,0,1) => x9f - | (0,0,0,0,0,1,0,1) => xa0 - | (1,0,0,0,0,1,0,1) => xa1 - | (0,1,0,0,0,1,0,1) => xa2 - | (1,1,0,0,0,1,0,1) => xa3 - | (0,0,1,0,0,1,0,1) => xa4 - | (1,0,1,0,0,1,0,1) => xa5 - | (0,1,1,0,0,1,0,1) => xa6 - | (1,1,1,0,0,1,0,1) => xa7 - | (0,0,0,1,0,1,0,1) => xa8 - | (1,0,0,1,0,1,0,1) => xa9 - | (0,1,0,1,0,1,0,1) => xaa - | (1,1,0,1,0,1,0,1) => xab - | (0,0,1,1,0,1,0,1) => xac - | (1,0,1,1,0,1,0,1) => xad - | (0,1,1,1,0,1,0,1) => xae - | (1,1,1,1,0,1,0,1) => xaf - | (0,0,0,0,1,1,0,1) => xb0 - | (1,0,0,0,1,1,0,1) => xb1 - | (0,1,0,0,1,1,0,1) => xb2 - | (1,1,0,0,1,1,0,1) => xb3 - | (0,0,1,0,1,1,0,1) => xb4 - | (1,0,1,0,1,1,0,1) => xb5 - | (0,1,1,0,1,1,0,1) => xb6 - | (1,1,1,0,1,1,0,1) => xb7 - | (0,0,0,1,1,1,0,1) => xb8 - | (1,0,0,1,1,1,0,1) => xb9 - | (0,1,0,1,1,1,0,1) => xba - | (1,1,0,1,1,1,0,1) => xbb - | (0,0,1,1,1,1,0,1) => xbc - | (1,0,1,1,1,1,0,1) => xbd - | (0,1,1,1,1,1,0,1) => xbe - | (1,1,1,1,1,1,0,1) => xbf - | (0,0,0,0,0,0,1,1) => xc0 - | (1,0,0,0,0,0,1,1) => xc1 - | (0,1,0,0,0,0,1,1) => xc2 - | (1,1,0,0,0,0,1,1) => xc3 - | (0,0,1,0,0,0,1,1) => xc4 - | (1,0,1,0,0,0,1,1) => xc5 - | (0,1,1,0,0,0,1,1) => xc6 - | (1,1,1,0,0,0,1,1) => xc7 - | (0,0,0,1,0,0,1,1) => xc8 - | (1,0,0,1,0,0,1,1) => xc9 - | (0,1,0,1,0,0,1,1) => xca - | (1,1,0,1,0,0,1,1) => xcb - | (0,0,1,1,0,0,1,1) => xcc - | (1,0,1,1,0,0,1,1) => xcd - | (0,1,1,1,0,0,1,1) => xce - | (1,1,1,1,0,0,1,1) => xcf - | (0,0,0,0,1,0,1,1) => xd0 - | (1,0,0,0,1,0,1,1) => xd1 - | (0,1,0,0,1,0,1,1) => xd2 - | (1,1,0,0,1,0,1,1) => xd3 - | (0,0,1,0,1,0,1,1) => xd4 - | (1,0,1,0,1,0,1,1) => xd5 - | (0,1,1,0,1,0,1,1) => xd6 - | (1,1,1,0,1,0,1,1) => xd7 - | (0,0,0,1,1,0,1,1) => xd8 - | (1,0,0,1,1,0,1,1) => xd9 - | (0,1,0,1,1,0,1,1) => xda - | (1,1,0,1,1,0,1,1) => xdb - | (0,0,1,1,1,0,1,1) => xdc - | (1,0,1,1,1,0,1,1) => xdd - | (0,1,1,1,1,0,1,1) => xde - | (1,1,1,1,1,0,1,1) => xdf - | (0,0,0,0,0,1,1,1) => xe0 - | (1,0,0,0,0,1,1,1) => xe1 - | (0,1,0,0,0,1,1,1) => xe2 - | (1,1,0,0,0,1,1,1) => xe3 - | (0,0,1,0,0,1,1,1) => xe4 - | (1,0,1,0,0,1,1,1) => xe5 - | (0,1,1,0,0,1,1,1) => xe6 - | (1,1,1,0,0,1,1,1) => xe7 - | (0,0,0,1,0,1,1,1) => xe8 - | (1,0,0,1,0,1,1,1) => xe9 - | (0,1,0,1,0,1,1,1) => xea - | (1,1,0,1,0,1,1,1) => xeb - | (0,0,1,1,0,1,1,1) => xec - | (1,0,1,1,0,1,1,1) => xed - | (0,1,1,1,0,1,1,1) => xee - | (1,1,1,1,0,1,1,1) => xef - | (0,0,0,0,1,1,1,1) => xf0 - | (1,0,0,0,1,1,1,1) => xf1 - | (0,1,0,0,1,1,1,1) => xf2 - | (1,1,0,0,1,1,1,1) => xf3 - | (0,0,1,0,1,1,1,1) => xf4 - | (1,0,1,0,1,1,1,1) => xf5 - | (0,1,1,0,1,1,1,1) => xf6 - | (1,1,1,0,1,1,1,1) => xf7 - | (0,0,0,1,1,1,1,1) => xf8 - | (1,0,0,1,1,1,1,1) => xf9 - | (0,1,0,1,1,1,1,1) => xfa - | (1,1,0,1,1,1,1,1) => xfb - | (0,0,1,1,1,1,1,1) => xfc - | (1,0,1,1,1,1,1,1) => xfd - | (0,1,1,1,1,1,1,1) => xfe - | (1,1,1,1,1,1,1,1) => xff + | (0,(0,(0,(0,(0,(0,(0,0))))))) => x00 + | (1,(0,(0,(0,(0,(0,(0,0))))))) => x01 + | (0,(1,(0,(0,(0,(0,(0,0))))))) => x02 + | (1,(1,(0,(0,(0,(0,(0,0))))))) => x03 + | (0,(0,(1,(0,(0,(0,(0,0))))))) => x04 + | (1,(0,(1,(0,(0,(0,(0,0))))))) => x05 + | (0,(1,(1,(0,(0,(0,(0,0))))))) => x06 + | (1,(1,(1,(0,(0,(0,(0,0))))))) => x07 + | (0,(0,(0,(1,(0,(0,(0,0))))))) => x08 + | (1,(0,(0,(1,(0,(0,(0,0))))))) => x09 + | (0,(1,(0,(1,(0,(0,(0,0))))))) => x0a + | (1,(1,(0,(1,(0,(0,(0,0))))))) => x0b + | (0,(0,(1,(1,(0,(0,(0,0))))))) => x0c + | (1,(0,(1,(1,(0,(0,(0,0))))))) => x0d + | (0,(1,(1,(1,(0,(0,(0,0))))))) => x0e + | (1,(1,(1,(1,(0,(0,(0,0))))))) => x0f + | (0,(0,(0,(0,(1,(0,(0,0))))))) => x10 + | (1,(0,(0,(0,(1,(0,(0,0))))))) => x11 + | (0,(1,(0,(0,(1,(0,(0,0))))))) => x12 + | (1,(1,(0,(0,(1,(0,(0,0))))))) => x13 + | (0,(0,(1,(0,(1,(0,(0,0))))))) => x14 + | (1,(0,(1,(0,(1,(0,(0,0))))))) => x15 + | (0,(1,(1,(0,(1,(0,(0,0))))))) => x16 + | (1,(1,(1,(0,(1,(0,(0,0))))))) => x17 + | (0,(0,(0,(1,(1,(0,(0,0))))))) => x18 + | (1,(0,(0,(1,(1,(0,(0,0))))))) => x19 + | (0,(1,(0,(1,(1,(0,(0,0))))))) => x1a + | (1,(1,(0,(1,(1,(0,(0,0))))))) => x1b + | (0,(0,(1,(1,(1,(0,(0,0))))))) => x1c + | (1,(0,(1,(1,(1,(0,(0,0))))))) => x1d + | (0,(1,(1,(1,(1,(0,(0,0))))))) => x1e + | (1,(1,(1,(1,(1,(0,(0,0))))))) => x1f + | (0,(0,(0,(0,(0,(1,(0,0))))))) => x20 + | (1,(0,(0,(0,(0,(1,(0,0))))))) => x21 + | (0,(1,(0,(0,(0,(1,(0,0))))))) => x22 + | (1,(1,(0,(0,(0,(1,(0,0))))))) => x23 + | (0,(0,(1,(0,(0,(1,(0,0))))))) => x24 + | (1,(0,(1,(0,(0,(1,(0,0))))))) => x25 + | (0,(1,(1,(0,(0,(1,(0,0))))))) => x26 + | (1,(1,(1,(0,(0,(1,(0,0))))))) => x27 + | (0,(0,(0,(1,(0,(1,(0,0))))))) => x28 + | (1,(0,(0,(1,(0,(1,(0,0))))))) => x29 + | (0,(1,(0,(1,(0,(1,(0,0))))))) => x2a + | (1,(1,(0,(1,(0,(1,(0,0))))))) => x2b + | (0,(0,(1,(1,(0,(1,(0,0))))))) => x2c + | (1,(0,(1,(1,(0,(1,(0,0))))))) => x2d + | (0,(1,(1,(1,(0,(1,(0,0))))))) => x2e + | (1,(1,(1,(1,(0,(1,(0,0))))))) => x2f + | (0,(0,(0,(0,(1,(1,(0,0))))))) => x30 + | (1,(0,(0,(0,(1,(1,(0,0))))))) => x31 + | (0,(1,(0,(0,(1,(1,(0,0))))))) => x32 + | (1,(1,(0,(0,(1,(1,(0,0))))))) => x33 + | (0,(0,(1,(0,(1,(1,(0,0))))))) => x34 + | (1,(0,(1,(0,(1,(1,(0,0))))))) => x35 + | (0,(1,(1,(0,(1,(1,(0,0))))))) => x36 + | (1,(1,(1,(0,(1,(1,(0,0))))))) => x37 + | (0,(0,(0,(1,(1,(1,(0,0))))))) => x38 + | (1,(0,(0,(1,(1,(1,(0,0))))))) => x39 + | (0,(1,(0,(1,(1,(1,(0,0))))))) => x3a + | (1,(1,(0,(1,(1,(1,(0,0))))))) => x3b + | (0,(0,(1,(1,(1,(1,(0,0))))))) => x3c + | (1,(0,(1,(1,(1,(1,(0,0))))))) => x3d + | (0,(1,(1,(1,(1,(1,(0,0))))))) => x3e + | (1,(1,(1,(1,(1,(1,(0,0))))))) => x3f + | (0,(0,(0,(0,(0,(0,(1,0))))))) => x40 + | (1,(0,(0,(0,(0,(0,(1,0))))))) => x41 + | (0,(1,(0,(0,(0,(0,(1,0))))))) => x42 + | (1,(1,(0,(0,(0,(0,(1,0))))))) => x43 + | (0,(0,(1,(0,(0,(0,(1,0))))))) => x44 + | (1,(0,(1,(0,(0,(0,(1,0))))))) => x45 + | (0,(1,(1,(0,(0,(0,(1,0))))))) => x46 + | (1,(1,(1,(0,(0,(0,(1,0))))))) => x47 + | (0,(0,(0,(1,(0,(0,(1,0))))))) => x48 + | (1,(0,(0,(1,(0,(0,(1,0))))))) => x49 + | (0,(1,(0,(1,(0,(0,(1,0))))))) => x4a + | (1,(1,(0,(1,(0,(0,(1,0))))))) => x4b + | (0,(0,(1,(1,(0,(0,(1,0))))))) => x4c + | (1,(0,(1,(1,(0,(0,(1,0))))))) => x4d + | (0,(1,(1,(1,(0,(0,(1,0))))))) => x4e + | (1,(1,(1,(1,(0,(0,(1,0))))))) => x4f + | (0,(0,(0,(0,(1,(0,(1,0))))))) => x50 + | (1,(0,(0,(0,(1,(0,(1,0))))))) => x51 + | (0,(1,(0,(0,(1,(0,(1,0))))))) => x52 + | (1,(1,(0,(0,(1,(0,(1,0))))))) => x53 + | (0,(0,(1,(0,(1,(0,(1,0))))))) => x54 + | (1,(0,(1,(0,(1,(0,(1,0))))))) => x55 + | (0,(1,(1,(0,(1,(0,(1,0))))))) => x56 + | (1,(1,(1,(0,(1,(0,(1,0))))))) => x57 + | (0,(0,(0,(1,(1,(0,(1,0))))))) => x58 + | (1,(0,(0,(1,(1,(0,(1,0))))))) => x59 + | (0,(1,(0,(1,(1,(0,(1,0))))))) => x5a + | (1,(1,(0,(1,(1,(0,(1,0))))))) => x5b + | (0,(0,(1,(1,(1,(0,(1,0))))))) => x5c + | (1,(0,(1,(1,(1,(0,(1,0))))))) => x5d + | (0,(1,(1,(1,(1,(0,(1,0))))))) => x5e + | (1,(1,(1,(1,(1,(0,(1,0))))))) => x5f + | (0,(0,(0,(0,(0,(1,(1,0))))))) => x60 + | (1,(0,(0,(0,(0,(1,(1,0))))))) => x61 + | (0,(1,(0,(0,(0,(1,(1,0))))))) => x62 + | (1,(1,(0,(0,(0,(1,(1,0))))))) => x63 + | (0,(0,(1,(0,(0,(1,(1,0))))))) => x64 + | (1,(0,(1,(0,(0,(1,(1,0))))))) => x65 + | (0,(1,(1,(0,(0,(1,(1,0))))))) => x66 + | (1,(1,(1,(0,(0,(1,(1,0))))))) => x67 + | (0,(0,(0,(1,(0,(1,(1,0))))))) => x68 + | (1,(0,(0,(1,(0,(1,(1,0))))))) => x69 + | (0,(1,(0,(1,(0,(1,(1,0))))))) => x6a + | (1,(1,(0,(1,(0,(1,(1,0))))))) => x6b + | (0,(0,(1,(1,(0,(1,(1,0))))))) => x6c + | (1,(0,(1,(1,(0,(1,(1,0))))))) => x6d + | (0,(1,(1,(1,(0,(1,(1,0))))))) => x6e + | (1,(1,(1,(1,(0,(1,(1,0))))))) => x6f + | (0,(0,(0,(0,(1,(1,(1,0))))))) => x70 + | (1,(0,(0,(0,(1,(1,(1,0))))))) => x71 + | (0,(1,(0,(0,(1,(1,(1,0))))))) => x72 + | (1,(1,(0,(0,(1,(1,(1,0))))))) => x73 + | (0,(0,(1,(0,(1,(1,(1,0))))))) => x74 + | (1,(0,(1,(0,(1,(1,(1,0))))))) => x75 + | (0,(1,(1,(0,(1,(1,(1,0))))))) => x76 + | (1,(1,(1,(0,(1,(1,(1,0))))))) => x77 + | (0,(0,(0,(1,(1,(1,(1,0))))))) => x78 + | (1,(0,(0,(1,(1,(1,(1,0))))))) => x79 + | (0,(1,(0,(1,(1,(1,(1,0))))))) => x7a + | (1,(1,(0,(1,(1,(1,(1,0))))))) => x7b + | (0,(0,(1,(1,(1,(1,(1,0))))))) => x7c + | (1,(0,(1,(1,(1,(1,(1,0))))))) => x7d + | (0,(1,(1,(1,(1,(1,(1,0))))))) => x7e + | (1,(1,(1,(1,(1,(1,(1,0))))))) => x7f + | (0,(0,(0,(0,(0,(0,(0,1))))))) => x80 + | (1,(0,(0,(0,(0,(0,(0,1))))))) => x81 + | (0,(1,(0,(0,(0,(0,(0,1))))))) => x82 + | (1,(1,(0,(0,(0,(0,(0,1))))))) => x83 + | (0,(0,(1,(0,(0,(0,(0,1))))))) => x84 + | (1,(0,(1,(0,(0,(0,(0,1))))))) => x85 + | (0,(1,(1,(0,(0,(0,(0,1))))))) => x86 + | (1,(1,(1,(0,(0,(0,(0,1))))))) => x87 + | (0,(0,(0,(1,(0,(0,(0,1))))))) => x88 + | (1,(0,(0,(1,(0,(0,(0,1))))))) => x89 + | (0,(1,(0,(1,(0,(0,(0,1))))))) => x8a + | (1,(1,(0,(1,(0,(0,(0,1))))))) => x8b + | (0,(0,(1,(1,(0,(0,(0,1))))))) => x8c + | (1,(0,(1,(1,(0,(0,(0,1))))))) => x8d + | (0,(1,(1,(1,(0,(0,(0,1))))))) => x8e + | (1,(1,(1,(1,(0,(0,(0,1))))))) => x8f + | (0,(0,(0,(0,(1,(0,(0,1))))))) => x90 + | (1,(0,(0,(0,(1,(0,(0,1))))))) => x91 + | (0,(1,(0,(0,(1,(0,(0,1))))))) => x92 + | (1,(1,(0,(0,(1,(0,(0,1))))))) => x93 + | (0,(0,(1,(0,(1,(0,(0,1))))))) => x94 + | (1,(0,(1,(0,(1,(0,(0,1))))))) => x95 + | (0,(1,(1,(0,(1,(0,(0,1))))))) => x96 + | (1,(1,(1,(0,(1,(0,(0,1))))))) => x97 + | (0,(0,(0,(1,(1,(0,(0,1))))))) => x98 + | (1,(0,(0,(1,(1,(0,(0,1))))))) => x99 + | (0,(1,(0,(1,(1,(0,(0,1))))))) => x9a + | (1,(1,(0,(1,(1,(0,(0,1))))))) => x9b + | (0,(0,(1,(1,(1,(0,(0,1))))))) => x9c + | (1,(0,(1,(1,(1,(0,(0,1))))))) => x9d + | (0,(1,(1,(1,(1,(0,(0,1))))))) => x9e + | (1,(1,(1,(1,(1,(0,(0,1))))))) => x9f + | (0,(0,(0,(0,(0,(1,(0,1))))))) => xa0 + | (1,(0,(0,(0,(0,(1,(0,1))))))) => xa1 + | (0,(1,(0,(0,(0,(1,(0,1))))))) => xa2 + | (1,(1,(0,(0,(0,(1,(0,1))))))) => xa3 + | (0,(0,(1,(0,(0,(1,(0,1))))))) => xa4 + | (1,(0,(1,(0,(0,(1,(0,1))))))) => xa5 + | (0,(1,(1,(0,(0,(1,(0,1))))))) => xa6 + | (1,(1,(1,(0,(0,(1,(0,1))))))) => xa7 + | (0,(0,(0,(1,(0,(1,(0,1))))))) => xa8 + | (1,(0,(0,(1,(0,(1,(0,1))))))) => xa9 + | (0,(1,(0,(1,(0,(1,(0,1))))))) => xaa + | (1,(1,(0,(1,(0,(1,(0,1))))))) => xab + | (0,(0,(1,(1,(0,(1,(0,1))))))) => xac + | (1,(0,(1,(1,(0,(1,(0,1))))))) => xad + | (0,(1,(1,(1,(0,(1,(0,1))))))) => xae + | (1,(1,(1,(1,(0,(1,(0,1))))))) => xaf + | (0,(0,(0,(0,(1,(1,(0,1))))))) => xb0 + | (1,(0,(0,(0,(1,(1,(0,1))))))) => xb1 + | (0,(1,(0,(0,(1,(1,(0,1))))))) => xb2 + | (1,(1,(0,(0,(1,(1,(0,1))))))) => xb3 + | (0,(0,(1,(0,(1,(1,(0,1))))))) => xb4 + | (1,(0,(1,(0,(1,(1,(0,1))))))) => xb5 + | (0,(1,(1,(0,(1,(1,(0,1))))))) => xb6 + | (1,(1,(1,(0,(1,(1,(0,1))))))) => xb7 + | (0,(0,(0,(1,(1,(1,(0,1))))))) => xb8 + | (1,(0,(0,(1,(1,(1,(0,1))))))) => xb9 + | (0,(1,(0,(1,(1,(1,(0,1))))))) => xba + | (1,(1,(0,(1,(1,(1,(0,1))))))) => xbb + | (0,(0,(1,(1,(1,(1,(0,1))))))) => xbc + | (1,(0,(1,(1,(1,(1,(0,1))))))) => xbd + | (0,(1,(1,(1,(1,(1,(0,1))))))) => xbe + | (1,(1,(1,(1,(1,(1,(0,1))))))) => xbf + | (0,(0,(0,(0,(0,(0,(1,1))))))) => xc0 + | (1,(0,(0,(0,(0,(0,(1,1))))))) => xc1 + | (0,(1,(0,(0,(0,(0,(1,1))))))) => xc2 + | (1,(1,(0,(0,(0,(0,(1,1))))))) => xc3 + | (0,(0,(1,(0,(0,(0,(1,1))))))) => xc4 + | (1,(0,(1,(0,(0,(0,(1,1))))))) => xc5 + | (0,(1,(1,(0,(0,(0,(1,1))))))) => xc6 + | (1,(1,(1,(0,(0,(0,(1,1))))))) => xc7 + | (0,(0,(0,(1,(0,(0,(1,1))))))) => xc8 + | (1,(0,(0,(1,(0,(0,(1,1))))))) => xc9 + | (0,(1,(0,(1,(0,(0,(1,1))))))) => xca + | (1,(1,(0,(1,(0,(0,(1,1))))))) => xcb + | (0,(0,(1,(1,(0,(0,(1,1))))))) => xcc + | (1,(0,(1,(1,(0,(0,(1,1))))))) => xcd + | (0,(1,(1,(1,(0,(0,(1,1))))))) => xce + | (1,(1,(1,(1,(0,(0,(1,1))))))) => xcf + | (0,(0,(0,(0,(1,(0,(1,1))))))) => xd0 + | (1,(0,(0,(0,(1,(0,(1,1))))))) => xd1 + | (0,(1,(0,(0,(1,(0,(1,1))))))) => xd2 + | (1,(1,(0,(0,(1,(0,(1,1))))))) => xd3 + | (0,(0,(1,(0,(1,(0,(1,1))))))) => xd4 + | (1,(0,(1,(0,(1,(0,(1,1))))))) => xd5 + | (0,(1,(1,(0,(1,(0,(1,1))))))) => xd6 + | (1,(1,(1,(0,(1,(0,(1,1))))))) => xd7 + | (0,(0,(0,(1,(1,(0,(1,1))))))) => xd8 + | (1,(0,(0,(1,(1,(0,(1,1))))))) => xd9 + | (0,(1,(0,(1,(1,(0,(1,1))))))) => xda + | (1,(1,(0,(1,(1,(0,(1,1))))))) => xdb + | (0,(0,(1,(1,(1,(0,(1,1))))))) => xdc + | (1,(0,(1,(1,(1,(0,(1,1))))))) => xdd + | (0,(1,(1,(1,(1,(0,(1,1))))))) => xde + | (1,(1,(1,(1,(1,(0,(1,1))))))) => xdf + | (0,(0,(0,(0,(0,(1,(1,1))))))) => xe0 + | (1,(0,(0,(0,(0,(1,(1,1))))))) => xe1 + | (0,(1,(0,(0,(0,(1,(1,1))))))) => xe2 + | (1,(1,(0,(0,(0,(1,(1,1))))))) => xe3 + | (0,(0,(1,(0,(0,(1,(1,1))))))) => xe4 + | (1,(0,(1,(0,(0,(1,(1,1))))))) => xe5 + | (0,(1,(1,(0,(0,(1,(1,1))))))) => xe6 + | (1,(1,(1,(0,(0,(1,(1,1))))))) => xe7 + | (0,(0,(0,(1,(0,(1,(1,1))))))) => xe8 + | (1,(0,(0,(1,(0,(1,(1,1))))))) => xe9 + | (0,(1,(0,(1,(0,(1,(1,1))))))) => xea + | (1,(1,(0,(1,(0,(1,(1,1))))))) => xeb + | (0,(0,(1,(1,(0,(1,(1,1))))))) => xec + | (1,(0,(1,(1,(0,(1,(1,1))))))) => xed + | (0,(1,(1,(1,(0,(1,(1,1))))))) => xee + | (1,(1,(1,(1,(0,(1,(1,1))))))) => xef + | (0,(0,(0,(0,(1,(1,(1,1))))))) => xf0 + | (1,(0,(0,(0,(1,(1,(1,1))))))) => xf1 + | (0,(1,(0,(0,(1,(1,(1,1))))))) => xf2 + | (1,(1,(0,(0,(1,(1,(1,1))))))) => xf3 + | (0,(0,(1,(0,(1,(1,(1,1))))))) => xf4 + | (1,(0,(1,(0,(1,(1,(1,1))))))) => xf5 + | (0,(1,(1,(0,(1,(1,(1,1))))))) => xf6 + | (1,(1,(1,(0,(1,(1,(1,1))))))) => xf7 + | (0,(0,(0,(1,(1,(1,(1,1))))))) => xf8 + | (1,(0,(0,(1,(1,(1,(1,1))))))) => xf9 + | (0,(1,(0,(1,(1,(1,(1,1))))))) => xfa + | (1,(1,(0,(1,(1,(1,(1,1))))))) => xfb + | (0,(0,(1,(1,(1,(1,(1,1))))))) => xfc + | (1,(0,(1,(1,(1,(1,(1,1))))))) => xfd + | (0,(1,(1,(1,(1,(1,(1,1))))))) => xfe + | (1,(1,(1,(1,(1,(1,(1,1))))))) => xff end. -Definition to_bits (b : byte) : bool * bool * bool * bool * bool * bool * bool * bool +Definition to_bits (b : byte) : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) := match b with - | x00 => (0,0,0,0,0,0,0,0) - | x01 => (1,0,0,0,0,0,0,0) - | x02 => (0,1,0,0,0,0,0,0) - | x03 => (1,1,0,0,0,0,0,0) - | x04 => (0,0,1,0,0,0,0,0) - | x05 => (1,0,1,0,0,0,0,0) - | x06 => (0,1,1,0,0,0,0,0) - | x07 => (1,1,1,0,0,0,0,0) - | x08 => (0,0,0,1,0,0,0,0) - | x09 => (1,0,0,1,0,0,0,0) - | x0a => (0,1,0,1,0,0,0,0) - | x0b => (1,1,0,1,0,0,0,0) - | x0c => (0,0,1,1,0,0,0,0) - | x0d => (1,0,1,1,0,0,0,0) - | x0e => (0,1,1,1,0,0,0,0) - | x0f => (1,1,1,1,0,0,0,0) - | x10 => (0,0,0,0,1,0,0,0) - | x11 => (1,0,0,0,1,0,0,0) - | x12 => (0,1,0,0,1,0,0,0) - | x13 => (1,1,0,0,1,0,0,0) - | x14 => (0,0,1,0,1,0,0,0) - | x15 => (1,0,1,0,1,0,0,0) - | x16 => (0,1,1,0,1,0,0,0) - | x17 => (1,1,1,0,1,0,0,0) - | x18 => (0,0,0,1,1,0,0,0) - | x19 => (1,0,0,1,1,0,0,0) - | x1a => (0,1,0,1,1,0,0,0) - | x1b => (1,1,0,1,1,0,0,0) - | x1c => (0,0,1,1,1,0,0,0) - | x1d => (1,0,1,1,1,0,0,0) - | x1e => (0,1,1,1,1,0,0,0) - | x1f => (1,1,1,1,1,0,0,0) - | x20 => (0,0,0,0,0,1,0,0) - | x21 => (1,0,0,0,0,1,0,0) - | x22 => (0,1,0,0,0,1,0,0) - | x23 => (1,1,0,0,0,1,0,0) - | x24 => (0,0,1,0,0,1,0,0) - | x25 => (1,0,1,0,0,1,0,0) - | x26 => (0,1,1,0,0,1,0,0) - | x27 => (1,1,1,0,0,1,0,0) - | x28 => (0,0,0,1,0,1,0,0) - | x29 => (1,0,0,1,0,1,0,0) - | x2a => (0,1,0,1,0,1,0,0) - | x2b => (1,1,0,1,0,1,0,0) - | x2c => (0,0,1,1,0,1,0,0) - | x2d => (1,0,1,1,0,1,0,0) - | x2e => (0,1,1,1,0,1,0,0) - | x2f => (1,1,1,1,0,1,0,0) - | x30 => (0,0,0,0,1,1,0,0) - | x31 => (1,0,0,0,1,1,0,0) - | x32 => (0,1,0,0,1,1,0,0) - | x33 => (1,1,0,0,1,1,0,0) - | x34 => (0,0,1,0,1,1,0,0) - | x35 => (1,0,1,0,1,1,0,0) - | x36 => (0,1,1,0,1,1,0,0) - | x37 => (1,1,1,0,1,1,0,0) - | x38 => (0,0,0,1,1,1,0,0) - | x39 => (1,0,0,1,1,1,0,0) - | x3a => (0,1,0,1,1,1,0,0) - | x3b => (1,1,0,1,1,1,0,0) - | x3c => (0,0,1,1,1,1,0,0) - | x3d => (1,0,1,1,1,1,0,0) - | x3e => (0,1,1,1,1,1,0,0) - | x3f => (1,1,1,1,1,1,0,0) - | x40 => (0,0,0,0,0,0,1,0) - | x41 => (1,0,0,0,0,0,1,0) - | x42 => (0,1,0,0,0,0,1,0) - | x43 => (1,1,0,0,0,0,1,0) - | x44 => (0,0,1,0,0,0,1,0) - | x45 => (1,0,1,0,0,0,1,0) - | x46 => (0,1,1,0,0,0,1,0) - | x47 => (1,1,1,0,0,0,1,0) - | x48 => (0,0,0,1,0,0,1,0) - | x49 => (1,0,0,1,0,0,1,0) - | x4a => (0,1,0,1,0,0,1,0) - | x4b => (1,1,0,1,0,0,1,0) - | x4c => (0,0,1,1,0,0,1,0) - | x4d => (1,0,1,1,0,0,1,0) - | x4e => (0,1,1,1,0,0,1,0) - | x4f => (1,1,1,1,0,0,1,0) - | x50 => (0,0,0,0,1,0,1,0) - | x51 => (1,0,0,0,1,0,1,0) - | x52 => (0,1,0,0,1,0,1,0) - | x53 => (1,1,0,0,1,0,1,0) - | x54 => (0,0,1,0,1,0,1,0) - | x55 => (1,0,1,0,1,0,1,0) - | x56 => (0,1,1,0,1,0,1,0) - | x57 => (1,1,1,0,1,0,1,0) - | x58 => (0,0,0,1,1,0,1,0) - | x59 => (1,0,0,1,1,0,1,0) - | x5a => (0,1,0,1,1,0,1,0) - | x5b => (1,1,0,1,1,0,1,0) - | x5c => (0,0,1,1,1,0,1,0) - | x5d => (1,0,1,1,1,0,1,0) - | x5e => (0,1,1,1,1,0,1,0) - | x5f => (1,1,1,1,1,0,1,0) - | x60 => (0,0,0,0,0,1,1,0) - | x61 => (1,0,0,0,0,1,1,0) - | x62 => (0,1,0,0,0,1,1,0) - | x63 => (1,1,0,0,0,1,1,0) - | x64 => (0,0,1,0,0,1,1,0) - | x65 => (1,0,1,0,0,1,1,0) - | x66 => (0,1,1,0,0,1,1,0) - | x67 => (1,1,1,0,0,1,1,0) - | x68 => (0,0,0,1,0,1,1,0) - | x69 => (1,0,0,1,0,1,1,0) - | x6a => (0,1,0,1,0,1,1,0) - | x6b => (1,1,0,1,0,1,1,0) - | x6c => (0,0,1,1,0,1,1,0) - | x6d => (1,0,1,1,0,1,1,0) - | x6e => (0,1,1,1,0,1,1,0) - | x6f => (1,1,1,1,0,1,1,0) - | x70 => (0,0,0,0,1,1,1,0) - | x71 => (1,0,0,0,1,1,1,0) - | x72 => (0,1,0,0,1,1,1,0) - | x73 => (1,1,0,0,1,1,1,0) - | x74 => (0,0,1,0,1,1,1,0) - | x75 => (1,0,1,0,1,1,1,0) - | x76 => (0,1,1,0,1,1,1,0) - | x77 => (1,1,1,0,1,1,1,0) - | x78 => (0,0,0,1,1,1,1,0) - | x79 => (1,0,0,1,1,1,1,0) - | x7a => (0,1,0,1,1,1,1,0) - | x7b => (1,1,0,1,1,1,1,0) - | x7c => (0,0,1,1,1,1,1,0) - | x7d => (1,0,1,1,1,1,1,0) - | x7e => (0,1,1,1,1,1,1,0) - | x7f => (1,1,1,1,1,1,1,0) - | x80 => (0,0,0,0,0,0,0,1) - | x81 => (1,0,0,0,0,0,0,1) - | x82 => (0,1,0,0,0,0,0,1) - | x83 => (1,1,0,0,0,0,0,1) - | x84 => (0,0,1,0,0,0,0,1) - | x85 => (1,0,1,0,0,0,0,1) - | x86 => (0,1,1,0,0,0,0,1) - | x87 => (1,1,1,0,0,0,0,1) - | x88 => (0,0,0,1,0,0,0,1) - | x89 => (1,0,0,1,0,0,0,1) - | x8a => (0,1,0,1,0,0,0,1) - | x8b => (1,1,0,1,0,0,0,1) - | x8c => (0,0,1,1,0,0,0,1) - | x8d => (1,0,1,1,0,0,0,1) - | x8e => (0,1,1,1,0,0,0,1) - | x8f => (1,1,1,1,0,0,0,1) - | x90 => (0,0,0,0,1,0,0,1) - | x91 => (1,0,0,0,1,0,0,1) - | x92 => (0,1,0,0,1,0,0,1) - | x93 => (1,1,0,0,1,0,0,1) - | x94 => (0,0,1,0,1,0,0,1) - | x95 => (1,0,1,0,1,0,0,1) - | x96 => (0,1,1,0,1,0,0,1) - | x97 => (1,1,1,0,1,0,0,1) - | x98 => (0,0,0,1,1,0,0,1) - | x99 => (1,0,0,1,1,0,0,1) - | x9a => (0,1,0,1,1,0,0,1) - | x9b => (1,1,0,1,1,0,0,1) - | x9c => (0,0,1,1,1,0,0,1) - | x9d => (1,0,1,1,1,0,0,1) - | x9e => (0,1,1,1,1,0,0,1) - | x9f => (1,1,1,1,1,0,0,1) - | xa0 => (0,0,0,0,0,1,0,1) - | xa1 => (1,0,0,0,0,1,0,1) - | xa2 => (0,1,0,0,0,1,0,1) - | xa3 => (1,1,0,0,0,1,0,1) - | xa4 => (0,0,1,0,0,1,0,1) - | xa5 => (1,0,1,0,0,1,0,1) - | xa6 => (0,1,1,0,0,1,0,1) - | xa7 => (1,1,1,0,0,1,0,1) - | xa8 => (0,0,0,1,0,1,0,1) - | xa9 => (1,0,0,1,0,1,0,1) - | xaa => (0,1,0,1,0,1,0,1) - | xab => (1,1,0,1,0,1,0,1) - | xac => (0,0,1,1,0,1,0,1) - | xad => (1,0,1,1,0,1,0,1) - | xae => (0,1,1,1,0,1,0,1) - | xaf => (1,1,1,1,0,1,0,1) - | xb0 => (0,0,0,0,1,1,0,1) - | xb1 => (1,0,0,0,1,1,0,1) - | xb2 => (0,1,0,0,1,1,0,1) - | xb3 => (1,1,0,0,1,1,0,1) - | xb4 => (0,0,1,0,1,1,0,1) - | xb5 => (1,0,1,0,1,1,0,1) - | xb6 => (0,1,1,0,1,1,0,1) - | xb7 => (1,1,1,0,1,1,0,1) - | xb8 => (0,0,0,1,1,1,0,1) - | xb9 => (1,0,0,1,1,1,0,1) - | xba => (0,1,0,1,1,1,0,1) - | xbb => (1,1,0,1,1,1,0,1) - | xbc => (0,0,1,1,1,1,0,1) - | xbd => (1,0,1,1,1,1,0,1) - | xbe => (0,1,1,1,1,1,0,1) - | xbf => (1,1,1,1,1,1,0,1) - | xc0 => (0,0,0,0,0,0,1,1) - | xc1 => (1,0,0,0,0,0,1,1) - | xc2 => (0,1,0,0,0,0,1,1) - | xc3 => (1,1,0,0,0,0,1,1) - | xc4 => (0,0,1,0,0,0,1,1) - | xc5 => (1,0,1,0,0,0,1,1) - | xc6 => (0,1,1,0,0,0,1,1) - | xc7 => (1,1,1,0,0,0,1,1) - | xc8 => (0,0,0,1,0,0,1,1) - | xc9 => (1,0,0,1,0,0,1,1) - | xca => (0,1,0,1,0,0,1,1) - | xcb => (1,1,0,1,0,0,1,1) - | xcc => (0,0,1,1,0,0,1,1) - | xcd => (1,0,1,1,0,0,1,1) - | xce => (0,1,1,1,0,0,1,1) - | xcf => (1,1,1,1,0,0,1,1) - | xd0 => (0,0,0,0,1,0,1,1) - | xd1 => (1,0,0,0,1,0,1,1) - | xd2 => (0,1,0,0,1,0,1,1) - | xd3 => (1,1,0,0,1,0,1,1) - | xd4 => (0,0,1,0,1,0,1,1) - | xd5 => (1,0,1,0,1,0,1,1) - | xd6 => (0,1,1,0,1,0,1,1) - | xd7 => (1,1,1,0,1,0,1,1) - | xd8 => (0,0,0,1,1,0,1,1) - | xd9 => (1,0,0,1,1,0,1,1) - | xda => (0,1,0,1,1,0,1,1) - | xdb => (1,1,0,1,1,0,1,1) - | xdc => (0,0,1,1,1,0,1,1) - | xdd => (1,0,1,1,1,0,1,1) - | xde => (0,1,1,1,1,0,1,1) - | xdf => (1,1,1,1,1,0,1,1) - | xe0 => (0,0,0,0,0,1,1,1) - | xe1 => (1,0,0,0,0,1,1,1) - | xe2 => (0,1,0,0,0,1,1,1) - | xe3 => (1,1,0,0,0,1,1,1) - | xe4 => (0,0,1,0,0,1,1,1) - | xe5 => (1,0,1,0,0,1,1,1) - | xe6 => (0,1,1,0,0,1,1,1) - | xe7 => (1,1,1,0,0,1,1,1) - | xe8 => (0,0,0,1,0,1,1,1) - | xe9 => (1,0,0,1,0,1,1,1) - | xea => (0,1,0,1,0,1,1,1) - | xeb => (1,1,0,1,0,1,1,1) - | xec => (0,0,1,1,0,1,1,1) - | xed => (1,0,1,1,0,1,1,1) - | xee => (0,1,1,1,0,1,1,1) - | xef => (1,1,1,1,0,1,1,1) - | xf0 => (0,0,0,0,1,1,1,1) - | xf1 => (1,0,0,0,1,1,1,1) - | xf2 => (0,1,0,0,1,1,1,1) - | xf3 => (1,1,0,0,1,1,1,1) - | xf4 => (0,0,1,0,1,1,1,1) - | xf5 => (1,0,1,0,1,1,1,1) - | xf6 => (0,1,1,0,1,1,1,1) - | xf7 => (1,1,1,0,1,1,1,1) - | xf8 => (0,0,0,1,1,1,1,1) - | xf9 => (1,0,0,1,1,1,1,1) - | xfa => (0,1,0,1,1,1,1,1) - | xfb => (1,1,0,1,1,1,1,1) - | xfc => (0,0,1,1,1,1,1,1) - | xfd => (1,0,1,1,1,1,1,1) - | xfe => (0,1,1,1,1,1,1,1) - | xff => (1,1,1,1,1,1,1,1) + | x00 => (0,(0,(0,(0,(0,(0,(0,0))))))) + | x01 => (1,(0,(0,(0,(0,(0,(0,0))))))) + | x02 => (0,(1,(0,(0,(0,(0,(0,0))))))) + | x03 => (1,(1,(0,(0,(0,(0,(0,0))))))) + | x04 => (0,(0,(1,(0,(0,(0,(0,0))))))) + | x05 => (1,(0,(1,(0,(0,(0,(0,0))))))) + | x06 => (0,(1,(1,(0,(0,(0,(0,0))))))) + | x07 => (1,(1,(1,(0,(0,(0,(0,0))))))) + | x08 => (0,(0,(0,(1,(0,(0,(0,0))))))) + | x09 => (1,(0,(0,(1,(0,(0,(0,0))))))) + | x0a => (0,(1,(0,(1,(0,(0,(0,0))))))) + | x0b => (1,(1,(0,(1,(0,(0,(0,0))))))) + | x0c => (0,(0,(1,(1,(0,(0,(0,0))))))) + | x0d => (1,(0,(1,(1,(0,(0,(0,0))))))) + | x0e => (0,(1,(1,(1,(0,(0,(0,0))))))) + | x0f => (1,(1,(1,(1,(0,(0,(0,0))))))) + | x10 => (0,(0,(0,(0,(1,(0,(0,0))))))) + | x11 => (1,(0,(0,(0,(1,(0,(0,0))))))) + | x12 => (0,(1,(0,(0,(1,(0,(0,0))))))) + | x13 => (1,(1,(0,(0,(1,(0,(0,0))))))) + | x14 => (0,(0,(1,(0,(1,(0,(0,0))))))) + | x15 => (1,(0,(1,(0,(1,(0,(0,0))))))) + | x16 => (0,(1,(1,(0,(1,(0,(0,0))))))) + | x17 => (1,(1,(1,(0,(1,(0,(0,0))))))) + | x18 => (0,(0,(0,(1,(1,(0,(0,0))))))) + | x19 => (1,(0,(0,(1,(1,(0,(0,0))))))) + | x1a => (0,(1,(0,(1,(1,(0,(0,0))))))) + | x1b => (1,(1,(0,(1,(1,(0,(0,0))))))) + | x1c => (0,(0,(1,(1,(1,(0,(0,0))))))) + | x1d => (1,(0,(1,(1,(1,(0,(0,0))))))) + | x1e => (0,(1,(1,(1,(1,(0,(0,0))))))) + | x1f => (1,(1,(1,(1,(1,(0,(0,0))))))) + | x20 => (0,(0,(0,(0,(0,(1,(0,0))))))) + | x21 => (1,(0,(0,(0,(0,(1,(0,0))))))) + | x22 => (0,(1,(0,(0,(0,(1,(0,0))))))) + | x23 => (1,(1,(0,(0,(0,(1,(0,0))))))) + | x24 => (0,(0,(1,(0,(0,(1,(0,0))))))) + | x25 => (1,(0,(1,(0,(0,(1,(0,0))))))) + | x26 => (0,(1,(1,(0,(0,(1,(0,0))))))) + | x27 => (1,(1,(1,(0,(0,(1,(0,0))))))) + | x28 => (0,(0,(0,(1,(0,(1,(0,0))))))) + | x29 => (1,(0,(0,(1,(0,(1,(0,0))))))) + | x2a => (0,(1,(0,(1,(0,(1,(0,0))))))) + | x2b => (1,(1,(0,(1,(0,(1,(0,0))))))) + | x2c => (0,(0,(1,(1,(0,(1,(0,0))))))) + | x2d => (1,(0,(1,(1,(0,(1,(0,0))))))) + | x2e => (0,(1,(1,(1,(0,(1,(0,0))))))) + | x2f => (1,(1,(1,(1,(0,(1,(0,0))))))) + | x30 => (0,(0,(0,(0,(1,(1,(0,0))))))) + | x31 => (1,(0,(0,(0,(1,(1,(0,0))))))) + | x32 => (0,(1,(0,(0,(1,(1,(0,0))))))) + | x33 => (1,(1,(0,(0,(1,(1,(0,0))))))) + | x34 => (0,(0,(1,(0,(1,(1,(0,0))))))) + | x35 => (1,(0,(1,(0,(1,(1,(0,0))))))) + | x36 => (0,(1,(1,(0,(1,(1,(0,0))))))) + | x37 => (1,(1,(1,(0,(1,(1,(0,0))))))) + | x38 => (0,(0,(0,(1,(1,(1,(0,0))))))) + | x39 => (1,(0,(0,(1,(1,(1,(0,0))))))) + | x3a => (0,(1,(0,(1,(1,(1,(0,0))))))) + | x3b => (1,(1,(0,(1,(1,(1,(0,0))))))) + | x3c => (0,(0,(1,(1,(1,(1,(0,0))))))) + | x3d => (1,(0,(1,(1,(1,(1,(0,0))))))) + | x3e => (0,(1,(1,(1,(1,(1,(0,0))))))) + | x3f => (1,(1,(1,(1,(1,(1,(0,0))))))) + | x40 => (0,(0,(0,(0,(0,(0,(1,0))))))) + | x41 => (1,(0,(0,(0,(0,(0,(1,0))))))) + | x42 => (0,(1,(0,(0,(0,(0,(1,0))))))) + | x43 => (1,(1,(0,(0,(0,(0,(1,0))))))) + | x44 => (0,(0,(1,(0,(0,(0,(1,0))))))) + | x45 => (1,(0,(1,(0,(0,(0,(1,0))))))) + | x46 => (0,(1,(1,(0,(0,(0,(1,0))))))) + | x47 => (1,(1,(1,(0,(0,(0,(1,0))))))) + | x48 => (0,(0,(0,(1,(0,(0,(1,0))))))) + | x49 => (1,(0,(0,(1,(0,(0,(1,0))))))) + | x4a => (0,(1,(0,(1,(0,(0,(1,0))))))) + | x4b => (1,(1,(0,(1,(0,(0,(1,0))))))) + | x4c => (0,(0,(1,(1,(0,(0,(1,0))))))) + | x4d => (1,(0,(1,(1,(0,(0,(1,0))))))) + | x4e => (0,(1,(1,(1,(0,(0,(1,0))))))) + | x4f => (1,(1,(1,(1,(0,(0,(1,0))))))) + | x50 => (0,(0,(0,(0,(1,(0,(1,0))))))) + | x51 => (1,(0,(0,(0,(1,(0,(1,0))))))) + | x52 => (0,(1,(0,(0,(1,(0,(1,0))))))) + | x53 => (1,(1,(0,(0,(1,(0,(1,0))))))) + | x54 => (0,(0,(1,(0,(1,(0,(1,0))))))) + | x55 => (1,(0,(1,(0,(1,(0,(1,0))))))) + | x56 => (0,(1,(1,(0,(1,(0,(1,0))))))) + | x57 => (1,(1,(1,(0,(1,(0,(1,0))))))) + | x58 => (0,(0,(0,(1,(1,(0,(1,0))))))) + | x59 => (1,(0,(0,(1,(1,(0,(1,0))))))) + | x5a => (0,(1,(0,(1,(1,(0,(1,0))))))) + | x5b => (1,(1,(0,(1,(1,(0,(1,0))))))) + | x5c => (0,(0,(1,(1,(1,(0,(1,0))))))) + | x5d => (1,(0,(1,(1,(1,(0,(1,0))))))) + | x5e => (0,(1,(1,(1,(1,(0,(1,0))))))) + | x5f => (1,(1,(1,(1,(1,(0,(1,0))))))) + | x60 => (0,(0,(0,(0,(0,(1,(1,0))))))) + | x61 => (1,(0,(0,(0,(0,(1,(1,0))))))) + | x62 => (0,(1,(0,(0,(0,(1,(1,0))))))) + | x63 => (1,(1,(0,(0,(0,(1,(1,0))))))) + | x64 => (0,(0,(1,(0,(0,(1,(1,0))))))) + | x65 => (1,(0,(1,(0,(0,(1,(1,0))))))) + | x66 => (0,(1,(1,(0,(0,(1,(1,0))))))) + | x67 => (1,(1,(1,(0,(0,(1,(1,0))))))) + | x68 => (0,(0,(0,(1,(0,(1,(1,0))))))) + | x69 => (1,(0,(0,(1,(0,(1,(1,0))))))) + | x6a => (0,(1,(0,(1,(0,(1,(1,0))))))) + | x6b => (1,(1,(0,(1,(0,(1,(1,0))))))) + | x6c => (0,(0,(1,(1,(0,(1,(1,0))))))) + | x6d => (1,(0,(1,(1,(0,(1,(1,0))))))) + | x6e => (0,(1,(1,(1,(0,(1,(1,0))))))) + | x6f => (1,(1,(1,(1,(0,(1,(1,0))))))) + | x70 => (0,(0,(0,(0,(1,(1,(1,0))))))) + | x71 => (1,(0,(0,(0,(1,(1,(1,0))))))) + | x72 => (0,(1,(0,(0,(1,(1,(1,0))))))) + | x73 => (1,(1,(0,(0,(1,(1,(1,0))))))) + | x74 => (0,(0,(1,(0,(1,(1,(1,0))))))) + | x75 => (1,(0,(1,(0,(1,(1,(1,0))))))) + | x76 => (0,(1,(1,(0,(1,(1,(1,0))))))) + | x77 => (1,(1,(1,(0,(1,(1,(1,0))))))) + | x78 => (0,(0,(0,(1,(1,(1,(1,0))))))) + | x79 => (1,(0,(0,(1,(1,(1,(1,0))))))) + | x7a => (0,(1,(0,(1,(1,(1,(1,0))))))) + | x7b => (1,(1,(0,(1,(1,(1,(1,0))))))) + | x7c => (0,(0,(1,(1,(1,(1,(1,0))))))) + | x7d => (1,(0,(1,(1,(1,(1,(1,0))))))) + | x7e => (0,(1,(1,(1,(1,(1,(1,0))))))) + | x7f => (1,(1,(1,(1,(1,(1,(1,0))))))) + | x80 => (0,(0,(0,(0,(0,(0,(0,1))))))) + | x81 => (1,(0,(0,(0,(0,(0,(0,1))))))) + | x82 => (0,(1,(0,(0,(0,(0,(0,1))))))) + | x83 => (1,(1,(0,(0,(0,(0,(0,1))))))) + | x84 => (0,(0,(1,(0,(0,(0,(0,1))))))) + | x85 => (1,(0,(1,(0,(0,(0,(0,1))))))) + | x86 => (0,(1,(1,(0,(0,(0,(0,1))))))) + | x87 => (1,(1,(1,(0,(0,(0,(0,1))))))) + | x88 => (0,(0,(0,(1,(0,(0,(0,1))))))) + | x89 => (1,(0,(0,(1,(0,(0,(0,1))))))) + | x8a => (0,(1,(0,(1,(0,(0,(0,1))))))) + | x8b => (1,(1,(0,(1,(0,(0,(0,1))))))) + | x8c => (0,(0,(1,(1,(0,(0,(0,1))))))) + | x8d => (1,(0,(1,(1,(0,(0,(0,1))))))) + | x8e => (0,(1,(1,(1,(0,(0,(0,1))))))) + | x8f => (1,(1,(1,(1,(0,(0,(0,1))))))) + | x90 => (0,(0,(0,(0,(1,(0,(0,1))))))) + | x91 => (1,(0,(0,(0,(1,(0,(0,1))))))) + | x92 => (0,(1,(0,(0,(1,(0,(0,1))))))) + | x93 => (1,(1,(0,(0,(1,(0,(0,1))))))) + | x94 => (0,(0,(1,(0,(1,(0,(0,1))))))) + | x95 => (1,(0,(1,(0,(1,(0,(0,1))))))) + | x96 => (0,(1,(1,(0,(1,(0,(0,1))))))) + | x97 => (1,(1,(1,(0,(1,(0,(0,1))))))) + | x98 => (0,(0,(0,(1,(1,(0,(0,1))))))) + | x99 => (1,(0,(0,(1,(1,(0,(0,1))))))) + | x9a => (0,(1,(0,(1,(1,(0,(0,1))))))) + | x9b => (1,(1,(0,(1,(1,(0,(0,1))))))) + | x9c => (0,(0,(1,(1,(1,(0,(0,1))))))) + | x9d => (1,(0,(1,(1,(1,(0,(0,1))))))) + | x9e => (0,(1,(1,(1,(1,(0,(0,1))))))) + | x9f => (1,(1,(1,(1,(1,(0,(0,1))))))) + | xa0 => (0,(0,(0,(0,(0,(1,(0,1))))))) + | xa1 => (1,(0,(0,(0,(0,(1,(0,1))))))) + | xa2 => (0,(1,(0,(0,(0,(1,(0,1))))))) + | xa3 => (1,(1,(0,(0,(0,(1,(0,1))))))) + | xa4 => (0,(0,(1,(0,(0,(1,(0,1))))))) + | xa5 => (1,(0,(1,(0,(0,(1,(0,1))))))) + | xa6 => (0,(1,(1,(0,(0,(1,(0,1))))))) + | xa7 => (1,(1,(1,(0,(0,(1,(0,1))))))) + | xa8 => (0,(0,(0,(1,(0,(1,(0,1))))))) + | xa9 => (1,(0,(0,(1,(0,(1,(0,1))))))) + | xaa => (0,(1,(0,(1,(0,(1,(0,1))))))) + | xab => (1,(1,(0,(1,(0,(1,(0,1))))))) + | xac => (0,(0,(1,(1,(0,(1,(0,1))))))) + | xad => (1,(0,(1,(1,(0,(1,(0,1))))))) + | xae => (0,(1,(1,(1,(0,(1,(0,1))))))) + | xaf => (1,(1,(1,(1,(0,(1,(0,1))))))) + | xb0 => (0,(0,(0,(0,(1,(1,(0,1))))))) + | xb1 => (1,(0,(0,(0,(1,(1,(0,1))))))) + | xb2 => (0,(1,(0,(0,(1,(1,(0,1))))))) + | xb3 => (1,(1,(0,(0,(1,(1,(0,1))))))) + | xb4 => (0,(0,(1,(0,(1,(1,(0,1))))))) + | xb5 => (1,(0,(1,(0,(1,(1,(0,1))))))) + | xb6 => (0,(1,(1,(0,(1,(1,(0,1))))))) + | xb7 => (1,(1,(1,(0,(1,(1,(0,1))))))) + | xb8 => (0,(0,(0,(1,(1,(1,(0,1))))))) + | xb9 => (1,(0,(0,(1,(1,(1,(0,1))))))) + | xba => (0,(1,(0,(1,(1,(1,(0,1))))))) + | xbb => (1,(1,(0,(1,(1,(1,(0,1))))))) + | xbc => (0,(0,(1,(1,(1,(1,(0,1))))))) + | xbd => (1,(0,(1,(1,(1,(1,(0,1))))))) + | xbe => (0,(1,(1,(1,(1,(1,(0,1))))))) + | xbf => (1,(1,(1,(1,(1,(1,(0,1))))))) + | xc0 => (0,(0,(0,(0,(0,(0,(1,1))))))) + | xc1 => (1,(0,(0,(0,(0,(0,(1,1))))))) + | xc2 => (0,(1,(0,(0,(0,(0,(1,1))))))) + | xc3 => (1,(1,(0,(0,(0,(0,(1,1))))))) + | xc4 => (0,(0,(1,(0,(0,(0,(1,1))))))) + | xc5 => (1,(0,(1,(0,(0,(0,(1,1))))))) + | xc6 => (0,(1,(1,(0,(0,(0,(1,1))))))) + | xc7 => (1,(1,(1,(0,(0,(0,(1,1))))))) + | xc8 => (0,(0,(0,(1,(0,(0,(1,1))))))) + | xc9 => (1,(0,(0,(1,(0,(0,(1,1))))))) + | xca => (0,(1,(0,(1,(0,(0,(1,1))))))) + | xcb => (1,(1,(0,(1,(0,(0,(1,1))))))) + | xcc => (0,(0,(1,(1,(0,(0,(1,1))))))) + | xcd => (1,(0,(1,(1,(0,(0,(1,1))))))) + | xce => (0,(1,(1,(1,(0,(0,(1,1))))))) + | xcf => (1,(1,(1,(1,(0,(0,(1,1))))))) + | xd0 => (0,(0,(0,(0,(1,(0,(1,1))))))) + | xd1 => (1,(0,(0,(0,(1,(0,(1,1))))))) + | xd2 => (0,(1,(0,(0,(1,(0,(1,1))))))) + | xd3 => (1,(1,(0,(0,(1,(0,(1,1))))))) + | xd4 => (0,(0,(1,(0,(1,(0,(1,1))))))) + | xd5 => (1,(0,(1,(0,(1,(0,(1,1))))))) + | xd6 => (0,(1,(1,(0,(1,(0,(1,1))))))) + | xd7 => (1,(1,(1,(0,(1,(0,(1,1))))))) + | xd8 => (0,(0,(0,(1,(1,(0,(1,1))))))) + | xd9 => (1,(0,(0,(1,(1,(0,(1,1))))))) + | xda => (0,(1,(0,(1,(1,(0,(1,1))))))) + | xdb => (1,(1,(0,(1,(1,(0,(1,1))))))) + | xdc => (0,(0,(1,(1,(1,(0,(1,1))))))) + | xdd => (1,(0,(1,(1,(1,(0,(1,1))))))) + | xde => (0,(1,(1,(1,(1,(0,(1,1))))))) + | xdf => (1,(1,(1,(1,(1,(0,(1,1))))))) + | xe0 => (0,(0,(0,(0,(0,(1,(1,1))))))) + | xe1 => (1,(0,(0,(0,(0,(1,(1,1))))))) + | xe2 => (0,(1,(0,(0,(0,(1,(1,1))))))) + | xe3 => (1,(1,(0,(0,(0,(1,(1,1))))))) + | xe4 => (0,(0,(1,(0,(0,(1,(1,1))))))) + | xe5 => (1,(0,(1,(0,(0,(1,(1,1))))))) + | xe6 => (0,(1,(1,(0,(0,(1,(1,1))))))) + | xe7 => (1,(1,(1,(0,(0,(1,(1,1))))))) + | xe8 => (0,(0,(0,(1,(0,(1,(1,1))))))) + | xe9 => (1,(0,(0,(1,(0,(1,(1,1))))))) + | xea => (0,(1,(0,(1,(0,(1,(1,1))))))) + | xeb => (1,(1,(0,(1,(0,(1,(1,1))))))) + | xec => (0,(0,(1,(1,(0,(1,(1,1))))))) + | xed => (1,(0,(1,(1,(0,(1,(1,1))))))) + | xee => (0,(1,(1,(1,(0,(1,(1,1))))))) + | xef => (1,(1,(1,(1,(0,(1,(1,1))))))) + | xf0 => (0,(0,(0,(0,(1,(1,(1,1))))))) + | xf1 => (1,(0,(0,(0,(1,(1,(1,1))))))) + | xf2 => (0,(1,(0,(0,(1,(1,(1,1))))))) + | xf3 => (1,(1,(0,(0,(1,(1,(1,1))))))) + | xf4 => (0,(0,(1,(0,(1,(1,(1,1))))))) + | xf5 => (1,(0,(1,(0,(1,(1,(1,1))))))) + | xf6 => (0,(1,(1,(0,(1,(1,(1,1))))))) + | xf7 => (1,(1,(1,(0,(1,(1,(1,1))))))) + | xf8 => (0,(0,(0,(1,(1,(1,(1,1))))))) + | xf9 => (1,(0,(0,(1,(1,(1,(1,1))))))) + | xfa => (0,(1,(0,(1,(1,(1,(1,1))))))) + | xfb => (1,(1,(0,(1,(1,(1,(1,1))))))) + | xfc => (0,(0,(1,(1,(1,(1,(1,1))))))) + | xfd => (1,(0,(1,(1,(1,(1,(1,1))))))) + | xfe => (0,(1,(1,(1,(1,(1,(1,1))))))) + | xff => (1,(1,(1,(1,(1,(1,(1,1))))))) end. Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 131147ff8d..6a0c5f066e 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -190,12 +190,12 @@ Qed. *) Definition ascii_of_byte (b : byte) : ascii - := let '(b7, b6, b5, b4, b3, b2, b1, b0) := Byte.to_bits b in - Ascii b7 b6 b5 b4 b3 b2 b1 b0. + := let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := Byte.to_bits b in + Ascii b0 b1 b2 b3 b4 b5 b6 b7. Definition byte_of_ascii (a : ascii) : byte - := let (b7, b6, b5, b4, b3, b2, b1, b0) := a in - Byte.of_bits (b7, b6, b5, b4, b3, b2, b1, b0). + := let (b0, b1, b2, b3, b4, b5, b6, b7) := a in + Byte.of_bits (b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))). Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. Proof. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v index 4daa0b196c..2759ea60cb 100644 --- a/theories/Strings/Byte.v +++ b/theories/Strings/Byte.v @@ -16,8 +16,8 @@ Require Export Coq.Init.Byte. Local Set Implicit Arguments. Definition eqb (a b : byte) : bool - := let '(a7, a6, a5, a4, a3, a2, a1, a0) := to_bits a in - let '(b7, b6, b5, b4, b3, b2, b1, b0) := to_bits b in + := let '(a0, (a1, (a2, (a3, (a4, (a5, (a6, a7))))))) := to_bits a in + let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := to_bits b in (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 && Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool. |