Ascii: simplier ascii_of_pos, conversion from/to N, proofs about nat-->ascii-->nat

 - ascii_of_pos isn't tail-recursive anymore, but recursivity is at most of depth 8.
 - (brutal) proof that N_of_ascii (ascii_of_N n) = n for all n<256, same for nat.

Ideally, we could say someday that N_of_ascii (ascii_of_N n) = n mod 256

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13077 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)
 
 (**