Add a parser/printer for extended-real integer constants (math-comp#1704)

Author: proux01

CHANGELOG_UNRELEASED.md

@@ -25,6 +25,13 @@
 - in `uniform_structure.v`:
   + lemma `continuous_injective_withinNx`
 
+- in `constructive_ereal.v`:
+  + variants `Ione`, `Idummy_placeholder`
+  + inductives `Inatmul`, `IEFin`
+  + definition `parse`, `print`
+  + number notations in scopes `ereal_dual_scope` and `ereal_scope`
+  + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:

reals/constructive_ereal.v

@@ -31,6 +31,12 @@ From mathcomp Require Import mathcomp_extra interval_inference.
 (* |               `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$| *)
 (* |                        |  | notation for `extended (R:Type)`           | *)
 (* |                 `r%:E` |==| injects real numbers into `\bar R`         | *)
+(* |                    - x |==| opposite of x : \bar R                     | *)
+(* |               0, 1, -1 |==| 0%R, 1%R%:E, - 1%R%:E                      | *)
+(* |               <number> |==| <number>%:R%:E with <number> a sequence    | *)
+(* |                        |  | of digits                                  | *)
+(* |              -<number> |==| - <number>%:R%:E with <number> a sequence  | *)
+(* |                        |  | of digits                                  | *)
 (* |        `+%E, -%E, *%E` |==| addition/opposite/multiplication for       | *)
 (* |                        |  | extended reals                             | *)
 (* |        `x^-1`, `x / y` |==| inverse and division for extended reals    | *)
@@ -59,6 +65,12 @@ From mathcomp Require Import mathcomp_extra interval_inference.
 (*                  \bar R == coproduct of R and {+oo, -oo};                  *)
 (*                            notation for extended (R:Type)                  *)
 (*                    r%:E == injects real numbers into \bar R                *)
+(*                     - x == opposite of x : \bar R                          *)
+(*                0, 1, -1 == 0%R, 1%R%:E, - 1%R%:E                           *)
+(*                <number> == <number>%:R%:E with <number> a sequence         *)
+(*                            of digits                                       *)
+(*               -<number> == - <number>%:R%:E with <number> a sequence       *)
+(*                            of digits                                       *)
 (*           +%E, -%E, *%E == addition/opposite/multiplication for extended   *)
 (*                            reals                                           *)
 (*             x^-1, x / y == inverse and division for extended reals         *)
@@ -582,6 +594,53 @@ Notation "x ^+ n" := (expe x%E n) : ereal_scope.
 Notation "x *+ n" := (ednatmul x%dE n) : ereal_dual_scope.
 Notation "x *+ n" := (enatmul x%E n) : ereal_scope.
 
+(**md Notation for constant numerals. This has been introduced so
+that, e.g., in the scope `ereal_scope`, `-<n>` is correctly parsed
+without requiring one writes `- <n>%:E`. See the Rocq reference manual
+for the `Number Notation` command
+and [PR #1704](https://github.com/math-comp/analysis/pull/1704)
+for more explanations. *)
+Variant Ione := IOne : Ione.
+Inductive Inatmul := INatmul : Ione -> nat -> Inatmul.
+Inductive IEFin := IEFinP : Inatmul -> IEFin | IEFinN : IEFin -> IEFin.
+Variant Idummy_placeholder :=.
+
+Definition parse (x : Number.int) : IEFin :=
+  match x with
+  | Number.IntDecimal (Decimal.Pos u) => IEFinP (INatmul IOne (Nat.of_uint u))
+  | Number.IntDecimal (Decimal.Neg u) =>
+      IEFinN (IEFinP (INatmul IOne (Nat.of_uint u)))
+  | Number.IntHexadecimal (Hexadecimal.Pos u) =>
+      IEFinP (INatmul IOne (Nat.of_hex_uint u))
+  | Number.IntHexadecimal (Hexadecimal.Neg u) =>
+      IEFinN (IEFinP (INatmul IOne (Nat.of_hex_uint u)))
+  end.
+
+Definition print (x : IEFin) : option Number.int :=
+  match x with
+  | IEFinP (INatmul IOne n) =>
+      Some (Number.IntDecimal (Decimal.Pos (Nat.to_uint n)))
+  | IEFinN (IEFinP (INatmul IOne n)) =>
+      Some (Number.IntDecimal (Decimal.Neg (Nat.to_uint n)))
+  | _ => None
+  end.
+
+Arguments GRing.one {_}.
+#[warnings="-via-type-remapping,-via-type-mismatch"]
+Number Notation Idummy_placeholder parse print (via IEFin
+  mapping [[EFin] => IEFinP, [oppe] => IEFinN,
+           [GRing.natmul] => INatmul, [GRing.one] => IOne])
+  : ereal_scope.
+#[warnings="-via-type-remapping,-via-type-mismatch"]
+Number Notation Idummy_placeholder parse print (via IEFin
+  mapping [[EFin] => IEFinP, [oppe] => IEFinN,
+           [GRing.natmul] => INatmul, [GRing.one] => IOne])
+  : ereal_dual_scope.
+Arguments GRing.one : clear implicits.
+
+Notation "- 1" := (oppe 1 : dual_extended _) : ereal_dual_scope.
+Notation "- 1" := (oppe 1) : ereal_scope.
+
 Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope.
 Notation "\- f" := (fun x => - f x)%E : ereal_scope.
 Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope.
@@ -684,10 +743,10 @@ Proof. by rewrite lee_fin ler0N1. Qed.
 Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.
 Proof. by rewrite lte_fin ltr0N1. Qed.
 
-Lemma lteN10 : - 1%E < 0 :> \bar R.
+Lemma lteN10 : -1 < 0 :> \bar R.
 Proof. by rewrite lte_fin ltrN10. Qed.
 
-Lemma leeN10 : - 1%E <= 0 :> \bar R.
+Lemma leeN10 : -1 <= 0 :> \bar R.
 Proof. by rewrite lee_fin lerN10. Qed.
 
 Lemma lte0n n : (0 < n%:R%:E :> \bar R) = (0 < n)%N.
@@ -1273,13 +1332,13 @@ Proof. by move=> rreal; rewrite muleC real_mulrNy. Qed.
 
 Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
 
-Lemma mulN1e x : (- 1%E) * x = - x.
+Lemma mulN1e x : -1 * x = - x.
 Proof.
 by case: x => [r| |]/=;
   rewrite /mule ?mulN1r// eqe oppr_eq0 oner_eq0/= lte_fin oppr_gt0 ltr10.
 Qed.
 
-Lemma muleN1 x : x * (- 1%E) = - x. Proof. by rewrite muleC mulN1e. Qed.
+Lemma muleN1 x : x * -1 = - x. Proof. by rewrite muleC mulN1e. Qed.
 
 Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0.
 Proof.
@@ -2311,7 +2370,7 @@ Qed.
 Lemma iter_mule n x y : iter n ( *%E x) y = x ^+ n * y.
 Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.
 
-HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1%E mule
+HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1 mule
   muleA muleC mul1e.
 
 Lemma muleCA : left_commutative ( *%E : \bar R -> \bar R -> \bar R ).

theories/ftc.v

@@ -99,7 +99,7 @@ apply: cvg_at_right_left_dnbhs.
     by rewrite -EFinD addrAC subrr add0r.
   have nice_E y : nicely_shrinking y (E y).
     split=> [n|]; first exact: measurable_itv.
-    exists (2, fun n => PosNum (d_gt0 n)); split => //= [n z|n].
+    exists (2%R, fun n => PosNum (d_gt0 n)); split => //= [n z|n].
       rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->].
       by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl.
     rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
@@ -153,7 +153,7 @@ apply: cvg_at_right_left_dnbhs.
     by rewrite ltrDl Nd_gt0 -EFinD opprD addrA subrr add0r.
   have nice_E y : nicely_shrinking y (E y).
     split=> [n|]; first exact: measurable_itv.
-    exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=.
+    exists (2%R, (fun n => PosNum (Nd_gt0 n))); split => //=.
       by rewrite -oppr0; exact: cvgN.
     move=> n z.
       rewrite /E/= in_itv/= /ball/= => /andP[yz zy].

theories/kernel.v

@@ -1666,7 +1666,7 @@ HB.instance Definition _ :=
 
 Let measure_uub : measure_fam_uub kernel_snd.
 Proof.
-exists 2 => /= -[x y].
+exists 2%R => /= -[x y].
 rewrite /kernel_snd/= (@le_lt_trans _ _ 1%:E) ?lte1n//.
 exact: sprob_kernel_le1.
 Qed.