From edea770457aea05a7e6a64c1217f66dfc6930419 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:20:00 +0200
Subject: [numeral notation] Specify R

---
 doc/stdlib/index-list.html.template |  2 ++
 theories/Numbers/DecimalR.v         | 56 +++++++++++++++++++++++++++++++++++
 theories/Numbers/HexadecimalR.v     | 58 +++++++++++++++++++++++++++++++++++++
 theories/Reals/Rdefinitions.v       | 12 ++++++++
 4 files changed, 128 insertions(+)
 create mode 100644 theories/Numbers/DecimalR.v
 create mode 100644 theories/Numbers/HexadecimalR.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index e42066d2ce..b08d7e9d2c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -238,6 +238,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/DecimalN.v
     theories/Numbers/DecimalZ.v
     theories/Numbers/DecimalQ.v
+    theories/Numbers/DecimalR.v
     theories/Numbers/DecimalString.v
     theories/Numbers/HexadecimalFacts.v
     theories/Numbers/HexadecimalNat.v
@@ -245,6 +246,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/HexadecimalN.v
     theories/Numbers/HexadecimalZ.v
     theories/Numbers/HexadecimalQ.v
+    theories/Numbers/HexadecimalR.v
     theories/Numbers/HexadecimalString.v
     </dd>
 
diff --git a/theories/Numbers/DecimalR.v b/theories/Numbers/DecimalR.v
new file mode 100644
index 0000000000..409ca88f1a
--- /dev/null
+++ b/theories/Numbers/DecimalR.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+(** * DecimalR
+
+    Proofs that conversions between decimal numbers and [R]
+    are bijections. *)
+
+Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions.
+
+Lemma of_to (q:IR) : forall d, to_decimal q = Some d -> of_decimal d = q.
+Admitted.
+
+Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d).
+Admitted.
+
+(** Some consequences *)
+
+Lemma to_decimal_inj q q' :
+  to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.
+Proof.
+intros Hnone EQ.
+generalize (of_to q) (of_to q').
+rewrite <-EQ.
+revert Hnone; case to_decimal; [|now simpl].
+now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
+Qed.
+
+Lemma to_decimal_surj d : exists q, to_decimal q = Some (dnorm d).
+Proof.
+  exists (of_decimal d). apply to_of.
+Qed.
+
+Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d.
+Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
+
+Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'.
+Proof.
+intro H.
+apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                (Some (dnorm d)) (Some (dnorm d'))).
+now rewrite <- !to_of, H.
+Qed.
+
+Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'.
+Proof.
+split. apply of_inj. intros E. rewrite <- of_decimal_dnorm, E.
+apply of_decimal_dnorm.
+Qed.
diff --git a/theories/Numbers/HexadecimalR.v b/theories/Numbers/HexadecimalR.v
new file mode 100644
index 0000000000..3a6e2c4992
--- /dev/null
+++ b/theories/Numbers/HexadecimalR.v
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+(** * HexadecimalR
+
+    Proofs that conversions between hexadecimal numbers and [R]
+    are bijections. *)
+
+Require Import Decimal DecimalFacts.
+Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ.
+Require Import HexadecimalQ Rdefinitions.
+
+Lemma of_to (q:IR) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
+Admitted.
+
+Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d).
+Admitted.
+
+(** Some consequences *)
+
+Lemma to_hexadecimal_inj q q' :
+  to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'.
+Proof.
+intros Hnone EQ.
+generalize (of_to q) (of_to q').
+rewrite <-EQ.
+revert Hnone; case to_hexadecimal; [|now simpl].
+now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
+Qed.
+
+Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm d).
+Proof.
+  exists (of_hexadecimal d). apply to_of.
+Qed.
+
+Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
+Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
+
+Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'.
+Proof.
+intro H.
+apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                (Some (dnorm d)) (Some (dnorm d'))).
+now rewrite <- !to_of, H.
+Qed.
+
+Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'.
+Proof.
+split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E.
+apply of_hexadecimal_dnorm.
+Qed.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index a4809a7513..ac82216474 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -284,6 +284,12 @@ Definition of_number (n : Number.number) : IR :=
   | Number.Hex h => of_hexadecimal h
   end.
 
+Definition IQmake_to_decimal num den :=
+  match den with
+  | 1%positive => None  (* this should be encoded as IRZ *)
+  | _ => IQmake_to_decimal num den
+  end.
+
 Definition to_decimal (n : IR) : option Decimal.decimal :=
   match n with
   | IRZ z =>
@@ -319,6 +325,12 @@ Definition to_decimal (n : IR) : option Decimal.decimal :=
   | _ => None
   end.
 
+Definition IQmake_to_hexadecimal num den :=
+  match den with
+  | 1%positive => None  (* this should be encoded as IRZ *)
+  | _ => IQmake_to_hexadecimal num den
+  end.
+
 Definition to_hexadecimal (n : IR) : option Hexadecimal.hexadecimal :=
   match n with
   | IRZ z =>
-- 
cgit v1.2.3