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

1 files changed, 83 insertions, 13 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 73cc5c21b..aa62ae76b 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -63,24 +63,31 @@ Arguments Scope BigZ.min [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.max [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.power_pos [bigZ_scope positive_scope].
+Arguments Scope BigZ.power [bigZ_scope N_scope].
 Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 
 Local Notation "0" := BigZ.zero : bigZ_scope.
+Local Notation "1" := BigZ.one : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
 Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
 Infix "*" := BigZ.mul : bigZ_scope.
 Infix "/" := BigZ.div : bigZ_scope.
-Infix "^" := BigZ.power_pos : bigZ_scope.
+Infix "^" := BigZ.power : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
+Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.
 Infix "<=" := BigZ.le : bigZ_scope.
 Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
 Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
+Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope.
+Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
+Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope.
 
@@ -118,31 +125,94 @@ Qed.
 (** [BigZ] is a ring *)
 
 Lemma BigZring :
- ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
+ ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
-exact BigZ.add_0_l.
-exact BigZ.add_comm.
-exact BigZ.add_assoc.
-exact BigZ.mul_1_l.
-exact BigZ.mul_comm.
-exact BigZ.mul_assoc.
+exact BigZ.add_0_l. exact BigZ.add_comm. exact BigZ.add_assoc.
+exact BigZ.mul_1_l. exact BigZ.mul_comm. exact BigZ.mul_assoc.
 exact BigZ.mul_add_distr_r.
 symmetry. apply BigZ.add_opp_r.
 exact BigZ.add_opp_diag_r.
 Qed.
 
-Add Ring BigZr : BigZring.
+Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.
+Proof. now apply BigZ.eqb_eq. Qed.
 
-(** [BigZ] benefits from an "order" tactic *)
+Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power.
+Proof.
+constructor.
+intros. red. rewrite BigZ.spec_power. unfold id.
+destruct Zpower_theory as [EQ]. rewrite EQ.
+destruct n; simpl. reflexivity.
+induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto.
+Qed.
+
+Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
+ (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b).
+Proof.
+constructor. unfold id. intros a b.
+BigZ.zify.
+generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+BigZ.zify. auto with zarith.
+intros NEQ.
+generalize (BigZ.spec_div_eucl a b).
+generalize (Z_div_mod_full [a] [b] NEQ).
+destruct BigZ.div_eucl as (q,r), Zdiv_eucl as (q',r').
+intros (EQ,_). injection 1. intros EQr EQq.
+BigZ.zify. rewrite EQr, EQq; auto.
+Qed.
+
+(** Detection of constants *)
+
+Ltac isBigZcst t :=
+ match t with
+ | BigZ.Pos ?t => isBigNcst t
+ | BigZ.Neg ?t => isBigNcst t
+ | BigZ.zero => constr:true
+ | BigZ.one => constr:true
+ | BigZ.minus_one => constr:true
+ | _ => constr:false
+ end.
+
+Ltac BigZcst t :=
+ match isBigZcst t with
+ | true => constr:t
+ | false => constr:NotConstant
+ end.
+
+(** Registration for the "ring" tactic *)
+
+Add Ring BigZr : BigZring
+ (decidable BigZeqb_correct,
+  constants [BigZcst],
+  power_tac BigZpower [Ncst],
+  div BigZdiv).
+
+Section TestRing.
+Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
+Proof.
+intros. ring_simplify. reflexivity.
+Qed.
+Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0.
+Proof.
+intros. ring_simplify. reflexivity.
+Qed.
+End TestRing.
+
+(** [BigZ] also benefits from an "order" tactic *)
 
 Ltac bigZ_order := BigZ.order.
 
-Section Test.
+Section TestOrder.
 Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
 Proof. bigZ_order. Qed.
-End Test.
+End TestOrder.
+
+(** We can use at least a bit of (r)omega by translating to [Z]. *)
 
-(** Todo: tactic translating from [BigZ] to [Z] + omega *)
+Section TestOmega.
+Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
+Proof. intros x y. BigZ.zify. omega. Qed.
+End TestOmega.
 
 (** Todo: micromega *)