aboutsummaryrefslogtreecommitdiff
path: root/theories/Strings
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Strings')
-rw-r--r--theories/Strings/Ascii.v68
-rw-r--r--theories/Strings/Byte.v1214
-rw-r--r--theories/Strings/String.v86
3 files changed, 1344 insertions, 24 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index b7c1eaa788..6a0c5f066e 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -12,7 +12,7 @@
(** Contributed by Laurent Théry (INRIA);
Adapted to Coq V8 by the Coq Development Team *)
-Require Import Bool BinPos BinNat PeanoNat Nnat.
+Require Import Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte.
(** * Definition of ascii characters *)
@@ -20,10 +20,7 @@ Require Import Bool BinPos BinNat PeanoNat Nnat.
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
-Register Ascii as plugins.syntax.Ascii.
-
Declare Scope char_scope.
-Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax.
Delimit Scope char_scope with char.
Bind Scope char_scope with ascii.
@@ -140,6 +137,12 @@ do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]);
intro H; vm_compute in H; destruct p; discriminate.
Qed.
+Theorem N_ascii_bounded :
+ forall a : ascii, (N_of_ascii a < 256)%N.
+Proof.
+ destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
+Qed.
+
Theorem ascii_nat_embedding :
forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
Proof.
@@ -158,6 +161,15 @@ Proof.
now apply Nat.compare_lt_iff.
Qed.
+Theorem nat_ascii_bounded :
+ forall a : ascii, nat_of_ascii a < 256.
+Proof.
+ intro a; unfold nat_of_ascii.
+ change 256 with (N.to_nat 256).
+ rewrite <- Nat.compare_lt_iff, <- N2Nat.inj_compare, N.compare_lt_iff.
+ apply N_ascii_bounded.
+Qed.
+
(** * Concrete syntax *)
@@ -175,7 +187,53 @@ Qed.
stand-alone utf8 characters so that only the notation "nnn" is
available for them (unless your terminal is able to represent them,
which is typically not the case in coqide).
-*)
+ *)
+
+Definition ascii_of_byte (b : byte) : ascii
+ := 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 (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.
+ cbv [ascii_of_byte byte_of_ascii].
+ 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].
+ 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.
+
+Lemma ascii_of_byte_via_N x : ascii_of_byte x = ascii_of_N (Byte.to_N x).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma ascii_of_byte_via_nat x : ascii_of_byte x = ascii_of_nat (Byte.to_nat x).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma byte_of_ascii_via_N x : Some (byte_of_ascii x) = Byte.of_N (N_of_ascii x).
+Proof.
+ rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity.
+Qed.
+
+Lemma byte_of_ascii_via_nat x : Some (byte_of_ascii x) = Byte.of_nat (nat_of_ascii x).
+Proof.
+ rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity.
+Qed.
+
+Module Export AsciiSyntax.
+ String Notation ascii ascii_of_byte byte_of_ascii : char_scope.
+End AsciiSyntax.
Local Open Scope char_scope.
diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v
new file mode 100644
index 0000000000..2759ea60cb
--- /dev/null
+++ b/theories/Strings/Byte.v
@@ -0,0 +1,1214 @@
+(************************************************************************)
+(* * 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.
+Proof. intro; subst y; destruct x; reflexivity. Defined.
+
+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 : 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 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.
+ Proof. destruct x; reflexivity. Qed.
+
+ Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x.
+ Proof.
+ do 256 try destruct x as [|x]; cbv [of_nat]; intro.
+ all: repeat match goal with
+ | _ => reflexivity
+ | _ => progress subst
+ | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H
+ | [ H : None = Some _ |- _ ] => solve [ inversion H ]
+ end.
+ Qed.
+
+ Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x.
+ Proof. 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.
+ Proof. do 256 try destruct x as [|x]; reflexivity. Qed.
+
+ Lemma to_nat_bounded x : to_nat x <= 255.
+ Proof.
+ generalize (to_of_nat_option_map (to_nat x)).
+ rewrite of_to_nat; cbn [option_map].
+ destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ].
+ rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H.
+ intro; assumption.
+ Qed.
+
+ Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x.
+ Proof.
+ generalize (to_of_nat_option_map x).
+ destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence.
+ { rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ].
+ rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. }
+ { rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ].
+ rewrite PeanoNat.Nat.lt_nge; intro; assumption. }
+ 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.
+ Proof. destruct x; reflexivity. Qed.
+
+ Lemma to_of_N x y : of_N x = Some y -> to_N y = x.
+ Proof.
+ 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.
+ Proof. 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.
+ Proof.
+ 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.
+ Proof.
+ generalize (to_of_N_option_map (to_N x)).
+ rewrite of_to_N; cbn [option_map].
+ destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ].
+ rewrite (N.leb_le (to_N x) 255) in H.
+ intro; assumption.
+ Qed.
+
+ Lemma of_N_None_iff x : of_N x = None <-> 255 < x.
+ Proof.
+ generalize (to_of_N_option_map x).
+ destruct (of_N x), (N.leb x 255) eqn:H; cbn [option_map]; try congruence.
+ { rewrite N.leb_le in H; split; [ congruence | ].
+ rewrite N.lt_nge; intro H'; exfalso; apply H'; assumption. }
+ { rewrite N.leb_nle in H; split; [ | reflexivity ].
+ rewrite N.lt_nge; intro; assumption. }
+ Qed.
+
+ Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x).
+ Proof. destruct x; reflexivity. Qed.
+
+ Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x).
+ Proof. destruct x; reflexivity. Qed.
+
+ Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x).
+ Proof.
+ destruct (of_N x) as [b|] eqn:H1.
+ { rewrite to_of_N_iff in H1; subst.
+ destruct b; reflexivity. }
+ { rewrite of_N_None_iff, <- N.compare_lt_iff in H1.
+ symmetry; rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff.
+ rewrite Nat2N.inj_compare, N2Nat.id; assumption. }
+ Qed.
+
+ Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).
+ Proof.
+ destruct (of_nat x) as [b|] eqn:H1.
+ { rewrite to_of_nat_iff in H1; subst.
+ destruct b; reflexivity. }
+ { rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1.
+ symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff.
+ rewrite N2Nat.inj_compare, Nat2N.id; assumption. }
+ Qed.
+End N.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index a09d518892..08ccfac877 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -15,6 +15,7 @@
Require Import Arith.
Require Import Ascii.
Require Import Bool.
+Require Import Coq.Strings.Byte.
(** *** Definition of strings *)
@@ -25,7 +26,6 @@ Inductive string : Set :=
| String : ascii -> string -> string.
Declare Scope string_scope.
-Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax.
Delimit Scope string_scope with string.
Bind Scope string_scope with string.
Local Open Scope string_scope.
@@ -114,12 +114,12 @@ Theorem get_correct :
Proof.
intros s1; elim s1; simpl.
intros s2; case s2; simpl; split; auto.
-intros H; generalize (H 0); intros H1; inversion H1.
+intros H; generalize (H O); intros H1; inversion H1.
intros; discriminate.
intros a s1' Rec s2; case s2; simpl; split; auto.
-intros H; generalize (H 0); intros H1; inversion H1.
+intros H; generalize (H O); intros H1; inversion H1.
intros; discriminate.
-intros H; generalize (H 0); simpl; intros H1; inversion H1.
+intros H; generalize (H O); simpl; intros H1; inversion H1.
case (Rec s).
intros H0; rewrite H0; auto.
intros n; exact (H (S n)).
@@ -150,7 +150,7 @@ Proof.
intros s1; elim s1; simpl; auto.
intros s2 n; rewrite plus_comm; simpl; auto.
intros a s1' Rec s2 n; case n; simpl; auto.
-generalize (Rec s2 0); simpl; auto. intros.
+generalize (Rec s2 O); simpl; auto. intros.
rewrite <- Plus.plus_Snm_nSm; auto.
Qed.
@@ -162,9 +162,9 @@ Qed.
Fixpoint substring (n m : nat) (s : string) : string :=
match n, m, s with
- | 0, 0, _ => EmptyString
- | 0, S m', EmptyString => s
- | 0, S m', String c s' => String c (substring 0 m' s')
+ | O, O, _ => EmptyString
+ | O, S m', EmptyString => s
+ | O, S m', String c s' => String c (substring 0 m' s')
| S n', _, EmptyString => s
| S n', _, String c s' => substring n' m s'
end.
@@ -257,16 +257,16 @@ Qed.
Fixpoint index (n : nat) (s1 s2 : string) : option nat :=
match s2, n with
- | EmptyString, 0 =>
+ | EmptyString, O =>
match s1 with
- | EmptyString => Some 0
+ | EmptyString => Some O
| String a s1' => None
end
| EmptyString, S n' => None
- | String b s2', 0 =>
- if prefix s1 s2 then Some 0
+ | String b s2', O =>
+ if prefix s1 s2 then Some O
else
- match index 0 s1 s2' with
+ match index O s1 s2' with
| Some n => Some (S n)
| None => None
end
@@ -300,8 +300,8 @@ generalize (prefix_correct s1 (String b s2'));
intros H0 H; injection H as <-; auto.
case H0; simpl; auto.
case m; simpl; auto.
-case (index 0 s1 s2'); intros; discriminate.
-intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+case (index O s1 s2'); intros; discriminate.
+intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto.
intros x H H0 H1; apply H; injection H1; auto.
intros; discriminate.
intros n'; case m; simpl; auto.
@@ -335,7 +335,7 @@ intros H0 H; injection H as <-; auto.
intros p H2 H3; inversion H3.
case m; simpl; auto.
case (index 0 s1 s2'); intros; discriminate.
-intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto.
intros x H H0 H1 p; try case p; simpl; auto.
intros H2 H3; red; intros H4; case H0.
intros H5 H6; absurd (false = true); auto with bool.
@@ -383,7 +383,7 @@ intros H4 H5; absurd (false = true); auto with bool.
case s1; simpl; auto.
intros a s n0 H H0 H1 H2;
change (substring n0 (length (String a s)) s2' <> String a s);
- apply (Rec 0); auto.
+ apply (Rec O); auto.
generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros;
discriminate.
apply Le.le_O_n.
@@ -423,9 +423,53 @@ Qed.
Definition findex n s1 s2 :=
match index n s1 s2 with
| Some n => n
- | None => 0
+ | None => O
end.
+(** *** Conversion to/from [list ascii] and [list byte] *)
+
+Fixpoint string_of_list_ascii (s : list ascii) : string
+ := match s with
+ | nil => EmptyString
+ | cons ch s => String ch (string_of_list_ascii s)
+ end.
+
+Fixpoint list_ascii_of_string (s : string) : list ascii
+ := match s with
+ | EmptyString => nil
+ | String ch s => cons ch (list_ascii_of_string s)
+ end.
+
+Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s.
+Proof.
+ induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
+Defined.
+
+Lemma list_ascii_of_string_of_list_ascii s : list_ascii_of_string (string_of_list_ascii s) = s.
+Proof.
+ induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
+Defined.
+
+Definition string_of_list_byte (s : list byte) : string
+ := string_of_list_ascii (List.map ascii_of_byte s).
+
+Definition list_byte_of_string (s : string) : list byte
+ := List.map byte_of_ascii (list_ascii_of_string s).
+
+Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s.
+Proof.
+ cbv [string_of_list_byte list_byte_of_string].
+ erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ].
+ apply ascii_of_byte_of_ascii.
+Qed.
+
+Lemma list_byte_of_string_of_list_byte s : list_byte_of_string (string_of_list_byte s) = s.
+Proof.
+ cbv [string_of_list_byte list_byte_of_string].
+ erewrite list_ascii_of_string_of_list_ascii, List.map_map, List.map_ext, List.map_id; [ reflexivity | intro ].
+ apply byte_of_ascii_of_byte.
+Qed.
+
(** *** Concrete syntax *)
(**
@@ -438,7 +482,11 @@ Definition findex n s1 s2 :=
part of a valid utf8 sequence of characters are not representable
using the Coq string notation (use explicitly the String constructor
with the ascii codes of the characters).
-*)
+ *)
+
+Module Export StringSyntax.
+ String Notation string string_of_list_byte list_byte_of_string : string_scope.
+End StringSyntax.
Example HelloWorld := " ""Hello world!""
".
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 01:45:09 +0000