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

3 files changed, 0 insertions, 956 deletions

diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
deleted file mode 100644
index 90d1f5940..000000000
--- a/contrib/omega/Zcomplements.v
+++ /dev/null
@@ -1,306 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require ZArith.
-Require Omega.
-Require Wf_nat.
-
-(* Multiplication by a number >0 preserves Zcompare. It also perserves
-  Zle, Zlt, Zge, Zgt *)
-
-Implicit Arguments On.
-
-Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`.
-NewDestruct x; NewDestruct y; Auto.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Simpl; Intros; Discriminate H.
-Save.
-
-Lemma Zeq_Zminus : (x,y:Z)x=y -> `x-y = 0`.
-Intros; Omega.
-Save.
-
-Lemma Zminus_Zeq : (x,y:Z)`x-y=0` -> x=y.
-Intros; Omega.
-Save.
-
-Lemma Zmult_Zminus_distr_l : (x,y,z:Z)`(x-y)*z = x*z - y*z`.
-Intros; Unfold Zminus.
-Rewrite <- Zopp_Zmult.
-Apply Zmult_plus_distr_l.
-Save.
-
-Lemma  Zmult_Zminus_distr_r : (x,y,z:Z)`z*(x-y) = z*x - z*y`.
-Intros; Rewrite (Zmult_sym z `x-y`).
-Rewrite (Zmult_sym  z x).
-Rewrite (Zmult_sym z y).
-Apply Zmult_Zminus_distr_l.
-Save.
-
-Lemma Zmult_reg_left : (x,y,z:Z)`z>0` -> `z*x=z*y` -> x=y.
-Intros.
-Generalize (Zeq_Zminus H0).
-Intro.
-Apply Zminus_Zeq.
-Rewrite <- (Zmult_Zminus_distr_r x y z) in H1. 
-Elim (Zmult_zero H1).
-Omega.
-Trivial.
-Save.
-
-Lemma Zmult_reg_right : (x,y,z:Z)`z>0` -> `x*z=y*z` -> x=y.
-Intros x y z Hz.
-Rewrite (Zmult_sym x z).
-Rewrite (Zmult_sym y z).
-Intro; Apply Zmult_reg_left with z; Assumption.
-Save.
-    
-Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`.
-Intro; Unfold Zpred; Omega.
-Save.
-
-Lemma Zlt_Zplus : 
-  (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`.
-Intros; Omega.
-Save.
-
-Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`.
-
-Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro;
-Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`;
-[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption
-| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r);
-  Repeat Rewrite Zmult_n_1;
-  Intro; Apply Zlt_Zplus; Assumption
-| Assumption ].
-Save.
-
-Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0`  -> `x*z < y*z` -> `x < y`.
-Intros x y z H; Rewrite (Zs_pred z).
-Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`.
-Simpl; Do 2 Rewrite Zmult_n_1; Auto 1.
-Unfold Zs.
-Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r.
-Repeat Rewrite Zmult_n_1.
-Omega. (* Auto with zarith. *)
-Unfold Zpred; Omega.
-Save.
-
-Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`.
-Intros x y z Hz Hxy.
-Elim (Zle_lt_or_eq x y Hxy).
-Intros; Apply Zlt_le_weak.
-Apply Zlt_Zmult_right; Trivial.
-Intros; Apply Zle_refl.
-Rewrite H; Trivial.
-Save.
-
-Lemma Zle_Zmult_right2 :  (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`.
-Intros x y z Hz Hxy.
-Elim (Zle_lt_or_eq `x*z` `y*z` Hxy).
-Intros; Apply Zlt_le_weak.
-Apply Zlt_Zmult_right2 with z; Trivial.
-Intros; Apply Zle_refl.
-Apply Zmult_reg_right with z; Trivial.
-Save.
-
-Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`.
-
-Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; 
-[ Assumption | Apply Zgt_lt ; Assumption ].
-Save.
-
-Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`.
-
-Intros;
-Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y);
-Apply Zlt_Zmult_right; Assumption.
-Save.
-
-Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`.
-Intros;
-Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y);
-Apply Zgt_Zmult_right; Assumption.
-Save.
-
-Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`.
-
-Intros; Apply Zcompare_egal_dec;
-[ Intros; Apply Zlt_Zmult_right; Trivial
-| Intro Hxy; Apply [a,b:Z](let (t1,t2)=(Zcompare_EGAL a b) in t2);
-  Rewrite ((let (t1,t2)=(Zcompare_EGAL x y) in t1) Hxy); Trivial
-| Intros; Apply Zgt_Zmult_right; Trivial
-].
-Save.
-
-Theorem  Zcompare_Zmult_left : (x,y,z:Z)`z>0` -> `x ?= y`=`z*x ?= z*y`.
-Intros;
-Rewrite (Zmult_sym z x);
-Rewrite (Zmult_sym z y);
-Apply Zcompare_Zmult_right; Assumption.
-Save.
-
-
-Section diveucl.
-
-Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. 
-NewDestruct x.
-Left ; Split with ZERO; Reflexivity.
-
-NewDestruct p.
-Right ; Split with (POS p); Reflexivity.
-
-Left ; Split with (POS p); Reflexivity.
-
-Right ; Split with ZERO; Reflexivity.
-
-NewDestruct p.
-Right ; Split with (NEG (add xH p)).
-Rewrite NEG_xI.
-Rewrite NEG_add.
-Omega.
-
-Left ; Split with (NEG p); Reflexivity.
-
-Right ; Split with `-1`; Reflexivity.
-Save.
-
-(* The biggest power of 2 that is stricly less than a *)
-(* Easy to compute : replace all "1" of the binary representation by
-   "0", except the first "1" (or the first one :-) *)
-Fixpoint floor_pos [a : positive] : positive :=
-  Cases a of
-  | xH => xH
-  | (xO a') => (xO (floor_pos a'))
-  | (xI b') => (xO (floor_pos b'))
-  end.
-
-Definition floor := [a:positive](POS (floor_pos a)).
-
-Lemma floor_gt0 : (x:positive) `(floor x) > 0`.
-Intro.
-Compute.
-Trivial.
-Save.
-
-Lemma floor_ok : (a:positive) 
-  `(floor a) <=  (POS a) < 2*(floor a)`. 
-Unfold floor.
-Induction a.
-
-Intro p; Simpl.
-Repeat Rewrite POS_xI.
-Rewrite (POS_xO (xO (floor_pos p))). 
-Rewrite (POS_xO (floor_pos p)).
-Omega.
-
-Intro p; Simpl.
-Repeat Rewrite POS_xI.
-Rewrite (POS_xO (xO (floor_pos p))).
-Rewrite (POS_xO (floor_pos p)).
-Rewrite (POS_xO p).
-Omega.
-
-Simpl; Omega.
-Save.
-
-Lemma Zdiv_eucl_POS : (b:Z)`b > 0` -> (p:positive)
-  { qr:Z*Z | let (q,r)=qr in `(POS p)=b*q+r` /\ `0 <= r < b` }.
-
-Induction p.
-
-(* p => (xI p) *)
-(* Notez l'utilisation des nouveaux patterns Intro *)
-Intros p' ((q,r), (Hrec1, Hrec2)).
-Elim (Z_lt_ge_dec `2*r+1` b); 
-[ Exists `(2*q, 2*r+1)`;
-  Rewrite POS_xI;
-  Rewrite Hrec1;
-  Split; 
-  [ Rewrite Zmult_Zplus_distr; 
-    Rewrite Zplus_assoc_l;
-    Rewrite (Zmult_permute b `2`);
-    Reflexivity
-  | Omega ]
-| Exists `(2*q+1, 2*r+1-b)`;
-  Rewrite POS_xI;
-  Rewrite Hrec1;
-  Split; 
-  [ Do 2 Rewrite Zmult_Zplus_distr; 
-    Unfold Zminus;
-    Do 2 Rewrite Zplus_assoc_l;
-    Rewrite <- (Zmult_permute `2` b);
-    Generalize `b*q`; Intros; Omega
-  | Omega ]
-].
-
-(* p => (xO p) *)
-Intros p' ((q,r), (Hrec1, Hrec2)).
-Elim (Z_lt_ge_dec `2*r` b); 
-[ Exists `(2*q,2*r)`;
-  Rewrite POS_xO;
-  Rewrite Hrec1;
-  Split; 
-  [ Rewrite Zmult_Zplus_distr; 
-    Rewrite (Zmult_permute b `2`);
-    Reflexivity
-  | Omega ]
-| Exists `(2*q+1, 2*r-b)`;
-  Rewrite POS_xO;
-  Rewrite Hrec1;
-  Split; 
-  [ Do 2 Rewrite Zmult_Zplus_distr; 
-    Unfold Zminus;
-    Rewrite <- (Zmult_permute `2` b);
-    Generalize `b*q`; Intros; Omega
-  | Omega ]
-].
-(* xH *)
-Elim (Z_le_gt_dec `2` b);
-[ Exists `(0,1)`; Omega
-| Exists `(1,0)`; Omega 
-].
-Save.
-
-Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z)
-  { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }.
-NewDestruct a;
-
-[ (* a=0 *) Exists `(0,0)`; Omega
-| (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto
-| (* a = (NEG p) *) Intros; Elim (Zdiv_eucl_POS H p);
-  Intros (q,r) (Hp1, Hp2);
-  Elim (Z_le_gt_dec r `0`); 
-  [ Exists `(-q,0)`; Split;
-    [ Apply Zopp_intro; Simpl; Rewrite Hp1;
-      Rewrite Zero_right; 
-      Rewrite <- Zopp_Zmult;
-      Rewrite Zmult_Zopp_Zopp;
-      Generalize `b*q`; Intro; Omega 
-    | Omega
-    ]
-  | Exists `(-(q+1),b-r)`; Split;
-    [ Apply Zopp_intro;
-      Unfold Zminus; Simpl; Rewrite Hp1;
-      Repeat Rewrite Zopp_Zplus;
-      Repeat Rewrite <- Zopp_Zmult;
-      Rewrite Zmult_Zplus_distr;
-      Rewrite Zmult_Zopp_Zopp;
-      Rewrite Zplus_assoc_r;
-      Apply f_equal with f:=[c:Z]`b*q+c`;
-      Omega
-    | Omega ]
-  ]
-].
-Save.
-
-End diveucl.
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
deleted file mode 100644
index 45ad93aba..000000000
--- a/contrib/omega/Zlogarithm.v
+++ /dev/null
@@ -1,264 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(****************************************************************************)
-(*  The integer logarithms with base 2. There are three logarithms,	    *)
-(*    depending on the rounding of the real 2-based logarithm : 	    *)
-(*									    *)
-(*  Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1)			    *)
-(*  Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y			    *)
-(*  Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)	    *)
-(*									    *)
-(*  (Log_inf x) is the biggest integer that is smaller than (Log x)	    *)
-(*  (Log_inf x) is the smallest integer that is bigger than (Log x)	    *)
-(*  (Log_nearest x) is the integer nearest from (Log x). 		    *)
-(****************************************************************************)
-
-Require ZArith.
-Require Omega.
-Require Zcomplements.
-Require Zpower.
-
-Section Log_pos. (* Log of positive integers *)
-
-(* First we build log_inf and log_sup *)
-
-Fixpoint log_inf [p:positive] : Z :=  
-  Cases p of
-    xH => `0`	 				(* 1 *)
-  | (xO q) => (Zs (log_inf q))		(* 2n *)
-  | (xI q) => (Zs (log_inf q))		(* 2n+1 *)
-  end.
-Fixpoint log_sup [p:positive] : Z :=
-  Cases p of
-    xH => `0`					(* 1 *)
-  | (xO n) => (Zs (log_sup n)) 		(* 2n *)
-  | (xI n) => (Zs (Zs (log_inf n)))		(* 2n+1 *)
-  end.
-
-Hints Unfold log_inf log_sup.
-
-(* Then we give the specifications of log_inf and log_sup 
-  and prove their validity *)
-
-(* Hints Resolve ZERO_le_S : zarith. *)
-Hints Resolve Zle_trans : zarith.
-
-Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\
-  ` (two_p (log_inf x)) <= (POS x) < (two_p (Zs (log_inf x)))`.
-Induction x; Intros; Simpl;
-[ Elim H; Intros Hp HR; Clear H; Split;
-  [ Auto with zarith
-  | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp));
-    Rewrite (two_p_S (log_inf p) Hp);
-    Rewrite (two_p_S (log_inf p) Hp) in HR;
-    Rewrite (POS_xI p); Omega ]
-| Elim H; Intros Hp HR; Clear H; Split;
-  [ Auto with zarith
-  | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp));
-    Rewrite (two_p_S (log_inf p) Hp);
-    Rewrite (two_p_S (log_inf p) Hp) in HR;
-    Rewrite (POS_xO p); Omega ]
-| Unfold two_power_pos; Unfold shift_pos; Simpl; Omega 
-].
-Save.
-
-Definition log_inf_correct1 :=
-	[p:positive](proj1 ? ? (log_inf_correct p)).
-Definition log_inf_correct2 := 
-	[p:positive](proj2 ? ? (log_inf_correct p)).
-
-Opaque log_inf_correct1 log_inf_correct2.
-
-Hints Resolve log_inf_correct1 log_inf_correct2 : zarith.
-
-Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`.
-Induction p; Intros; Simpl; Auto with zarith.
-Save.
-
-(* For every p, either p is a power of two and (log_inf p)=(log_sup p)
-  either (log_sup p)=(log_inf p)+1 *)
-
-Theorem log_sup_log_inf : (p:positive)
-  either (POS p)=(two_p (log_inf p)) 
-  and_then (POS p)=(two_p (log_sup p))
-  or_else ` (log_sup p)=(Zs (log_inf p))`.
-
-Induction p; Intros;
-[ Elim H; Right; Simpl;
-  Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
-  Rewrite POS_xI; Unfold Zs; Omega
-| Elim H; Clear H; Intro Hif;
-  [ Left; Simpl;
-    Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
-    Rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0));
-    Rewrite <- (proj1 ? ? Hif); Rewrite <- (proj2 ? ? Hif);
-    Auto
-  | Right; Simpl;
-    Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
-    Rewrite POS_xO; Unfold Zs; Omega ]
-| Left; Auto ].
-Save.
-
-Theorem log_sup_correct2 : (x:positive)
-  ` (two_p (Zpred (log_sup x))) < (POS x) <= (two_p (log_sup x))`.
-
-Intro.
-Elim (log_sup_log_inf x).
-(* x is a power of two and log_sup = log_inf *)
-Intros (E1,E2); Rewrite E2.
-Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ].
-Intros (E1,E2); Rewrite E2.
-Rewrite <- (Zpred_Sn (log_inf x)).
-Generalize (log_inf_correct2 x); Omega.
-Save.
-
-Lemma log_inf_le_log_sup : 
-	(p:positive) `(log_inf p) <= (log_sup p)`.
-Induction p; Simpl; Intros; Omega.
-Save.
-
-Lemma log_sup_le_Slog_inf : 
-	(p:positive) `(log_sup p) <= (Zs (log_inf p))`.
-Induction p; Simpl; Intros; Omega.
-Save.
-
-(* Now it's possible to specify and build the Log rounded to the nearest *)
-
-Fixpoint log_near[x:positive] : Z :=
-  Cases x of 
-    xH => `0`
-  | (xO xH) => `1`
-  | (xI xH) => `2`
-  | (xO y)  => (Zs (log_near y))
-  | (xI y)  => (Zs (log_near y))
-  end.    
-
-Theorem log_near_correct1 : (p:positive)` 0 <= (log_near p)`.
-Induction p; Simpl; Intros; 
-[Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ].
-Intros; Apply Zle_le_S.
-Generalize H0; Elim p1; Intros; Simpl;
-    [ Assumption | Assumption | Apply ZERO_le_POS ].
-Intros; Apply Zle_le_S.
-Generalize H0; Elim p1; Intros; Simpl;
-    [ Assumption | Assumption | Apply ZERO_le_POS ].
-Save.
-
-Theorem log_near_correct2: (p:positive)
-  (log_near p)=(log_inf p)
-\/(log_near p)=(log_sup p).
-Induction p.
-Intros p0 [Einf|Esup].
-Simpl. Rewrite Einf.
-Case p0; [Left | Left | Right]; Reflexivity.
-Simpl; Rewrite Esup.
-Elim (log_sup_log_inf p0).
-Generalize (log_inf_le_log_sup p0).
-Generalize (log_sup_le_Slog_inf p0).
-Case p0; Auto with zarith.
-Intros; Omega.
-Case p0; Intros; Auto with zarith.
-Intros p0 [Einf|Esup].
-Simpl.
-Repeat Rewrite Einf.
-Case p0; Intros; Auto with zarith.
-Simpl.
-Repeat Rewrite Esup.
-Case p0; Intros; Auto with zarith.
-Auto.
-Save.
-
-(*******************
-Theorem log_near_correct: (p:positive)
-  `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))`
-  /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`.
-Intro.
-Induction p.
-Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)].
-Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup.
-Rewrite Einf1.
-Repeat Rewrite two_p_S.
-Case p0; [Left | Left | Right].
-
-Split.
-Simpl.
-Rewrite E1; Case p0; Try Reflexivity.
-Compute.
-Unfold log_near; Fold log_near.
-Unfold log_inf; Fold log_inf.
-Repeat Rewrite E1.
-Split.
-***********************************)
-
-End Log_pos.
-
-Section divers.
-
-(* Number of significative digits. *)
-
-Definition N_digits :=
-  [x:Z]Cases x of 
-       	  (POS p) => (log_inf p)
-        | (NEG p) => (log_inf p)
-	|  ZERO   => `0`
-       end.
-
-Lemma ZERO_le_N_digits : (x:Z) ` 0 <= (N_digits x)`.
-Induction x; Simpl;
-[ Apply Zle_n
-| Exact log_inf_correct1
-| Exact log_inf_correct1].
-Save.
-
-Lemma log_inf_shift_nat : 
-  (n:nat)(log_inf (shift_nat n xH))=(inject_nat n).
-Induction n; Intros;
-[ Try Trivial
-| Rewrite -> inj_S; Rewrite <- H; Reflexivity].
-Save.
-
-Lemma log_sup_shift_nat : 
-  (n:nat)(log_sup (shift_nat n xH))=(inject_nat n).
-Induction n; Intros;
-[ Try Trivial
-| Rewrite -> inj_S; Rewrite <- H; Reflexivity].
-Save.
-
-(* (Is_power p) means that p is a power of two *)
-Fixpoint Is_power[p:positive] : Prop :=
-  Cases p of
-    xH => True
-  | (xO q) => (Is_power q)
-  | (xI q) => False
-  end.
-
-Lemma Is_power_correct :
-  (p:positive) (Is_power p) <-> (Ex [y:nat](p=(shift_nat y xH))).
-
-Split; 
-[ Elim p; 
-   [ Simpl; Tauto
-   | Simpl; Intros; Generalize (H H0); Intro H1; Elim H1; Intros y0 Hy0;
-     Exists (S y0); Rewrite Hy0; Reflexivity
-   | Intro; Exists O; Reflexivity]
-| Intros; Elim H; Intros; Rewrite -> H0; Elim x; Intros; Simpl; Trivial].
-Save.
-
-Lemma Is_power_or : (p:positive) (Is_power p)\/~(Is_power p).
-Induction p;
-[ Intros; Right; Simpl; Tauto
-| Intros; Elim H; 
-   [ Intros; Left; Simpl; Exact H0
-   | Intros; Right; Simpl; Exact H0]
-| Left; Simpl; Trivial].
-Save.
-
-End divers.
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
deleted file mode 100644
index 1d9727573..000000000
--- a/contrib/omega/Zpower.v
+++ /dev/null
@@ -1,386 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require ZArith.
-Require Omega.
-Require Zcomplements.
-
-Section section1.
-
-(* (Zpower_nat z n) is the n-th power of x when n is an unary
-    integer (type nat) and z an signed integer (type Z) *) 
-
-Definition Zpower_nat := 
-  [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`).
- 
-(* Zpower_nat_is_exp says Zpower_nat is a morphism for
-   plus : nat->nat and Zmult : Z->Z *)
-
-Lemma Zpower_nat_is_exp : 
-  (n,m:nat)(z:Z)
-  `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`.
-
-Intros; Elim n; 
-[ Simpl; Elim (Zpower_nat z m); Auto with zarith
-| Unfold Zpower_nat; Intros;  Simpl; Rewrite H;
-  Apply Zmult_assoc].
-Save.
-
-(* (Zpower_nat z n) is the n-th power of x when n is an binary
-   integer (type positive) and z an signed integer (type Z) *) 
-
-Definition Zpower_pos := 
-  [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`).
-
-(* This theorem shows that powers of unary and binary integers
-   are the same thing, modulo the function convert : positive -> nat *)
-
-Theorem Zpower_pos_nat : 
-  (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)).
-
-Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert.
-Save.
-
-(* Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we
-   deduce that the function [n:positive](Zpower_pos z n) is a morphism
-   for add : positive->positive and Zmult : Z->Z *)
-
-Theorem Zpower_pos_is_exp : 
-  (n,m:positive)(z:Z) 
-  ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`.
-
-Intros.
-Rewrite -> (Zpower_pos_nat z n).
-Rewrite -> (Zpower_pos_nat z m).
-Rewrite -> (Zpower_pos_nat z (add n m)).
-Rewrite -> (convert_add n m).
-Apply Zpower_nat_is_exp.
-Save.
-
-Definition Zpower :=
-  [x,y:Z]Cases y of
-    (POS p) => (Zpower_pos x p)
-  | ZERO => `1`
-  | (NEG p) => `0`
-  end.
-
-Hints Immediate Zpower_nat_is_exp : zarith.
-Hints Immediate Zpower_pos_is_exp : zarith.
-Hints Unfold  Zpower_pos : zarith.
-Hints Unfold  Zpower_nat : zarith.
-
-Lemma Zpower_exp : (x:Z)(n,m:Z)
-  `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
-NewDestruct n; NewDestruct m; Auto with zarith.
-Simpl; Intros; Apply Zred_factor0.
-Simpl; Auto with zarith.
-Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
-Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
-Save.
-
-End section1.
-
-Hints Immediate Zpower_nat_is_exp : zarith.
-Hints Immediate Zpower_pos_is_exp : zarith.
-Hints Unfold  Zpower_pos : zarith.
-Hints Unfold  Zpower_nat : zarith.
-
-Section Powers_of_2.
-
-(* For the powers of two, that will be widely used, a more direct
-   calculus is possible. We will also prove some properties such
-   as (x:positive) x < 2^x that are true for all integers bigger
-   than 2 but more difficult to prove and useless. *)     
-
-(* shift n m computes 2^n * m, or m shifted by n positions *)
-
-Definition shift_nat := 
-  [n:nat][z:positive](iter_nat n positive xO z). 
-Definition shift_pos :=
-  [n:positive][z:positive](iter_pos n positive xO z). 
-Definition shift :=
-  [n:Z][z:positive]
-  Cases n of
-    ZERO => z
-  | (POS p) => (iter_pos p positive xO z)
-  | (NEG p) => z
-  end.
-
-Definition two_power_nat := [n:nat] (POS (shift_nat n xH)).
-Definition two_power_pos := [x:positive] (POS (shift_pos x xH)).
-
-Lemma two_power_nat_S : 
-  (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`.
-Intro; Simpl; Apply refl_equal.
-Save.
-
-Lemma shift_nat_plus :
-  (n,m:nat)(x:positive)
-    (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)).
-
-Intros; Unfold shift_nat; Apply iter_nat_plus.
-Save.
-
-Theorem shift_nat_correct :
-  (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`.
-
-Unfold shift_nat; Induction n; 
-[ Simpl; Trivial with zarith
-| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`;
-[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity
-| Auto with zarith ]
-].
-Save.
-
-Theorem two_power_nat_correct :
-  (n:nat)(two_power_nat n)=(Zpower_nat `2` n).
-
-Intro n.
-Unfold two_power_nat.
-Rewrite -> (shift_nat_correct n).
-Omega.
-Save.
-  
-(* Second we show that two_power_pos and two_power_nat are the same *)
-Lemma shift_pos_nat : (p:positive)(x:positive)
-  (shift_pos p x)=(shift_nat (convert p) x).
-
-Unfold shift_pos.
-Unfold shift_nat.
-Intros; Apply iter_convert.
-Save.
-
-Lemma two_power_pos_nat : 
-  (p:positive) (two_power_pos p)=(two_power_nat (convert p)).
-
-Intro; Unfold two_power_pos; Unfold two_power_nat.
-Apply f_equal with f:=POS.
-Apply shift_pos_nat.
-Save.
-
-(* Then we deduce that two_power_pos is also correct *)
-
-Theorem shift_pos_correct :
-  (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`.
-
-Intros.
-Rewrite -> (shift_pos_nat p x).
-Rewrite -> (Zpower_pos_nat `2` p).
-Apply shift_nat_correct.
-Save.
-
-Theorem two_power_pos_correct : 
-  (x:positive) (two_power_pos x)=(Zpower_pos `2` x).
-
-Intro.
-Rewrite -> two_power_pos_nat.
-Rewrite -> Zpower_pos_nat.
-Apply two_power_nat_correct.
-Save.
-
-(* Some consequences *)
-
-Theorem two_power_pos_is_exp :
-  (x,y:positive) (two_power_pos (add x y))
-    =(Zmult (two_power_pos x) (two_power_pos y)).
-Intros.
-Rewrite -> (two_power_pos_correct (add x y)).
-Rewrite -> (two_power_pos_correct x).
-Rewrite -> (two_power_pos_correct y).
-Apply Zpower_pos_is_exp.
-Save.
-
-(* The exponentiation z -> 2^z for z a signed integer.   *)
-(* For convenience, we assume that 2^z = 0 for all z <0 *)
-(* We could also define a inductive type Log_result with *)
-(* 3 contructors Zero | Pos positive -> | minus_infty    *)
-(* but it's more complexe and not so useful.		 *)
- 
-Definition two_p :=
-  [x:Z]Cases x of
-         ZERO    => `1`
-       | (POS y) => (two_power_pos y)
-       | (NEG y) => `0`
-       end.
-
-Theorem two_p_is_exp :
-  (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> 
-    ` (two_p (x+y)) = (two_p x)*(two_p y)`.
-Induction x; 
-[ Induction y; Simpl; Auto with zarith
-| Induction y; 
-  [ Unfold two_p;  Rewrite -> (Zmult_sym (two_power_pos p) `1`);
-    Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith
-  | Unfold Zplus; Unfold two_p;
-    Intros; Apply two_power_pos_is_exp
-  | Intros; Unfold Zle in H0; Unfold Zcompare in H0; 
-    Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith
-  ]
-| Induction y; 
-  [ Simpl; Auto with zarith
-  | Intros; Unfold Zle in H; Unfold Zcompare in H;
-    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
-  | Intros; Unfold Zle in H; Unfold Zcompare in H;
-    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
-  ]
-].
-Save.
-
-Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`.
-Induction x; Intros;
-[ Simpl; Omega
-| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO
-| Absurd ` 0 <= (NEG p)`;
-  [ Simpl; Unfold Zle; Unfold Zcompare;
-    Do 2 Unfold not; Auto with zarith
-  | Assumption ]
-].
-Save.
-
-Lemma two_p_S : (x:Z) ` 0 <= x` -> 
- `(two_p (Zs x)) = 2 * (two_p x)`.
-Intros; Unfold Zs. 
-Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)).
-Apply Zmult_sym.
-Save.
-
-Lemma two_p_pred : 
-  (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`.
-Intros; Apply natlike_ind 
-with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`;
-[ Simpl; Unfold Zlt; Auto with zarith
-| Intros; Elim (Zle_lt_or_eq `0` x0 H0);
-  [ Intros;
-    Replace (two_p (Zpred (Zs x0)))
-    with (two_p (Zs (Zpred x0)));
-    [ Rewrite -> (two_p_S (Zpred x0));
-      [ Rewrite -> (two_p_S x0);
-      	[ Omega
-      	| Assumption]
-      | Apply Zlt_ZERO_pred_le_ZERO; Assumption]
-    | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith]
-  | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith]
-| Assumption].
-Save. 
-
-Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`.
-Intros; Omega. Save. 
-
-End Powers_of_2.
-
-Hints Resolve two_p_gt_ZERO : zarith.
-Hints Immediate two_p_pred two_p_S : zarith.
-
-Section power_div_with_rest.
-
-(* Division by a power of two
-  To n:Z and p:positive q,r are associated such that
-    n = 2^p.q + r and 0 <= r < 2^p *)
-
-(* Invariant : d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d' *)
-Definition Zdiv_rest_aux :=
-  [qrd:(Z*Z)*Z] 
-  let (qr,d)=qrd in let (q,r)=qr in
-  (Cases q of
-     ZERO => ` (0, r)`
-   | (POS xH) => ` (0, d + r)`
-   | (POS (xI n)) => ` ((POS n), d + r)`
-   | (POS (xO n)) => ` ((POS n), r)`
-   | (NEG xH) => ` (-1, d + r)`
-   | (NEG (xI n)) => ` ((NEG n) - 1, d + r)`
-   | (NEG (xO n)) => ` ((NEG n), r)`
-   end, ` 2*d`).
-
-Definition Zdiv_rest := 
-  [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr.
-
-Lemma Zdiv_rest_correct1 :
-  (x:Z)(p:positive)
-  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p).
-
-Intros x p; 
-Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`));
-Rewrite (two_power_pos_nat p);
-Elim (convert p); Simpl;
-[ Trivial with zarith
-| Intro n; Rewrite (two_power_nat_S n);
-  Unfold 2 Zdiv_rest_aux;
-  Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`));
-  NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
-Save.
-
-Lemma Zdiv_rest_correct2 :
-  (x:Z)(p:positive)
-  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in
-  let (q,r)=qr in
-  ` x=q*d + r` /\ ` 0 <= r < d`.
-
-Intros; Apply iter_pos_invariant with
-  f:=Zdiv_rest_aux
-  Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in
-                      ` x=q*d + r` /\ ` 0 <= r < d`;
-[ Intro x0; Elim x0; Intro y0; Elim y0;
-  Intros q r d; Unfold Zdiv_rest_aux; 
-  Elim q;
-  [ Omega
-  | NewDestruct p0; 
-    [ Rewrite POS_xI; Intro; Elim H; Intros; Split; 
-      [ Rewrite H0; Rewrite Zplus_assoc;
-      	Rewrite Zmult_plus_distr_l;
-      	Rewrite Zmult_1_n; Rewrite Zmult_assoc;
-      	Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal
-      | Omega ]
-    | Rewrite POS_xO; Intro; Elim H; Intros; Split;
-      [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`);
-      	Apply refl_equal  
-      | Omega ]
-    | Omega ]
-  | NewDestruct p0; 
-    [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
-      [ Rewrite H0; Rewrite Zplus_assoc;
-      	Apply f_equal with f:=[z:Z]`z+r`;
-      	Do 2 (Rewrite Zmult_plus_distr_l);
-       	Rewrite Zmult_assoc; 
-      	Rewrite (Zmult_sym (NEG p0) `2`);
-      	Rewrite <- Zplus_assoc;
-	Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; 
-      	Omega
-      | Omega ]
-    | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split;
-      [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`);
-      	Apply refl_equal  
-      | Omega ]
-    | Omega ] ]
-| Omega].
-Save.
-
-Inductive Set Zdiv_rest_proofs[x:Z; p:positive] :=
-  Zdiv_rest_proof : (q:Z)(r:Z) 
-     `x = q * (two_power_pos p) + r` 
-       -> `0 <= r`
-        -> `r < (two_power_pos p)` 
-      	 -> (Zdiv_rest_proofs x p).
-
-Lemma  Zdiv_rest_correct :
-  (x:Z)(p:positive)(Zdiv_rest_proofs x p).
-Intros x p.
-Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p).
-Elim  (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)).
-Induction a.
-Intros.
-Elim H; Intros H1 H2; Clear H.
-Rewrite -> H0 in H1; Rewrite -> H0 in H2;
-Elim H2; Intros;
-Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption.
-Save.
-
-End power_div_with_rest.