diff options
Diffstat (limited to 'theories/Strings')
| -rw-r--r-- | theories/Strings/Ascii.v | 143 | ||||
| -rw-r--r-- | theories/Strings/String.v | 52 | ||||
| -rw-r--r-- | theories/Strings/vo.itarget | 2 |
3 files changed, 107 insertions, 90 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 1c02be7f..9e760d21 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,39 +7,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ascii.v 9245 2006-10-17 12:53:34Z notin $ *) +(* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) -Require Import Bool. -Require Import BinPos. +Require Import Bool BinPos BinNat Nnat. +Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) (** Definition of ascii character as a 8 bits constructor *) - + Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). Delimit Scope char_scope with char. Bind Scope char_scope with ascii. - + Definition zero := Ascii false false false false false false false false. - + Definition one := Ascii true false false false false false false false. - -Definition app1 (f : bool -> bool) (a : ascii) := - match a with - | Ascii a1 a2 a3 a4 a5 a6 a7 a8 => - Ascii (f a1) (f a2) (f a3) (f a4) (f a5) (f a6) (f a7) (f a8) - end. - -Definition app2 (f : bool -> bool -> bool) (a b : ascii) := - match a, b with - | Ascii a1 a2 a3 a4 a5 a6 a7 a8, Ascii b1 b2 b3 b4 b5 b6 b7 b8 => - Ascii (f a1 b1) (f a2 b2) (f a3 b3) (f a4 b4) - (f a5 b5) (f a6 b6) (f a7 b7) (f a8 b8) - end. Definition shift (c : bool) (a : ascii) := match a with @@ -46,7 +34,7 @@ Definition shift (c : bool) (a : ascii) := end. (** Definition of a decidable function that is effective *) - + Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}. decide equality; apply bool_dec. Defined. @@ -54,60 +42,85 @@ Defined. (** * Conversion between natural numbers modulo 256 and ascii characters *) (** Auxillary function that turns a positive into an ascii by - looking at the last n bits, ie z mod 2^n *) - -Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) - (n : nat) {struct n} : ascii := + looking at the last 8 bits, ie z mod 2^8 *) + +Definition ascii_of_pos : positive -> ascii := + let loop := fix loop n p := + match n with + | O => zero + | S n' => + match p with + | xH => one + | xI p' => shift true (loop n' p') + | xO p' => shift false (loop n' p') + end + end + in loop 8. + +(** Conversion from [N] to [ascii] *) + +Definition ascii_of_N (n : N) := match n with - | O => res - | S n1 => - match z with - | xH => app2 orb res acc - | xI z' => ascii_of_pos_aux (app2 orb res acc) (shift false acc) z' n1 - | xO z' => ascii_of_pos_aux res (shift false acc) z' n1 - end + | N0 => zero + | Npos p => ascii_of_pos p end. +(** Same for [nat] *) -(** Function that turns a positive into an ascii by - looking at the last 8 bits, ie a mod 8 *) - -Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8. +Definition ascii_of_nat (a : nat) := ascii_of_N (N_of_nat a). -(** Function that turns a Peano number into an ascii by converting it - to positive *) +(** The opposite functions *) -Definition ascii_of_nat (a : nat) := - match a with - | O => zero - | S a' => ascii_of_pos (P_of_succ_nat a') - end. - -(** The opposite function *) - -Definition nat_of_ascii (a : ascii) : nat := - let (a1, a2, a3, a4, a5, a6, a7, a8) := a in - 2 * - (2 * - (2 * - (2 * - (2 * - (2 * - (2 * (if a8 then 1 else 0) - + (if a7 then 1 else 0)) - + (if a6 then 1 else 0)) - + (if a5 then 1 else 0)) - + (if a4 then 1 else 0)) - + (if a3 then 1 else 0)) - + (if a2 then 1 else 0)) - + (if a1 then 1 else 0). - -Theorem ascii_nat_embedding : +Local Open Scope list_scope. + +Fixpoint N_of_digits (l:list bool) : N := + match l with + | nil => 0 + | b :: l' => (if b then 1 else 0) + 2*(N_of_digits l') + end%N. + +Definition N_of_ascii (a : ascii) : N := + let (a0,a1,a2,a3,a4,a5,a6,a7) := a in + N_of_digits (a0::a1::a2::a3::a4::a5::a6::a7::nil). + +Definition nat_of_ascii (a : ascii) : nat := nat_of_N (N_of_ascii a). + +(** Proofs that we have indeed opposite function (below 256) *) + +Theorem ascii_N_embedding : + forall a : ascii, ascii_of_N (N_of_ascii a) = a. +Proof. + destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. +Qed. + +Theorem N_ascii_embedding : + forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n. +Proof. +destruct n. +reflexivity. +do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]); + intro H; vm_compute in H; destruct p; discriminate. +Qed. + +Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a. Proof. destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. Qed. +Theorem nat_ascii_embedding : + forall n : nat, n < 256 -> nat_of_ascii (ascii_of_nat n) = n. +Proof. + intros. unfold nat_of_ascii, ascii_of_nat. + rewrite N_ascii_embedding. + apply nat_of_N_of_nat. + unfold Nlt. + change 256%N with (N_of_nat 256). + rewrite <- N_of_nat_compare. + rewrite <- Compare_dec.nat_compare_lt. auto. +Qed. + + (** * Concrete syntax *) (** @@ -123,7 +136,7 @@ Qed. Notice that the ascii characters of code >= 128 do not denote 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). + which is typically not the case in coqide). *) Open Local Scope char_scope. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 00f28a9c..15f29821 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,18 +7,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: String.v 11206 2008-07-04 16:21:28Z letouzey $ *) +(* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) Require Import Arith. Require Import Ascii. +Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) (** Implementation of string as list of ascii characters *) - + Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. @@ -36,7 +38,7 @@ Defined. Reserved Notation "x ++ y" (right associativity, at level 60). -Fixpoint append (s1 s2 : string) {struct s1} : string := +Fixpoint append (s1 s2 : string) : string := match s1 with | EmptyString => s2 | String c s1' => String c (s1' ++ s2) @@ -47,7 +49,7 @@ where "s1 ++ s2" := (append s1 s2) : string_scope. (******************************) (** Length *) (******************************) - + Fixpoint length (s : string) : nat := match s with | EmptyString => 0 @@ -57,7 +59,7 @@ Fixpoint length (s : string) : nat := (******************************) (** Nth character of a string *) (******************************) - + Fixpoint get (n : nat) (s : string) {struct s} : option ascii := match s with | EmptyString => None @@ -68,7 +70,7 @@ Fixpoint get (n : nat) (s : string) {struct s} : option ascii := end. (** Two lists that are identical through get are syntactically equal *) - + Theorem get_correct : forall s1 s2 : string, (forall n : nat, get n s1 = get n s2) <-> s1 = s2. Proof. @@ -89,7 +91,7 @@ rewrite H1; auto. Qed. (** The first elements of [s1 ++ s2] are the ones of [s1] *) - + Theorem append_correct1 : forall (s1 s2 : string) (n : nat), n < length s1 -> get n s1 = get n (s1 ++ s2). @@ -102,7 +104,7 @@ apply lt_S_n; auto. Qed. (** The last elements of [s1 ++ s2] are the ones of [s2] *) - + Theorem append_correct2 : forall (s1 s2 : string) (n : nat), get n s2 = get (n + length s1) (s1 ++ s2). @@ -119,8 +121,8 @@ Qed. (** [substring n m s] returns the substring of [s] that starts at position [n] and of length [m]; if this does not make sense it returns [""] *) - -Fixpoint substring (n m : nat) (s : string) {struct s} : string := + +Fixpoint substring (n m : nat) (s : string) : string := match n, m, s with | 0, 0, _ => EmptyString | 0, S m', EmptyString => s @@ -130,7 +132,7 @@ Fixpoint substring (n m : nat) (s : string) {struct s} : string := end. (** The substring is included in the initial string *) - + Theorem substring_correct1 : forall (s : string) (n m p : nat), p < m -> get p (substring n m s) = get (p + n) s. @@ -148,7 +150,7 @@ intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl in |- *; auto. Qed. (** The substring has at most [m] elements *) - + Theorem substring_correct2 : forall (s : string) (n m p : nat), m <= p -> get p (substring n m s) = None. Proof. @@ -166,7 +168,7 @@ Qed. (** *** Test functions *) (** Test if [s1] is a prefix of [s2] *) - + Fixpoint prefix (s1 s2 : string) {struct s2} : bool := match s1 with | EmptyString => true @@ -183,7 +185,7 @@ Fixpoint prefix (s1 s2 : string) {struct s2} : bool := (** If [s1] is a prefix of [s2], it is the [substring] of length [length s1] starting at position [O] of [s2] *) - + Theorem prefix_correct : forall s1 s2 : string, prefix s1 s2 = true <-> substring 0 (length s1) s2 = s1. @@ -202,8 +204,8 @@ Qed. (** Test if, starting at position [n], [s1] occurs in [s2]; if so it returns the position *) - -Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := + +Fixpoint index (n : nat) (s1 s2 : string) : option nat := match s2, n with | EmptyString, 0 => match s1 with @@ -211,7 +213,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := | String a s1' => None end | EmptyString, S n' => None - | String b s2', 0 => + | String b s2', 0 => if prefix s1 s2 then Some 0 else match index 0 s1 s2' with @@ -229,7 +231,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := Opaque prefix. (** If the result of [index] is [Some m], [s1] in [s2] at position [m] *) - + Theorem index_correct1 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some m -> substring m (length s1) s2 = s1. @@ -259,9 +261,9 @@ intros x H H1; apply H; injection H1; intros H2; injection H2; auto. intros; discriminate. Qed. -(** If the result of [index] is [Some m], +(** If the result of [index] is [Some m], [s1] does not occur in [s2] before [m] *) - + Theorem index_correct2 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = Some m -> @@ -304,9 +306,9 @@ apply Lt.lt_S_n; auto. intros; discriminate. Qed. -(** If the result of [index] is [None], [s1] does not occur in [s2] +(** If the result of [index] is [None], [s1] does not occur in [s2] after [n] *) - + Theorem index_correct3 : forall (n m : nat) (s1 s2 : string), index n s1 s2 = None -> @@ -348,7 +350,7 @@ Transparent prefix. (** If we are searching for the [Empty] string and the answer is no this means that [n] is greater than the size of [s] *) - + Theorem index_correct4 : forall (n : nat) (s : string), index n EmptyString s = None -> length s < n. @@ -367,7 +369,7 @@ Qed. (** Same as [index] but with no optional type, we return [0] when it does not occur *) - + Definition findex n s1 s2 := match index n s1 s2 with | Some n => n diff --git a/theories/Strings/vo.itarget b/theories/Strings/vo.itarget new file mode 100644 index 00000000..20813b42 --- /dev/null +++ b/theories/Strings/vo.itarget @@ -0,0 +1,2 @@ +Ascii.vo +String.vo |