BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)

 - In fact, Bind Scope has no retrospective effect. Since we don't want
  it inside functor, we use it late, and hence we are forced to use manual
  "Arguments Scope" commands.
 - Added syntax for power in BigN / BigZ / BigQ.
 - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq)
   as in QArith. Display of a rational numeral is hence either an integer
   (constructor BigQ.Qz) or something like 6756 # 8798.
 - Fix of function BigQ.Qred that was not simplifing (67#1) into 67.
 - More tests in test-suite/output/NumbersSyntax.v

A nice one not in the test-suite:

Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)).
     = 1
     : bigQ
Finished transaction in 3. secs (3.284206u,0.004s)

:-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 63 insertions, 43 deletions

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index eb0237f4a..d0cf499ab 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -45,13 +45,37 @@ Delimit Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with BigQ.t.
 Bind Scope bigQ_scope with BigQ.t_.
-
-(** BUG: the previous Bind Scope don't seem to work, and idem with BigN/BigZ.
-    For instance "Check (BigQ.opp 10)" fails when bigQ_scope is closed.
-    (whereas "Check (Int31.add31 10 10)" is ok). Something with modules ?
-    Adding an Arguments Scope helps, but this isn't a satisfactory solution.
-*)
-
+(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
+Arguments Scope BigQ.Qz [bigZ_scope].
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].
+Arguments Scope BigQ.to_Q [bigQ_scope].
+Arguments Scope BigQ.red [bigQ_scope].
+Arguments Scope BigQ.opp [bigQ_scope].
+Arguments Scope BigQ.inv [bigQ_scope].
+Arguments Scope BigQ.square [bigQ_scope].
+Arguments Scope BigQ.add [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.lt [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.le [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.compare [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.min [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.max [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq_bool [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_pos [bigQ_scope positive_scope].
+Arguments Scope BigQ.power [bigQ_scope Z_scope].
+Arguments Scope BigQ.inv_norm [bigQ_scope].
+Arguments Scope BigQ.add_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_norm [bigQ_scope bigQ_scope].
+
+(** As in QArith, we use [#] to denote fractions *)
+Notation "p # q" := (BigQ.Qq p q) (at level 55, no associativity) : bigQ_scope.
 Infix "+" := BigQ.add : bigQ_scope.
 Infix "-" := BigQ.sub : bigQ_scope.
 Notation "- x" := (BigQ.opp x) : bigQ_scope.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 59bd57084..efe76d916 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -193,20 +193,32 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  intros H H'; rewrite H in H'; discriminate.
  Qed.
 
+ (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)
+
+ Definition check_int n d :=
+  match N.compare N.one d with
+  | Lt => Qq n d
+  | Eq => Qz n
+  | Gt => zero  (* n/0 encodes 0 *)
+  end.
+
+ Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d].
+ Proof.
+ intros; unfold check_int.
+ nzsimpl.
+ destr_zcompare.
+ simpl. rewrite <- H; qsimpl. congruence.
+ reflexivity.
+ qsimpl. exfalso. generalize (N.spec_pos d); romega.
+ Qed.
+
  (** Normalisation function *)
 
  Definition norm n d : t :=
   let gcd := N.gcd (Zabs_N n) d in
   match N.compare N.one gcd with
-  | Lt =>
-    let n := Z.div n (Z_of_N gcd) in
-    let d := N.div d gcd in
-    match N.compare d N.one with
-    | Gt => Qq n d
-    | Eq => Qz n
-    | Lt => zero
-    end
-  | Eq => Qq n d
+  | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd)
+  | Eq => check_int n d
   | Gt => zero (* gcd = 0 => both numbers are 0 *)
   end.
 
@@ -217,29 +229,19 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hq := N.spec_pos q).
  nzsimpl.
  destr_zcompare.
+ (* Eq *)
+ rewrite strong_spec_check_int; reflexivity.
+ (* Lt *)
+ rewrite strong_spec_check_int.
  qsimpl.
-
- simpl_ndiv.
- destr_zcompare.
- qsimpl.
- rewrite H1 in *; rewrite Zdiv_0_l in H0; discriminate.
- rewrite N_to_Z2P; auto.
- simpl_zdiv; nzsimpl.
- rewrite Zgcd_div_swap0, H0; romega.
-
- qsimpl.
- assert (0 < N.to_Z q / Zgcd (Z.to_Z p) (N.to_Z q))%Z.
-  apply Zgcd_div_pos; romega.
- romega.
-
- qsimpl.
- simpl_ndiv in *; nzsimpl; romega.
+ simpl_ndiv in *; nzsimpl.
+ generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). omega.
  simpl_ndiv in *.
- rewrite H1, Zdiv_0_l in H2; elim H2; auto.
+ rewrite H0 in *. rewrite Zdiv_0_l in H1; elim H1; auto.
  rewrite 2 N_to_Z2P; auto.
  simpl_ndiv; simpl_zdiv; nzsimpl.
  apply Zgcd_div_swap0; romega.
-
+ (* Gt *)
  qsimpl.
  assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z).
   generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega.
@@ -256,28 +258,22 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hp := N.spec_pos (Zabs_N p)).
  assert (Hq := N.spec_pos q).
  nzsimpl.
- destr_zcompare.
+ destr_zcompare; rewrite ?strong_spec_check_int.
  (* Eq *)
  simpl.
  destr_neq_bool; nzsimpl; simpl; auto.
  intros.
  rewrite N_to_Z2P; auto.
  (* Lt *)
- simpl_ndiv.
- destr_zcompare.
- qsimpl; auto.
- qsimpl.
  qsimpl.
- simpl_zdiv; nzsimpl.
  rewrite N_to_Z2P; auto.
- clear H1.
- simpl_ndiv; nzsimpl.
+ simpl_zdiv; simpl_ndiv in *; nzsimpl.
  rewrite Zgcd_1_rel_prime.
  destruct (Z_lt_le_dec 0 (N.to_Z q)).
  apply Zis_gcd_rel_prime; auto with zarith.
  apply Zgcd_is_gcd.
  replace (N.to_Z q) with 0%Z in * by romega.
- rewrite Zdiv_0_l in H0; discriminate.
+ simpl in H0; elim H0; auto.
  (* Gt *)
  simpl; auto with zarith.
  Qed.