diff options
| -rw-r--r-- | theories/Strings/Ascii.v | 16 | ||||
| -rw-r--r-- | theories/Strings/Byte.v | 27 |
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. |