Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team

Require Import Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte.

Definition of ascii characters

Definition of ascii character as a 8 bits constructor

Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).

Declare Scope char_scope.
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 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
  end.

Definition of a decidable function that is effective

Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.forall a b : ascii, {a = b} + {a <> b}
Proof.forall a b : ascii, {a = b} + {a <> b}
  decide equality; apply bool_dec.
Defined.

Local Open Scope lazy_bool_scope.

Definition eqb (a b : ascii) : bool :=
 match a, b with
 | Ascii a0 a1 a2 a3 a4 a5 a6 a7,
   Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
    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
 end.

Infix "=?" := eqb : char_scope.

Lemma eqb_spec (a b : ascii) : reflect (a = b) (a =? b)%char.a, b:ascii
reflect (a = b) (a =? b)%char
Proof.a, b:ascii
reflect (a = b) (a =? b)%char
 destruct a, b; simpl.b0, b1, b2, b3, b4, b5, b6, b7, b, b8, b9, b10, b11, b12, b13, b14:bool
reflect
  (Ascii b0 b1 b2 b3 b4 b5 b6 b7 =
   Ascii b b8 b9 b10 b11 b12 b13 b14)
  (Bool.eqb b0 b &&& Bool.eqb b1 b8 &&& Bool.eqb b2 b9 &&&
   Bool.eqb b3 b10 &&& Bool.eqb b4 b11 &&&
   Bool.eqb b5 b12 &&& Bool.eqb b6 b13 &&&
   Bool.eqb b7 b14)
 do 8 (case Bool.eqb_spec; [ intros -> | constructor; now intros [= ] ]).b, b8, b9, b10, b11, b12, b13, b14:bool
reflect
  (Ascii b b8 b9 b10 b11 b12 b13 b14 =
   Ascii b b8 b9 b10 b11 b12 b13 b14) true
 now constructor.
Qed.

Ltac t_eqb :=
  repeat first [ congruence
               | progress subst
               | apply conj
               | match goal with
                 | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y)
                 end
               | intro ].
Lemma eqb_refl x : (x =? x)%char = true.x:ascii
(x =? x)%char = true Proof.x:ascii
(x =? x)%char = true t_eqb. Qed.
Lemma eqb_sym x y : (x =? y)%char = (y =? x)%char.x, y:ascii
(x =? y)%char = (y =? x)%char Proof.x, y:ascii
(x =? y)%char = (y =? x)%char t_eqb. Qed.
Lemma eqb_eq n m : (n =? m)%char = true <-> n = m.n, m:ascii
(n =? m)%char = true <-> n = m Proof.n, m:ascii
(n =? m)%char = true <-> n = m t_eqb. Qed.
Lemma eqb_neq x y : (x =? y)%char = false <-> x <> y.x, y:ascii
(x =? y)%char = false <-> x <> y Proof.x, y:ascii
(x =? y)%char = false <-> x <> y t_eqb. Qed.
Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb.Morphisms.Proper
  (Morphisms.respectful eq
     (Morphisms.respectful eq eq)) eqb
Proof.Morphisms.Proper
  (Morphisms.respectful eq
     (Morphisms.respectful eq eq)) eqb t_eqb. Qed.

Conversion between natural numbers modulo 256 and ascii characters

Auxiliary function that turns a positive into an ascii by 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
    | N0 => zero
    | Npos p => ascii_of_pos p
  end.

Same for nat

Definition ascii_of_nat (a : nat) := ascii_of_N (N.of_nat a).

The opposite functions

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 := N.to_nat (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.forall a : ascii, ascii_of_N (N_of_ascii a) = a
Proof.forall a : ascii, ascii_of_N (N_of_ascii a) = a
  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.forall n : N,
(n < 256)%N -> N_of_ascii (ascii_of_N n) = n
Proof.forall n : N,
(n < 256)%N -> N_of_ascii (ascii_of_N n) = n
destruct n.(0 < 256)%N -> N_of_ascii (ascii_of_N 0) = 0%N
p:positive
(N.pos p < 256)%N ->
N_of_ascii (ascii_of_N (N.pos p)) = N.pos p
reflexivity.p:positive
(N.pos p < 256)%N ->
N_of_ascii (ascii_of_N (N.pos p)) = N.pos p
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.forall a : ascii, (N_of_ascii a < 256)%N
Proof.forall a : ascii, (N_of_ascii a < 256)%N
  destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
Qed.

Theorem ascii_nat_embedding :
  forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.forall a : ascii, ascii_of_nat (nat_of_ascii a) = a
Proof.forall a : ascii, ascii_of_nat (nat_of_ascii a) = a
  destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
Qed.

Theorem nat_ascii_embedding :
  forall n : nat, n < 256 -> nat_of_ascii (ascii_of_nat n) = n.forall n : nat,
n < 256 -> nat_of_ascii (ascii_of_nat n) = n
Proof.forall n : nat,
n < 256 -> nat_of_ascii (ascii_of_nat n) = n
 intros.n:nat
H:n < 256
nat_of_ascii (ascii_of_nat n) = n unfold nat_of_ascii, ascii_of_nat.n:nat
H:n < 256
N.to_nat (N_of_ascii (ascii_of_N (N.of_nat n))) = n
 rewrite N_ascii_embedding.n:nat
H:n < 256
N.to_nat (N.of_nat n) = n
n:nat
H:n < 256
(N.of_nat n < 256)%N
 apply Nat2N.id.n:nat
H:n < 256
(N.of_nat n < 256)%N
 unfold N.lt.n:nat
H:n < 256
(N.of_nat n ?= 256)%N = Lt
 change 256%N with (N.of_nat 256).n:nat
H:n < 256
(N.of_nat n ?= N.of_nat 256)%N = Lt
 rewrite <- Nat2N.inj_compare.n:nat
H:n < 256
(n ?= 256) = Lt
 now apply Nat.compare_lt_iff.
Qed.

Theorem nat_ascii_bounded :
  forall a : ascii, nat_of_ascii a < 256.forall a : ascii, nat_of_ascii a < 256
Proof.forall a : ascii, nat_of_ascii a < 256
  intro a; unfold nat_of_ascii.a:ascii
N.to_nat (N_of_ascii a) < 256
  change 256 with (N.to_nat 256).a:ascii
N.to_nat (N_of_ascii a) < N.to_nat 256
  rewrite <- Nat.compare_lt_iff, <- N2Nat.inj_compare, N.compare_lt_iff.a:ascii
(N_of_ascii a < 256)%N
  apply N_ascii_bounded.
Qed.

Concrete syntax

Ascii characters can be represented in scope char_scope as follows:

"c" represents itself if c is a character of code < 128,
"""" is an exception: it represents the ascii character 34 (double quote),
"nnn" represents the ascii character of decimal code nnn.

For instance, both "065" and "A" denote the character `uppercase A', and both "034" and """" denote the character `double quote'.

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).

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.x:ascii
ascii_of_byte (byte_of_ascii x) = x
Proof.x:ascii
ascii_of_byte (byte_of_ascii x) = x
  cbv [ascii_of_byte byte_of_ascii].x:ascii
(let
 '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) :=
  to_bits
    (let (b0, b1, b2, b3, b4, b5, b6, b7) := x in
     of_bits
       (b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))))
  in Ascii b0 b1 b2 b3 b4 b5 b6 b7) = x
  destruct x; rewrite to_bits_of_bits; reflexivity.
Qed.

Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x.x:byte
byte_of_ascii (ascii_of_byte x) = x
Proof.x:byte
byte_of_ascii (ascii_of_byte x) = x
  cbv [ascii_of_byte byte_of_ascii].x:byte
(let (b0, b1, b2, b3, b4, b5, b6, b7) :=
   let
   '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) :=
    to_bits x in Ascii b0 b1 b2 b3 b4 b5 b6 b7 in
 of_bits (b0, (b1, (b2, (b3, (b4, (b5, (b6, b7)))))))) =
x
  repeat match goal with
         | [ |- context[match ?x with pair _ _ => _ end] ]
           => rewrite (surjective_pairing x)
         | [ |- context[(fst ?x, snd ?x)] ]
           => rewrite <- (surjective_pairing x)
         end.x:byte
of_bits (to_bits x) = x
  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).x:byte
ascii_of_byte x = ascii_of_N (to_N x)
Proof.x:byte
ascii_of_byte x = ascii_of_N (to_N x) destruct x; reflexivity. Qed.

Lemma ascii_of_byte_via_nat x : ascii_of_byte x = ascii_of_nat (Byte.to_nat x).x:byte
ascii_of_byte x = ascii_of_nat (to_nat x)
Proof.x:byte
ascii_of_byte x = ascii_of_nat (to_nat x) destruct x; reflexivity. Qed.

Lemma byte_of_ascii_via_N x : Some (byte_of_ascii x) = Byte.of_N (N_of_ascii x).x:ascii
Some (byte_of_ascii x) = of_N (N_of_ascii x)
Proof.x:ascii
Some (byte_of_ascii x) = of_N (N_of_ascii x)
  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).x:ascii
Some (byte_of_ascii x) = of_nat (nat_of_ascii x)
Proof.x:ascii
Some (byte_of_ascii x) = of_nat (nat_of_ascii x)
  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.

Example Space := " ".
Example DoubleQuote := """".
Example Beep := "007".