ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contrib/omega vers theories/ZArith

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

8 files changed, 144 insertions, 8 deletions

diff --git a/.depend.coq b/.depend.coq
index eb774f7956..e9f6c7de7c 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -28,10 +28,7 @@ contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
 contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
-contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/OmegaSyntax.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
@@ -46,7 +43,7 @@ theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
 theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo contrib/omega/Zpower.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
 theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo
@@ -117,6 +114,9 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
 theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
 theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo
 theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo
diff --git a/Makefile b/Makefile
index 65046fa90a..8117134042 100644
--- a/Makefile
+++ b/Makefile
@@ -396,7 +396,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/ZArith.vo      theories/ZArith/auxiliary.vo \
 	 theories/ZArith/ZArith_dec.vo  theories/ZArith/fast_integer.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
-	 theories/ZArith/Zhints.vo
+	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
+	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
@@ -493,9 +494,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo				\
 	contrib/correctness/Tuples.vo
 #	contrib/correctness/ProgramsExtraction.vo			
 
-OMEGAVO = contrib/omega/Omega.vo       contrib/omega/Zlogarithm.vo \
-          contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
-          contrib/omega/Zcomplements.vo
+OMEGAVO = contrib/omega/Omega.vo  	contrib/omega/OmegaSyntax.vo
 
 ROMEGAVO = contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo 
 
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 65571855e1..5935555869 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -84,6 +84,15 @@ Intros Hn; Elim Hn; Intros.
 Rewrite -> H1; Apply H.
 Save.
 
+Lemma inject_nat_set :
+  (P:Z->Set)((n:nat)(P (inject_nat n))) -> 
+    (x:Z) `0 <= x` -> (P x).
+Intros.
+Specialize (inject_nat_complete_inf x H0).
+Intros Hn; Elim Hn; Intros.
+Rewrite -> p; Apply H.
+Save.
+
 Lemma ZERO_le_inj :
   (n:nat) `0 <= (inject_nat n)`.
 Induction n; Simpl; Intros;
@@ -102,6 +111,17 @@ Intros; Apply inject_nat_prop;
 | Assumption].
 Save.
 
+Lemma natlike_rec : (P:Z->Set) (P `0`) ->
+  ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
+  (x:Z) `0 <= x` -> (P x).
+Intros; Apply inject_nat_set;
+[ Induction n;
+  [ Simpl; Assumption
+  | Intros; Rewrite -> (inj_S n0);
+    Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ]
+| Assumption].
+Save.
+
 Lemma Z_lt_induction : 
   (P:Z->Prop)
      ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
@@ -131,3 +151,33 @@ Apply Zgt_S_le. Apply Zlt_gt. Intuition.
 
 Assumption.
 Save.
+
+Lemma Z_lt_rec : 
+  (P:Z->Set)
+     ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
+  -> (x:Z)`0 <= x`->(P x).
+Proof.
+Intros P H x Hx.
+Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y).
+Intro.
+Apply (H0 (Zs x)).
+Auto with zarith.
+
+Split; [ Assumption | Exact (Zlt_n_Sn x) ].
+
+Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec.
+Intros.
+Absurd `0 <= 0`; Try Assumption.
+Apply Zgt_not_le.
+Apply Zgt_le_trans with m:=y.
+Apply Zlt_gt.
+Intuition. Intuition.
+
+Intros. Apply H. Intros.
+Apply (H1 H0).
+Split; [ Intuition | Idtac ].
+Apply Zlt_le_trans with y. Intuition.
+Apply Zgt_S_le. Apply Zlt_gt. Intuition.
+
+Assumption.
+Save.
diff --git a/contrib/omega/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 90d1f59408..69ce3b6f89 100644
--- a/contrib/omega/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -303,4 +303,57 @@ NewDestruct a;
 ].
 Save.
 
+Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z)
+  { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }.
+Proof.
+Intros b Hb a.
+Elim (Z_le_gt_dec `0` b);Intro Hb'.
+Cut `b>0`;[Intro Hb''|Omega].
+Rewrite Zabs_eq;[Apply Zdiv_eucl;Assumption|Assumption].
+Cut `-b>0`;[Intro Hb''|Omega].
+Elim (Zdiv_eucl Hb'' a);Intros qr.
+Elim qr;Intros q r Hqr.
+Exists (pair ? ? `-q` r).
+Elim Hqr;Intros.
+Split.
+Rewrite <- Zmult_Zopp_left;Assumption.
+Rewrite Zabs_non_eq;[Assumption|Omega].
+Save.
+
 End diveucl.
+
+(* Two more induction principles upon Z. *)
+
+Theorem Z_lt_abs_rec : (P: Z -> Set)
+  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Intros P HP p.
+LetTac Q:=[z]`0<=z`->(P z)*(P `-z`).
+Cut (Q `|p|`);[Intros|Apply (Z_lt_rec Q);Auto with zarith].
+Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
+Unfold Q;Clear Q;Intros.
+Apply pair;Apply HP.
+Rewrite Zabs_eq;Auto;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Rewrite Zabs_non_eq;Auto with zarith.
+Rewrite Zopp_Zopp;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Qed.
+
+Theorem Z_lt_abs_induction : (P: Z -> Prop)
+  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Intros P HP p.
+LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`).
+Cut (Q `|p|`);[Intros|Apply (Z_lt_induction Q);Auto with zarith].
+Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
+Unfold Q;Clear Q;Intros.
+Split;Apply HP.
+Rewrite Zabs_eq;Auto;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Rewrite Zabs_non_eq;Auto with zarith.
+Rewrite Zopp_Zopp;Intros.
+Elim (H `|m|`);Intros;Auto with zarith.
+Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+Qed.
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index d54d1a0a26..19f71b3221 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -69,6 +69,7 @@ Hints Resolve
   Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *)
   Zle_reg_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *)
   Zle_reg_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *)
+  Zabs_pos (* :(x:Z)`0 <= |x|` *)
   
   (* B) Irreversible simplification lemmas : Probably to be declared as *)
   (* hints, when no other simplification is possible *)
diff --git a/contrib/omega/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 45ad93aba0..45ad93aba0 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
diff --git a/contrib/omega/Zpower.v b/theories/ZArith/Zpower.v
index 1d97275736..1d97275736 100644
--- a/contrib/omega/Zpower.v
+++ b/theories/ZArith/Zpower.v
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 7eb1e37c23..bdb56fb910 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -28,6 +28,14 @@ Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
 Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
 Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
 
+(* Sign function *)
+Definition Zsgn [z:Z] : Z :=
+  Cases z of 
+     ZERO   => ZERO
+  | (POS p) => (POS xH)
+  | (NEG p) => (NEG xH)
+  end.
+
 (*s Absolu function *)
 Definition absolu [x:Z] : nat :=
   Cases x of
@@ -50,6 +58,31 @@ NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Save.
 
+Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
+Proof.
+NewDestruct x; Auto with arith.
+Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
+Save.
+
+Lemma Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
+Proof.
+NewDestruct x;Auto with arith.
+Save.
+
+Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
+NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Save.
+
+Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
+Proof.
+Destruct x;Intros;Rewrite Zmult_sym;Auto with arith.
+Save.
+
+Lemma Zabs_Zsgn: (x:Z)(Zabs x)=(Zmult (Zsgn x) x).
+Proof.
+Destruct x;Intros;Auto with arith.
+Qed.
+
 (*s From nat to Z *)
 Definition inject_nat := 
   [x:nat]Cases x of