1 files changed, 78 insertions, 65 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.