diff options
| -rw-r--r-- | test-suite/output/Search.out | 28 | ||||
| -rw-r--r-- | test-suite/output/SearchHead.out | 1 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.out | 1 | ||||
| -rw-r--r-- | theories/Init/Byte.v | 542 | ||||
| -rw-r--r-- | theories/Strings/Ascii.v | 31 | ||||
| -rw-r--r-- | theories/Strings/Byte.v | 294 |
6 files changed, 592 insertions, 305 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 1d0485ecd4..20b154b5d0 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -25,34 +25,40 @@ xorb: bool -> bool -> bool Nat.even: nat -> bool Nat.odd: nat -> bool BoolSpec: Prop -> Prop -> bool -> Prop -Byte.byte_beq: Byte.byte -> Byte.byte -> bool -Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -eq_true_rect_r: - forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_rect_r: + forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true eq_true_rec_r: forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_ind_r: forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +Byte.to_bits: + Byte.byte -> bool * bool * bool * bool * bool * bool * bool * bool +Byte.of_bits: + 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 BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (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, + Byte.to_bits (Byte.of_bits b) = b bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 04cd7c6c91..7038eac22c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -17,7 +17,6 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool -Byte.byte_beq: Byte.byte -> Byte.byte -> bool mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 5f63b3343d..b0ac9ea29f 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,7 +11,6 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool -Byte.byte_beq: Byte.byte -> Byte.byte -> bool Nat.two: nat Nat.one: nat Nat.zero: nat diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 2d8ee30a43..59b5f5ebe3 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -21,7 +21,6 @@ Declare ML Module "string_notation_plugin". which contains all ascii characters. We use 256 constructors for efficiency and ease of conversion. *) -Local Set Boolean Equality Schemes. Declare Scope byte_scope. Delimit Scope byte_scope with byte. @@ -288,15 +287,544 @@ Bind Scope byte_scope with byte. Register byte as core.byte.type. -Notation eqb := byte_beq. +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 + := 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 + end. + +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) + end. + +Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b. +Proof. destruct b; exact eq_refl. Qed. + +Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b. +Proof. + repeat match goal with + | p : prod _ _ |- _ => destruct p + | b : bool |- _ => destruct b + end; + exact eq_refl. +Qed. Definition byte_of_byte (b : byte) : byte := b. Module Export ByteSyntaxNotations. String Notation byte byte_of_byte byte_of_byte : byte_scope. End ByteSyntaxNotations. - -Module Export ByteNotations. - Export ByteSyntaxNotations. - Infix "=?" := eqb (at level 70) : byte_scope. -End ByteNotations. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 13757c6007..a7bb1732be 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -190,36 +190,29 @@ Qed. *) Definition ascii_of_byte (b : byte) : ascii - := ascii_of_N (Byte.to_N b). + := let '(b7, b6, b5, b4, b3, b2, b1, b0) := Byte.to_bits b in + Ascii b7 b6 b5 b4 b3 b2 b1 b0. Definition byte_of_ascii (a : ascii) : byte - := match Byte.of_N (N_of_ascii a) with - | Some v => v - | None => x00 (* can't happen *) - end. + := let (b7, b6, b5, b4, b3, b2, b1, b0) := a in + Byte.of_bits (b7, b6, b5, b4, b3, b2, b1, b0). Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x. Proof. cbv [ascii_of_byte byte_of_ascii]. - pose proof (to_of_N (N_of_ascii x)). - destruct (of_N (N_of_ascii x)) as [x'|] eqn:H1. - { specialize (H x' eq_refl); rewrite H. - apply ascii_N_embedding. } - { exfalso. - rewrite of_N_None_iff in H1. - pose proof (N_ascii_bounded x) as H2. - rewrite N.lt_nge in H1, H2. - destruct (N.le_gt_cases (N_of_ascii x) 255) as [H3|H3]. - { apply H1, H3. } - { rewrite <- N.le_succ_l in H3; apply H2, H3. } } + destruct x; rewrite to_bits_of_bits; reflexivity. Qed. Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x. Proof. cbv [ascii_of_byte byte_of_ascii]. - rewrite N_ascii_embedding, of_to_N; [ reflexivity | ]. - pose proof (to_N_bounded x) as H. - rewrite <- N.lt_succ_r in H; exact H. + repeat match goal with + | [ |- context[match ?x with pair _ _ => _ end] ] + => rewrite (surjective_pairing x) + | [ |- context[(fst ?x, snd ?x)] ] + => rewrite <- (surjective_pairing x) + end. + rewrite of_bits_to_bits; reflexivity. Qed. Module Export AsciiSyntax. diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v index 581094a8b5..d4c719bb4c 100644 --- a/theories/Strings/Byte.v +++ b/theories/Strings/Byte.v @@ -14,278 +14,40 @@ Require Export Coq.Init.Byte. Local Set Implicit Arguments. -Lemma byte_dec_lb x y : x = y -> Byte.eqb x y = true. +Definition eqb (a b : byte) : bool + := let '(a7, a6, a5, a4, a3, a2, a1, a0) := to_bits a in + let '(b7, b6, b5, b4, b3, b2, b1, b0) := to_bits b in + (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 && + Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool. + +Module Export ByteNotations. + Export ByteSyntaxNotations. + Infix "=?" := eqb (at level 70) : byte_scope. +End ByteNotations. + +Lemma byte_dec_lb x y : x = y -> eqb x y = true. Proof. intro; subst y; destruct x; reflexivity. Defined. -Definition byte_dec_bl x y (H : Byte.eqb x y = true) : x = y - := match H in (_ = tr) return if tr then x = y else True with - | eq_refl - => match x, y return if Byte.eqb x y then x = y else True with - | x00, x00 => eq_refl - | x01, x01 => eq_refl - | x02, x02 => eq_refl - | x03, x03 => eq_refl - | x04, x04 => eq_refl - | x05, x05 => eq_refl - | x06, x06 => eq_refl - | x07, x07 => eq_refl - | x08, x08 => eq_refl - | x09, x09 => eq_refl - | x0a, x0a => eq_refl - | x0b, x0b => eq_refl - | x0c, x0c => eq_refl - | x0d, x0d => eq_refl - | x0e, x0e => eq_refl - | x0f, x0f => eq_refl - | x10, x10 => eq_refl - | x11, x11 => eq_refl - | x12, x12 => eq_refl - | x13, x13 => eq_refl - | x14, x14 => eq_refl - | x15, x15 => eq_refl - | x16, x16 => eq_refl - | x17, x17 => eq_refl - | x18, x18 => eq_refl - | x19, x19 => eq_refl - | x1a, x1a => eq_refl - | x1b, x1b => eq_refl - | x1c, x1c => eq_refl - | x1d, x1d => eq_refl - | x1e, x1e => eq_refl - | x1f, x1f => eq_refl - | x20, x20 => eq_refl - | x21, x21 => eq_refl - | x22, x22 => eq_refl - | x23, x23 => eq_refl - | x24, x24 => eq_refl - | x25, x25 => eq_refl - | x26, x26 => eq_refl - | x27, x27 => eq_refl - | x28, x28 => eq_refl - | x29, x29 => eq_refl - | x2a, x2a => eq_refl - | x2b, x2b => eq_refl - | x2c, x2c => eq_refl - | x2d, x2d => eq_refl - | x2e, x2e => eq_refl - | x2f, x2f => eq_refl - | x30, x30 => eq_refl - | x31, x31 => eq_refl - | x32, x32 => eq_refl - | x33, x33 => eq_refl - | x34, x34 => eq_refl - | x35, x35 => eq_refl - | x36, x36 => eq_refl - | x37, x37 => eq_refl - | x38, x38 => eq_refl - | x39, x39 => eq_refl - | x3a, x3a => eq_refl - | x3b, x3b => eq_refl - | x3c, x3c => eq_refl - | x3d, x3d => eq_refl - | x3e, x3e => eq_refl - | x3f, x3f => eq_refl - | x40, x40 => eq_refl - | x41, x41 => eq_refl - | x42, x42 => eq_refl - | x43, x43 => eq_refl - | x44, x44 => eq_refl - | x45, x45 => eq_refl - | x46, x46 => eq_refl - | x47, x47 => eq_refl - | x48, x48 => eq_refl - | x49, x49 => eq_refl - | x4a, x4a => eq_refl - | x4b, x4b => eq_refl - | x4c, x4c => eq_refl - | x4d, x4d => eq_refl - | x4e, x4e => eq_refl - | x4f, x4f => eq_refl - | x50, x50 => eq_refl - | x51, x51 => eq_refl - | x52, x52 => eq_refl - | x53, x53 => eq_refl - | x54, x54 => eq_refl - | x55, x55 => eq_refl - | x56, x56 => eq_refl - | x57, x57 => eq_refl - | x58, x58 => eq_refl - | x59, x59 => eq_refl - | x5a, x5a => eq_refl - | x5b, x5b => eq_refl - | x5c, x5c => eq_refl - | x5d, x5d => eq_refl - | x5e, x5e => eq_refl - | x5f, x5f => eq_refl - | x60, x60 => eq_refl - | x61, x61 => eq_refl - | x62, x62 => eq_refl - | x63, x63 => eq_refl - | x64, x64 => eq_refl - | x65, x65 => eq_refl - | x66, x66 => eq_refl - | x67, x67 => eq_refl - | x68, x68 => eq_refl - | x69, x69 => eq_refl - | x6a, x6a => eq_refl - | x6b, x6b => eq_refl - | x6c, x6c => eq_refl - | x6d, x6d => eq_refl - | x6e, x6e => eq_refl - | x6f, x6f => eq_refl - | x70, x70 => eq_refl - | x71, x71 => eq_refl - | x72, x72 => eq_refl - | x73, x73 => eq_refl - | x74, x74 => eq_refl - | x75, x75 => eq_refl - | x76, x76 => eq_refl - | x77, x77 => eq_refl - | x78, x78 => eq_refl - | x79, x79 => eq_refl - | x7a, x7a => eq_refl - | x7b, x7b => eq_refl - | x7c, x7c => eq_refl - | x7d, x7d => eq_refl - | x7e, x7e => eq_refl - | x7f, x7f => eq_refl - | x80, x80 => eq_refl - | x81, x81 => eq_refl - | x82, x82 => eq_refl - | x83, x83 => eq_refl - | x84, x84 => eq_refl - | x85, x85 => eq_refl - | x86, x86 => eq_refl - | x87, x87 => eq_refl - | x88, x88 => eq_refl - | x89, x89 => eq_refl - | x8a, x8a => eq_refl - | x8b, x8b => eq_refl - | x8c, x8c => eq_refl - | x8d, x8d => eq_refl - | x8e, x8e => eq_refl - | x8f, x8f => eq_refl - | x90, x90 => eq_refl - | x91, x91 => eq_refl - | x92, x92 => eq_refl - | x93, x93 => eq_refl - | x94, x94 => eq_refl - | x95, x95 => eq_refl - | x96, x96 => eq_refl - | x97, x97 => eq_refl - | x98, x98 => eq_refl - | x99, x99 => eq_refl - | x9a, x9a => eq_refl - | x9b, x9b => eq_refl - | x9c, x9c => eq_refl - | x9d, x9d => eq_refl - | x9e, x9e => eq_refl - | x9f, x9f => eq_refl - | xa0, xa0 => eq_refl - | xa1, xa1 => eq_refl - | xa2, xa2 => eq_refl - | xa3, xa3 => eq_refl - | xa4, xa4 => eq_refl - | xa5, xa5 => eq_refl - | xa6, xa6 => eq_refl - | xa7, xa7 => eq_refl - | xa8, xa8 => eq_refl - | xa9, xa9 => eq_refl - | xaa, xaa => eq_refl - | xab, xab => eq_refl - | xac, xac => eq_refl - | xad, xad => eq_refl - | xae, xae => eq_refl - | xaf, xaf => eq_refl - | xb0, xb0 => eq_refl - | xb1, xb1 => eq_refl - | xb2, xb2 => eq_refl - | xb3, xb3 => eq_refl - | xb4, xb4 => eq_refl - | xb5, xb5 => eq_refl - | xb6, xb6 => eq_refl - | xb7, xb7 => eq_refl - | xb8, xb8 => eq_refl - | xb9, xb9 => eq_refl - | xba, xba => eq_refl - | xbb, xbb => eq_refl - | xbc, xbc => eq_refl - | xbd, xbd => eq_refl - | xbe, xbe => eq_refl - | xbf, xbf => eq_refl - | xc0, xc0 => eq_refl - | xc1, xc1 => eq_refl - | xc2, xc2 => eq_refl - | xc3, xc3 => eq_refl - | xc4, xc4 => eq_refl - | xc5, xc5 => eq_refl - | xc6, xc6 => eq_refl - | xc7, xc7 => eq_refl - | xc8, xc8 => eq_refl - | xc9, xc9 => eq_refl - | xca, xca => eq_refl - | xcb, xcb => eq_refl - | xcc, xcc => eq_refl - | xcd, xcd => eq_refl - | xce, xce => eq_refl - | xcf, xcf => eq_refl - | xd0, xd0 => eq_refl - | xd1, xd1 => eq_refl - | xd2, xd2 => eq_refl - | xd3, xd3 => eq_refl - | xd4, xd4 => eq_refl - | xd5, xd5 => eq_refl - | xd6, xd6 => eq_refl - | xd7, xd7 => eq_refl - | xd8, xd8 => eq_refl - | xd9, xd9 => eq_refl - | xda, xda => eq_refl - | xdb, xdb => eq_refl - | xdc, xdc => eq_refl - | xdd, xdd => eq_refl - | xde, xde => eq_refl - | xdf, xdf => eq_refl - | xe0, xe0 => eq_refl - | xe1, xe1 => eq_refl - | xe2, xe2 => eq_refl - | xe3, xe3 => eq_refl - | xe4, xe4 => eq_refl - | xe5, xe5 => eq_refl - | xe6, xe6 => eq_refl - | xe7, xe7 => eq_refl - | xe8, xe8 => eq_refl - | xe9, xe9 => eq_refl - | xea, xea => eq_refl - | xeb, xeb => eq_refl - | xec, xec => eq_refl - | xed, xed => eq_refl - | xee, xee => eq_refl - | xef, xef => eq_refl - | xf0, xf0 => eq_refl - | xf1, xf1 => eq_refl - | xf2, xf2 => eq_refl - | xf3, xf3 => eq_refl - | xf4, xf4 => eq_refl - | xf5, xf5 => eq_refl - | xf6, xf6 => eq_refl - | xf7, xf7 => eq_refl - | xf8, xf8 => eq_refl - | xf9, xf9 => eq_refl - | xfa, xfa => eq_refl - | xfb, xfb => eq_refl - | xfc, xfc => eq_refl - | xfd, xfd => eq_refl - | xfe, xfe => eq_refl - | xff, xff => eq_refl - | _, _ => I - end - end. +Lemma byte_dec_bl x y (H : eqb x y = true) : x = y. +Proof. + rewrite <- (of_bits_to_bits x), <- (of_bits_to_bits y). + cbv [eqb] in H; revert H. + generalize (to_bits x) (to_bits y); clear x y; intros x y H. + repeat match goal with + | [ H : and _ _ |- _ ] => destruct H + | [ H : prod _ _ |- _ ] => destruct H + | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H + | [ H : context[Bool.eqb _ _ = true] |- _ ] => rewrite Bool.eqb_true_iff in H + | _ => progress subst + | _ => reflexivity + end. +Qed. -Lemma eqb_false x y : Byte.eqb x y = false -> x <> y. +Lemma eqb_false x y : eqb x y = false -> x <> y. Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed. Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y} - := (if Byte.eqb x y as beq return Byte.eqb x y = beq -> _ + := (if eqb x y as beq return eqb x y = beq -> _ then fun pf => left (byte_dec_bl x y pf) else fun pf => right (eqb_false pf)) eq_refl. |