Proofs to ensure that conversions round-trip

We already have roundtrip proofs for byte<->nat, byte<->N, byte<->ascii,
N<->nat, ascii<->N, ascii<->nat, and this commit shows that all
roundtrips involving byte commute appropriately.  This ensures, e.g.,
that we don't mess up and reverse the bits in conversion between byte
and ascii.

2 files changed, 43 insertions, 0 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index a7bb1732be..131147ff8d 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -215,6 +215,22 @@ Proof.
   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).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma ascii_of_byte_via_nat x : ascii_of_byte x = ascii_of_nat (Byte.to_nat x).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma byte_of_ascii_via_N x : Some (byte_of_ascii x) = Byte.of_N (N_of_ascii x).
+Proof.
+  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).
+Proof.
+  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.
diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v
index d4c719bb4c..4daa0b196c 100644
--- a/theories/Strings/Byte.v
+++ b/theories/Strings/Byte.v
@@ -10,6 +10,7 @@
 
 Require Import Coq.Arith.EqNat.
 Require Import Coq.NArith.BinNat.
+Require Import Coq.NArith.Nnat.
 Require Export Coq.Init.Byte.
 
 Local Set Implicit Arguments.
@@ -1184,4 +1185,30 @@ Section N.
     { rewrite N.leb_nle in H; split; [ | reflexivity ].
       rewrite N.lt_nge; intro; assumption. }
   Qed.
+
+  Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x).
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x).
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x).
+  Proof.
+    destruct (of_N x) as [b|] eqn:H1.
+    { rewrite to_of_N_iff in H1; subst.
+      destruct b; reflexivity. }
+    { rewrite of_N_None_iff, <- N.compare_lt_iff in H1.
+      symmetry; rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff.
+      rewrite Nat2N.inj_compare, N2Nat.id; assumption. }
+  Qed.
+
+  Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).
+  Proof.
+    destruct (of_nat x) as [b|] eqn:H1.
+    { rewrite to_of_nat_iff in H1; subst.
+      destruct b; reflexivity. }
+    { rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1.
+      symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff.
+      rewrite N2Nat.inj_compare, Nat2N.id; assumption. }
+  Qed.
 End N.