diff options
Diffstat (limited to 'theories/Strings')
| -rw-r--r-- | theories/Strings/Ascii.v | 119 |
1 files changed, 65 insertions, 54 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index ba01f3d4c..38245f59e 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -10,8 +10,7 @@ (** 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 *) @@ -27,19 +26,6 @@ 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 | Ascii a1 a2 a3 a4 a5 a6 a7 a8 => Ascii c a1 a2 a3 a4 a5 a6 a7 @@ -54,53 +40,65 @@ 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) : 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_nat (a : nat) := ascii_of_N (N_of_nat a). -Definition ascii_of_pos (a : positive) := ascii_of_pos_aux zero one a 8. +(** The opposite functions *) -(** Function that turns a Peano number into an ascii by converting it - to positive *) +Local Open Scope list_scope. -Definition ascii_of_nat (a : nat) := - match a with - | O => zero - | S a' => ascii_of_pos (P_of_succ_nat a') - end. +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). -(** 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). +(** 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. @@ -108,6 +106,19 @@ 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 *) (** |