More improvements of BigN, BigZ, BigQ:

 - ring/field: detection of constants for ring/field,
   detection of power, potential use of euclidean division.
 - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
 - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
   By the way, BigN.zify could still be improved (no insertion of positivity
   hyps yet, unlike the original zify).
 - debug of BigQ.qify (autorewrite was looping on spec_0).
 - for BigQ, start of a generic functor of properties QProperties.
 - BigQ now implements OrderedType, TotalOrder, and contains facts
   about min and max.

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

4 files changed, 145 insertions, 15 deletions

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 64d2e58e62..9a4d7a9b04 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -59,23 +59,30 @@ Arguments Scope BigN.min [bigN_scope bigN_scope].
 Arguments Scope BigN.max [bigN_scope bigN_scope].
 Arguments Scope BigN.eq_bool [bigN_scope bigN_scope].
 Arguments Scope BigN.power_pos [bigN_scope positive_scope].
+Arguments Scope BigN.power [bigN_scope N_scope].
 Arguments Scope BigN.sqrt [bigN_scope].
 Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
 Arguments Scope BigN.modulo [bigN_scope bigN_scope].
 Arguments Scope BigN.gcd [bigN_scope bigN_scope].
 
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
+Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Infix "+" := BigN.add : bigN_scope.
 Infix "-" := BigN.sub : bigN_scope.
 Infix "*" := BigN.mul : bigN_scope.
 Infix "/" := BigN.div : bigN_scope.
-Infix "^" := BigN.power_pos : bigN_scope.
+Infix "^" := BigN.power : bigN_scope.
 Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
+Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
 Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
 Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
+Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope.
+Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope.
+Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
 
@@ -92,23 +99,130 @@ Qed.
 
 (** [BigN] is a semi-ring *)
 
-Lemma BigNring :
- semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
+Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq.
 Proof.
 constructor.
-exact BigN.add_0_l.
-exact BigN.add_comm.
-exact BigN.add_assoc.
-exact BigN.mul_1_l.
-exact BigN.mul_0_l.
-exact BigN.mul_comm.
-exact BigN.mul_assoc.
-exact BigN.mul_add_distr_r.
+exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc.
+exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
+exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
 Qed.
 
-Add Ring BigNr : BigNring.
+Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y.
+Proof. now apply BigN.eqb_eq. Qed.
 
-(** We benefit from an "order" tactic *)
+Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power.
+Proof.
+constructor.
+intros. red. rewrite BigN.spec_power. unfold id.
+destruct Zpower_theory as [EQ]. rewrite EQ.
+destruct n; simpl. reflexivity.
+induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
+Qed.
+
+Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
+ (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b).
+Proof.
+constructor. unfold id. intros a b.
+BigN.zify.
+generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+BigN.zify. auto with zarith.
+intros NEQ.
+generalize (BigN.spec_div_eucl a b).
+generalize (Z_div_mod_full [a] [b] NEQ).
+destruct BigN.div_eucl as (q,r), Zdiv_eucl as (q',r').
+intros (EQ,_). injection 1. intros EQr EQq.
+BigN.zify. rewrite EQr, EQq; auto.
+Qed.
+
+
+(** Detection of constants *)
+
+Local Open Scope list_scope.
+
+Ltac isInt31cst_lst l :=
+ match l with
+ | nil => constr:true
+ | ?t::?l => match t with
+               | D1 => isInt31cst_lst l
+               | D0 => isInt31cst_lst l
+               | _ => constr:false
+             end
+ | _ => constr:false
+ end.
+
+Ltac isInt31cst t :=
+ match t with
+ | I31 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
+       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
+       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30 =>
+    let l :=
+      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
+      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
+      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
+    in isInt31cst_lst l
+ | Int31.On => constr:true
+ | Int31.In => constr:true
+ | Int31.Tn => constr:true
+ | Int31.Twon => constr:true
+ | _ => constr:false
+ end.
+
+Ltac isStaticWordCst t :=
+ match t with
+ | W0 => constr:true
+ | WW ?t1 ?t2 =>
+   match isStaticWordCst t1 with
+   | false => constr:false
+   | true => isStaticWordCst t2
+   end
+ | _ => isInt31cst t
+ end.
+
+Ltac isBigNcst t :=
+ match t with
+ | BigN.N0 ?t => isStaticWordCst t
+ | BigN.N1 ?t => isStaticWordCst t
+ | BigN.N2 ?t => isStaticWordCst t
+ | BigN.N3 ?t => isStaticWordCst t
+ | BigN.N4 ?t => isStaticWordCst t
+ | BigN.N5 ?t => isStaticWordCst t
+ | BigN.N6 ?t => isStaticWordCst t
+ | BigN.Nn ?n ?t => match isnatcst n with
+   | true => isStaticWordCst t
+   | false => constr:false
+   end
+ | BigN.zero => constr:true
+ | BigN.one => constr:true
+ | _ => constr:false
+ end.
+
+Ltac BigNcst t :=
+ match isBigNcst t with
+ | true => constr:t
+ | false => constr:NotConstant
+ end.
+
+Ltac Ncst t :=
+ match isNcst t with
+ | true => constr:t
+ | false => constr:NotConstant
+ end.
+
+(** Registration for the "ring" tactic *)
+
+Add Ring BigNr : BigNring
+ (decidable BigNeqb_correct,
+  constants [BigNcst],
+  power_tac BigNpower [Ncst],
+  div BigNdiv).
+
+Section TestRing.
+Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
+intros. ring_simplify. reflexivity.
+Qed.
+End TestRing.
+
+(** We benefit also from an "order" tactic *)
 
 Ltac bigN_order := BigN.order.
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 6257e8e630..8240604c2f 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1780,6 +1780,20 @@ let _ =
   pp " intros; rewrite Zpower_1_r; auto.";
   pp " Qed.";
   pp "";
+
+  pr " Definition power x (n:N) := match n with";
+  pr "  | BinNat.N0 => one";
+  pr "  | BinNat.Npos p => power_pos x p";
+  pr " end.";
+  pr "";
+
+  pr " Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.";
+  pa " Admitted.";
+  pp " Proof.";
+  pp " destruct n; simpl. apply (spec_1 w0_spec).";
+  pp " apply spec_power_pos.";
+  pp " Qed.";
+  pr "";
   pr "";
 
   pr " (***************************************************************)";
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 586e4992e2..116927766e 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -49,6 +49,7 @@ Module Type NType.
  Parameter mul : t -> t -> t.
  Parameter square : t -> t.
  Parameter power_pos : t -> positive -> t.
+ Parameter power : t -> N -> t.
  Parameter sqrt : t -> t.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
@@ -68,6 +69,7 @@ Module Type NType.
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
  Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
  Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
  Parameter spec_div_eucl: forall x y,
   let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 9e3674a23d..49a60916aa 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -17,7 +17,7 @@ Module NTypeIsNAxioms (Import N : NType').
 Hint Rewrite
  spec_0 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
- spec_max spec_min
+ spec_max spec_min spec_power_pos spec_power
  : nsimpl.
 Ltac nsimpl := autorewrite with nsimpl.
 Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence.
@@ -252,5 +252,5 @@ Qed.
 End NTypeIsNAxioms.
 
 Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N
+ <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N
  := N <+ NTypeIsNAxioms.